api: Rename BOUND_VAR_LIST to VARIABLE_LIST. (#7632)

diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java
index 0d78562bbe9b4a584c64e03558129d93741048c6..fb082fc11e184f719713fc6c7afc5a5241693da8 100644 (file)
--- a/examples/api/java/Relations.java
+++ b/examples/api/java/Relations.java
@@ -164,7 +164,7 @@ public class Relations
       Term member = solver.mkTerm(MEMBER, xxTuple, ancestor);
       Term notMember = solver.mkTerm(NOT, member);
 
-      Term quantifiedVariables = solver.mkTerm(BOUND_VAR_LIST, x);
+      Term quantifiedVariables = solver.mkTerm(VARIABLE_LIST, x);
       Term noSelfAncestor = solver.mkTerm(FORALL, quantifiedVariables, notMember);
 
       // formulas

diff --git a/examples/api/java/Statistics.java b/examples/api/java/Statistics.java
index 751dda94767e0dbd9970a8794e7878766fa62c56..7db7cc4f34d83aa108eddc5a2ad5c0e53b1a371f 100644 (file)
--- a/examples/api/java/Statistics.java
+++ b/examples/api/java/Statistics.java
@@ -206,7 +206,7 @@ public class Statistics
     Term member = solver.mkTerm(MEMBER, xxTuple, ancestor);
     Term notMember = solver.mkTerm(NOT, member);
 
-    Term quantifiedVariables = solver.mkTerm(BOUND_VAR_LIST, var);
+    Term quantifiedVariables = solver.mkTerm(VARIABLE_LIST, var);
     Term noSelfAncestor = solver.mkTerm(FORALL, quantifiedVariables, notMember);
 
     // formulas

diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp
index 1bdadfca2534e473a950850c52d5bb28ccbd7439..ea8aa10a435b212ddee5d9577f4e3d8d84e91906 100644 (file)
--- a/examples/simple_vc_quant_cxx.cpp
+++ b/examples/simple_vc_quant_cxx.cpp
@@ -33,7 +33,7 @@ int main() {
   Term x = slv.mkVar(integer, "x");
 
   // make forall x. P( x )
-  Term var_list = slv.mkTerm(Kind::BOUND_VAR_LIST, x);
+  Term var_list = slv.mkTerm(Kind::VARIABLE_LIST, x);
   Term px = slv.mkTerm(Kind::APPLY_UF, p, x);
   Term quantpospx = slv.mkTerm(Kind::FORALL, var_list, px);
   std::cout << "Made expression : " << quantpospx << std::endl;

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 0c7e86c8634b9b71588bc0216f772a515dbe567c..b80f68202c540364c6160794770601aafce61a65 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -373,7 +373,7 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
     /* Quantifiers --------------------------------------------------------- */
     {FORALL, cvc5::Kind::FORALL},
     {EXISTS, cvc5::Kind::EXISTS},
-    {BOUND_VAR_LIST, cvc5::Kind::BOUND_VAR_LIST},
+    {VARIABLE_LIST, cvc5::Kind::BOUND_VAR_LIST},
     {INST_PATTERN, cvc5::Kind::INST_PATTERN},
     {INST_NO_PATTERN, cvc5::Kind::INST_NO_PATTERN},
     {INST_POOL, cvc5::Kind::INST_POOL},
@@ -673,7 +673,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
         /* Quantifiers ----------------------------------------------------- */
         {cvc5::Kind::FORALL, FORALL},
         {cvc5::Kind::EXISTS, EXISTS},
-        {cvc5::Kind::BOUND_VAR_LIST, BOUND_VAR_LIST},
+        {cvc5::Kind::BOUND_VAR_LIST, VARIABLE_LIST},
         {cvc5::Kind::INST_PATTERN, INST_PATTERN},
         {cvc5::Kind::INST_NO_PATTERN, INST_NO_PATTERN},
         {cvc5::Kind::INST_POOL, INST_POOL},

diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 29cb130d4f0f8c75673ebe1735fb68d3948cf38a..1c181988959b372daabf345d22e1f7c76285fb32 100644 (file)
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -159,7 +159,7 @@ enum Kind : int32_t
    * Lambda expression.
    *
    * Parameters:
-   *   - 1: BOUND_VAR_LIST
+   *   - 1: VARIABLE_LIST
    *   - 2: Lambda body
    *
    * Create with:
@@ -169,7 +169,7 @@ enum Kind : int32_t
   LAMBDA,
   /**
    * The syntax of a witness term is similar to a quantified formula except that
-   * only one bound variable is allowed.
+   * only one variable is allowed.
    * The term `(witness ((x T)) F)` returns an element `x` of type `T`
    * and asserts `F`.
    *
@@ -201,7 +201,7 @@ enum Kind : int32_t
    * whereas notice that `(or (= z 0) (not (= z 0)))` is true for any `z`.
    *
    * Parameters:
-   *   - 1: BOUND_VAR_LIST
+   *   - 1: VARIABLE_LIST
    *   - 2: Witness body
    *
    * Create with:
@@ -1954,7 +1954,7 @@ enum Kind : int32_t
    * is represented by the AST
    *
    *     (MATCH l
-   *       (MATCH_BIND_CASE (BOUND_VAR_LIST h t) (cons h t) h)
+   *       (MATCH_BIND_CASE (VARIABLE_LIST h t) (cons h t) h)
    *       (MATCH_CASE nil 0))
    *
    * The type of the last argument of each case term could be equal.
@@ -1987,7 +1987,7 @@ enum Kind : int32_t
    * A (non-constant) case expression to be used within a match expression.
    *
    * Parameters:
-   *   - 1: a BOUND_VAR_LIST Term containing the free variables of the case
+   *   - 1: a VARIABLE_LIST Term containing the free variables of the case
    *   - 2: Term denoting the pattern expression
    *   - 3: Term denoting the return value
    *
@@ -2228,7 +2228,7 @@ enum Kind : int32_t
   SET_UNIVERSE,
   /**
    * Set comprehension
-   * A set comprehension is specified by a bound variable list x1 ... xn,
+   * A set comprehension is specified by a variable list x1 ... xn,
    * a predicate P[x1...xn], and a term t[x1...xn]. A comprehension C with the
    * above form has members given by the following semantics:
    * @f[
@@ -2240,7 +2240,7 @@ enum Kind : int32_t
    * y in the above formula.
    *
    * Parameters:
-   *   - 1: Term BOUND_VAR_LIST
+   *   - 1: Term VARIABLE_LIST
    *   - 2: Term denoting the predicate of the comprehension
    *   - 3: (optional) a Term denoting the generator for the comprehension
    *
@@ -3273,7 +3273,7 @@ enum Kind : int32_t
    * Universally quantified formula.
    *
    * Parameters:
-   *   - 1: BOUND_VAR_LIST Term
+   *   - 1: VARIABLE_LIST Term
    *   - 2: Quantifier body
    *   - 3: (optional) INST_PATTERN_LIST Term
    *
@@ -3287,7 +3287,7 @@ enum Kind : int32_t
    * Existentially quantified formula.
    *
    * Parameters:
-   *   - 1: BOUND_VAR_LIST Term
+   *   - 1: VARIABLE_LIST Term
    *   - 2: Quantifier body
    *   - 3: (optional) INST_PATTERN_LIST Term
    *
@@ -3298,24 +3298,24 @@ enum Kind : int32_t
    */
   EXISTS,
   /**
-   * A list of bound variables (used to bind variables under a quantifier)
+   * A list of variables (used to bind variables under a quantifier)
    *
    * Parameters: n > 1
-   *   - 1..n: Terms with kind BOUND_VARIABLE
+   *   - 1..n: Terms with kind VARIABLE
    *
    * Create with:
    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
    */
-  BOUND_VAR_LIST,
+  VARIABLE_LIST,
   /**
    * An instantiation pattern.
    * Specifies a (list of) terms to be used as a pattern for quantifier
    * instantiation.
    *
    * Parameters: n > 1
-   *   - 1..n: Terms with kind BOUND_VARIABLE
+   *   - 1..n: Terms of any sort
    *
    * Create with:
    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
@@ -3329,7 +3329,7 @@ enum Kind : int32_t
    * quantifier instantiation.
    *
    * Parameters: n > 1
-   *   - 1..n: Terms with kind BOUND_VARIABLE
+   *   - 1..n: Terms of any sort
    *
    * Create with:
    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 4b4b7c10bf0c7fff736e5b20f3c84dac2b892c07..211fb4c80d7f89fa782796d1c12ee3e989a43d0c 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1396,7 +1396,7 @@ termNonVariable[cvc5::api::Term& expr, cvc5::api::Term& expr2]
           cargs.push_back(f);
           cargs.insert(cargs.end(),args.begin(),args.end());
           api::Term c = MK_TERM(api::APPLY_CONSTRUCTOR,cargs);
-          api::Term bvla = MK_TERM(api::BOUND_VAR_LIST,args);
+          api::Term bvla = MK_TERM(api::VARIABLE_LIST,args);
           api::Term mc = MK_TERM(api::MATCH_BIND_CASE, bvla, c, f3);
           matchcases.push_back(mc);
           // now, pop the scope
@@ -1427,7 +1427,7 @@ termNonVariable[cvc5::api::Term& expr, cvc5::api::Term& expr2]
           api::Term mc;
           if (f.getKind() == api::VARIABLE)
           {
-            api::Term bvlf = MK_TERM(api::BOUND_VAR_LIST, f);
+            api::Term bvlf = MK_TERM(api::VARIABLE_LIST, f);
             mc = MK_TERM(api::MATCH_BIND_CASE, bvlf, f, f3);
           }
           else
@@ -1935,7 +1935,7 @@ boundVarList[cvc5::api::Term& expr]
    {
      std::vector<cvc5::api::Term> args =
          PARSER_STATE->bindBoundVars(sortedVarNames);
-     expr = MK_TERM(api::BOUND_VAR_LIST, args);
+     expr = MK_TERM(api::VARIABLE_LIST, args);
    }
  ;
 

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 9ef04c348eea3d53188a64d3dd1163fde2baa610..419acafc014c7f8a71e1cf34eca0e60619aeb279 100644 (file)
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -151,7 +151,7 @@ parseCommand returns [cvc5::Command* cmd = NULL]
   { PARSER_STATE->popScope();
     std::vector<api::Term> bvl = PARSER_STATE->getFreeVar();
     if(!bvl.empty()) {
-      expr = MK_TERM(api::FORALL,MK_TERM(api::BOUND_VAR_LIST,bvl),expr);
+      expr = MK_TERM(api::FORALL,MK_TERM(api::VARIABLE_LIST,bvl),expr);
     };
   }
     (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK
@@ -469,9 +469,9 @@ definedPred[cvc5::ParseOp& p]
                   MK_TERM(api::NOT,
                           MK_TERM(api::EQUAL, r, SOLVER->mkInteger(0))),
                   MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr)));
-      api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r);
+      api::Term bvl = MK_TERM(api::VARIABLE_LIST, q, r);
       body = MK_TERM(api::EXISTS, bvl, body);
-      api::Term lbvl = MK_TERM(api::BOUND_VAR_LIST, n);
+      api::Term lbvl = MK_TERM(api::VARIABLE_LIST, n);
       p.d_kind = api::LAMBDA;
       p.d_expr = MK_TERM(api::LAMBDA, lbvl, body);
     }
@@ -529,9 +529,9 @@ thfDefinedPred[cvc5::ParseOp& p]
           MK_TERM(api::NOT,
                   MK_TERM(api::EQUAL, r, SOLVER->mkInteger(0))),
           MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr)));
-      api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r);
+      api::Term bvl = MK_TERM(api::VARIABLE_LIST, q, r);
       body = MK_TERM(api::EXISTS, bvl, body);
-      api::Term lbvl = MK_TERM(api::BOUND_VAR_LIST, n);
+      api::Term lbvl = MK_TERM(api::VARIABLE_LIST, n);
       p.d_kind = api::LAMBDA;
       p.d_expr = MK_TERM(api::LAMBDA, lbvl, body);
     }
@@ -591,7 +591,7 @@ definedFun[cvc5::ParseOp& p]
     {
       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
       api::Term d = SOLVER->mkVar(SOLVER->getRealSort(), "D");
-      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n, d);
+      api::Term formals = MK_TERM(api::VARIABLE_LIST, n, d);
       api::Term expr = MK_TERM(api::DIVISION, n, d);
       expr = MK_TERM(api::ITE,
                      MK_TERM(api::GEQ, d, SOLVER->mkReal(0)),
@@ -614,7 +614,7 @@ definedFun[cvc5::ParseOp& p]
     {
       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
       api::Term d = SOLVER->mkVar(SOLVER->getRealSort(), "D");
-      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n, d);
+      api::Term formals = MK_TERM(api::VARIABLE_LIST, n, d);
       api::Term expr = MK_TERM(api::DIVISION, n, d);
       expr = MK_TERM(api::ITE,
                      MK_TERM(api::GEQ, expr, SOLVER->mkReal(0)),
@@ -637,7 +637,7 @@ definedFun[cvc5::ParseOp& p]
     {
       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
       api::Term d = SOLVER->mkVar(SOLVER->getRealSort(), "D");
-      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n, d);
+      api::Term formals = MK_TERM(api::VARIABLE_LIST, n, d);
       api::Term expr = MK_TERM(api::DIVISION, n, d);
       expr = MK_TERM(api::TO_INTEGER, expr);
       if (remainder)
@@ -655,7 +655,7 @@ definedFun[cvc5::ParseOp& p]
   | '$ceiling'
     {
       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
-      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n);
+      api::Term formals = MK_TERM(api::VARIABLE_LIST, n);
       api::Term expr = MK_TERM(api::UMINUS,
                           MK_TERM(api::TO_INTEGER, MK_TERM(api::UMINUS, n)));
       p.d_kind = api::LAMBDA;
@@ -664,7 +664,7 @@ definedFun[cvc5::ParseOp& p]
   | '$truncate'
     {
       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
-      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n);
+      api::Term formals = MK_TERM(api::VARIABLE_LIST, n);
       api::Term expr =
           MK_TERM(api::ITE,
                   MK_TERM(api::GEQ, n, SOLVER->mkReal(0)),
@@ -677,7 +677,7 @@ definedFun[cvc5::ParseOp& p]
   | '$round'
     {
       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
-      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n);
+      api::Term formals = MK_TERM(api::VARIABLE_LIST, n);
       api::Term decPart = MK_TERM(api::MINUS, n, MK_TERM(api::TO_INTEGER, n));
       api::Term expr = MK_TERM(
           api::ITE,
@@ -884,7 +884,7 @@ fofUnitaryFormula[cvc5::api::Term& expr]
       ( COMMA_TOK bindvariable[expr] { bv.push_back(expr); } )* ) RBRACK_TOK
     COLON_TOK fofUnitaryFormula[expr]
     { PARSER_STATE->popScope();
-      expr = MK_TERM(kind, MK_TERM(api::BOUND_VAR_LIST, bv), expr);
+      expr = MK_TERM(kind, MK_TERM(api::VARIABLE_LIST, bv), expr);
     }
   ;
 
@@ -1280,10 +1280,10 @@ thfUnitaryFormula[cvc5::ParseOp& p]
       {
         // apply body of lambda to flatten vars
         expr = PARSER_STATE->mkHoApply(expr, flattenVars);
-        // add variables to BOUND_VAR_LIST
+        // add variables to VARIABLE_LIST
         bv.insert(bv.end(), flattenVars.begin(), flattenVars.end());
       }
-      p.d_expr = MK_TERM(p.d_kind, MK_TERM(api::BOUND_VAR_LIST, bv), expr);
+      p.d_expr = MK_TERM(p.d_kind, MK_TERM(api::VARIABLE_LIST, bv), expr);
     }
   ;
 
@@ -1393,7 +1393,7 @@ tffUnitaryFormula[cvc5::api::Term& expr]
       ( COMMA_TOK tffbindvariable[expr] { bv.push_back(expr); } )* ) RBRACK_TOK
     COLON_TOK tffUnitaryFormula[expr]
     { PARSER_STATE->popScope();
-      expr = MK_TERM(kind, MK_TERM(api::BOUND_VAR_LIST, bv), expr);
+      expr = MK_TERM(kind, MK_TERM(api::VARIABLE_LIST, bv), expr);
     }
   | '$ite_f' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK tffLogicFormula[lhs] COMMA_TOK tffLogicFormula[rhs] RPAREN_TOK
     { expr = MK_TERM(api::ITE, expr, lhs, rhs); }
@@ -1428,7 +1428,7 @@ tffLetTermBinding[std::vector<cvc5::api::Term> & bvlist,
   {
     PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false);
     std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
-    rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
+    rhs = MK_TERM(api::LAMBDA, MK_TERM(api::VARIABLE_LIST, lchildren), rhs);
     // since lhs is always APPLY_UF (otherwise we'd have had a parser error in
     // checkLetBinding) the function to be replaced is always the first
     // argument. Note that the way in which lchildren is built above is also
@@ -1454,7 +1454,7 @@ tffLetFormulaBinding[std::vector<cvc5::api::Term> & bvlist,
   {
     PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true);
     std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
-    rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
+    rhs = MK_TERM(api::LAMBDA, MK_TERM(api::VARIABLE_LIST, lchildren), rhs);
     // since lhs is always APPLY_UF (otherwise we'd have had a parser error in
     // checkLetBinding) the function to be replaced is always the first
     // argument. Note that the way in which lchildren is built above is also

diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 7c65f5c57f390fc8a355aba9058ce18a08f176d3..b8b81df249a30519bf05247a529d51d8b95fcda2 100644 (file)
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -524,7 +524,7 @@ api::Term Tptp::mkLambdaWrapper(api::Kind k, api::Sort argType)
   // apply body of lambda to variables
   api::Term wrapper =
       d_solver->mkTerm(api::LAMBDA,
-                       d_solver->mkTerm(api::BOUND_VAR_LIST, lvars),
+                       d_solver->mkTerm(api::VARIABLE_LIST, lvars),
                        d_solver->mkTerm(k, lvars));
 
   return wrapper;

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 51a0f38b5a9956116482d159a534c02f9fb61108..b24c854964c9778accdeb2ace8861afc5e1c146b 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -1601,7 +1601,7 @@ TEST_F(TestApiBlackSolver, getModelDomainElements2)
   Term x = d_solver.mkVar(uSort, "x");
   Term y = d_solver.mkVar(uSort, "y");
   Term eq = d_solver.mkTerm(EQUAL, x, y);
-  Term bvl = d_solver.mkTerm(BOUND_VAR_LIST, x, y);
+  Term bvl = d_solver.mkTerm(VARIABLE_LIST, x, y);
   Term f = d_solver.mkTerm(FORALL, bvl, eq);
   d_solver.assertFormula(f);
   d_solver.checkSat();
@@ -1674,7 +1674,7 @@ TEST_F(TestApiBlackSolver, getQuantifierElimination)
   Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
   Term forall =
       d_solver.mkTerm(FORALL,
-                      d_solver.mkTerm(BOUND_VAR_LIST, x),
+                      d_solver.mkTerm(VARIABLE_LIST, x),
                       d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
   ASSERT_THROW(d_solver.getQuantifierElimination(Term()), CVC5ApiException);
   ASSERT_THROW(d_solver.getQuantifierElimination(Solver().mkBoolean(false)),
@@ -1687,7 +1687,7 @@ TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct)
   Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
   Term forall =
       d_solver.mkTerm(FORALL,
-                      d_solver.mkTerm(BOUND_VAR_LIST, x),
+                      d_solver.mkTerm(VARIABLE_LIST, x),
                       d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
   ASSERT_THROW(d_solver.getQuantifierEliminationDisjunct(Term()),
                CVC5ApiException);

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 6a08d79c64750421089a27f71167311fdd3de305..40a7d41576f6410e734a7ba96e20f9006a92f3a4 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -1645,7 +1645,7 @@ class SolverTest
     Term x = d_solver.mkVar(uSort, "x");
     Term y = d_solver.mkVar(uSort, "y");
     Term eq = d_solver.mkTerm(EQUAL, x, y);
-    Term bvl = d_solver.mkTerm(BOUND_VAR_LIST, x, y);
+    Term bvl = d_solver.mkTerm(VARIABLE_LIST, x, y);
     Term f = d_solver.mkTerm(FORALL, bvl, eq);
     d_solver.assertFormula(f);
     d_solver.checkSat();
@@ -1713,9 +1713,8 @@ class SolverTest
   @Test void getQuantifierElimination()
   {
     Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
-    Term forall = d_solver.mkTerm(FORALL,
-        d_solver.mkTerm(BOUND_VAR_LIST, x),
-        d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
+    Term forall = d_solver.mkTerm(
+        FORALL, d_solver.mkTerm(VARIABLE_LIST, x), d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
     assertThrows(
         CVC5ApiException.class, () -> d_solver.getQuantifierElimination(d_solver.getNullTerm()));
     Solver slv = new Solver();
@@ -1729,9 +1728,8 @@ class SolverTest
   @Test void getQuantifierEliminationDisjunct()
   {
     Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
-    Term forall = d_solver.mkTerm(FORALL,
-        d_solver.mkTerm(BOUND_VAR_LIST, x),
-        d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
+    Term forall = d_solver.mkTerm(
+        FORALL, d_solver.mkTerm(VARIABLE_LIST, x), d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
     assertThrows(CVC5ApiException.class,
         () -> d_solver.getQuantifierEliminationDisjunct(d_solver.getNullTerm()));