diff --git a/doc/tutorial/code/double.saw b/doc/tutorial/code/double.saw
index 4c217363f7..223355b5f5 100644
--- a/doc/tutorial/code/double.saw
+++ b/doc/tutorial/code/double.saw
@@ -6,9 +6,6 @@ let thm = {{ \x -> double_ref x == double_imp x }};
 r <- prove yices thm;
 print r;
 
-r <- prove yices thm;
-print r;
-
 r <- prove z3 thm;
 print r;
 
diff --git a/doc/tutorial/sawScriptTutorial.pdf b/doc/tutorial/sawScriptTutorial.pdf
index 5676fc062e..bb5f420e58 100644
Binary files a/doc/tutorial/sawScriptTutorial.pdf and b/doc/tutorial/sawScriptTutorial.pdf differ
diff --git a/doc/tutorial/tutorial.md b/doc/tutorial/tutorial.md
index c8647dfa9f..9580829897 100644
--- a/doc/tutorial/tutorial.md
+++ b/doc/tutorial/tutorial.md
@@ -276,7 +276,7 @@ $include all code/double.c
 In this trivial example, an integer can be doubled either using
 multiplication or shifting. The following SAWScript program (in
 `double.saw`) verifies that the two are equivalent using both internal
-ABC, Yices, and Z3 modes, and by exporting an SMT-Lib theorem to be
+Yices and Z3 modes, and by exporting an SMT-Lib theorem to be
 checked later, by an external SAT solver.
 
 ```