diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-20 20:23:09 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-20 20:23:09 -0700 |
commit | 29b2e5a74eb007f04a18e01d7a9c21eff577c9b1 (patch) | |
tree | b6ea5c072884fd78bd3a0dfec9b0b45ebf0d3b25 /test/regress | |
parent | a82837a03cf3bd33f906901f45b2c6f36cf420de (diff) |
Remove support for *.expect files in regressions (#2341)
Currently, we can optionally specify an *.expect file with the metadata
of a regression test. This commit removes that option because it was not
widely used, adds maintenance overhead and makes the transition to a new
build system more cumbersome. Regression files can still be fed to a
solver without removing the metadata first since they are in comments of
the corresponding input format (note that this was not always the case,
it changed in efc6163629c6c5de446eccfe81777c93829995d5).
Diffstat (limited to 'test/regress')
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 |