Fix various regression tests (#1657)

While reorganizing the regression tests, I found three tests with a
wrong status, one that CVC4 reported unknown for and some regression
tests that had command line options set in the Makefile.am instead of
the tests themselves. This commit fixes the status of the three
regression tests (verified the status with Z3), adds command line
options to make the previously "unknown" test work, and moves the
command line options from the Makefile.am into the individual regression
tests. The latter also required some minor changes to the regression
script because it would not try to determine the expected output from
the (set-info :status ...) command if there was one directive (such as
EXPECT/COMMAND-LINE/etc.).  This was an issue with the tests that now
have a COMMAND-LINE directive.

50 files changed, 49 insertions, 4 deletions

diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am
index 0d0c7cdb2..7a8577677 100644
--- a/test/regress/regress0/unconstrained/Makefile.am
+++ b/test/regress/regress0/unconstrained/Makefile.am
@@ -13,10 +13,6 @@ TESTS_ENVIRONMENT = \
 	$(AM_LOG_FLAGS) $(LOG_FLAGS)
 endif
 
-# models not supported with unconstrained simp
-override CVC4_REGRESSION_ARGS += --unconstrained-simp --no-check-models
-export CVC4_REGRESSION_ARGS
-
 MAKEFLAGS = -k
 
 # These are run for all build profiles.
diff --git a/test/regress/regress0/unconstrained/arith.smt2 b/test/regress/regress0/unconstrained/arith.smt2
index dc2b27414..3dfab3b0e 100644
--- a/test/regress/regress0/unconstrained/arith.smt2
+++ b/test/regress/regress0/unconstrained/arith.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/arith2.smt2 b/test/regress/regress0/unconstrained/arith2.smt2
index f9e829e45..d6206287a 100644
--- a/test/regress/regress0/unconstrained/arith2.smt2
+++ b/test/regress/regress0/unconstrained/arith2.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFLIRA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/arith3.smt2 b/test/regress/regress0/unconstrained/arith3.smt2
index 83634a50a..fd24c3f65 100644
--- a/test/regress/regress0/unconstrained/arith3.smt2
+++ b/test/regress/regress0/unconstrained/arith3.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFLIRA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/arith4.smt2 b/test/regress/regress0/unconstrained/arith4.smt2
index 2b06d5ea8..507a18a78 100644
--- a/test/regress/regress0/unconstrained/arith4.smt2
+++ b/test/regress/regress0/unconstrained/arith4.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFNIRA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/arith5.smt2 b/test/regress/regress0/unconstrained/arith5.smt2
index de1e305bc..5e54083a5 100644
--- a/test/regress/regress0/unconstrained/arith5.smt2
+++ b/test/regress/regress0/unconstrained/arith5.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLRA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/arith6.smt2 b/test/regress/regress0/unconstrained/arith6.smt2
index 05653415f..ce3630264 100644
--- a/test/regress/regress0/unconstrained/arith6.smt2
+++ b/test/regress/regress0/unconstrained/arith6.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLRA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/arith7.smt2 b/test/regress/regress0/unconstrained/arith7.smt2
index 6cc063ca4..105320632 100644
--- a/test/regress/regress0/unconstrained/arith7.smt2
+++ b/test/regress/regress0/unconstrained/arith7.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFLIRA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/array1.smt2 b/test/regress/regress0/unconstrained/array1.smt2
index 82f084e87..f1acfa759 100644
--- a/test/regress/regress0/unconstrained/array1.smt2
+++ b/test/regress/regress0/unconstrained/array1.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBV)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvbool.smt2 b/test/regress/regress0/unconstrained/bvbool.smt2
index 0dded2a2f..b1943124e 100644
--- a/test/regress/regress0/unconstrained/bvbool.smt2
+++ b/test/regress/regress0/unconstrained/bvbool.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvbool2.smt2 b/test/regress/regress0/unconstrained/bvbool2.smt2
index 949096224..49b7d5fc8 100644
--- a/test/regress/regress0/unconstrained/bvbool2.smt2
+++ b/test/regress/regress0/unconstrained/bvbool2.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvbool3.smt2 b/test/regress/regress0/unconstrained/bvbool3.smt2
index a689804f7..f24b129e0 100644
--- a/test/regress/regress0/unconstrained/bvbool3.smt2
+++ b/test/regress/regress0/unconstrained/bvbool3.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvcmp.smt2 b/test/regress/regress0/unconstrained/bvcmp.smt2
index ba7316324..ae50d350c 100644
--- a/test/regress/regress0/unconstrained/bvcmp.smt2
+++ b/test/regress/regress0/unconstrained/bvcmp.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvconcat.smt2 b/test/regress/regress0/unconstrained/bvconcat.smt2
index e2941b34a..6f4e38ec7 100644
--- a/test/regress/regress0/unconstrained/bvconcat.smt2
+++ b/test/regress/regress0/unconstrained/bvconcat.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvconcat2.smt2 b/test/regress/regress0/unconstrained/bvconcat2.smt2
index aa901b9b0..789e4c6c8 100644
--- a/test/regress/regress0/unconstrained/bvconcat2.smt2
+++ b/test/regress/regress0/unconstrained/bvconcat2.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvdiv.smt2 b/test/regress/regress0/unconstrained/bvdiv.smt2
index d3cadf6c8..990a8d457 100644
--- a/test/regress/regress0/unconstrained/bvdiv.smt2
+++ b/test/regress/regress0/unconstrained/bvdiv.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvext.smt2 b/test/regress/regress0/unconstrained/bvext.smt2
index 56289e245..b31efe3aa 100644
--- a/test/regress/regress0/unconstrained/bvext.smt2
+++ b/test/regress/regress0/unconstrained/bvext.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvite.smt2 b/test/regress/regress0/unconstrained/bvite.smt2
index 9e1ecc193..3cac4670b 100644
--- a/test/regress/regress0/unconstrained/bvite.smt2
+++ b/test/regress/regress0/unconstrained/bvite.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvmul.smt2 b/test/regress/regress0/unconstrained/bvmul.smt2
index fc56695f5..a109d9471 100644
--- a/test/regress/regress0/unconstrained/bvmul.smt2
+++ b/test/regress/regress0/unconstrained/bvmul.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvmul2.smt2 b/test/regress/regress0/unconstrained/bvmul2.smt2
index 89e4ff569..4e413c24f 100644
--- a/test/regress/regress0/unconstrained/bvmul2.smt2
+++ b/test/regress/regress0/unconstrained/bvmul2.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvmul3.smt2 b/test/regress/regress0/unconstrained/bvmul3.smt2
index ea67a1b5a..71cf37371 100644
--- a/test/regress/regress0/unconstrained/bvmul3.smt2
+++ b/test/regress/regress0/unconstrained/bvmul3.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvnot.smt2 b/test/regress/regress0/unconstrained/bvnot.smt2
index 22fc7e7d2..4f62d2a0d 100644
--- a/test/regress/regress0/unconstrained/bvnot.smt2
+++ b/test/regress/regress0/unconstrained/bvnot.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvsle.smt2 b/test/regress/regress0/unconstrained/bvsle.smt2
index 702f9d7a0..391a6c9d7 100644
--- a/test/regress/regress0/unconstrained/bvsle.smt2
+++ b/test/regress/regress0/unconstrained/bvsle.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvsle2.smt2 b/test/regress/regress0/unconstrained/bvsle2.smt2
index b797fa4e8..f23b119fe 100644
--- a/test/regress/regress0/unconstrained/bvsle2.smt2
+++ b/test/regress/regress0/unconstrained/bvsle2.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvsle3.smt2 b/test/regress/regress0/unconstrained/bvsle3.smt2
index 4d897830c..2887cdca8 100644
--- a/test/regress/regress0/unconstrained/bvsle3.smt2
+++ b/test/regress/regress0/unconstrained/bvsle3.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvsle4.smt2 b/test/regress/regress0/unconstrained/bvsle4.smt2
index 8927a5f2e..289104ec8 100644
--- a/test/regress/regress0/unconstrained/bvsle4.smt2
+++ b/test/regress/regress0/unconstrained/bvsle4.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvsle5.smt2 b/test/regress/regress0/unconstrained/bvsle5.smt2
index 1aceacbe3..cbe15db58 100644
--- a/test/regress/regress0/unconstrained/bvsle5.smt2
+++ b/test/regress/regress0/unconstrained/bvsle5.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvslt.smt2 b/test/regress/regress0/unconstrained/bvslt.smt2
index f98375653..2e20460c5 100644
--- a/test/regress/regress0/unconstrained/bvslt.smt2
+++ b/test/regress/regress0/unconstrained/bvslt.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvslt2.smt2 b/test/regress/regress0/unconstrained/bvslt2.smt2
index e56500ad2..743cfbebe 100644
--- a/test/regress/regress0/unconstrained/bvslt2.smt2
+++ b/test/regress/regress0/unconstrained/bvslt2.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvslt3.smt2 b/test/regress/regress0/unconstrained/bvslt3.smt2
index a4af152f1..db1f3dcd9 100644
--- a/test/regress/regress0/unconstrained/bvslt3.smt2
+++ b/test/regress/regress0/unconstrained/bvslt3.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvslt4.smt2 b/test/regress/regress0/unconstrained/bvslt4.smt2
index d702b6d1a..9c696d48b 100644
--- a/test/regress/regress0/unconstrained/bvslt4.smt2
+++ b/test/regress/regress0/unconstrained/bvslt4.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvslt5.smt2 b/test/regress/regress0/unconstrained/bvslt5.smt2
index f4b6a7a63..c5696f0a2 100644
--- a/test/regress/regress0/unconstrained/bvslt5.smt2
+++ b/test/regress/regress0/unconstrained/bvslt5.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvule.smt2 b/test/regress/regress0/unconstrained/bvule.smt2
index cbbb4cc6e..d0678d87c 100644
--- a/test/regress/regress0/unconstrained/bvule.smt2
+++ b/test/regress/regress0/unconstrained/bvule.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvule2.smt2 b/test/regress/regress0/unconstrained/bvule2.smt2
index 0e6f5916b..5dfa6c1b1 100644
--- a/test/regress/regress0/unconstrained/bvule2.smt2
+++ b/test/regress/regress0/unconstrained/bvule2.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvule3.smt2 b/test/regress/regress0/unconstrained/bvule3.smt2
index 11e3a9877..e9892e598 100644
--- a/test/regress/regress0/unconstrained/bvule3.smt2
+++ b/test/regress/regress0/unconstrained/bvule3.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvule4.smt2 b/test/regress/regress0/unconstrained/bvule4.smt2
index b8d978b71..0fccae301 100644
--- a/test/regress/regress0/unconstrained/bvule4.smt2
+++ b/test/regress/regress0/unconstrained/bvule4.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvule5.smt2 b/test/regress/regress0/unconstrained/bvule5.smt2
index cd927d0c6..4d4e0e95f 100644
--- a/test/regress/regress0/unconstrained/bvule5.smt2
+++ b/test/regress/regress0/unconstrained/bvule5.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvult.smt2 b/test/regress/regress0/unconstrained/bvult.smt2
index fb94994b4..9429237a4 100644
--- a/test/regress/regress0/unconstrained/bvult.smt2
+++ b/test/regress/regress0/unconstrained/bvult.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvult2.smt2 b/test/regress/regress0/unconstrained/bvult2.smt2
index 3fb4a0d23..c86699b48 100644
--- a/test/regress/regress0/unconstrained/bvult2.smt2
+++ b/test/regress/regress0/unconstrained/bvult2.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvult3.smt2 b/test/regress/regress0/unconstrained/bvult3.smt2
index b11ab9da3..ceb19ea75 100644
--- a/test/regress/regress0/unconstrained/bvult3.smt2
+++ b/test/regress/regress0/unconstrained/bvult3.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvult4.smt2 b/test/regress/regress0/unconstrained/bvult4.smt2
index 8170ec280..04008c006 100644
--- a/test/regress/regress0/unconstrained/bvult4.smt2
+++ b/test/regress/regress0/unconstrained/bvult4.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/bvult5.smt2 b/test/regress/regress0/unconstrained/bvult5.smt2
index 545bcbf64..53f76f0d3 100644
--- a/test/regress/regress0/unconstrained/bvult5.smt2
+++ b/test/regress/regress0/unconstrained/bvult5.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/geq.smt2 b/test/regress/regress0/unconstrained/geq.smt2
index 818bb55b3..d3bcc506f 100644
--- a/test/regress/regress0/unconstrained/geq.smt2
+++ b/test/regress/regress0/unconstrained/geq.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/gt.smt2 b/test/regress/regress0/unconstrained/gt.smt2
index 76b119e42..d4d6d4a5d 100644
--- a/test/regress/regress0/unconstrained/gt.smt2
+++ b/test/regress/regress0/unconstrained/gt.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/ite.smt2 b/test/regress/regress0/unconstrained/ite.smt2
index 4dc1cc295..54f092b8c 100644
--- a/test/regress/regress0/unconstrained/ite.smt2
+++ b/test/regress/regress0/unconstrained/ite.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBV )
 (set-info :status sat)
 (declare-sort U 0)
