Check for free variables in several SolverEngine calls (#8130)

Fixes the nightlies due to ensuring that a unit test fails in production (it was failing only in debug).

Fixes #8127.

diff --git a/examples/api/cpp/helloworld.cpp b/examples/api/cpp/helloworld.cpp
index 3d11d1bd0df076c2572b5e86fdaefc008cf04b23..d8c9327b8bb8b354dbc88c8c8b6b8701d8b03ed7 100644 (file)
--- a/examples/api/cpp/helloworld.cpp
+++ b/examples/api/cpp/helloworld.cpp
@@ -22,7 +22,7 @@ using namespace cvc5::api;
 int main()
 {
   Solver slv;
-  Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!");
+  Term helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!");
   std::cout << helloworld << " is " << slv.checkEntailed(helloworld)
             << std::endl;
   return 0;

diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java
index 7535430e3b4679a7b83e73da03c2aa2af1db99c6..3c2de1e2dcdff4c8609510a6fc9e98ca19b19db7 100644 (file)
--- a/examples/api/java/HelloWorld.java
+++ b/examples/api/java/HelloWorld.java
@@ -21,7 +21,7 @@ public class HelloWorld
   {
     try (Solver slv = new Solver())
     {
-      Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!");
+      Term helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!");
 
       System.out.println(helloworld + " is " + slv.checkEntailed(helloworld));
     }

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 99fec60b42e0bb43c207a3b2f34ae3860fc2fb81..51f8b911d5819dfd9215c435d9620371a4c5f3bc 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -57,6 +57,7 @@
 #include "expr/sequence.h"
 #include "expr/type_node.h"
 #include "options/base_options.h"
+#include "options/expr_options.h"
 #include "options/main_options.h"
 #include "options/option_exception.h"
 #include "options/options.h"
@@ -5435,6 +5436,34 @@ bool Solver::isValidInteger(const std::string& s) const
   return true;
 }
 
+void Solver::ensureWellFormedTerm(const Term& t) const
+{
+  // only check if option is set
+  if (d_slv->getOptions().expr.wellFormedChecking)
+  {
+    bool wasShadow = false;
+    if (expr::hasFreeOrShadowedVar(*t.d_node, wasShadow))
+    {
+      std::stringstream se;
+      se << "Cannot process term with " << (wasShadow ? "shadowed" : "free")
+         << " variable";
+      throw CVC5ApiException(se.str().c_str());
+    }
+  }
+}
+
+void Solver::ensureWellFormedTerms(const std::vector<Term>& ts) const
+{
+  // only check if option is set
+  if (d_slv->getOptions().expr.wellFormedChecking)
+  {
+    for (const Term& t : ts)
+    {
+      ensureWellFormedTerm(t);
+    }
+  }
+}
+
 void Solver::resetStatistics()
 {
   if constexpr (configuration::isStatisticsBuild())
@@ -6631,6 +6660,7 @@ Result Solver::checkEntailed(const Term& term) const
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   CVC5_API_SOLVER_CHECK_TERM(term);
+  ensureWellFormedTerm(term);
   //////// all checks before this line
   return d_slv->checkEntailed(*term.d_node);
   ////////
@@ -6645,6 +6675,7 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   CVC5_API_SOLVER_CHECK_TERMS(terms);
+  ensureWellFormedTerms(terms);
   //////// all checks before this line
   return d_slv->checkEntailed(Term::termVectorToNodes(terms));
   ////////
@@ -6659,6 +6690,7 @@ void Solver::assertFormula(const Term& term) const
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(term);
   CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(term, getBooleanSort());
+  ensureWellFormedTerm(term);
   //////// all checks before this line
   d_slv->assertFormula(*term.d_node);
   ////////
@@ -6686,6 +6718,7 @@ Result Solver::checkSatAssuming(const Term& assumption) const
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort());
+  ensureWellFormedTerm(assumption);
   //////// all checks before this line
   return d_slv->checkSat(*assumption.d_node);
   ////////
@@ -6700,6 +6733,7 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions, getBooleanSort());
+  ensureWellFormedTerms(assumptions);
   //////// all checks before this line
   for (const Term& term : assumptions)
   {
@@ -7286,6 +7320,7 @@ Term Solver::getValue(const Term& term) const
   CVC5_API_RECOVERABLE_CHECK(!term.getSort().isDatatype()
                              || term.getSort().getDatatype().isWellFounded())
       << "Cannot get value of a term of non-well-founded datatype sort.";
+  ensureWellFormedTerm(term);
   //////// all checks before this line
   return getValueHelper(term);
   ////////
@@ -7309,6 +7344,7 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
         << "Cannot get value of a term of non-well-founded datatype sort.";
   }
   CVC5_API_SOLVER_CHECK_TERMS(terms);
+  ensureWellFormedTerms(terms);
   //////// all checks before this line
 
   std::vector<Term> res;
@@ -7644,6 +7680,7 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const
   CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms)
       << "a non-empty set of terms";
   CVC5_API_SOLVER_CHECK_TERMS(terms);
