* fixing the simple_vc_cxx.cpp compile issue (no more Integer constants)

* adding as examples the programs i used to translate nonlinear smt2 problems to other formats

1 files changed, 3 insertions, 3 deletions

diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp
index 819b1fc97..557199e75 100644
--- a/examples/simple_vc_cxx.cpp
+++ b/examples/simple_vc_cxx.cpp
@@ -37,16 +37,16 @@ int main() {
 
   Expr x = em.mkVar("x", integer);
   Expr y = em.mkVar("y", integer);
-  Expr zero = em.mkConst(Integer(0));
+  Expr zero = em.mkConst(Rational(0));
 
   Expr x_positive = em.mkExpr(kind::GT, x, zero);
   Expr y_positive = em.mkExpr(kind::GT, y, zero);
 
-  Expr two = em.mkConst(Integer(2));
+  Expr two = em.mkConst(Rational(2));
   Expr twox = em.mkExpr(kind::MULT, two, x);
   Expr twox_plus_y = em.mkExpr(kind::PLUS, twox, y);
 
-  Expr three = em.mkConst(Integer(3));
+  Expr three = em.mkConst(Rational(3));
   Expr twox_plus_y_geq_3 = em.mkExpr(kind::GEQ, twox_plus_y, three);
 
   BoolExpr formula =