From e4e8d99ec19598c77144d3ffde2b5792db4430d3 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 2 Jan 2019 20:07:43 -0800
Subject: New C++ API: Add tests for mk-functions in solver object. (#2764)

---
 examples/api/combination-new.cpp  | 4 ++--
 examples/api/datatypes-new.cpp    | 4 ++--
 examples/api/linear_arith-new.cpp | 4 ++--
 examples/api/sets-new.cpp         | 6 +++---
 examples/api/strings-new.cpp      | 2 +-
 5 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'examples')

diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp
index 2956d76e6..8c968c95e 100644
--- a/examples/api/combination-new.cpp
+++ b/examples/api/combination-new.cpp
@@ -59,8 +59,8 @@ int main()
   Term p = slv.mkVar("p", intPred);
 
   // Constants
-  Term zero = slv.mkInteger(0);
-  Term one = slv.mkInteger(1);
+  Term zero = slv.mkReal(0);
+  Term one = slv.mkReal(1);
 
   // Terms
   Term f_x = slv.mkTerm(APPLY_UF, f, x);
diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index b6a816db4..48560e894 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -39,7 +39,7 @@ void test(Solver& slv, Sort& consListSort)
   Term t = slv.mkTerm(
       APPLY_CONSTRUCTOR,
       consList.getConstructorTerm("cons"),
-      slv.mkInteger(0),
+      slv.mkReal(0),
       slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
 
   std::cout << "t is " << t << std::endl
@@ -127,7 +127,7 @@ void test(Solver& slv, Sort& consListSort)
             << "sort of cons is "
             << paramConsList.getConstructorTerm("cons").getSort() << std::endl
             << std::endl;
-  Term assertion = slv.mkTerm(GT, head_a, slv.mkInteger(50));
+  Term assertion = slv.mkTerm(GT, head_a, slv.mkReal(50));
   std::cout << "Assert " << assertion << std::endl;
   slv.assertFormula(assertion);
   std::cout << "Expect sat." << std::endl;
diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp
index ef8faade9..d643b85bc 100644
--- a/examples/api/linear_arith-new.cpp
+++ b/examples/api/linear_arith-new.cpp
@@ -40,8 +40,8 @@ int main()
   Term y = slv.mkVar("y", real);
 
   // Constants
-  Term three = slv.mkInteger(3);
-  Term neg2 = slv.mkInteger(-2);
+  Term three = slv.mkReal(3);
+  Term neg2 = slv.mkReal(-2);
   Term two_thirds = slv.mkReal(2, 3);
 
   // Terms
diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp
index be35bcc21..2dcfbbc02 100644
--- a/examples/api/sets-new.cpp
+++ b/examples/api/sets-new.cpp
@@ -70,9 +70,9 @@ int main()
 
   // Find me an element in {1, 2} intersection {2, 3}, if there is one.
   {
-    Term one = slv.mkInteger(1);
-    Term two = slv.mkInteger(2);
-    Term three = slv.mkInteger(3);
+    Term one = slv.mkReal(1);
+    Term two = slv.mkReal(2);
+    Term three = slv.mkReal(3);
 
     Term singleton_one = slv.mkTerm(SINGLETON, one);
     Term singleton_two = slv.mkTerm(SINGLETON, two);
diff --git a/examples/api/strings-new.cpp b/examples/api/strings-new.cpp
index 2010c6909..c88ccc9c0 100644
--- a/examples/api/strings-new.cpp
+++ b/examples/api/strings-new.cpp
@@ -57,7 +57,7 @@ int main()
   // Length of y: |y|
   Term leny = slv.mkTerm(STRING_LENGTH, y);
   // |y| >= 0
-  Term formula2 = slv.mkTerm(GEQ, leny, slv.mkInteger(0));
+  Term formula2 = slv.mkTerm(GEQ, leny, slv.mkReal(0));
 
   // Regular expression: (ab[c-e]*f)|g|h
   Term r = slv.mkTerm(REGEXP_UNION,
-- 
cgit v1.2.3