Make "unknown" non-critical for unsat cores check (#3728)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4cb76eda6cb9d5d2ef8df2f556461738a0b0e485..4a7c9def3653af0fe77aa309134203990c79e5bc 100644 (file)
--- 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 4ea9a3d1c55341cd799e85cc21733e56859717a2..3bac0b2615b15392aae40790b671c01473d587e4 100644 (file)
--- 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 (file)
index 0000000..7609ad3
--- /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 (file)
index 0000000..f96a2e9
--- /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)