Make spurious assertion into warning (#8051)

Fixes cvc5/cvc5-projects#401.

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 4fb7dbc26efcd85972778f28c44dd45b2b247878..546fdc34f22b1002edda6c081c2bc9c71882536b 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -1017,7 +1017,11 @@ Node SolverEngine::getValue(const Node& ex) const
   // Ensure it's a value (constant or const-ish like real algebraic
   // numbers), or a lambda (for uninterpreted functions). This assertion only
   // holds for models that do not have approximate values.
-  Assert(m->hasApproximations() || TheoryModel::isValue(resultNode));
+  if (!TheoryModel::isValue(resultNode))
+  {
+    d_env->warning() << "Could not evaluate " << resultNode
+                     << " in getValue." << std::endl;
+  }
 
   if (d_env->getOptions().smt.abstractValues && resultNode.getType().isArray())
   {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 48f26f9d20c7b4692a23cd274221ef66c69e3e32..c2b2e30c90b520a382d20d5748cd2eb2003bc22b 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -636,6 +636,7 @@ set(regress_0_tests
   regress0/fuzz_3.smtv1.smt2
   regress0/get-value-incremental.smt2
   regress0/get-value-ints.smt2
+  regress0/get-value-no-evaluate.smt2
   regress0/get-value-reals-ints.smt2
   regress0/get-value-reals.smt2
   regress0/ho/apply-collapse-sat.smt2

diff --git a/test/regress/regress0/get-value-no-evaluate.smt2 b/test/regress/regress0/get-value-no-evaluate.smt2
new file mode 100644 (file)
index 0000000..7b4b7f5
--- /dev/null
+++ b/test/regress/regress0/get-value-no-evaluate.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: -q
+; SCRUBBER: sed 's/(.*//g'
+; EXPECT: sat
+(set-logic ALL)
+(set-option :global-declarations true)
+(set-option :produce-models true)
+(declare-const _x29 Real)
+(check-sat)
+(get-value ((forall ((_x56 Real)) (=> (>= _x29 _x56 _x29) (>= _x29 _x56 _x29)))))
\ No newline at end of file