summaryrefslogtreecommitdiff
path: root/examples/SimpleVC.java
diff options
context:
space:
mode:
Diffstat (limited to 'examples/SimpleVC.java')
-rw-r--r--examples/SimpleVC.java6
1 files changed, 3 insertions, 3 deletions
diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java
index 41c4542fd..4f4d19f24 100644
--- a/examples/SimpleVC.java
+++ b/examples/SimpleVC.java
@@ -61,9 +61,9 @@ public class SimpleVC {
Expr three = em.mkConst(new Rational(3));
Expr twox_plus_y_geq_3 = em.mkExpr(Kind.GEQ, twox_plus_y, three);
- BoolExpr formula =
- new BoolExpr(em.mkExpr(Kind.AND, x_positive, y_positive)).
- impExpr(new BoolExpr(twox_plus_y_geq_3));
+ Expr formula =
+ new Expr(em.mkExpr(Kind.AND, x_positive, y_positive)).
+ impExpr(new Expr(twox_plus_y_geq_3));
System.out.println("Checking validity of formula " + formula + " with CVC4.");
System.out.println("CVC4 should report VALID.");
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback