From 04f95f314db1c9fd8ac1ef475cab90c1709e6e47 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 30 Jan 2020 12:18:27 -0600
Subject: Weaken assertion for models with approximations (#3667)

---
 src/smt/smt_engine.cpp                           |  8 ++++----
 test/regress/CMakeLists.txt                      |  1 +
 test/regress/regress1/quantifiers/issue3628.smt2 | 13 +++++++++++++
 3 files changed, 18 insertions(+), 4 deletions(-)
 create mode 100644 test/regress/regress1/quantifiers/issue3628.smt2

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 910855505..d10678bf6 100644
--- 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 b35c13757..c744227e4 100644
--- 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
index 000000000..9843b92ff
--- /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)
-- 
cgit v1.2.3