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/regress0 | |
| 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/regress0')
50 files changed, 82 insertions, 63 deletions
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 |