New C++: Remove redundant mkVar function.

s

diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp
index 7070f67482c91b3fc6490b6d3104cb7abe8f146d..102cc2314471fe0bdbe5c933304695ef718dc8d9 100644 (file)
--- a/examples/api/bitvectors-new.cpp
+++ b/examples/api/bitvectors-new.cpp
@@ -50,9 +50,9 @@ int main()
   Sort bitvector32 = slv.mkBitVectorSort(32);
 
   // Variables
-  Term x = slv.mkVar("x", bitvector32);
-  Term a = slv.mkVar("a", bitvector32);
-  Term b = slv.mkVar("b", bitvector32);
+  Term x = slv.mkVar(bitvector32, "x");
+  Term a = slv.mkVar(bitvector32, "a");
+  Term b = slv.mkVar(bitvector32, "b");
 
   // First encode the assumption that x must be equal to a or b
   Term x_eq_a = slv.mkTerm(EQUAL, x, a);
@@ -63,9 +63,9 @@ int main()
   slv.assertFormula(assumption);
 
   // Introduce a new variable for the new value of x after assignment.
-  Term new_x = slv.mkVar("new_x", bitvector32);  // x after executing code (0)
+  Term new_x = slv.mkVar(bitvector32, "new_x");  // x after executing code (0)
   Term new_x_ =
-      slv.mkVar("new_x_", bitvector32);  // x after executing code (1) or (2)
+      slv.mkVar(bitvector32, "new_x_");  // x after executing code (1) or (2)
 
   // Encoding code (0)
   // new_x = x == a ? b : a;

diff --git a/examples/api/bitvectors_and_arrays-new.cpp b/examples/api/bitvectors_and_arrays-new.cpp
index 3d4e6bca0bcc3602e3f1a92bfa597e4fd0c54c06..294cf66c014d066ca81b5a5099365d043056b54f 100644 (file)
--- a/examples/api/bitvectors_and_arrays-new.cpp
+++ b/examples/api/bitvectors_and_arrays-new.cpp
@@ -52,7 +52,7 @@ int main()
   Sort arraySort = slv.mkArraySort(indexSort, elementSort);
 
   // Variables
-  Term current_array = slv.mkVar("current_array", arraySort);
+  Term current_array = slv.mkVar(arraySort, "current_array");
 
   // Making a bit-vector constant
   Term zero = slv.mkBitVector(index_size, 0u);

diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp
index 8c968c95e1e83565b6ecff517879754a74cdfd63..24ed32ad5fb1e495c544b7adaf35aa557d867820 100644 (file)
--- a/examples/api/combination-new.cpp
+++ b/examples/api/combination-new.cpp
@@ -51,12 +51,12 @@ int main()
   Sort intPred = slv.mkFunctionSort(integer, boolean);
 
   // Variables
-  Term x = slv.mkVar("x", u);
-  Term y = slv.mkVar("y", u);
+  Term x = slv.mkVar(u, "x");
+  Term y = slv.mkVar(u, "y");
 
   // Functions
-  Term f = slv.mkVar("f", uToInt);
-  Term p = slv.mkVar("p", intPred);
+  Term f = slv.mkVar(uToInt, "f");
+  Term p = slv.mkVar(intPred, "p");
 
   // Constants
   Term zero = slv.mkReal(0);

diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp
index 96961458e0a067d030e572dd9837b6fa9af48106..05be327b9315af55d16d9a1d87b6384b301fc90d 100644 (file)
--- a/examples/api/extract-new.cpp
+++ b/examples/api/extract-new.cpp
@@ -29,7 +29,7 @@ int main()
 
   Sort bitvector32 = slv.mkBitVectorSort(32);
 
-  Term x = slv.mkVar("a", bitvector32);
+  Term x = slv.mkVar(bitvector32, "a");
 
   OpTerm ext_31_1 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
   Term x_31_1 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_1, x);

