From 283822d8dc26004cd5b15a5b8e198d4f3068ebd0 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 18 Sep 2012 14:50:45 +0000 Subject: 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.) --- test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2 | 1 + test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect | 3 ++- test/regress/regress0/quantifiers/array-unsat-simp3.smt2 | 1 + test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect | 3 ++- test/regress/regress0/quantifiers/bug291.smt2 | 1 + test/regress/regress0/quantifiers/bug291.smt2.expect | 3 ++- test/regress/regress0/quantifiers/ex1.smt2 | 1 + test/regress/regress0/quantifiers/ex1.smt2.expect | 3 ++- test/regress/regress0/quantifiers/ex7.smt2 | 1 + test/regress/regress0/quantifiers/ex7.smt2.expect | 3 ++- test/regress/regress0/tptp_parser5.p | 2 +- test/regress/regress0/tptp_parser6.p | 2 +- test/regress/regress0/tptp_parser7.p | 2 +- test/regress/regress0/tptp_parser8.p | 2 +- test/regress/regress0/tptp_parser9.p | 2 +- 15 files changed, 20 insertions(+), 10 deletions(-) (limited to 'test/regress/regress0') 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 %-------------------------------------------------------------------------- -- cgit v1.2.3