Fix typo in bitvectors example; thanks to Adam Gashlin for reporting the issue.

diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp
index b69ee5d17f1826f8cf17221d0deb6af14fa5df41..09bf9c2994eaa94953a2b4d7477c4d6f430c9c5c 100644 (file)
--- a/examples/api/bitvectors.cpp
+++ b/examples/api/bitvectors.cpp
@@ -101,7 +101,7 @@ int main() {
 
   // Assert encoding to CVC4 in current context;
   cout << "Asserting " << assignment2 << " to CVC4 " << endl;
-  smt.assertFormula(assignment1);
+  smt.assertFormula(assignment2);
 
   cout << " Querying: " << new_x_eq_new_x_ << endl;
   cout << " Expect valid. " << endl;

diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java
index f6e719735f857b1dce05e5fc76822f0a45997dd5..946c221b66779b62be89efef7c7e78fd88860f5c 100644 (file)
--- a/examples/api/java/BitVectors.java
+++ b/examples/api/java/BitVectors.java
@@ -99,7 +99,7 @@ public class BitVectors {
 
     // Assert encoding to CVC4 in current context;
     System.out.println("Asserting " + assignment2 + " to CVC4 ");
-    smt.assertFormula(assignment1);
+    smt.assertFormula(assignment2);
 
     System.out.println(" Querying: " + new_x_eq_new_x_);
     System.out.println(" Expect valid. ");