diff --git a/examples/api/helloworld-new.cpp b/examples/api/helloworld-new.cpp
index 484995143ad529bffe87a81433b39ee91b941796..3e3c7426b18a9f85f054c03316a9ceaec6cd38c7 100644 (file)
--- a/examples/api/helloworld-new.cpp
+++ b/examples/api/helloworld-new.cpp
@@ -24,7 +24,7 @@ using namespace CVC4::api;
 int main()
 {
   Solver slv;
-  Term helloworld = slv.mkVar("Hello World!", slv.getBooleanSort());
+  Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!");
   std::cout << helloworld << " is " << slv.checkValidAssuming(helloworld)
             << std::endl;
   return 0;

diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp
index d643b85bc9c4d4c60073738238364e8fee7f04d1..c194458ae02b8e782eccf38e0b25abad6cc5b323 100644 (file)
--- a/examples/api/linear_arith-new.cpp
+++ b/examples/api/linear_arith-new.cpp
@@ -36,8 +36,8 @@ int main()
   Sort integer = slv.getIntegerSort();
 
   // Variables
-  Term x = slv.mkVar("x", integer);
-  Term y = slv.mkVar("y", real);
+  Term x = slv.mkVar(integer, "x");
+  Term y = slv.mkVar(real, "y");
 
   // Constants
   Term three = slv.mkReal(3);

diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp
index 2dcfbbc024ceb5ce80fe00d4121b1c5333f8026e..95e1aa17509c0c7f032d9bcc975fd7a03e312990 100644 (file)
--- a/examples/api/sets-new.cpp
+++ b/examples/api/sets-new.cpp
@@ -40,9 +40,9 @@ int main()
   // Verify union distributions over intersection
   // (A union B) intersection C = (A intersection C) union (B intersection C)
   {
-    Term A = slv.mkVar("A", set);
-    Term B = slv.mkVar("B", set);
-    Term C = slv.mkVar("C", set);
+    Term A = slv.mkVar(set, "A");
+    Term B = slv.mkVar(set, "B");
+    Term C = slv.mkVar(set, "C");
 
     Term unionAB = slv.mkTerm(UNION, A, B);
     Term lhs = slv.mkTerm(INTERSECTION, unionAB, C);
@@ -59,7 +59,7 @@ int main()
 
   // Verify emptset is a subset of any set
   {
-    Term A = slv.mkVar("A", set);
+    Term A = slv.mkVar(set, "A");
     Term emptyset = slv.mkEmptySet(set);
 
     Term theorem = slv.mkTerm(SUBSET, emptyset, A);
@@ -81,7 +81,7 @@ int main()
     Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three);
     Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three);
 
-    Term x = slv.mkVar("x", integer);
+    Term x = slv.mkVar(integer, "x");
 
     Term e = slv.mkTerm(MEMBER, x, intersection);
 

diff --git a/examples/api/strings-new.cpp b/examples/api/strings-new.cpp
index c88ccc9c082c09eadf2c0325c4ea90d5caa6cdfe..d5f4312cd218aa9f6e016589daa9a014f83fdc1c 100644 (file)
--- a/examples/api/strings-new.cpp
+++ b/examples/api/strings-new.cpp
@@ -43,9 +43,9 @@ int main()
   Term ab  = slv.mkString(str_ab);
   Term abc = slv.mkString("abc");
   // String variables
-  Term x = slv.mkVar("x", string);
-  Term y = slv.mkVar("y", string);
-  Term z = slv.mkVar("z", string);
+  Term x = slv.mkVar(string, "x");
+  Term y = slv.mkVar(string, "y");
+  Term z = slv.mkVar(string, "z");
 
   // String concatenation: x.ab.y
   Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y);
@@ -70,8 +70,8 @@ int main()
     slv.mkTerm(STRING_TO_REGEXP, slv.mkString("h")));
 
   // String variables
-  Term s1 = slv.mkVar("s1", string);
-  Term s2 = slv.mkVar("s2", string);
+  Term s1 = slv.mkVar(string, "s1");
+  Term s2 = slv.mkVar(string, "s2");
   // String concatenation: s1.s2
   Term s = slv.mkTerm(STRING_CONCAT, s1, s2);
 

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 9d56bb88a0297abfe98a828b36194895eb15b273..032326c268902b5950ff5d92792e5279ea8ff325 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2392,27 +2392,13 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
 /* Create variables                                                           */
 /* -------------------------------------------------------------------------- */
 
