From 5cd263060e0b1e23937aaa2fa978794dbe81aee6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 18 Feb 2022 14:50:41 -0600 Subject: [PATCH] Make spurious assertion into warning (#8051) Fixes cvc5/cvc5-projects#401. --- src/smt/solver_engine.cpp | 6 +++++- test/regress/CMakeLists.txt | 1 + test/regress/regress0/get-value-no-evaluate.smt2 | 9 +++++++++ 3 files changed, 15 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/get-value-no-evaluate.smt2 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 -- 2.30.2