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/regress2 | |
| 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/regress2')
6 files changed, 10 insertions, 7 deletions
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 |