diff options
Diffstat (limited to 'test/regress/regress0/decision')
30 files changed, 42 insertions, 32 deletions
diff --git a/test/regress/regress0/decision/aufbv-fuzz01.smt b/test/regress/regress0/decision/aufbv-fuzz01.smt index 6605e2f09..0846c4c38 100644 --- a/test/regress/regress0/decision/aufbv-fuzz01.smt +++ b/test/regress/regress0/decision/aufbv-fuzz01.smt @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat + (benchmark fuzzsmt :logic QF_AUFBV :status sat diff --git a/test/regress/regress0/decision/aufbv-fuzz01.smt.expect b/test/regress/regress0/decision/aufbv-fuzz01.smt.expect deleted file mode 100644 index 849b886a7..000000000 --- a/test/regress/regress0/decision/aufbv-fuzz01.smt.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: sat diff --git a/test/regress/regress0/decision/bitvec0.delta01.smt b/test/regress/regress0/decision/bitvec0.delta01.smt index 55aec063d..c9078b7b9 100644 --- a/test/regress/regress0/decision/bitvec0.delta01.smt +++ b/test/regress/regress0/decision/bitvec0.delta01.smt @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: unsat + (benchmark bitvec0.smt :logic QF_BV :extrafuns ((t BitVec[32])) diff --git a/test/regress/regress0/decision/bitvec0.delta01.smt.expect b/test/regress/regress0/decision/bitvec0.delta01.smt.expect deleted file mode 100644 index 7fd1d5a98..000000000 --- a/test/regress/regress0/decision/bitvec0.delta01.smt.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: unsat diff --git a/test/regress/regress0/decision/bitvec0.smt b/test/regress/regress0/decision/bitvec0.smt index 12766375f..860ca78ee 100644 --- a/test/regress/regress0/decision/bitvec0.smt +++ b/test/regress/regress0/decision/bitvec0.smt @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: unsat + (benchmark bitvec0.smt :source { Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite. diff --git a/test/regress/regress0/decision/bitvec0.smt.expect b/test/regress/regress0/decision/bitvec0.smt.expect deleted file mode 100644 index 7fd1d5a98..000000000 --- a/test/regress/regress0/decision/bitvec0.smt.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: unsat diff --git a/test/regress/regress0/decision/bitvec5.smt b/test/regress/regress0/decision/bitvec5.smt index 3b6f2f3b9..6bf931bb5 100644 --- a/test/regress/regress0/decision/bitvec5.smt +++ b/test/regress/regress0/decision/bitvec5.smt @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: unsat + (benchmark bitvec5.smt :source { Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite. diff --git a/test/regress/regress0/decision/bitvec5.smt.expect b/test/regress/regress0/decision/bitvec5.smt.expect deleted file mode 100644 index 7fd1d5a98..000000000 --- a/test/regress/regress0/decision/bitvec5.smt.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: unsat diff --git a/test/regress/regress0/decision/bug347.smt b/test/regress/regress0/decision/bug347.smt index f467cd4b3..db0e5fbff 100644 --- a/test/regress/regress0/decision/bug347.smt +++ b/test/regress/regress0/decision/bug347.smt @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat + (benchmark B_ :status sat :category { unknown } diff --git a/test/regress/regress0/decision/bug347.smt.expect b/test/regress/regress0/decision/bug347.smt.expect deleted file mode 100644 index 849b886a7..000000000 --- a/test/regress/regress0/decision/bug347.smt.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: sat diff --git a/test/regress/regress0/decision/bug374a.smt b/test/regress/regress0/decision/bug374a.smt index e338417c5..7dffa939c 100644 --- a/test/regress/regress0/decision/bug374a.smt +++ b/test/regress/regress0/decision/bug374a.smt @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: unsat + (benchmark fuzzsmt :logic AUFLIA :status unknown diff --git a/test/regress/regress0/decision/bug374a.smt.expect b/test/regress/regress0/decision/bug374a.smt.expect deleted file mode 100644 index 7fd1d5a98..000000000 --- a/test/regress/regress0/decision/bug374a.smt.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: unsat diff --git a/test/regress/regress0/decision/bug374b.smt2 b/test/regress/regress0/decision/bug374b.smt2 index a253cf12f..f9d3f440d 100644 --- a/test/regress/regress0/decision/bug374b.smt2 +++ b/test/regress/regress0/decision/bug374b.smt2 @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification --no-unconstrained +; EXPECT: unsat + (set-logic QF_ALL_SUPPORTED) (declare-fun _substvar_245_ () Bool) (declare-fun _substvar_246_ () Bool) diff --git a/test/regress/regress0/decision/bug374b.smt2.expect b/test/regress/regress0/decision/bug374b.smt2.expect deleted file mode 100644 index 0be471367..000000000 --- a/test/regress/regress0/decision/bug374b.smt2.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification --no-unconstrained -% EXPECT: unsat diff --git a/test/regress/regress0/decision/just_sat.expect b/test/regress/regress0/decision/just_sat.expect deleted file mode 100644 index 849b886a7..000000000 --- a/test/regress/regress0/decision/just_sat.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: sat diff --git a/test/regress/regress0/decision/just_unsat.expect b/test/regress/regress0/decision/just_unsat.expect deleted file mode 100644 index 7fd1d5a98..000000000 --- a/test/regress/regress0/decision/just_unsat.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: unsat diff --git a/test/regress/regress0/decision/pp-regfile.delta01.smt b/test/regress/regress0/decision/pp-regfile.delta01.smt index 7eb3277be..2f475e8de 100644 --- a/test/regress/regress0/decision/pp-regfile.delta01.smt +++ b/test/regress/regress0/decision/pp-regfile.delta01.smt @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: unsat + (benchmark pp_regfile.smt :logic QF_AUFLIA :extrafuns ((REGFILE_INIT Array)) diff --git a/test/regress/regress0/decision/pp-regfile.delta01.smt.expect b/test/regress/regress0/decision/pp-regfile.delta01.smt.expect deleted file mode 100644 index 7fd1d5a98..000000000 --- a/test/regress/regress0/decision/pp-regfile.delta01.smt.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: unsat diff --git a/test/regress/regress0/decision/pp-regfile.delta02.smt b/test/regress/regress0/decision/pp-regfile.delta02.smt index 1c461eb6f..f00f26a45 100644 --- a/test/regress/regress0/decision/pp-regfile.delta02.smt +++ b/test/regress/regress0/decision/pp-regfile.delta02.smt @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: unsat + (benchmark pp_regfile.smt :logic QF_AUFLIA :extrafuns ((REGFILE_INIT Array)) diff --git a/test/regress/regress0/decision/pp-regfile.delta02.smt.expect b/test/regress/regress0/decision/pp-regfile.delta02.smt.expect deleted file mode 100644 index 7fd1d5a98..000000000 --- a/test/regress/regress0/decision/pp-regfile.delta02.smt.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: unsat diff --git a/test/regress/regress0/decision/quant-ex1.smt2 b/test/regress/regress0/decision/quant-ex1.smt2 index a8f4ff2b9..21fa06270 100644 --- a/test/regress/regress0/decision/quant-ex1.smt2 +++ b/test/regress/regress0/decision/quant-ex1.smt2 @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat + (set-logic AUFLIRA) (set-info :smt-lib-version 2.0) (set-info :category "industrial") diff --git a/test/regress/regress0/decision/quant-ex1.smt2.expect b/test/regress/regress0/decision/quant-ex1.smt2.expect deleted file mode 100644 index 849b886a7..000000000 --- a/test/regress/regress0/decision/quant-ex1.smt2.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: sat diff --git a/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt b/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt index 6f65e83ec..9dfba13d5 100644 --- a/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt +++ b/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: sat + (benchmark mathsat :logic QF_UFLIA :extrafuns ((fmt_length Int)) diff --git a/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt.expect b/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt.expect deleted file mode 100644 index 849b886a7..000000000 --- a/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: sat diff --git a/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.smt b/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.smt index 549306c5b..a6e54626e 100644 --- a/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.smt +++ b/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.smt @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: unsat + (benchmark mathsat :source { MathSat group } :logic QF_UFLIA diff --git a/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.smt.expect b/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.smt.expect deleted file mode 100644 index 7fd1d5a98..000000000 --- a/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.smt.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: unsat diff --git a/test/regress/regress0/decision/wchains010ue.delta02.smt b/test/regress/regress0/decision/wchains010ue.delta02.smt index d5ddf6446..0ca1d9e44 100644 --- a/test/regress/regress0/decision/wchains010ue.delta02.smt +++ b/test/regress/regress0/decision/wchains010ue.delta02.smt @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: unsat + (benchmark wchains010ue.smt :logic QF_AUFBV :extrafuns ((v6 BitVec[32])) diff --git a/test/regress/regress0/decision/wchains010ue.delta02.smt.expect b/test/regress/regress0/decision/wchains010ue.delta02.smt.expect deleted file mode 100644 index 7fd1d5a98..000000000 --- a/test/regress/regress0/decision/wchains010ue.delta02.smt.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: unsat diff --git a/test/regress/regress0/decision/wchains010ue.smt b/test/regress/regress0/decision/wchains010ue.smt index a4d0f1ddb..ad47c6260 100644 --- a/test/regress/regress0/decision/wchains010ue.smt +++ b/test/regress/regress0/decision/wchains010ue.smt @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: unsat + (benchmark wchains010ue.smt :source { This benchmark generates write chain permutations and tries to show diff --git a/test/regress/regress0/decision/wchains010ue.smt.expect b/test/regress/regress0/decision/wchains010ue.smt.expect deleted file mode 100644 index 7fd1d5a98..000000000 --- a/test/regress/regress0/decision/wchains010ue.smt.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: unsat |