diff options
Diffstat (limited to 'test/regress/regress0')
64 files changed, 64 insertions, 10 deletions
diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am index 5df254bad..179398c9d 100644 --- a/test/regress/regress0/rewriterules/Makefile.am +++ b/test/regress/regress0/rewriterules/Makefile.am @@ -13,9 +13,6 @@ TESTS_ENVIRONMENT = \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif -override CVC4_REGRESSION_ARGS += --rewrite-rules -export CVC4_REGRESSION_ARGS - MAKEFLAGS = -k # These are run for all build profiles. diff --git a/test/regress/regress0/rewriterules/datatypes.smt2 b/test/regress/regress0/rewriterules/datatypes.smt2 index a914a0c1f..9a5f68100 100644 --- a/test/regress/regress0/rewriterules/datatypes.smt2 +++ b/test/regress/regress0/rewriterules/datatypes.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; try to solve datatypes with rewriterules (set-logic AUFLIA) (set-info :status unsat) diff --git a/test/regress/regress0/rewriterules/datatypes_clark.smt2 b/test/regress/regress0/rewriterules/datatypes_clark.smt2 index 19163f49d..cc217fc79 100644 --- a/test/regress/regress0/rewriterules/datatypes_clark.smt2 +++ b/test/regress/regress0/rewriterules/datatypes_clark.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules (set-logic AUFLIRA) ;; DATATYPE diff --git a/test/regress/regress0/rewriterules/length.smt2 b/test/regress/regress0/rewriterules/length.smt2 index 215698ade..b144d7745 100644 --- a/test/regress/regress0/rewriterules/length.smt2 +++ b/test/regress/regress0/rewriterules/length.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules (set-logic AUFLIA) (set-info :status unsat) diff --git a/test/regress/regress0/rewriterules/length_gen_n.smt2 b/test/regress/regress0/rewriterules/length_gen_n.smt2 index 5d1255eb0..7da2f6777 100644 --- a/test/regress/regress0/rewriterules/length_gen_n.smt2 +++ b/test/regress/regress0/rewriterules/length_gen_n.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 b/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 index b1462cf98..7d65356ad 100644 --- a/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 +++ b/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress0/rewriterules/length_trick.smt2 b/test/regress/regress0/rewriterules/length_trick.smt2 index 84afc5815..e01e97b84 100644 --- a/test/regress/regress0/rewriterules/length_trick.smt2 +++ b/test/regress/regress0/rewriterules/length_trick.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress0/rewriterules/length_trick2.smt2 b/test/regress/regress0/rewriterules/length_trick2.smt2 index af9e7f07d..8d47d9550 100644 --- a/test/regress/regress0/rewriterules/length_trick2.smt2 +++ b/test/regress/regress0/rewriterules/length_trick2.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress0/rewriterules/native_arrays.smt2 b/test/regress/regress0/rewriterules/native_arrays.smt2 index b7d19b612..83de7d8f4 100644 --- a/test/regress/regress0/rewriterules/native_arrays.smt2 +++ b/test/regress/regress0/rewriterules/native_arrays.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; This example can't be done if we don't access the EqualityEngine of ;; the theory of arrays diff --git a/test/regress/regress0/rewriterules/native_datatypes.smt2 b/test/regress/regress0/rewriterules/native_datatypes.smt2 index c3c4aad73..365ec0624 100644 --- a/test/regress/regress0/rewriterules/native_datatypes.smt2 +++ b/test/regress/regress0/rewriterules/native_datatypes.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length diff --git a/test/regress/regress0/rewriterules/relation.smt2 b/test/regress/regress0/rewriterules/relation.smt2 index e8c0139e8..6b55a9677 100644 --- a/test/regress/regress0/rewriterules/relation.smt2 +++ b/test/regress/regress0/rewriterules/relation.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules (set-logic AUFLIA) (set-info :status unsat) diff --git a/test/regress/regress0/rewriterules/simulate_rewriting.smt2 b/test/regress/regress0/rewriterules/simulate_rewriting.smt2 index 838c0cd16..f67a0e6a2 100644 --- a/test/regress/regress0/rewriterules/simulate_rewriting.smt2 +++ b/test/regress/regress0/rewriterules/simulate_rewriting.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba (set-logic AUFLIA) (set-info :status unsat) diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index dd8621618..65f96f469 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -49,7 +49,8 @@ TESTS = \ cnf-ite.smt2 \ cnf-and-neg.smt2 \ cnf_abc.smt2 \ - bool-pred-nested.smt2 + bool-pred-nested.smt2 \ + pred.smt EXTRA_DIST = $(TESTS) \ mkpidgeon diff --git a/test/regress/regress0/uf/pred.smt b/test/regress/regress0/uf/pred.smt index e6f82727e..bdc49e7ce 100644 --- a/test/regress/regress0/uf/pred.smt +++ b/test/regress/regress0/uf/pred.smt @@ -1,5 +1,5 @@ -(benchmark euf_simp1.smt -:status sat +(benchmark pred.smt +:status unsat :logic QF_UF :category { crafted } 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") |