diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-16 01:29:19 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-16 01:29:19 +0000 |
commit | 8406fd17c82dd3caa5d769d07e2c122e937df688 (patch) | |
tree | 2a07f3a868070516e42c3123d00940b805608670 /examples/SimpleVC.java | |
parent | d8fd737fb9ca867f53a287de1c4a87f16a6834f7 (diff) |
some fixes for language bindings
Diffstat (limited to 'examples/SimpleVC.java')
-rw-r--r-- | examples/SimpleVC.java | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java index 8159cdc0e..a5e2d4e4f 100644 --- a/examples/SimpleVC.java +++ b/examples/SimpleVC.java @@ -34,7 +34,6 @@ **/ import edu.nyu.acsys.CVC4.*; -import edu.nyu.acsys.CVC4.Integer;// to override java.lang.Integer name lookup public class SimpleVC { public static void main(String[] args) { @@ -50,16 +49,16 @@ public class SimpleVC { Expr x = em.mkVar("x", integer); Expr y = em.mkVar("y", integer); - Expr zero = em.mkConst(new Integer(0)); + Expr zero = em.mkConst(new Rational(0)); Expr x_positive = em.mkExpr(Kind.GT, x, zero); Expr y_positive = em.mkExpr(Kind.GT, y, zero); - Expr two = em.mkConst(new Integer(2)); + Expr two = em.mkConst(new Rational(2)); Expr twox = em.mkExpr(Kind.MULT, two, x); Expr twox_plus_y = em.mkExpr(Kind.PLUS, twox, y); - Expr three = em.mkConst(new Integer(3)); + Expr three = em.mkConst(new Rational(3)); Expr twox_plus_y_geq_3 = em.mkExpr(Kind.GEQ, twox_plus_y, three); BoolExpr formula = |