SMT-LIBv2 compliance regarding outputting "unknown".

Thanks to Peter Collingbourne for the report, and the patch!

(this commit was certified error- and warning-free by the test-and-commit script.)

15 files changed, 20 insertions, 10 deletions

diff --git a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2 b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2
index a8f4ff2b9..20230a6fa 100644
--- a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2
+++ b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2
@@ -9,4 +9,5 @@
 (declare-fun p () Bool)
 (assert (and (= a b) (forall ((x U)) (=> (and (= (f x) a) (not (= (f x) b))) p))))
 (check-sat)
+(get-info :reason-unknown)
 (exit)
diff --git a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect
index 9d5c95cdd..e2cc320e1 100644
--- a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect
+++ b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect
@@ -1,3 +1,4 @@
 % COMMAND-LINE: --decision=justification --disable-miniscope-quant-fv --disable-miniscope-quant
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
+% EXPECT: (:reason-unknown incomplete)
 % EXIT: 0
diff --git a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2 b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2
index 40e07ada7..a16c9395d 100644
--- a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2
+++ b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2
@@ -18,4 +18,5 @@
 (assert (not (= i1 i2)))
 (assert (not (= (store_uf (store_uf a1 i1 e1) i2 e2) (store_uf (store_uf a1 i2 e2) i1 e1))))
 (check-sat)
+(get-info :reason-unknown)
 (exit)
diff --git a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect
index df24647ad..2aefdcfc3 100644
--- a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect
+++ b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect
@@ -1,2 +1,3 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
+% EXPECT: (:reason-unknown incomplete)
 % EXIT: 0
diff --git a/test/regress/regress0/quantifiers/bug291.smt2 b/test/regress/regress0/quantifiers/bug291.smt2
index dbc230599..b39e415a8 100644
--- a/test/regress/regress0/quantifiers/bug291.smt2
+++ b/test/regress/regress0/quantifiers/bug291.smt2
@@ -10,4 +10,5 @@
 (declare-fun store2 (Int) Int)
 (assert (forall ((?A Int) (?o Int) (?f Int) (?p Int) (?g Int) (?v Int)) (=> (not (= ?o ?p)) (= (select2 (store2 ?A)) (select2 ?A)))))
 (check-sat)
+(get-info :reason-unknown)
 (exit)
diff --git a/test/regress/regress0/quantifiers/bug291.smt2.expect b/test/regress/regress0/quantifiers/bug291.smt2.expect
index df24647ad..2aefdcfc3 100644
--- a/test/regress/regress0/quantifiers/bug291.smt2.expect
+++ b/test/regress/regress0/quantifiers/bug291.smt2.expect
@@ -1,2 +1,3 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
+% EXPECT: (:reason-unknown incomplete)
 % EXIT: 0
diff --git a/test/regress/regress0/quantifiers/ex1.smt2 b/test/regress/regress0/quantifiers/ex1.smt2
index a8f4ff2b9..20230a6fa 100644
--- a/test/regress/regress0/quantifiers/ex1.smt2
+++ b/test/regress/regress0/quantifiers/ex1.smt2
@@ -9,4 +9,5 @@
 (declare-fun p () Bool)
 (assert (and (= a b) (forall ((x U)) (=> (and (= (f x) a) (not (= (f x) b))) p))))
 (check-sat)
+(get-info :reason-unknown)
 (exit)
diff --git a/test/regress/regress0/quantifiers/ex1.smt2.expect b/test/regress/regress0/quantifiers/ex1.smt2.expect
index df24647ad..2aefdcfc3 100644
--- a/test/regress/regress0/quantifiers/ex1.smt2.expect
+++ b/test/regress/regress0/quantifiers/ex1.smt2.expect
@@ -1,2 +1,3 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
+% EXPECT: (:reason-unknown incomplete)
 % EXIT: 0
diff --git a/test/regress/regress0/quantifiers/ex7.smt2 b/test/regress/regress0/quantifiers/ex7.smt2
index 0cac5ff54..11a83fdc4 100644
--- a/test/regress/regress0/quantifiers/ex7.smt2
+++ b/test/regress/regress0/quantifiers/ex7.smt2
@@ -9,4 +9,5 @@
 (declare-fun f (U) U)
 (assert (and (= a b) (forall ((x U)) (=> (or (= (f x) c) (= x a)) (= x b)))))
 (check-sat)
+(get-info :reason-unknown)
 (exit)
diff --git a/test/regress/regress0/quantifiers/ex7.smt2.expect b/test/regress/regress0/quantifiers/ex7.smt2.expect
index df24647ad..2aefdcfc3 100644
--- a/test/regress/regress0/quantifiers/ex7.smt2.expect
+++ b/test/regress/regress0/quantifiers/ex7.smt2.expect
@@ -1,2 +1,3 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
+% EXPECT: (:reason-unknown incomplete)
 % EXIT: 0
diff --git a/test/regress/regress0/tptp_parser5.p b/test/regress/regress0/tptp_parser5.p
index faacfdccc..23ddf3e60 100644
--- a/test/regress/regress0/tptp_parser5.p
+++ b/test/regress/regress0/tptp_parser5.p
@@ -1,4 +1,4 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
 % EXIT: 0
 
 %--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser6.p b/test/regress/regress0/tptp_parser6.p
index 0684a6a3d..799bc4c6d 100644
--- a/test/regress/regress0/tptp_parser6.p
+++ b/test/regress/regress0/tptp_parser6.p
@@ -1,4 +1,4 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
 % EXIT: 0
 
 %--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser7.p b/test/regress/regress0/tptp_parser7.p
index ec90157e7..f87c3484c 100644
--- a/test/regress/regress0/tptp_parser7.p
+++ b/test/regress/regress0/tptp_parser7.p
@@ -1,4 +1,4 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
 % EXIT: 0
 
 %--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser8.p b/test/regress/regress0/tptp_parser8.p
index 3bfd8efb6..4bb2694ea 100644
--- a/test/regress/regress0/tptp_parser8.p
+++ b/test/regress/regress0/tptp_parser8.p
@@ -1,4 +1,4 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
 % EXIT: 0
 
 %--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp_parser9.p b/test/regress/regress0/tptp_parser9.p
index dab8065b5..bcbb88598 100644
--- a/test/regress/regress0/tptp_parser9.p
+++ b/test/regress/regress0/tptp_parser9.p
@@ -1,4 +1,4 @@
-% EXPECT: unknown (INCOMPLETE)
+% EXPECT: unknown
 % EXIT: 0
 
 %--------------------------------------------------------------------------