-Term Solver::mkVar(const std::string& symbol, Sort sort) const
+Term Solver::mkVar(Sort sort, const std::string& symbol) const
 {
   try
   {
     CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
-    Term res = d_exprMgr->mkVar(symbol, *sort.d_type);
-    (void)res.d_expr->getType(true); /* kick off type checking */
-    return res;
-  }
-  catch (const CVC4::TypeCheckingException& e)
-  {
-    throw CVC4ApiException(e.getMessage());
-  }
-}
-
-Term Solver::mkVar(Sort sort) const
-{
-  try
-  {
-    CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
-    Term res = d_exprMgr->mkVar(*sort.d_type);
+    Term res = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type)
+                              : d_exprMgr->mkVar(symbol, *sort.d_type);
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 2c266b11d4424f29895a40d88dd40ac2795d6764..3999dd2ede3fbbb8a397ef82623a9cd07f84207d 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2165,20 +2165,13 @@ class CVC4_PUBLIC Solver
   /* Create Variables                                                     */
   /* .................................................................... */
 
-  /**
-   * Create variable.
-   * @param symbol the name of the variable
-   * @param sort the sort of the variable
-   * @return the variable
-   */
-  Term mkVar(const std::string& symbol, Sort sort) const;
-
   /**
    * Create variable.
    * @param sort the sort of the variable
+   * @param symbol the name of the variable
    * @return the variable
    */
-  Term mkVar(Sort sort) const;
+  Term mkVar(Sort sort, const std::string& symbol = std::string()) const;
 
   /**
    * Create bound variable.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index c72a4f99b7827c5395c6cf2d5dd7ed655c8a626d..81f01c13891a770f518b86cdfc0316a4974f51ca 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2306,8 +2306,8 @@ termAtomic[CVC4::api::Term& atomTerm]
       sortSymbol[type,CHECK_DECLARED]
       sortSymbol[type2,CHECK_DECLARED]
       {
-        api::Term v1 = SOLVER->mkVar("_emp1", api::Sort(type));
-        api::Term v2 = SOLVER->mkVar("_emp2", api::Sort(type2));
+        api::Term v1 = SOLVER->mkVar(api::Sort(type), "_emp1");
+        api::Term v2 = SOLVER->mkVar(api::Sort(type2), "_emp2");
         atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2);
       }
 

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index c42854fce22b0cc6f2ba7d04d0e63410c711f4c6..f64751d0176f106fb2985c6374fb5f5967228f1b 100644 (file)
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -510,7 +510,7 @@ void SolverBlack::testMkReal()
 void SolverBlack::testMkRegexpEmpty()
 {
   Sort strSort = d_solver->getStringSort();
-  Term s = d_solver->mkVar("s", strSort);
+  Term s = d_solver->mkVar(strSort, "s");
   TS_ASSERT_THROWS_NOTHING(
       d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpEmpty()));
 }
@@ -518,7 +518,7 @@ void SolverBlack::testMkRegexpEmpty()
 void SolverBlack::testMkRegexpSigma()
 {
   Sort strSort = d_solver->getStringSort();
-  Term s = d_solver->mkVar("s", strSort);
+  Term s = d_solver->mkVar(strSort, "s");
   TS_ASSERT_THROWS_NOTHING(
       d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpSigma()));
 }
@@ -542,8 +542,8 @@ void SolverBlack::testMkString()
 void SolverBlack::testMkTerm()
 {
   Sort bv32 = d_solver->mkBitVectorSort(32);
-  Term a = d_solver->mkVar("a", bv32);
-  Term b = d_solver->mkVar("b", bv32);
+  Term a = d_solver->mkVar(bv32, "a");
+  Term b = d_solver->mkVar(bv32, "b");
   std::vector<Term> v1 = {a, b};
   std::vector<Term> v2 = {a, Term()};
   std::vector<Term> v3 = {a, d_solver->mkTrue()};
@@ -595,8 +595,8 @@ void SolverBlack::testMkTerm()
 void SolverBlack::testMkTermFromOpTerm()
 {
   Sort bv32 = d_solver->mkBitVectorSort(32);
-  Term a = d_solver->mkVar("a", bv32);
-  Term b = d_solver->mkVar("b", bv32);
+  Term a = d_solver->mkVar(bv32, "a");
+  Term b = d_solver->mkVar(bv32, "b");
   std::vector<Term> v1 = {d_solver->mkReal(1), d_solver->mkReal(2)};
   std::vector<Term> v2 = {d_solver->mkReal(1), Term()};
   std::vector<Term> v3 = {};
@@ -731,12 +731,12 @@ void SolverBlack::testMkVar()
   Sort boolSort = d_solver->getBooleanSort();
   Sort intSort = d_solver->getIntegerSort();
   Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
-  TS_ASSERT_THROWS(d_solver->mkVar(Sort()), CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort));
-  TS_ASSERT_THROWS(d_solver->mkVar("a", Sort()), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(std::string("b"), boolSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar("", funSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort, std::string("b")));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort, ""));
+  TS_ASSERT_THROWS(d_solver->mkVar(Sort()), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkVar(Sort(), "a"), CVC4ApiException&);
 }
 
 void SolverBlack::testDeclareConst()
@@ -801,7 +801,7 @@ void SolverBlack::testDefineFun()
   Term b3 = d_solver->mkBoundVar("b3", funSort2);
   Term v1 = d_solver->mkBoundVar("v1", bvSort);
   Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort());
-  Term v3 = d_solver->mkVar("v3", funSort2);
+  Term v3 = d_solver->mkVar(funSort2, "v3");
   Term f1 = d_solver->declareConst("f1", funSort1);
   Term f2 = d_solver->declareConst("f2", funSort2);
   Term f3 = d_solver->declareConst("f3", bvSort);
@@ -833,7 +833,7 @@ void SolverBlack::testDefineFunRec()
   Term b3 = d_solver->mkBoundVar("b3", funSort2);
   Term v1 = d_solver->mkBoundVar("v1", bvSort);
   Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort());
-  Term v3 = d_solver->mkVar("v3", funSort2);
+  Term v3 = d_solver->mkVar(funSort2, "v3");
   Term f1 = d_solver->declareConst("f1", funSort1);
   Term f2 = d_solver->declareConst("f2", funSort2);
   Term f3 = d_solver->declareConst("f3", bvSort);
@@ -868,8 +868,8 @@ void SolverBlack::testDefineFunsRec()
   Term b4 = d_solver->mkBoundVar("b4", uSort);
   Term v1 = d_solver->mkBoundVar("v1", bvSort);
   Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort());
-  Term v3 = d_solver->mkVar("v3", funSort2);
-  Term v4 = d_solver->mkVar("v4", uSort);
+  Term v3 = d_solver->mkVar(funSort2, "v3");
+  Term v4 = d_solver->mkVar(uSort, "v4");
   Term f1 = d_solver->declareConst("f1", funSort1);
   Term f2 = d_solver->declareConst("f2", funSort2);
   Term f3 = d_solver->declareConst("f3", bvSort);

diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index a7f735651d06a2e1c3a28beffc4d9b7f6e4518a3..5bb99ff2a75c7788fa3f06d38266c26008dc8158 100644 (file)
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -45,8 +45,8 @@ class TermBlack : public CxxTest::TestSuite
 void TermBlack::testEq()
 {
   Sort uSort = d_solver.mkUninterpretedSort("u");
-  Term x = d_solver.mkVar("x", uSort);
-  Term y = d_solver.mkVar("y", uSort);
+  Term x = d_solver.mkVar(uSort, "x");
+  Term y = d_solver.mkVar(uSort, "y");
   Term z;
 
   TS_ASSERT(x == x);
@@ -67,14 +67,14 @@ void TermBlack::testGetKind()
 
   Term n;
   TS_ASSERT_THROWS(n.getKind(), CVC4ApiException&);
-  Term x = d_solver.mkVar("x", uSort);
+  Term x = d_solver.mkVar(uSort, "x");
   TS_ASSERT_THROWS_NOTHING(x.getKind());
-  Term y = d_solver.mkVar("y", uSort);
+  Term y = d_solver.mkVar(uSort, "y");
   TS_ASSERT_THROWS_NOTHING(y.getKind());
 
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS_NOTHING(f.getKind());
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS_NOTHING(p.getKind());
 
   Term zero = d_solver.mkReal(0);
@@ -102,17 +102,17 @@ void TermBlack::testGetSort()
 
   Term n;
   TS_ASSERT_THROWS(n.getSort(), CVC4ApiException&);
-  Term x = d_solver.mkVar("x", bvSort);
+  Term x = d_solver.mkVar(bvSort, "x");
   TS_ASSERT_THROWS_NOTHING(x.getSort());
   TS_ASSERT(x.getSort() == bvSort);
-  Term y = d_solver.mkVar("y", bvSort);
+  Term y = d_solver.mkVar(bvSort, "y");
   TS_ASSERT_THROWS_NOTHING(y.getSort());
   TS_ASSERT(y.getSort() == bvSort);
 
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS_NOTHING(f.getSort());
   TS_ASSERT(f.getSort() == funSort1);
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS_NOTHING(p.getSort());
   TS_ASSERT(p.getSort() == funSort2);
 
@@ -141,7 +141,7 @@ void TermBlack::testIsNull()
 {
   Term x;
   TS_ASSERT(x.isNull());
-  x = d_solver.mkVar("x", d_solver.mkBitVectorSort(4));
+  x = d_solver.mkVar(d_solver.mkBitVectorSort(4), "x");
   TS_ASSERT(!x.isNull());
 }
 
@@ -155,11 +155,11 @@ void TermBlack::testNotTerm()
 
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS_NOTHING(b.notTerm());
-  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS(x.notTerm(), CVC4ApiException&);
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS(f.notTerm(), CVC4ApiException&);
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.notTerm(), CVC4ApiException&);
   Term zero = d_solver.mkReal(0);
   TS_ASSERT_THROWS(zero.notTerm(), CVC4ApiException&);
@@ -183,14 +183,14 @@ void TermBlack::testAndTerm()
 
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS_NOTHING(b.andTerm(b));
-  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS(x.andTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(x.andTerm(x), CVC4ApiException&);
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS(f.andTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(f.andTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(f.andTerm(f), CVC4ApiException&);
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.andTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(p.andTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.andTerm(f), CVC4ApiException&);
@@ -247,14 +247,14 @@ void TermBlack::testOrTerm()
 
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS_NOTHING(b.orTerm(b));
-  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS(x.orTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(x.orTerm(x), CVC4ApiException&);
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS(f.orTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(f.orTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(f.orTerm(f), CVC4ApiException&);
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.orTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(p.orTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.orTerm(f), CVC4ApiException&);
@@ -311,14 +311,14 @@ void TermBlack::testXorTerm()
 
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS_NOTHING(b.xorTerm(b));
-  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS(x.xorTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(x.xorTerm(x), CVC4ApiException&);
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS(f.xorTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(f.xorTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(f.xorTerm(f), CVC4ApiException&);
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.xorTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(p.xorTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.xorTerm(f), CVC4ApiException&);
@@ -375,14 +375,14 @@ void TermBlack::testEqTerm()
 
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS_NOTHING(b.eqTerm(b));
-  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS(x.eqTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(x.eqTerm(x));
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS(f.eqTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(f.eqTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(f.eqTerm(f));
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.eqTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(p.eqTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.eqTerm(f), CVC4ApiException&);
@@ -439,14 +439,14 @@ void TermBlack::testImpTerm()
 
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS_NOTHING(b.impTerm(b));
-  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS(x.impTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(x.impTerm(x), CVC4ApiException&);
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS(f.impTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(f.impTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(f.impTerm(f), CVC4ApiException&);
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.impTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(p.impTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.impTerm(f), CVC4ApiException&);
@@ -503,16 +503,16 @@ void TermBlack::testIteTerm()
 
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b));
-  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS_NOTHING(b.iteTerm(x, x));
   TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b));
   TS_ASSERT_THROWS(b.iteTerm(x, b), CVC4ApiException&);
   TS_ASSERT_THROWS(x.iteTerm(x, x), CVC4ApiException&);
   TS_ASSERT_THROWS(x.iteTerm(x, b), CVC4ApiException&);
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS(f.iteTerm(b, b), CVC4ApiException&);
   TS_ASSERT_THROWS(x.iteTerm(b, x), CVC4ApiException&);
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.iteTerm(b, b), CVC4ApiException&);
   TS_ASSERT_THROWS(p.iteTerm(x, b), CVC4ApiException&);
   Term zero = d_solver.mkReal(0);