Small fix to SAW tutorial

* Fixed minor bug in Interpreter, and in tutorial file * Fixing previous tutorial fix, and undoing interpreter fix so it can be separately pushed * Modified text in tutorial and regenerated PDF with modified text and code * Update doc/tutorial/tutorial.md Co-authored-by: Ryan Scott <[email protected]> Co-authored-by: Arjun Viswanathan <[email protected]> Co-authored-by: Ryan Scott <[email protected]>
GaloisInc · Jun 15, 2022 · 49cb220 · 49cb220
1 parent 761f535
commit 49cb220
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 4 deletions.
diff --git 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
diff --git 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.
 
 ```