diff options
82 files changed, 141 insertions, 172 deletions
diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index ba1442c69..295335ed4 100644 --- a/test/regress/Makefile.am +++ b/test/regress/Makefile.am @@ -49,7 +49,6 @@ EXTRA_DIST = \ $(REG2_TESTS) \ $(REG3_TESTS) \ $(REG4_TESTS) \ - $(TESTS_EXPECT) \ regress0/uf/mkpidgeon \ regress0/tptp/Axioms/BOO004-0.ax \ regress0/tptp/Axioms/SYN000+0.ax \ diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 383ee5162..08f64a925 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -2016,46 +2016,3 @@ DISABLED_TESTS = \ regress2/quantifiers/small-bug1-fixpoint-3.smt2 \ regress2/xs-11-20-5-2-5-3.smt \ regress2/xs-11-20-5-2-5-3.smt2 - -TESTS_EXPECT = \ - regress0/arith/miplib-opt1217--27.smt.expect \ - regress0/arith/miplib-pp08a-3000.smt.expect \ - regress0/decision/aufbv-fuzz01.smt.expect \ - regress0/decision/bitvec0.delta01.smt.expect \ - regress0/decision/bitvec0.smt.expect \ - regress0/decision/bitvec5.smt.expect \ - regress0/decision/bug347.smt.expect \ - regress0/decision/bug374a.smt.expect \ - regress0/decision/bug374b.smt2.expect \ - regress0/decision/just_sat.expect \ - regress0/decision/just_unsat.expect \ - regress0/decision/pp-regfile.delta01.smt.expect \ - regress0/decision/pp-regfile.delta02.smt.expect \ - regress0/decision/quant-ex1.smt2.expect \ - regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt.expect \ - regress0/decision/uflia-xs-09-16-3-4-1-5.smt.expect \ - regress0/decision/wchains010ue.delta02.smt.expect \ - regress0/decision/wchains010ue.smt.expect \ - regress0/expect/scrub.01.smt.expect \ - regress0/expect/scrub.03.smt2.expect \ - regress0/quantifiers/bug291.smt2.expect \ - regress0/uflia/check02.smt2.expect \ - regress0/uflia/check03.smt2.expect \ - regress0/uflia/check04.smt2.expect \ - regress0/uflia/check04.smt2.expect \ - regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2.expect \ - regress0/uflia/tiny.smt2.expect \ - regress1/bug216.smt2.expect \ - regress1/bug590.smt2.expect \ - regress1/decision/quant-Arrays_Q1-noinfer.smt2.expect \ - regress1/decision/quant-symmetric_unsat_7.smt2.expect \ - regress1/push-pop/bug216.smt2.expect \ - regress1/simplification_bug4.smt2.expect \ - regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2.expect \ - regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect \ - regress1/uflia/speed2_e8_449_e8_517.ec.smt2.expect \ - regress1/uflia/stalmark_e7_27_e7_31.ec.smt2.expect \ - regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect \ - regress2/uflia-error0.smt2.expect \ - regress2/xs-09-16-3-4-1-5.decn.smt.expect \ - regress3/pp-regfile.smt.expect diff --git a/test/regress/README.md b/test/regress/README.md index e1ac79976..d43ebf337 100644 --- a/test/regress/README.md +++ b/test/regress/README.md @@ -121,9 +121,3 @@ This benchmark is only run when symfpu has been configured. Multiple as a requirement, refer to CVC4's `--show-config` output. Features can also be excluded by adding the `no-` prefix, e.g. `no-symfpu` means that the test is not valid for builds that include symfpu support. - -Sometimes it is useful to keep the directives separate. You can separate the -benchmark from the output expectations by putting the benchmark in `<benchmark -file>.smt` and the directives in `<benchmark file>.smt.expect`, which is looked -for by the regression script. Note that `*.expect` files should be added to the -`EXTRA_DIST` variable in [Makefile.am](Makefile.am). diff --git a/test/regress/regress0/arith/miplib-opt1217--27.smt b/test/regress/regress0/arith/miplib-opt1217--27.smt index f942cbc75..4bb2846fe 100644 --- a/test/regress/regress0/arith/miplib-opt1217--27.smt +++ b/test/regress/regress0/arith/miplib-opt1217--27.smt @@ -1,3 +1,6 @@ +; COMMAND-LINE: --miplib-trick +; EXPECT: unsat + (benchmark mip_opt1217 :source { Relaxation of the Mixed-Integer Programming diff --git a/test/regress/regress0/arith/miplib-opt1217--27.smt.expect b/test/regress/regress0/arith/miplib-opt1217--27.smt.expect deleted file mode 100644 index 24c63a495..000000000 --- a/test/regress/regress0/arith/miplib-opt1217--27.smt.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --miplib-trick -% EXPECT: unsat diff --git a/test/regress/regress0/arith/miplib-pp08a-3000.smt b/test/regress/regress0/arith/miplib-pp08a-3000.smt index 21c588ad3..9ad3a0753 100644 --- a/test/regress/regress0/arith/miplib-pp08a-3000.smt +++ b/test/regress/regress0/arith/miplib-pp08a-3000.smt @@ -1,3 +1,6 @@ +; COMMAND-LINE: --miplib-trick +; EXPECT: unsat + (benchmark mip_pp08a :source { Relaxation of the Mixed-Integer Programming diff --git a/test/regress/regress0/arith/miplib-pp08a-3000.smt.expect b/test/regress/regress0/arith/miplib-pp08a-3000.smt.expect deleted file mode 100644 index 24c63a495..000000000 --- a/test/regress/regress0/arith/miplib-pp08a-3000.smt.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --miplib-trick -% EXPECT: unsat 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 diff --git a/test/regress/regress0/expect/scrub.01.smt b/test/regress/regress0/expect/scrub.01.smt index 592a3501f..ee7d56f29 100644 --- a/test/regress/regress0/expect/scrub.01.smt +++ b/test/regress/regress0/expect/scrub.01.smt @@ -1,3 +1,9 @@ +; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' +; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. +; EXPECT: The fact in question: TERM +; EXPECT: ") +; EXIT: 1 + (benchmark reject_nonlinear :logic QF_LRA :extrafuns ((n Real)) diff --git a/test/regress/regress0/expect/scrub.01.smt.expect b/test/regress/regress0/expect/scrub.01.smt.expect deleted file mode 100644 index 4c5aa1491..000000000 --- a/test/regress/regress0/expect/scrub.01.smt.expect +++ /dev/null @@ -1,5 +0,0 @@ -% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. -% EXPECT: The fact in question: TERM -% EXPECT: ") -% EXIT: 1 diff --git a/test/regress/regress0/expect/scrub.03.smt2 b/test/regress/regress0/expect/scrub.03.smt2 index a5a2c9be1..9f773e13d 100644 --- a/test/regress/regress0/expect/scrub.03.smt2 +++ b/test/regress/regress0/expect/scrub.03.smt2 @@ -1,3 +1,9 @@ +; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' +; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. +; EXPECT: The fact in question: TERM +; EXPECT: ") +; EXIT: 1 + (set-logic QF_LRA) (set-info :status unknown) (declare-fun n () Real) diff --git a/test/regress/regress0/expect/scrub.03.smt2.expect b/test/regress/regress0/expect/scrub.03.smt2.expect deleted file mode 100644 index 4c5aa1491..000000000 --- a/test/regress/regress0/expect/scrub.03.smt2.expect +++ /dev/null @@ -1,5 +0,0 @@ -% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. -% EXPECT: The fact in question: TERM -% EXPECT: ") -% EXIT: 1 diff --git a/test/regress/regress0/quantifiers/bug291.smt2 b/test/regress/regress0/quantifiers/bug291.smt2 index b39e415a8..959d83c7f 100644 --- a/test/regress/regress0/quantifiers/bug291.smt2 +++ b/test/regress/regress0/quantifiers/bug291.smt2 @@ -1,3 +1,5 @@ +; EXPECT: unknown +; EXPECT: (:reason-unknown incomplete) (set-logic AUFLIA) (set-info :source | Boogie/Spec# benchmarks. diff --git a/test/regress/regress0/quantifiers/bug291.smt2.expect b/test/regress/regress0/quantifiers/bug291.smt2.expect deleted file mode 100644 index f97ed61b6..000000000 --- a/test/regress/regress0/quantifiers/bug291.smt2.expect +++ /dev/null @@ -1,2 +0,0 @@ -% EXPECT: unknown -% EXPECT: (:reason-unknown incomplete)
\ No newline at end of file diff --git a/test/regress/regress0/uflia/check02.smt2 b/test/regress/regress0/uflia/check02.smt2 index 0920170c6..daa3ca417 100644 --- a/test/regress/regress0/uflia/check02.smt2 +++ b/test/regress/regress0/uflia/check02.smt2 @@ -1,3 +1,7 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat + (set-logic QF_UFLIA) (declare-fun b () Int) (declare-fun n () Int) diff --git a/test/regress/regress0/uflia/check02.smt2.expect b/test/regress/regress0/uflia/check02.smt2.expect deleted file mode 100644 index fe118171a..000000000 --- a/test/regress/regress0/uflia/check02.smt2.expect +++ /dev/null @@ -1,3 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: sat -% EXPECT: unsat diff --git a/test/regress/regress0/uflia/check03.smt2 b/test/regress/regress0/uflia/check03.smt2 index f561e1964..e4503ba1d 100644 --- a/test/regress/regress0/uflia/check03.smt2 +++ b/test/regress/regress0/uflia/check03.smt2 @@ -1,3 +1,7 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat + (set-logic QF_UFLIA) (declare-fun _n () Int) diff --git a/test/regress/regress0/uflia/check03.smt2.expect b/test/regress/regress0/uflia/check03.smt2.expect deleted file mode 100644 index fe118171a..000000000 --- a/test/regress/regress0/uflia/check03.smt2.expect +++ /dev/null @@ -1,3 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: sat -% EXPECT: unsat diff --git a/test/regress/regress0/uflia/check04.smt2 b/test/regress/regress0/uflia/check04.smt2 index 61bc8a5d6..a6630dfa3 100644 --- a/test/regress/regress0/uflia/check04.smt2 +++ b/test/regress/regress0/uflia/check04.smt2 @@ -1,3 +1,7 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat + (set-logic QF_LIA) (declare-fun _b () Int) (declare-fun _n () Int) diff --git a/test/regress/regress0/uflia/check04.smt2.expect b/test/regress/regress0/uflia/check04.smt2.expect deleted file mode 100644 index fe118171a..000000000 --- a/test/regress/regress0/uflia/check04.smt2.expect +++ /dev/null @@ -1,3 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: sat -% EXPECT: unsat diff --git a/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2 b/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2 index 019d70de9..779b6237b 100644 --- a/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2 +++ b/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2 @@ -1,3 +1,7 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat + (set-logic QF_UFLIA) (declare-fun _base () Int) (declare-fun _n () Int) diff --git a/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2.expect b/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2.expect deleted file mode 100644 index fe118171a..000000000 --- a/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2.expect +++ /dev/null @@ -1,3 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: sat -% EXPECT: unsat diff --git a/test/regress/regress0/uflia/tiny.smt2 b/test/regress/regress0/uflia/tiny.smt2 index fc0251a55..bad1964c2 100644 --- a/test/regress/regress0/uflia/tiny.smt2 +++ b/test/regress/regress0/uflia/tiny.smt2 @@ -1,3 +1,7 @@ +; COMMAND-LINE: --incremental --simplification=none +; EXPECT: sat +; EXPECT: unsat + (set-logic QF_UFLIA) (declare-fun base () Int) (declare-fun n () Int) diff --git a/test/regress/regress0/uflia/tiny.smt2.expect b/test/regress/regress0/uflia/tiny.smt2.expect deleted file mode 100644 index 7081f83db..000000000 --- a/test/regress/regress0/uflia/tiny.smt2.expect +++ /dev/null @@ -1,3 +0,0 @@ -% COMMAND-LINE: --incremental --simplification=none -% EXPECT: sat -% EXPECT: unsat diff --git a/test/regress/regress1/bug216.smt2 b/test/regress/regress1/bug216.smt2 index 78e0f716c..53f4fac9c 100644 --- a/test/regress/regress1/bug216.smt2 +++ b/test/regress/regress1/bug216.smt2 @@ -1,3 +1,7 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat + (set-logic QF_UF) (declare-fun x () Bool) (declare-fun y () Bool) diff --git a/test/regress/regress1/bug216.smt2.expect b/test/regress/regress1/bug216.smt2.expect deleted file mode 100644 index fe118171a..000000000 --- a/test/regress/regress1/bug216.smt2.expect +++ /dev/null @@ -1,3 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: sat -% EXPECT: unsat diff --git a/test/regress/regress1/bug590.smt2 b/test/regress/regress1/bug590.smt2 index 68665f629..448c65f99 100644 --- a/test/regress/regress1/bug590.smt2 +++ b/test/regress/regress1/bug590.smt2 @@ -1,3 +1,6 @@ +; EXPECT: unknown +; EXPECT: ((charlst2 ((as const (Array Int String)) ""))) + (set-logic QF_ALL_SUPPORTED) (set-option :strings-exp true) (set-option :produce-models true) diff --git a/test/regress/regress1/bug590.smt2.expect b/test/regress/regress1/bug590.smt2.expect deleted file mode 100644 index b24a807f7..000000000 --- a/test/regress/regress1/bug590.smt2.expect +++ /dev/null @@ -1,2 +0,0 @@ -% EXPECT: unknown -% EXPECT: ((charlst2 ((as const (Array Int String)) ""))) diff --git a/test/regress/regress1/decision/quant-Arrays_Q1-noinfer.smt2 b/test/regress/regress1/decision/quant-Arrays_Q1-noinfer.smt2 index 3398f5f84..cfb036f16 100644 --- a/test/regress/regress1/decision/quant-Arrays_Q1-noinfer.smt2 +++ b/test/regress/regress1/decision/quant-Arrays_Q1-noinfer.smt2 @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: unsat + (set-logic AUFLIA) (set-info :source | Boogie/Spec# benchmarks. diff --git a/test/regress/regress1/decision/quant-Arrays_Q1-noinfer.smt2.expect b/test/regress/regress1/decision/quant-Arrays_Q1-noinfer.smt2.expect deleted file mode 100644 index 7fd1d5a98..000000000 --- a/test/regress/regress1/decision/quant-Arrays_Q1-noinfer.smt2.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: unsat diff --git a/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2 b/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2 index 6acf4a3c6..37accd35b 100644 --- a/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2 +++ b/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2 @@ -1,3 +1,6 @@ +; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores --decision=justification +; EXPECT: unsat + (set-logic AUFLIRA) (set-info :source | Example extracted from Peter Baumgartner's talk at CADE-21: Logical Engineering with Instance-Based Methods. diff --git a/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2.expect b/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2.expect deleted file mode 100644 index 9d6ac53ca..000000000 --- a/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --no-check-proofs --no-check-unsat-cores --decision=justification -% EXPECT: unsat diff --git a/test/regress/regress1/push-pop/bug216.smt2 b/test/regress/regress1/push-pop/bug216.smt2 index 78e0f716c..53f4fac9c 100644 --- a/test/regress/regress1/push-pop/bug216.smt2 +++ b/test/regress/regress1/push-pop/bug216.smt2 @@ -1,3 +1,7 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat + (set-logic QF_UF) (declare-fun x () Bool) (declare-fun y () Bool) diff --git a/test/regress/regress1/push-pop/bug216.smt2.expect b/test/regress/regress1/push-pop/bug216.smt2.expect deleted file mode 100644 index fe118171a..000000000 --- a/test/regress/regress1/push-pop/bug216.smt2.expect +++ /dev/null @@ -1,3 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: sat -% EXPECT: unsat diff --git a/test/regress/regress1/simplification_bug4.smt2 b/test/regress/regress1/simplification_bug4.smt2 index 0d62d6921..5f74efa7a 100644 --- a/test/regress/regress1/simplification_bug4.smt2 +++ b/test/regress/regress1/simplification_bug4.smt2 @@ -1,3 +1,6 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat + (set-logic QF_LIA) ;; Simplified benchmark, derived from NuSMV output durationThm_1.bmc_k100.smt2 ;; diff --git a/test/regress/regress1/simplification_bug4.smt2.expect b/test/regress/regress1/simplification_bug4.smt2.expect deleted file mode 100644 index 1ed776c9e..000000000 --- a/test/regress/regress1/simplification_bug4.smt2.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: unsat diff --git a/test/regress/regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2 b/test/regress/regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2 index ab8e5d1da..fd945c64f 100644 --- a/test/regress/regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2 +++ b/test/regress/regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2 @@ -1,3 +1,7 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat + (set-logic QF_UFLIA) (declare-fun _base () Int) (declare-fun _n () Int) diff --git a/test/regress/regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2.expect b/test/regress/regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2.expect deleted file mode 100644 index 9403b1a25..000000000 --- a/test/regress/regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2.expect +++ /dev/null @@ -1,3 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: sat -% EXPECT: sat diff --git a/test/regress/regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 b/test/regress/regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 index 0274e4390..84ed4b199 100644 --- a/test/regress/regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 +++ b/test/regress/regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 @@ -1,3 +1,6 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat + (set-logic QF_UFLIA) (set-info :smt-lib-version 2.0) (declare-fun _base () Int) diff --git a/test/regress/regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect b/test/regress/regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect deleted file mode 100644 index 85c180889..000000000 --- a/test/regress/regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: sat diff --git a/test/regress/regress1/uflia/speed2_e8_449_e8_517.ec.smt2 b/test/regress/regress1/uflia/speed2_e8_449_e8_517.ec.smt2 index 11fdfa51d..4dfa9c727 100644 --- a/test/regress/regress1/uflia/speed2_e8_449_e8_517.ec.smt2 +++ b/test/regress/regress1/uflia/speed2_e8_449_e8_517.ec.smt2 @@ -1,3 +1,9 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: unsat + (set-logic QF_UFLIA) (declare-fun _base () Int) (declare-fun _n () Int) diff --git a/test/regress/regress1/uflia/speed2_e8_449_e8_517.ec.smt2.expect b/test/regress/regress1/uflia/speed2_e8_449_e8_517.ec.smt2.expect deleted file mode 100644 index 65fb9b33f..000000000 --- a/test/regress/regress1/uflia/speed2_e8_449_e8_517.ec.smt2.expect +++ /dev/null @@ -1,5 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: unsat -% EXPECT: sat -% EXPECT: unsat -% EXPECT: unsat diff --git a/test/regress/regress1/uflia/stalmark_e7_27_e7_31.ec.smt2 b/test/regress/regress1/uflia/stalmark_e7_27_e7_31.ec.smt2 index 381eb740b..1faef0109 100644 --- a/test/regress/regress1/uflia/stalmark_e7_27_e7_31.ec.smt2 +++ b/test/regress/regress1/uflia/stalmark_e7_27_e7_31.ec.smt2 @@ -1,3 +1,11 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: unsat + (set-logic QF_UFLIA) (declare-fun _base () Int) (declare-fun _n () Int) diff --git a/test/regress/regress1/uflia/stalmark_e7_27_e7_31.ec.smt2.expect b/test/regress/regress1/uflia/stalmark_e7_27_e7_31.ec.smt2.expect deleted file mode 100644 index 70b8fa26d..000000000 --- a/test/regress/regress1/uflia/stalmark_e7_27_e7_31.ec.smt2.expect +++ /dev/null @@ -1,7 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: unsat -% EXPECT: sat -% EXPECT: unsat -% EXPECT: sat -% EXPECT: unsat -% EXPECT: unsat diff --git a/test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 b/test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 index 25f006d30..ebea5b80a 100644 --- a/test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 +++ b/test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 @@ -1,3 +1,7 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +; EXPECT: sat + (set-logic QF_UFLIA) (declare-fun _base () Int) (declare-fun _n () Int) diff --git a/test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect b/test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect deleted file mode 100644 index 7cb6ba8c2..000000000 --- a/test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect +++ /dev/null @@ -1,3 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: unsat -% EXPECT: sat diff --git a/test/regress/regress2/uflia-error0.smt2 b/test/regress/regress2/uflia-error0.smt2 index 73177a252..b43c326c0 100644 --- a/test/regress/regress2/uflia-error0.smt2 +++ b/test/regress/regress2/uflia-error0.smt2 @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: unsat + (set-logic QF_UFLIA) (declare-sort U 0) diff --git a/test/regress/regress2/uflia-error0.smt2.expect b/test/regress/regress2/uflia-error0.smt2.expect deleted file mode 100644 index 7fd1d5a98..000000000 --- a/test/regress/regress2/uflia-error0.smt2.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: unsat diff --git a/test/regress/regress2/xs-09-16-3-4-1-5.decn.smt b/test/regress/regress2/xs-09-16-3-4-1-5.decn.smt index 549306c5b..a6e54626e 100644 --- a/test/regress/regress2/xs-09-16-3-4-1-5.decn.smt +++ b/test/regress/regress2/xs-09-16-3-4-1-5.decn.smt @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: unsat + (benchmark mathsat :source { MathSat group } :logic QF_UFLIA diff --git a/test/regress/regress2/xs-09-16-3-4-1-5.decn.smt.expect b/test/regress/regress2/xs-09-16-3-4-1-5.decn.smt.expect deleted file mode 100644 index 7fd1d5a98..000000000 --- a/test/regress/regress2/xs-09-16-3-4-1-5.decn.smt.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: unsat diff --git a/test/regress/regress3/pp-regfile.smt b/test/regress/regress3/pp-regfile.smt index 0b9d07b84..f3eedd758 100644 --- a/test/regress/regress3/pp-regfile.smt +++ b/test/regress/regress3/pp-regfile.smt @@ -1,3 +1,6 @@ +; COMMAND-LINE: --decision=justification +; EXPECT: unsat + (benchmark pp_regfile.smt :source { Translated from old SVC processor verification benchmarks. Contact Clark diff --git a/test/regress/regress3/pp-regfile.smt.expect b/test/regress/regress3/pp-regfile.smt.expect deleted file mode 100644 index 7fd1d5a98..000000000 --- a/test/regress/regress3/pp-regfile.smt.expect +++ /dev/null @@ -1,2 +0,0 @@ -% COMMAND-LINE: --decision=justification -% EXPECT: unsat diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index 1114b4a2c..6f6edf058 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -169,24 +169,10 @@ def run_regression(unsat_cores, proofs, dump, wrapper, cvc4_binary, sys.exit('"{}" must be *.cvc or *.smt or *.smt2 or *.p or *.sy'.format( benchmark_basename)) - # If there is an ".expect" file for the benchmark, read the metadata - # from there, otherwise from the benchmark file. - metadata_filename = benchmark_path + '.expect' - if os.path.isfile(metadata_filename): - comment_char = '%' - else: - metadata_filename = benchmark_path - - metadata_lines = None - with open(metadata_filename, 'r') as metadata_file: - metadata_lines = metadata_file.readlines() - - benchmark_content = None - if metadata_filename == benchmark_path: - benchmark_content = ''.join(metadata_lines) - else: - with open(benchmark_path, 'r') as benchmark_file: - benchmark_content = benchmark_file.read() + benchmark_lines = None + with open(benchmark_path, 'r') as benchmark_file: + benchmark_lines = benchmark_file.readlines() + benchmark_content = ''.join(benchmark_lines) # Extract the metadata for the benchmark. scrubber = None @@ -196,7 +182,7 @@ def run_regression(unsat_cores, proofs, dump, wrapper, cvc4_binary, expected_exit_status = None command_lines = [] requires = [] - for line in metadata_lines: + for line in benchmark_lines: # Skip lines that do not start with a comment character. if line[0] != comment_char: continue |