From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 2 May 2014 23:22:26 +0000 (-0400)
Subject: Fix typo in bitvectors example; thanks to Adam Gashlin for reporting the issue.
X-Git-Tag: cvc5-1.0.0~6933
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9b59e12cf7eb284d4d99bf19036ba28fc5fb32cf;p=cvc5.git

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 b69ee5d17..09bf9c299 100644
--- 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 f6e719735..946c221b6 100644
--- 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. ");