summaryrefslogtreecommitdiff
path: root/examples/SimpleVC.java
diff options
context:
space:
mode:
Diffstat (limited to 'examples/SimpleVC.java')
-rw-r--r--examples/SimpleVC.java3
1 files changed, 1 insertions, 2 deletions
diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java
index 943ac3aa0..81e7a1f64 100644
--- a/examples/SimpleVC.java
+++ b/examples/SimpleVC.java
@@ -52,8 +52,7 @@ public class SimpleVC {
Expr twox_plus_y_geq_3 = em.mkExpr(Kind.GEQ, twox_plus_y, three);
Expr formula =
- new Expr(em.mkExpr(Kind.AND, x_positive, y_positive)).
- impExpr(new Expr(twox_plus_y_geq_3));
+ em.mkExpr(Kind.AND, x_positive, y_positive).impExpr(twox_plus_y_geq_3);
System.out.println(
"Checking entailment of formula " + formula + " with CVC4.");
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback