summaryrefslogtreecommitdiff
path: root/examples/api/java/Combination.java
diff options
context:
space:
mode:
Diffstat (limited to 'examples/api/java/Combination.java')
-rw-r--r--examples/api/java/Combination.java7
1 files changed, 3 insertions, 4 deletions
diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java
index 0c9ca84d6..53b1fa92d 100644
--- a/examples/api/java/Combination.java
+++ b/examples/api/java/Combination.java
@@ -83,10 +83,9 @@ public class Combination {
System.out.println("Given the following assumptions:");
System.out.println(assumptions);
- System.out.println("Prove x /= y is valid. " +
- "CVC4 says: " + smt.query(em.mkExpr(Kind.DISTINCT, x, y)) +
- ".");
-
+ System.out.println("Prove x /= y is entailed. "
+ + "CVC4 says: " + smt.checkEntailed(em.mkExpr(Kind.DISTINCT, x, y))
+ + ".");
System.out.println("Now we call checksat on a trivial query to show that");
System.out.println("the assumptions are satisfiable: " +
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback