some fixes for language bindings

diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java
index 8159cdc0e2751ccaa94c6f0337c3466ba4072912..a5e2d4e4f30b57d51ce2c2ab9a04ef1ea6771fc6 100644 (file)
--- 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 =

diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 3759763301287e4814cc29f1144d72b81bdcec52..960ba8f84e76ebb95a6786eda01825df748528fa 100644 (file)
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -17,7 +17,6 @@
 
 %include "expr/expr_manager.h"
 
-%template(mkConst) CVC4::ExprManager::mkConst< CVC4::Integer >;
 %template(mkConst) CVC4::ExprManager::mkConst< CVC4::Rational >;
 
 %include "expr/expr_manager.h"