From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 18 Feb 2022 20:50:41 +0000 (-0600)
Subject: Make spurious assertion into warning (#8051)
X-Git-Tag: cvc5-1.0.0~415
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5cd263060e0b1e23937aaa2fa978794dbe81aee6;p=cvc5.git

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 4fb7dbc26..546fdc34f 100644
--- 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 48f26f9d2..c2b2e30c9 100644
--- 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
index 000000000..7b4b7f502
--- /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