+  ensureWellFormedTerms(terms);
   //////// all checks before this line
   d_slv->blockModelValues(Term::termVectorToNodes(terms));
   ////////

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 0256f0e61168fd1da86bc496dfffeec6900fc1d5..e75bef2938777cd4fc5308932a39a443494600be 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -5001,6 +5001,16 @@ class CVC5_EXPORT Solver
   /** Check whether string s is a valid decimal integer. */
   bool isValidInteger(const std::string& s) const;
 
+  /**
+   * Check that the given term is a valid closed term, which can be used as an
+   * argument to, e.g., assert, get-value, block-model-values, etc.
+   *
+   * @param t The term to check
+   */
+  void ensureWellFormedTerm(const Term& t) const;
+  /** Vector version of above. */
+  void ensureWellFormedTerms(const std::vector<Term>& ts) const;
+
   /** Increment the term stats counter. */
   void increment_term_stats(Kind kind) const;
   /** Increment the vars stats (if 'is_var') or consts stats counter. */

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 73aa3ae7db936ec7ab69b3c8a21d73249553b812..1b33f5ac6774d49299ed6460f023cdbd680f80e4 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -197,6 +197,12 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
       {
         solver->setOption("incremental", "false");
       }
+      // we don't need to check that terms passed to API methods are well
+      // formed, since this should be an invariant of the parser
+      if (!solver->getOptionInfo("wf-checking").setByUser)
+      {
+        solver->setOption("wf-checking", "false");
+      }
 
       ParserBuilder parserBuilder(
           pExecutor->getSolver(), pExecutor->getSymbolManager(), true);

diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml
index 79bbc9f19c238ed0e97f230efc9d46147728b34b..6f2174a4f5a259740d70447b5d6c5bf80fa50c6f 100644 (file)
--- a/src/options/expr_options.toml
+++ b/src/options/expr_options.toml
@@ -28,3 +28,11 @@ name   = "Expression"
   type       = "bool"
   default    = "DO_SEMANTIC_CHECKS_BY_DEFAULT"
   help       = "type check expressions"
