Weaken assertion for models with approximations (#3667)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 910855505374e75b0bc3f286daae2142bb6537a1..d10678bf653cfc615b4fbd36d913547d8aafd246 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4278,10 +4278,10 @@ Expr SmtEngine::getValue(const Expr& ex) const
          || resultNode.getType().isSubtypeOf(expectedType))
       << "Run with -t smt for details.";
 
-  // Ensure it's a constant, or a lambda (for uninterpreted functions), or
-  // a choice (for approximate values).
-  Assert(resultNode.getKind() == kind::LAMBDA
-         || resultNode.getKind() == kind::CHOICE || resultNode.isConst());
+  // Ensure it's a constant, or a lambda (for uninterpreted functions). This
+  // assertion only holds for models that do not have approximate values.
+  Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA
+         || resultNode.isConst());
 
   if(options::abstractValues() && resultNode.getType().isArray()) {
     resultNode = d_private->mkAbstractValue(resultNode);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b35c13757f636c4f151775a0a7c0fc3594e873ff..c744227e40c2dfde3f6144268d70fa126ad14654 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1431,6 +1431,7 @@ set(regress_1_tests
   regress1/quantifiers/issue3317.smt2
   regress1/quantifiers/issue3481.smt2
   regress1/quantifiers/issue3537.smt2
+  regress1/quantifiers/issue3628.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lra-vts-inf.smt2

diff --git a/test/regress/regress1/quantifiers/issue3628.smt2 b/test/regress/regress1/quantifiers/issue3628.smt2
new file mode 100644 (file)
index 0000000..9843b92
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue3628.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic NIRA)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(declare-fun c () Real)
+(declare-fun d () Real)
+(declare-fun e () Real)
+(assert (let ((f (exists ((g Real))
+             (= (< 0.0 (* b d)) (distinct (* (to_real 1) a c) 1.0)))))
+  (not f)))
+(assert (= a (* c e)))
+(check-sat)