some fixes to language bindings and function visibility

3 files changed, 7 insertions, 6 deletions

diff --git a/examples/SimpleVC.py b/examples/SimpleVC.py
index a1cd1a6bd..18be0fdc0 100755
--- a/examples/SimpleVC.py
+++ b/examples/SimpleVC.py
@@ -24,7 +24,7 @@
 ####
 
 import CVC4
-from CVC4 import ExprManager, SmtEngine, Integer, Expr
+from CVC4 import ExprManager, SmtEngine, Rational, Expr
 
 import sys
 
@@ -39,16 +39,16 @@ def main():
 
   x = em.mkVar("x", integer)
   y = em.mkVar("y", integer)
-  zero = em.mkConst(Integer(0))
+  zero = em.mkConst(Rational(0))
 
   x_positive = em.mkExpr(CVC4.GT, x, zero)
   y_positive = em.mkExpr(CVC4.GT, y, zero)
 
-  two = em.mkConst(Integer(2))
+  two = em.mkConst(Rational(2))
   twox = em.mkExpr(CVC4.MULT, two, x)
   twox_plus_y = em.mkExpr(CVC4.PLUS, twox, y)
 
-  three = em.mkConst(Integer(3))
+  three = em.mkConst(Rational(3))
   twox_plus_y_geq_3 = em.mkExpr(CVC4.GEQ, twox_plus_y, three)
 
   formula = Expr(em.mkExpr(CVC4.AND, x_positive, y_positive)).impExpr(Expr(twox_plus_y_geq_3))
diff --git a/src/parser/input.h b/src/parser/input.h
index 586b35231..0203ed806 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -45,7 +45,7 @@ public:
 };
 
 /** Wrapper around an input stream. */
-class InputStream {
+class CVC4_PUBLIC InputStream {
 
   /** The name of this input stream. */
   std::string d_name;
@@ -73,7 +73,7 @@ public:
 
   /** Get the name of this input stream. */
   const std::string getName() const;
-};
+};/* class InputStream */
 
 class Parser;
 
diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i
index 7fdb59467..c53bb8ce5 100644
--- a/src/smt/smt_engine.i
+++ b/src/smt/smt_engine.i
@@ -4,5 +4,6 @@
 
 %ignore CVC4::SmtEngine::getProof;
 %ignore CVC4::stats::getStatisticsRegistry(SmtEngine*);
+%ignore CVC4::smt::beforeSearch(std::string, bool, SmtEngine*);
 
 %include "smt/smt_engine.h"