diff --git a/test/regress/regress0/unconstrained/leq.smt2 b/test/regress/regress0/unconstrained/leq.smt2
index 6c03fc254..4eea4df9c 100644
--- a/test/regress/regress0/unconstrained/leq.smt2
+++ b/test/regress/regress0/unconstrained/leq.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/lt.smt2 b/test/regress/regress0/unconstrained/lt.smt2
index 637a6407f..a0a42f4ef 100644
--- a/test/regress/regress0/unconstrained/lt.smt2
+++ b/test/regress/regress0/unconstrained/lt.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/mult1.smt2 b/test/regress/regress0/unconstrained/mult1.smt2
index fdad322af..4a29d9a92 100644
--- a/test/regress/regress0/unconstrained/mult1.smt2
+++ b/test/regress/regress0/unconstrained/mult1.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_LIA)
 (set-info :status sat)
 
diff --git a/test/regress/regress0/unconstrained/uf1.smt2 b/test/regress/regress0/unconstrained/uf1.smt2
index 0b2a95f49..3e28c2f8b 100644
--- a/test/regress/regress0/unconstrained/uf1.smt2
+++ b/test/regress/regress0/unconstrained/uf1.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/unconstrained/xor.smt2 b/test/regress/regress0/unconstrained/xor.smt2
index 4089bb5dc..fcc66b015 100644
--- a/test/regress/regress0/unconstrained/xor.smt2
+++ b/test/regress/regress0/unconstrained/xor.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")