+
+[[option]]
+  name       = "wellFormedChecking"
+  category   = "regular"
+  long       = "wf-checking"
+  type       = "bool"
+  default    = "true"
+  help       = "check that terms passed to API methods are well formed (default false for text interface)"

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 39ee661a063d0352f5ef5d3623a2e0b7a318c7c1..1223e9875ebc4243fec3457297dd601ab6b5c26c 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -740,6 +740,7 @@ Result SolverEngine::checkSat()
 
 Result SolverEngine::checkSat(const Node& assumption)
 {
+  ensureWellFormedTerm(assumption, "checkSat");
   std::vector<Node> assump;
   if (!assumption.isNull())
   {
@@ -750,11 +751,13 @@ Result SolverEngine::checkSat(const Node& assumption)
 
 Result SolverEngine::checkSat(const std::vector<Node>& assumptions)
 {
+  ensureWellFormedTerms(assumptions, "checkSat");
   return checkSatInternal(assumptions, false);
 }
 
 Result SolverEngine::checkEntailed(const Node& node)
 {
+  ensureWellFormedTerm(node, "checkEntailed");
   return checkSatInternal(
              node.isNull() ? std::vector<Node>() : std::vector<Node>{node},
              true)
@@ -763,6 +766,7 @@ Result SolverEngine::checkEntailed(const Node& node)
 
 Result SolverEngine::checkEntailed(const std::vector<Node>& nodes)
 {
+  ensureWellFormedTerms(nodes, "checkEntailed");
   return checkSatInternal(nodes, true).asEntailmentResult();
 }
 
@@ -853,7 +857,12 @@ Result SolverEngine::assertFormula(const Node& formula)
   SolverEngineScope smts(this);
   finishInit();
   d_state->doPendingPops();
+  ensureWellFormedTerm(formula, "assertFormula");
+  return assertFormulaInternal(formula);
+}
 
+Result SolverEngine::assertFormulaInternal(const Node& formula)
+{
   // as an optimization we do not check whether formula is well-formed here, and
   // defer this check for certain cases within the assertions module.
   Trace("smt") << "SolverEngine::assertFormula(" << formula << ")" << endl;
@@ -863,7 +872,7 @@ Result SolverEngine::assertFormula(const Node& formula)
 
   d_asserts->assertFormula(n);
   return quickCheck().asEntailmentResult();
-} /* SolverEngine::assertFormula() */
+}
 
 /*
    --------------------------------------------------------------------------
@@ -1130,7 +1139,7 @@ Result SolverEngine::blockModel()
   Node eblocker = mb.getModelBlocker(
       eassertsProc, m, d_env->getOptions().smt.blockModelsMode);
   Trace("smt") << "Block formula: " << eblocker << std::endl;
-  return assertFormula(eblocker);
+  return assertFormulaInternal(eblocker);
 }
 
 Result SolverEngine::blockModelValues(const std::vector<Node>& exprs)
@@ -1153,7 +1162,7 @@ Result SolverEngine::blockModelValues(const std::vector<Node>& exprs)
   ModelBlocker mb(*d_env.get());
   Node eblocker = mb.getModelBlocker(
       eassertsProc, m, options::BlockModelsMode::VALUES, exprs);
-  return assertFormula(eblocker);
+  return assertFormulaInternal(eblocker);
 }
 
 std::pair<Node, Node> SolverEngine::getSepHeapAndNilExpr(void)
@@ -1195,14 +1204,29 @@ const Options& SolverEngine::options() const { return d_env->getOptions(); }
 void SolverEngine::ensureWellFormedTerm(const Node& n,
                                         const std::string& src) const
 {
-  bool wasShadow = false;
-  if (expr::hasFreeOrShadowedVar(n, wasShadow))
+  if (Configuration::isAssertionBuild())
+  {
+    bool wasShadow = false;
+    if (expr::hasFreeOrShadowedVar(n, wasShadow))
+    {
+      std::string varType(wasShadow ? "shadowed" : "free");
+      std::stringstream se;
+      se << "Cannot process term with " << varType << " variable in " << src
+         << ".";
+      throw ModalException(se.str().c_str());
+    }
+  }
+}
+
+void SolverEngine::ensureWellFormedTerms(const std::vector<Node>& ns,
+                                         const std::string& src) const
+{
+  if (Configuration::isAssertionBuild())
   {
-    std::string varType(wasShadow ? "shadowed" : "free");
-    std::stringstream se;
-    se << "Cannot process term with " << varType << " variable in " << src
-       << ".";
-    throw ModalException(se.str().c_str());
+    for (const Node& n : ns)
+    {
+      ensureWellFormedTerm(n, src);
+    }
   }
 }
 

diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index a0c81f5fa0844d4d672f1da6b7448ef47d14badf..fd1057f3ddc40af7ddefa21a78e10ee29e40515f 100644 (file)
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -903,6 +903,9 @@ class CVC5_EXPORT SolverEngine
    */
   UnsatCore getUnsatCoreInternal();
 
+  /** Internal version of assertFormula */
+  Result assertFormulaInternal(const Node& formula);
+
   /**
    * Check that a generated proof checks. This method is the same as printProof,
    * but does not print the proof. Like that method, it should be called
@@ -1056,6 +1059,9 @@ class CVC5_EXPORT SolverEngine
    * this check fails.
    */
   void ensureWellFormedTerm(const Node& n, const std::string& src) const;
+  /** Vector version of above. */
+  void ensureWellFormedTerms(const std::vector<Node>& ns,
+                             const std::string& src) const;
 
   /* Members -------------------------------------------------------------- */
 

diff --git a/test/unit/api/cpp/result_black.cpp b/test/unit/api/cpp/result_black.cpp
index 9bf6b8491131f9c8debf91ca6981ec542fcc6e68..23f48caa21bb754f561fe7f5a39d7c0d2d8a4bd4 100644 (file)
--- a/test/unit/api/cpp/result_black.cpp
+++ b/test/unit/api/cpp/result_black.cpp
@@ -36,7 +36,7 @@ TEST_F(TestApiBlackResult, isNull)
   ASSERT_FALSE(res_null.isNotEntailed());
   ASSERT_FALSE(res_null.isEntailmentUnknown());
   Sort u_sort = d_solver.mkUninterpretedSort("u");
-  Term x = d_solver.mkVar(u_sort, "x");
+  Term x = d_solver.mkConst(u_sort, "x");
   d_solver.assertFormula(x.eqTerm(x));
   cvc5::api::Result res = d_solver.checkSat();
   ASSERT_FALSE(res.isNull());
@@ -45,7 +45,7 @@ TEST_F(TestApiBlackResult, isNull)
 TEST_F(TestApiBlackResult, eq)
 {
   Sort u_sort = d_solver.mkUninterpretedSort("u");
-  Term x = d_solver.mkVar(u_sort, "x");
+  Term x = d_solver.mkConst(u_sort, "x");
   d_solver.assertFormula(x.eqTerm(x));
   cvc5::api::Result res;
   cvc5::api::Result res2 = d_solver.checkSat();
@@ -58,7 +58,7 @@ TEST_F(TestApiBlackResult, eq)
 TEST_F(TestApiBlackResult, isSat)
 {
   Sort u_sort = d_solver.mkUninterpretedSort("u");
-  Term x = d_solver.mkVar(u_sort, "x");
+  Term x = d_solver.mkConst(u_sort, "x");
   d_solver.assertFormula(x.eqTerm(x));
   cvc5::api::Result res = d_solver.checkSat();
   ASSERT_TRUE(res.isSat());
@@ -68,7 +68,7 @@ TEST_F(TestApiBlackResult, isSat)
 TEST_F(TestApiBlackResult, isUnsat)
 {
   Sort u_sort = d_solver.mkUninterpretedSort("u");
-  Term x = d_solver.mkVar(u_sort, "x");
+  Term x = d_solver.mkConst(u_sort, "x");
   d_solver.assertFormula(x.eqTerm(x).notTerm());
   cvc5::api::Result res = d_solver.checkSat();
   ASSERT_TRUE(res.isUnsat());
@@ -81,7 +81,7 @@ TEST_F(TestApiBlackResult, isSatUnknown)
   d_solver.setOption("incremental", "false");
   d_solver.setOption("solve-int-as-bv", "32");
   Sort int_sort = d_solver.getIntegerSort();
-  Term x = d_solver.mkVar(int_sort, "x");
+  Term x = d_solver.mkConst(int_sort, "x");
   d_solver.assertFormula(x.eqTerm(x).notTerm());
   cvc5::api::Result res = d_solver.checkSat();
   ASSERT_FALSE(res.isSat());
@@ -111,7 +111,7 @@ TEST_F(TestApiBlackResult, isEntailmentUnknown)
   d_solver.setOption("incremental", "false");
   d_solver.setOption("solve-int-as-bv", "32");
   Sort int_sort = d_solver.getIntegerSort();
-  Term x = d_solver.mkVar(int_sort, "x");
+  Term x = d_solver.mkConst(int_sort, "x");
   d_solver.assertFormula(x.eqTerm(x).notTerm());
   cvc5::api::Result res = d_solver.checkEntailed(x.eqTerm(x));
   ASSERT_FALSE(res.isEntailed());

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index c6a303c8fb3db6543e9400d00cc77b61509c553a..7234dc796740a25907965b79ada18ba17d71dcd1 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -3052,7 +3052,8 @@ TEST_F(TestApiBlackSolver, proj_issue434)
   Term t1040 = slv.defineFun("_f45", {t1014}, t1039.getSort(), t1039);
   Term t1072 = slv.mkTerm(Kind::APPLY_UF, {t1040, t510});
   Term t1073 = slv.mkTerm(Kind::APPLY_UF, {t73, t1072});
-  ASSERT_NO_THROW(slv.checkSatAssuming({t1073, t510}));
+  // the query has free variables, and should throw an exception
+  ASSERT_THROW(slv.checkSatAssuming({t1073, t510}), CVC5ApiException);
 }
   
 TEST_F(TestApiBlackSolver, proj_issue436)

diff --git a/test/unit/api/java/ResultTest.java b/test/unit/api/java/ResultTest.java
index 59bd752cac4ed6872861b49a693e5d421663bc7b..96266bce91f95973274bac08c13736f471088bde 100644 (file)
--- a/test/unit/api/java/ResultTest.java
+++ b/test/unit/api/java/ResultTest.java
@@ -47,7 +47,7 @@ class ResultTest
     assertFalse(res_null.isNotEntailed());
     assertFalse(res_null.isEntailmentUnknown());
     Sort u_sort = d_solver.mkUninterpretedSort("u");
-    Term x = d_solver.mkVar(u_sort, "x");
+    Term x = d_solver.mkConst(u_sort, "x");
     d_solver.assertFormula(x.eqTerm(x));
     Result res = d_solver.checkSat();
     assertFalse(res.isNull());
@@ -56,7 +56,7 @@ class ResultTest
   @Test void eq()
   {
     Sort u_sort = d_solver.mkUninterpretedSort("u");
-    Term x = d_solver.mkVar(u_sort, "x");
+    Term x = d_solver.mkConst(u_sort, "x");
     d_solver.assertFormula(x.eqTerm(x));
     Result res;
     Result res2 = d_solver.checkSat();
@@ -69,7 +69,7 @@ class ResultTest
   @Test void isSat()
   {
     Sort u_sort = d_solver.mkUninterpretedSort("u");
-    Term x = d_solver.mkVar(u_sort, "x");
+    Term x = d_solver.mkConst(u_sort, "x");
     d_solver.assertFormula(x.eqTerm(x));
     Result res = d_solver.checkSat();
     assertTrue(res.isSat());
@@ -79,7 +79,7 @@ class ResultTest
   @Test void isUnsat()
   {
     Sort u_sort = d_solver.mkUninterpretedSort("u");
-    Term x = d_solver.mkVar(u_sort, "x");
+    Term x = d_solver.mkConst(u_sort, "x");
     d_solver.assertFormula(x.eqTerm(x).notTerm());
     Result res = d_solver.checkSat();
     assertTrue(res.isUnsat());
@@ -92,7 +92,7 @@ class ResultTest
     d_solver.setOption("incremental", "false");
     d_solver.setOption("solve-int-as-bv", "32");
     Sort int_sort = d_solver.getIntegerSort();
-    Term x = d_solver.mkVar(int_sort, "x");
+    Term x = d_solver.mkConst(int_sort, "x");
     d_solver.assertFormula(x.eqTerm(x).notTerm());
     Result res = d_solver.checkSat();
     assertFalse(res.isSat());
@@ -122,7 +122,7 @@ class ResultTest
     d_solver.setOption("incremental", "false");
     d_solver.setOption("solve-int-as-bv", "32");
     Sort int_sort = d_solver.getIntegerSort();
-    Term x = d_solver.mkVar(int_sort, "x");
+    Term x = d_solver.mkConst(int_sort, "x");
     d_solver.assertFormula(x.eqTerm(x).notTerm());
     Result res = d_solver.checkEntailed(x.eqTerm(x));
     assertFalse(res.isEntailed());

diff --git a/test/unit/api/python/test_result.py b/test/unit/api/python/test_result.py
index 27160f5434c4f230aa7b512a9a5a0a77d093de52..247451756c9d7d9edd5e8276c5cd37be99fa08ef 100644 (file)
--- a/test/unit/api/python/test_result.py
+++ b/test/unit/api/python/test_result.py
@@ -36,7 +36,7 @@ def test_is_null(solver):
     assert not res_null.isNotEntailed()
     assert not res_null.isEntailmentUnknown()
     u_sort = solver.mkUninterpretedSort("u")
-    x = solver.mkVar(u_sort, "x")
+    x = solver.mkConst(u_sort, "x")
     solver.assertFormula(x.eqTerm(x))
     res = solver.checkSat()
     assert not res.isNull()
@@ -44,7 +44,7 @@ def test_is_null(solver):
 
 def test_eq(solver):
     u_sort = solver.mkUninterpretedSort("u")
-    x = solver.mkVar(u_sort, "x")
+    x = solver.mkConst(u_sort, "x")
     solver.assertFormula(x.eqTerm(x))
     res2 = solver.checkSat()
     res3 = solver.checkSat()
@@ -55,7 +55,7 @@ def test_eq(solver):
 
 def test_is_sat(solver):
     u_sort = solver.mkUninterpretedSort("u")
-    x = solver.mkVar(u_sort, "x")
+    x = solver.mkConst(u_sort, "x")
     solver.assertFormula(x.eqTerm(x))
     res = solver.checkSat()
     assert res.isSat()
@@ -64,7 +64,7 @@ def test_is_sat(solver):
 
 def test_is_unsat(solver):
     u_sort = solver.mkUninterpretedSort("u")
-    x = solver.mkVar(u_sort, "x")
+    x = solver.mkConst(u_sort, "x")
     solver.assertFormula(x.eqTerm(x).notTerm())
     res = solver.checkSat()
     assert res.isUnsat()
@@ -76,7 +76,7 @@ def test_is_sat_unknown(solver):
     solver.setOption("incremental", "false")
     solver.setOption("solve-int-as-bv", "32")
     int_sort = solver.getIntegerSort()
-    x = solver.mkVar(int_sort, "x")
+    x = solver.mkConst(int_sort, "x")
     solver.assertFormula(x.eqTerm(x).notTerm())
     res = solver.checkSat()
     assert not res.isSat()
@@ -104,7 +104,7 @@ def test_is_entailment_unknown(solver):
     solver.setOption("incremental", "false")
     solver.setOption("solve-int-as-bv", "32")
     int_sort = solver.getIntegerSort()
-    x = solver.mkVar(int_sort, "x")
+    x = solver.mkConst(int_sort, "x")
     solver.assertFormula(x.eqTerm(x).notTerm())
     res = solver.checkEntailed(x.eqTerm(x))
     assert not res.isEntailed()