New C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977)

This cleans up naming of API functions to create first-order constants and variables.

mkVar -> mkConst
mkBoundVar -> mkVar
declareConst is redundant (= mkConst) and thus, in an effort to avoid redundancy, removed.

Note that we want to avoid redundancy in order to reduce code duplication and maintenance
overhead (we do not allow nested API calls, since this is problematic when tracing API calls).

13 files changed, 168 insertions, 202 deletions

diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp
index 6aea56163..d0c26f134 100644
--- 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(bitvector32, "x");
-  Term a = slv.mkVar(bitvector32, "a");
-  Term b = slv.mkVar(bitvector32, "b");
+  Term x = slv.mkConst(bitvector32, "x");
+  Term a = slv.mkConst(bitvector32, "a");
+  Term b = slv.mkConst(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(bitvector32, "new_x");  // x after executing code (0)
+  Term new_x = slv.mkConst(bitvector32, "new_x");  // x after executing code (0)
   Term new_x_ =
-      slv.mkVar(bitvector32, "new_x_");  // x after executing code (1) or (2)
+      slv.mkConst(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 f0883d634..955a83cff 100644
--- a/examples/api/bitvectors_and_arrays-new.cpp
+++ b/examples/api/bitvectors_and_arrays-new.cpp
@@ -53,7 +53,7 @@ int main()
   Sort arraySort = slv.mkArraySort(indexSort, elementSort);
 
   // Variables
-  Term current_array = slv.mkVar(arraySort, "current_array");
+  Term current_array = slv.mkConst(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 a3ff4421f..e78e8919f 100644
--- 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(u, "x");
-  Term y = slv.mkVar(u, "y");
+  Term x = slv.mkConst(u, "x");
+  Term y = slv.mkConst(u, "y");
 
   // Functions
-  Term f = slv.mkVar(uToInt, "f");
-  Term p = slv.mkVar(intPred, "p");
+  Term f = slv.mkConst(uToInt, "f");
+  Term p = slv.mkConst(intPred, "p");
 
   // Constants
   Term zero = slv.mkReal(0);
diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index c499fa111..08918fc87 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -116,7 +116,7 @@ void test(Solver& slv, Sort& consListSort)
     }
   }
 
-  Term a = slv.declareConst("a", paramConsIntListSort);
+  Term a = slv.mkConst(paramConsIntListSort, "a");
   std::cout << "term " << a << " is of sort " << a.getSort() << std::endl;
 
   Term head_a = slv.mkTerm(
diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp
index aad9e0fb5..cb7d96fa5 100644
--- 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(bitvector32, "a");
+  Term x = slv.mkConst(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/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp
index aae2fa67e..2edcaf71e 100644
--- 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(integer, "x");
-  Term y = slv.mkVar(real, "y");
+  Term x = slv.mkConst(integer, "x");
+  Term y = slv.mkConst(real, "y");
 
   // Constants
   Term three = slv.mkReal(3);
diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp
index 6c0352302..60df7a82f 100644
--- 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(set, "A");
-    Term B = slv.mkVar(set, "B");
-    Term C = slv.mkVar(set, "C");
+    Term A = slv.mkConst(set, "A");
+    Term B = slv.mkConst(set, "B");
+    Term C = slv.mkConst(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(set, "A");
+    Term A = slv.mkConst(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(integer, "x");
+    Term x = slv.mkConst(integer, "x");
 
     Term e = slv.mkTerm(MEMBER, x, intersection);
 
diff --git a/examples/api/strings-new.cpp b/examples/api/strings-new.cpp
index a9c6dd491..42630dc0e 100644
--- 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(string, "x");
-  Term y = slv.mkVar(string, "y");
-  Term z = slv.mkVar(string, "z");
+  Term x = slv.mkConst(string, "x");
+  Term y = slv.mkConst(string, "y");
+  Term z = slv.mkConst(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(string, "s1");
-  Term s2 = slv.mkVar(string, "s2");
+  Term s1 = slv.mkConst(string, "s1");
+  Term s2 = slv.mkConst(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 86072d601..4cd9f4923 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -56,8 +56,8 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {APPLY, CVC4::Kind::APPLY},
     {EQUAL, CVC4::Kind::EQUAL},
     {DISTINCT, CVC4::Kind::DISTINCT},
-    {VARIABLE, CVC4::Kind::VARIABLE},
-    {BOUND_VARIABLE, CVC4::Kind::BOUND_VARIABLE},
+    {CONSTANT, CVC4::Kind::VARIABLE},
+    {VARIABLE, CVC4::Kind::BOUND_VARIABLE},
     {LAMBDA, CVC4::Kind::LAMBDA},
     {CHOICE, CVC4::Kind::CHOICE},
     {CHAIN, CVC4::Kind::CHAIN},
@@ -304,8 +304,8 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::APPLY, APPLY},
         {CVC4::Kind::EQUAL, EQUAL},
         {CVC4::Kind::DISTINCT, DISTINCT},
-        {CVC4::Kind::VARIABLE, VARIABLE},
-        {CVC4::Kind::BOUND_VARIABLE, BOUND_VARIABLE},
+        {CVC4::Kind::VARIABLE, CONSTANT},
+        {CVC4::Kind::BOUND_VARIABLE, VARIABLE},
         {CVC4::Kind::LAMBDA, LAMBDA},
         {CVC4::Kind::CHOICE, CHOICE},
         {CVC4::Kind::CHAIN, CHAIN},
@@ -1970,7 +1970,7 @@ Term Solver::mkPi() const
 }
 
 template <typename T>
-Term Solver::mkConstHelper(T t) const
+Term Solver::mkValHelper(T t) const
 {
   try
   {
@@ -1997,7 +1997,7 @@ Term Solver::mkRealFromStrHelper(std::string s) const
     CVC4::Rational r = s.find('/') != std::string::npos
                            ? CVC4::Rational(s)
                            : CVC4::Rational::fromDecimal(s);
-    return mkConstHelper<CVC4::Rational>(r);
+    return mkValHelper<CVC4::Rational>(r);
   }
   catch (const std::invalid_argument& e)
   {
@@ -2020,7 +2020,7 @@ Term Solver::mkReal(int32_t val) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2032,7 +2032,7 @@ Term Solver::mkReal(int64_t val) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2044,7 +2044,7 @@ Term Solver::mkReal(uint32_t val) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2056,7 +2056,7 @@ Term Solver::mkReal(uint64_t val) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2068,7 +2068,7 @@ Term Solver::mkReal(int32_t num, int32_t den) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2080,7 +2080,7 @@ Term Solver::mkReal(int64_t num, int64_t den) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2092,7 +2092,7 @@ Term Solver::mkReal(uint32_t num, uint32_t den) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2104,7 +2104,7 @@ Term Solver::mkReal(uint64_t num, uint64_t den) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2146,7 +2146,7 @@ Term Solver::mkEmptySet(Sort s) const
 {
   CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isSet(), s)
       << "null sort or set sort";
-  return mkConstHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type));
+  return mkValHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type));
 }
 
 Term Solver::mkSepNil(Sort sort) const
@@ -2166,22 +2166,22 @@ Term Solver::mkSepNil(Sort sort) const
 
 Term Solver::mkString(const char* s, bool useEscSequences) const
 {
-  return mkConstHelper<CVC4::String>(CVC4::String(s, useEscSequences));
+  return mkValHelper<CVC4::String>(CVC4::String(s, useEscSequences));
 }
 
 Term Solver::mkString(const std::string& s, bool useEscSequences) const
 {
-  return mkConstHelper<CVC4::String>(CVC4::String(s, useEscSequences));
+  return mkValHelper<CVC4::String>(CVC4::String(s, useEscSequences));
 }
 
 Term Solver::mkString(const unsigned char c) const
 {
-  return mkConstHelper<CVC4::String>(CVC4::String(std::string(1, c)));
+  return mkValHelper<CVC4::String>(CVC4::String(std::string(1, c)));
 }
 
 Term Solver::mkString(const std::vector<unsigned>& s) const
 {
-  return mkConstHelper<CVC4::String>(CVC4::String(s));
+  return mkValHelper<CVC4::String>(CVC4::String(s));
 }
 
 Term Solver::mkUniverseSet(Sort sort) const
@@ -2207,7 +2207,7 @@ Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
   CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0";
   try
   {
-    return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
+    return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2228,7 +2228,7 @@ Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const
       << "base 2, 10, or 16";
   try
   {
-    return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
+    return mkValHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2249,7 +2249,7 @@ Term Solver::mkBVFromStrHelper(uint32_t size,
     CVC4_API_CHECK(val.modByPow2(size) == val)
         << "Overflow in bitvector construction (specified bitvector size "
         << size << " too small to hold value " << s << ")";
-    return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
+    return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2283,7 +2283,7 @@ Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const
 {
   CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
       << "Expected CVC4 to be compiled with SymFPU support";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeInf(FloatingPointSize(exp, sig), false));
 }
 
@@ -2291,7 +2291,7 @@ Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const
 {
   CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
       << "Expected CVC4 to be compiled with SymFPU support";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeInf(FloatingPointSize(exp, sig), true));
 }
 
@@ -2299,7 +2299,7 @@ Term Solver::mkNaN(uint32_t exp, uint32_t sig) const
 {
   CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
       << "Expected CVC4 to be compiled with SymFPU support";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeNaN(FloatingPointSize(exp, sig)));
 }
 
@@ -2307,7 +2307,7 @@ Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const
 {
   CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
       << "Expected CVC4 to be compiled with SymFPU support";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeZero(FloatingPointSize(exp, sig), false));
 }
 
@@ -2315,19 +2315,19 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const
 {
   CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
       << "Expected CVC4 to be compiled with SymFPU support";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeZero(FloatingPointSize(exp, sig), true));
 }
 
 Term Solver::mkRoundingMode(RoundingMode rm) const
 {
-  return mkConstHelper<CVC4::RoundingMode>(s_rmodes.at(rm));
+  return mkValHelper<CVC4::RoundingMode>(s_rmodes.at(rm));
 }
 
 Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const
 {
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
-  return mkConstHelper<CVC4::UninterpretedConstant>(
+  return mkValHelper<CVC4::UninterpretedConstant>(
       CVC4::UninterpretedConstant(*sort.d_type, index));
 }
 
@@ -2385,14 +2385,14 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
   CVC4_API_ARG_CHECK_EXPECTED(
       val.getSort().isBitVector() && val.d_expr->isConst(), val)
       << "bit-vector constant";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       CVC4::FloatingPoint(exp, sig, val.d_expr->getConst<BitVector>()));
 }
 
