From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 16 Aug 2012 01:29:19 +0000 (+0000)
Subject: some fixes for language bindings
X-Git-Tag: cvc5-1.0.0~7868
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8406fd17c82dd3caa5d769d07e2c122e937df688;p=cvc5.git

some fixes for language bindings
---

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 =
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 375976330..960ba8f84 100644
--- 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"