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/regress1/uflia | |
| 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/regress1/uflia')
8 files changed, 21 insertions, 17 deletions
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 |