From 618282e081393683c3d986726b8601ba33310e79 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 7 Feb 2020 22:31:08 -0800
Subject: [PATCH] Make "unknown" non-critical for unsat cores check (#3728)

---
 src/smt/smt_engine.cpp                           |  9 +++++----
 test/regress/CMakeLists.txt                      |  8 +++++---
 test/regress/regress0/arith/issue3480.smt2       |  9 +++++++++
 test/regress/regress0/quantifiers/issue3655.smt2 | 13 +++++++++++++
 4 files changed, 32 insertions(+), 7 deletions(-)
 create mode 100644 test/regress/regress0/arith/issue3480.smt2
 create mode 100644 test/regress/regress0/quantifiers/issue3655.smt2

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4cb76eda6..4a7c9def3 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4641,11 +4641,12 @@ void SmtEngine::checkUnsatCore() {
   }
   Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl;
   if(r.asSatisfiabilityResult().isUnknown()) {
-    InternalError()
-        << "SmtEngine::checkUnsatCore(): could not check core result unknown.";
+    Warning()
+        << "SmtEngine::checkUnsatCore(): could not check core result unknown."
+        << std::endl;
   }
-
-  if(r.asSatisfiabilityResult().isSat()) {
+  else if (r.asSatisfiabilityResult().isSat())
+  {
     InternalError()
         << "SmtEngine::checkUnsatCore(): produced core was satisfiable.";
   }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4ea9a3d1c..3bac0b261 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -4,11 +4,11 @@
 set(regress_0_tests
   regress0/arith/ackermann.real.smt2
   regress0/arith/arith-eq.smt2
+  regress0/arith/arith-mixed-types-no-tighten.smt2
+  regress0/arith/arith-mixed-types-tighten.smt2
   regress0/arith/arith-mixed.smt2
-  regress0/arith/arith-tighten-1.smt2
   regress0/arith/arith-strict.smt2
-  regress0/arith/arith-mixed-types-tighten.smt2
-  regress0/arith/arith-mixed-types-no-tighten.smt2
+  regress0/arith/arith-tighten-1.smt2
   regress0/arith/arith.01.cvc
   regress0/arith/arith.02.cvc
   regress0/arith/arith.03.cvc
@@ -34,6 +34,7 @@ set(regress_0_tests
   regress0/arith/issue1399.smt2
   regress0/arith/issue3412.smt2
   regress0/arith/issue3413.smt2
+  regress0/arith/issue3480.smt2
   regress0/arith/issue3683.smt2
   regress0/arith/ite-lift.smt2
   regress0/arith/leq.01.smtv1.smt2
@@ -700,6 +701,7 @@ set(regress_0_tests
   regress0/quantifiers/issue2031-bv-var-elim.smt2
   regress0/quantifiers/issue2033-macro-arith.smt2
   regress0/quantifiers/issue2035.smt2
+  regress0/quantifiers/issue3655.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macros-int-real.smt2
   regress0/quantifiers/macros-real-arg.smt2
diff --git a/test/regress/regress0/arith/issue3480.smt2 b/test/regress/regress0/arith/issue3480.smt2
new file mode 100644
index 000000000..7609ad3e7
--- /dev/null
+++ b/test/regress/regress0/arith/issue3480.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --quiet
+(set-logic QF_NIA)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(assert (and (= a (- 7 (* a a))) (>= (* 9 b) 7) (>= (* a b) 45)))
+(assert (= b (* (div 7 c) (- 96 (div 45 b)))))
+(set-info :status unsat)
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/issue3655.smt2 b/test/regress/regress0/quantifiers/issue3655.smt2
new file mode 100644
index 000000000..f96a2e9d6
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue3655.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --quiet
+(declare-sort A 0)
+(declare-fun e (A) A)
+(declare-fun c (A A) A)
+(declare-fun h (A A) A)
+(declare-fun b (A) Bool)
+(declare-fun d (A) Bool)
+(assert (let ((a!1 (forall ((f A) (i A)) (distinct (h f i) (e (c f i))))))
+ (not a!1)))
+(assert (let ((a!1 (forall ((j A)) (or (not (b j)) (d (e j))))))
+  (and a!1 (forall ((i A)) (b i)) (forall ((g A)) (not (b g))))))
+(set-info :status unsat)
+(check-sat)
-- 
2.30.2