-/* Create variables                                                           */
+/* Create constants                                                           */
 /* -------------------------------------------------------------------------- */
 
-Term Solver::mkVar(Sort sort, const std::string& symbol) const
+Term Solver::mkConst(Sort sort, const std::string& symbol) const
 {
   try
   {
@@ -2408,7 +2408,10 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const
   }
 }
 
-Term Solver::mkBoundVar(Sort sort, const std::string& symbol) const
+/* Create variables                                                           */
+/* -------------------------------------------------------------------------- */
+
+Term Solver::mkVar(Sort sort, const std::string& symbol) const
 {
   try
   {
@@ -2436,8 +2439,9 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
       mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR,
       kind)
       << "Only operator-style terms are created with mkTerm(), "
-         "to create variables and constants see mkVar(), mkBoundVar(), "
-         "and mkConst().";
+         "to create variables, constants and values see mkVar(), mkConst() "
+         "and the respective theory-specific functions to create values, "
+         "e.g., mkBitVector().";
   CVC4_API_KIND_CHECK_EXPECTED(
       nchildren >= minArity(kind) && nchildren <= maxArity(kind), kind)
       << "Terms with kind " << kindToString(kind) << " must have at least "
@@ -2729,15 +2733,14 @@ std::vector<Expr> Solver::termVectorToExprs(
 OpTerm Solver::mkOpTerm(Kind kind, Kind k)
 {
   CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP";
-  return *mkConstHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get();
+  return *mkValHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get();
 }
 
 OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg)
 {
   CVC4_API_KIND_CHECK_EXPECTED(kind == RECORD_UPDATE_OP, kind)
       << "RECORD_UPDATE_OP";
-  return *mkConstHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg))
-              .d_expr.get();
+  return *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get();
 }
 
 OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg)
