summaryrefslogtreecommitdiff
path: root/test/regress/regress2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress2')
-rw-r--r--test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt24
-rw-r--r--test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect3
-rw-r--r--test/regress/regress2/uflia-error0.smt23
-rw-r--r--test/regress/regress2/uflia-error0.smt2.expect2
-rw-r--r--test/regress/regress2/xs-09-16-3-4-1-5.decn.smt3
-rw-r--r--test/regress/regress2/xs-09-16-3-4-1-5.decn.smt.expect2
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback