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).

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