@@ -2747,59 +2750,59 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg)
   switch (kind)
   {
     case DIVISIBLE_OP:
-      res = *mkConstHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get();
+      res = *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get();
       break;
     case BITVECTOR_REPEAT_OP:
-      res = *mkConstHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
+      res = *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
                  .d_expr.get();
       break;
     case BITVECTOR_ZERO_EXTEND_OP:
-      res = *mkConstHelper<CVC4::BitVectorZeroExtend>(
+      res = *mkValHelper<CVC4::BitVectorZeroExtend>(
                  CVC4::BitVectorZeroExtend(arg))
                  .d_expr.get();
       break;
     case BITVECTOR_SIGN_EXTEND_OP:
-      res = *mkConstHelper<CVC4::BitVectorSignExtend>(
+      res = *mkValHelper<CVC4::BitVectorSignExtend>(
                  CVC4::BitVectorSignExtend(arg))
                  .d_expr.get();
       break;
     case BITVECTOR_ROTATE_LEFT_OP:
-      res = *mkConstHelper<CVC4::BitVectorRotateLeft>(
+      res = *mkValHelper<CVC4::BitVectorRotateLeft>(
                  CVC4::BitVectorRotateLeft(arg))
                  .d_expr.get();
       break;
     case BITVECTOR_ROTATE_RIGHT_OP:
-      res = *mkConstHelper<CVC4::BitVectorRotateRight>(
+      res = *mkValHelper<CVC4::BitVectorRotateRight>(
                  CVC4::BitVectorRotateRight(arg))
                  .d_expr.get();
       break;
     case INT_TO_BITVECTOR_OP:
-      res = *mkConstHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
+      res = *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_UBV_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToUBV>(
-                 CVC4::FloatingPointToUBV(arg))
-                 .d_expr.get();
+      res =
+          *mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg))
+               .d_expr.get();
       break;
     case FLOATINGPOINT_TO_UBV_TOTAL_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToUBVTotal>(
+      res = *mkValHelper<CVC4::FloatingPointToUBVTotal>(
                  CVC4::FloatingPointToUBVTotal(arg))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_SBV_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToSBV>(
-                 CVC4::FloatingPointToSBV(arg))
-                 .d_expr.get();
+      res =
+          *mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg))
+               .d_expr.get();
       break;
     case FLOATINGPOINT_TO_SBV_TOTAL_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToSBVTotal>(
+      res = *mkValHelper<CVC4::FloatingPointToSBVTotal>(
                  CVC4::FloatingPointToSBVTotal(arg))
                  .d_expr.get();
       break;
     case TUPLE_UPDATE_OP:
-      res = *mkConstHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg))
-                 .d_expr.get();
+      res =
+          *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get();
       break;
     default:
       CVC4_API_KIND_CHECK_EXPECTED(false, kind)
@@ -2816,37 +2819,37 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2)
   switch (kind)
   {
     case BITVECTOR_EXTRACT_OP:
-      res = *mkConstHelper<CVC4::BitVectorExtract>(
+      res = *mkValHelper<CVC4::BitVectorExtract>(
                  CVC4::BitVectorExtract(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPIEEEBitVector>(
+      res = *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>(
                  CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPFloatingPoint>(
+      res = *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>(
                  CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_REAL_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPReal>(
+      res = *mkValHelper<CVC4::FloatingPointToFPReal>(
                  CVC4::FloatingPointToFPReal(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPSignedBitVector>(
+      res = *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>(
                  CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
+      res = *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
                  CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_GENERIC_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPGeneric>(
+      res = *mkValHelper<CVC4::FloatingPointToFPGeneric>(
                  CVC4::FloatingPointToFPGeneric(arg1, arg2))
                  .d_expr.get();
       break;
@@ -2940,24 +2943,6 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
 }
 
 /**
- *  ( declare-const <symbol> <sort> )
- */
-Term Solver::declareConst(const std::string& symbol, Sort sort) 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());
-  }
-}
-
-/**
  *  ( declare-datatype <symbol> <datatype_decl> )
  */
 Sort Solver::declareDatatype(
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 203586066..c13c7919e 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2166,20 +2166,23 @@ class CVC4_PUBLIC Solver
   /* .................................................................... */
 
   /**
-   * Create variable.
-   * @param sort the sort of the variable
-   * @param symbol the name of the variable
-   * @return the variable
+   * Create (first-order) constant (0-arity function symbol).
+   * SMT-LIB: ( declare-const <symbol> <sort> )
+   * SMT-LIB: ( declare-fun <symbol> ( ) <sort> )
+   *
+   * @param sort the sort of the constant
+   * @param symbol the name of the constant
+   * @return the first-order constant
    */
-  Term mkVar(Sort sort, const std::string& symbol = std::string()) const;
+  Term mkConst(Sort sort, const std::string& symbol = std::string()) const;
 
   /**
-   * Create bound variable.
+   * Create (bound) variable.
    * @param sort the sort of the variable
    * @param symbol the name of the variable
    * @return the variable
    */
-  Term mkBoundVar(Sort sort, const std::string& symbol = std::string()) const;
+  Term mkVar(Sort sort, const std::string& symbol = std::string()) const;
 
   /* .................................................................... */
   /* Formula Handling                                                     */
@@ -2246,17 +2249,6 @@ class CVC4_PUBLIC Solver
   Result checkValidAssuming(const std::vector<Term>& assumptions) const;
 
   /**
-   * Declare first-order constant (0-arity function symbol).
-   * SMT-LIB: ( declare-const <symbol> <sort> )
-   * SMT-LIB: ( declare-fun <symbol> ( ) <sort> )
-   * This command corresponds to mkVar().
-   * @param symbol the name of the first-order constant
-   * @param sort the sort of the first-order constant
-   * @return the first-order constant
-   */
-  Term declareConst(const std::string& symbol, Sort sort) const;
-
-  /**
    * Create datatype sort.
    * SMT-LIB: ( declare-datatype <symbol> <datatype_decl> )
    * @param symbol the name of the datatype sort
@@ -2303,7 +2295,7 @@ class CVC4_PUBLIC Solver
   /**
    * Define n-ary function.
    * SMT-LIB: ( define-fun <function_def> )
-   * Create parameter 'fun' with mkVar().
+   * Create parameter 'fun' with mkConst().
    * @param fun the sorted function
    * @param bound_vars the parameters to this function
    * @param term the function body
@@ -2330,7 +2322,7 @@ class CVC4_PUBLIC Solver
   /**
    * Define recursive function.
    * SMT-LIB: ( define-fun-rec <function_def> )
-   * Create parameter 'fun' with mkVar().
+   * Create parameter 'fun' with mkConst().
    * @param fun the sorted function
    * @param bound_vars the parameters to this function
    * @param term the function body
@@ -2343,7 +2335,7 @@ class CVC4_PUBLIC Solver
   /**
    * Define recursive functions.
    * SMT-LIB: ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
-   * Create elements of parameter 'funs' with mkVar().
+   * Create elements of parameter 'funs' with mkConst().
    * @param funs the sorted functions
    * @param bound_vars the list of parameters to the functions
    * @param term the list of function bodies of the functions
@@ -2506,7 +2498,7 @@ class CVC4_PUBLIC Solver
   void checkMkTerm(Kind kind, uint32_t nchildren) const;
   /* Helper for mk-functions that call d_exprMgr->mkConst(). */
   template <typename T>
-  Term mkConstHelper(T t) const;
+  Term mkValHelper(T t) const;
   /* Helper for mkReal functions that take a string as argument. */
   Term mkRealFromStrHelper(std::string s) const;
   /* Helper for mkBitVector functions that take a string as argument. */
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 3aba6cebb..d4f6880f9 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -123,25 +123,25 @@ enum CVC4_PUBLIC Kind : int32_t
    */
   DISTINCT,
   /**
-   * Variable.
+   * First-order constant.
    * Not permitted in bindings (forall, exists, ...).
    * Parameters:
-   *   See mkVar().
+   *   See mkConst().
    * Create with:
-   *   mkVar(const std::string& symbol, Sort sort)
-   *   mkVar(Sort sort)
+   *   mkConst(const std::string& symbol, Sort sort)
+   *   mkConst(Sort sort)
    */
-  VARIABLE,
+  CONSTANT,
   /**
-   * Bound variable.
+   * (Bound) variable.
    * Permitted in bindings and in the lambda and quantifier bodies only.
    * Parameters:
-   *   See mkBoundVar().
+   *   See mkVar().
    * Create with:
-   *   mkBoundVar(const std::string& symbol, Sort sort)
-   *   mkBoundVar(Sort sort)
+   *   mkVar(const std::string& symbol, Sort sort)
+   *   mkVar(Sort sort)
    */
-  BOUND_VARIABLE,
+  VARIABLE,
 #if 0
   /* Skolem variable (internal only) */
   SKOLEM,
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 00f2e944d..75df38637 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2307,8 +2307,8 @@ termAtomic[CVC4::api::Term& atomTerm]
       sortSymbol[type,CHECK_DECLARED]
       sortSymbol[type2,CHECK_DECLARED]
       {
-        api::Term v1 = SOLVER->mkVar(api::Sort(type), "_emp1");
-        api::Term v2 = SOLVER->mkVar(api::Sort(type2), "_emp2");
+        api::Term v1 = SOLVER->mkConst(api::Sort(type), "_emp1");
+        api::Term v2 = SOLVER->mkConst(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 a5d927812..289fc26f0 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -76,7 +76,6 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkUniverseSet();
   void testMkVar();
 
-  void testDeclareConst();
   void testDeclareDatatype();
   void testDeclareFun();
   void testDeclareSort();
@@ -295,12 +294,12 @@ void SolverBlack::testMkBoundVar()
   Sort boolSort = d_solver->getBooleanSort();
   Sort intSort = d_solver->getIntegerSort();
   Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(boolSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(funSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(boolSort, std::string("b")));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(funSort, ""));
-  TS_ASSERT_THROWS(d_solver->mkBoundVar(Sort()), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkBoundVar(Sort(), "a"), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(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::testMkBoolean()
@@ -512,7 +511,7 @@ void SolverBlack::testMkReal()
 void SolverBlack::testMkRegexpEmpty()
 {
   Sort strSort = d_solver->getStringSort();
-  Term s = d_solver->mkVar(strSort, "s");
+  Term s = d_solver->mkConst(strSort, "s");
   TS_ASSERT_THROWS_NOTHING(
       d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpEmpty()));
 }
@@ -520,7 +519,7 @@ void SolverBlack::testMkRegexpEmpty()
 void SolverBlack::testMkRegexpSigma()
 {
   Sort strSort = d_solver->getStringSort();
-  Term s = d_solver->mkVar(strSort, "s");
+  Term s = d_solver->mkConst(strSort, "s");
   TS_ASSERT_THROWS_NOTHING(
       d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpSigma()));
 }
@@ -544,8 +543,8 @@ void SolverBlack::testMkString()
 void SolverBlack::testMkTerm()
 {
   Sort bv32 = d_solver->mkBitVectorSort(32);
-  Term a = d_solver->mkVar(bv32, "a");
-  Term b = d_solver->mkVar(bv32, "b");
+  Term a = d_solver->mkConst(bv32, "a");
+  Term b = d_solver->mkConst(bv32, "b");
   std::vector<Term> v1 = {a, b};
   std::vector<Term> v2 = {a, Term()};
   std::vector<Term> v3 = {a, d_solver->mkTrue()};
@@ -597,8 +596,8 @@ void SolverBlack::testMkTerm()
 void SolverBlack::testMkTermFromOpTerm()
 {
   Sort bv32 = d_solver->mkBitVectorSort(32);
-  Term a = d_solver->mkVar(bv32, "a");
-  Term b = d_solver->mkVar(bv32, "b");
+  Term a = d_solver->mkConst(bv32, "a");
+  Term b = d_solver->mkConst(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 = {};
@@ -620,7 +619,7 @@ void SolverBlack::testMkTermFromOpTerm()
   Sort listSort = d_solver->mkDatatypeSort(listDecl);
   Sort intListSort =
       listSort.instantiate(std::vector<Sort>{d_solver->getIntegerSort()});
-  Term c = d_solver->declareConst("c", intListSort);
+  Term c = d_solver->mkConst(intListSort, "c");
   Datatype list = listSort.getDatatype();
   // list datatype constructor and selector operator terms
   OpTerm consTerm1 = list.getConstructorTerm("cons");
@@ -733,24 +732,14 @@ void SolverBlack::testMkVar()
   Sort boolSort = d_solver->getBooleanSort();
   Sort intSort = d_solver->getIntegerSort();
   Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(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()
-{
-  Sort boolSort = d_solver->getBooleanSort();
-  Sort intSort = d_solver->getIntegerSort();
-  Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareConst(std::string("b"), boolSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareConst(std::string("i"), intSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareConst("f", funSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareConst("", funSort));
-  TS_ASSERT_THROWS(d_solver->declareConst("a", Sort()), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(boolSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(boolSort, std::string("b")));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(intSort, std::string("i")));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort, "f"));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort, ""));
+  TS_ASSERT_THROWS(d_solver->mkConst(Sort()), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkConst(Sort(), "a"), CVC4ApiException&);
 }
 
 void SolverBlack::testDeclareDatatype()
@@ -797,16 +786,16 @@ void SolverBlack::testDefineFun()
   Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
   Sort funSort2 = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"),
                                            d_solver->getIntegerSort());
-  Term b1 = d_solver->mkBoundVar(bvSort, "b1");
-  Term b11 = d_solver->mkBoundVar(bvSort, "b1");
-  Term b2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "b2");
-  Term b3 = d_solver->mkBoundVar(funSort2, "b3");
-  Term v1 = d_solver->mkBoundVar(bvSort, "v1");
-  Term v2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "v2");
-  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);
+  Term b1 = d_solver->mkVar(bvSort, "b1");
+  Term b11 = d_solver->mkVar(bvSort, "b1");
+  Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2");
+  Term b3 = d_solver->mkVar(funSort2, "b3");
+  Term v1 = d_solver->mkVar(bvSort, "v1");
+  Term v2 = d_solver->mkVar(d_solver->getIntegerSort(), "v2");
+  Term v3 = d_solver->mkConst(funSort2, "v3");
+  Term f1 = d_solver->mkConst(funSort1, "f1");
+  Term f2 = d_solver->mkConst(funSort2, "f2");
+  Term f3 = d_solver->mkConst(bvSort, "f3");
   TS_ASSERT_THROWS_NOTHING(d_solver->defineFun("f", {}, bvSort, v1));
   TS_ASSERT_THROWS_NOTHING(d_solver->defineFun("ff", {b1, b2}, bvSort, v1));
   TS_ASSERT_THROWS_NOTHING(d_solver->defineFun(f1, {b1, b11}, v1));
@@ -829,16 +818,16 @@ void SolverBlack::testDefineFunRec()
   Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
   Sort funSort2 = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"),
                                            d_solver->getIntegerSort());
-  Term b1 = d_solver->mkBoundVar(bvSort, "b1");
-  Term b11 = d_solver->mkBoundVar(bvSort, "b1");
-  Term b2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "b2");
-  Term b3 = d_solver->mkBoundVar(funSort2, "b3");
-  Term v1 = d_solver->mkBoundVar(bvSort, "v1");
-  Term v2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "v2");
-  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);
+  Term b1 = d_solver->mkVar(bvSort, "b1");
+  Term b11 = d_solver->mkVar(bvSort, "b1");
+  Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2");
+  Term b3 = d_solver->mkVar(funSort2, "b3");
+  Term v1 = d_solver->mkVar(bvSort, "v1");
+  Term v2 = d_solver->mkVar(d_solver->getIntegerSort(), "v2");
+  Term v3 = d_solver->mkConst(funSort2, "v3");
+  Term f1 = d_solver->mkConst(funSort1, "f1");
+  Term f2 = d_solver->mkConst(funSort2, "f2");
+  Term f3 = d_solver->mkConst(bvSort, "f3");
   TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec("f", {}, bvSort, v1));
   TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec("ff", {b1, b2}, bvSort, v1));
   TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec(f1, {b1, b11}, v1));
@@ -863,18 +852,18 @@ void SolverBlack::testDefineFunsRec()
   Sort bvSort = d_solver->mkBitVectorSort(32);
   Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
   Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort());
-  Term b1 = d_solver->mkBoundVar(bvSort, "b1");
-  Term b11 = d_solver->mkBoundVar(bvSort, "b1");
-  Term b2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "b2");
-  Term b3 = d_solver->mkBoundVar(funSort2, "b3");
-  Term b4 = d_solver->mkBoundVar(uSort, "b4");
-  Term v1 = d_solver->mkBoundVar(bvSort, "v1");
-  Term v2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "v2");
-  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);
+  Term b1 = d_solver->mkVar(bvSort, "b1");
+  Term b11 = d_solver->mkVar(bvSort, "b1");
+  Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2");
+  Term b3 = d_solver->mkVar(funSort2, "b3");
+  Term b4 = d_solver->mkVar(uSort, "b4");
+  Term v1 = d_solver->mkVar(bvSort, "v1");
+  Term v2 = d_solver->mkVar(d_solver->getIntegerSort(), "v2");
+  Term v3 = d_solver->mkConst(funSort2, "v3");
+  Term v4 = d_solver->mkConst(uSort, "v4");
+  Term f1 = d_solver->mkConst(funSort1, "f1");
+  Term f2 = d_solver->mkConst(funSort2, "f2");
+  Term f3 = d_solver->mkConst(bvSort, "f3");
   TS_ASSERT_THROWS_NOTHING(
       d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2}));
   TS_ASSERT_THROWS(