diff options
Diffstat (limited to 'test/regress/regress0/unconstrained')
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") |