diff options
Diffstat (limited to 'test/regress/regress1')
26 files changed, 26 insertions, 4 deletions
diff --git a/test/regress/regress1/quantifiers/Makefile.am b/test/regress/regress1/quantifiers/Makefile.am index 159f2e088..af277af90 100644 --- a/test/regress/regress1/quantifiers/Makefile.am +++ b/test/regress/regress1/quantifiers/Makefile.am @@ -80,7 +80,8 @@ TESTS = \ RNDPRE_4_1-dd-nqe.smt2 \ set8.smt2 \ z3.620661-no-fv-trigger.smt2 \ - arith-rec-fun.smt2 + arith-rec-fun.smt2 \ + set3.smt2 # removed because they take more than 20s # javafe.ast.ArrayInit.35.smt2 diff --git a/test/regress/regress1/quantifiers/set3.smt2 b/test/regress/regress1/quantifiers/set3.smt2 index d3e51d996..bd208c6d3 100644 --- a/test/regress/regress1/quantifiers/set3.smt2 +++ b/test/regress/regress1/quantifiers/set3.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --full-saturate-quant (set-logic AUFLIA) (set-info :source | Assertion verification of simple set manipulation programs. |) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress1/rewriterules/Makefile.am b/test/regress/regress1/rewriterules/Makefile.am index fbf3db47a..6c5ce19fb 100644 --- a/test/regress/regress1/rewriterules/Makefile.am +++ b/test/regress/regress1/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/regress1/rewriterules/datatypes2.smt2 b/test/regress/regress1/rewriterules/datatypes2.smt2 index 277ddc3ae..4ef40597a 100644 --- a/test/regress/regress1/rewriterules/datatypes2.smt2 +++ b/test/regress/regress1/rewriterules/datatypes2.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/regress1/rewriterules/datatypes3.smt2 b/test/regress/regress1/rewriterules/datatypes3.smt2 index 1ec5dcbc4..fb9d79121 100644 --- a/test/regress/regress1/rewriterules/datatypes3.smt2 +++ b/test/regress/regress1/rewriterules/datatypes3.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/regress1/rewriterules/datatypes_clark_quantification.smt2 b/test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2 index 6e22816d7..a8dc5227a 100644 --- a/test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2 +++ b/test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules (set-logic AUFLIRA) ;; DATATYPE diff --git a/test/regress/regress1/rewriterules/datatypes_sat.smt2 b/test/regress/regress1/rewriterules/datatypes_sat.smt2 index 92576f976..428598c5b 100644 --- a/test/regress/regress1/rewriterules/datatypes_sat.smt2 +++ b/test/regress/regress1/rewriterules/datatypes_sat.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; try to solve datatypes with rewriterules (set-logic AUFLIA) (set-info :status sat) diff --git a/test/regress/regress1/rewriterules/length_gen.smt2 b/test/regress/regress1/rewriterules/length_gen.smt2 index dda478357..df876ef08 100644 --- a/test/regress/regress1/rewriterules/length_gen.smt2 +++ b/test/regress/regress1/rewriterules/length_gen.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/regress1/rewriterules/length_gen_010.smt2 b/test/regress/regress1/rewriterules/length_gen_010.smt2 index 052f5905b..aee09cc96 100644 --- a/test/regress/regress1/rewriterules/length_gen_010.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_010.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/regress1/rewriterules/length_gen_010_lemma.smt2 b/test/regress/regress1/rewriterules/length_gen_010_lemma.smt2 index 02bc877fc..49e6f970d 100644 --- a/test/regress/regress1/rewriterules/length_gen_010_lemma.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_010_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/regress1/rewriterules/length_gen_020.smt2 b/test/regress/regress1/rewriterules/length_gen_020.smt2 index 8e0021175..b7c2e5fd2 100644 --- a/test/regress/regress1/rewriterules/length_gen_020.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_020.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/regress1/rewriterules/length_gen_020_sat.smt2 b/test/regress/regress1/rewriterules/length_gen_020_sat.smt2 index cc75eb85a..70511d9b3 100644 --- a/test/regress/regress1/rewriterules/length_gen_020_sat.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_020_sat.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/regress1/rewriterules/length_gen_040.smt2 b/test/regress/regress1/rewriterules/length_gen_040.smt2 index 687422223..93a04cb7c 100644 --- a/test/regress/regress1/rewriterules/length_gen_040.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_040.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/regress1/rewriterules/length_gen_040_lemma.smt2 b/test/regress/regress1/rewriterules/length_gen_040_lemma.smt2 index 293ea147b..cabd84575 100644 --- a/test/regress/regress1/rewriterules/length_gen_040_lemma.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_040_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/regress1/rewriterules/length_gen_040_lemma_trigger.smt2 b/test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.smt2 index 69f9f97be..7530269e8 100644 --- a/test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.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/regress1/rewriterules/length_gen_080.smt2 b/test/regress/regress1/rewriterules/length_gen_080.smt2 index 061042be3..451ea091e 100644 --- a/test/regress/regress1/rewriterules/length_gen_080.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_080.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/regress1/rewriterules/length_gen_160_lemma.smt2 b/test/regress/regress1/rewriterules/length_gen_160_lemma.smt2 index 28b58183e..7a81652ea 100644 --- a/test/regress/regress1/rewriterules/length_gen_160_lemma.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_160_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/regress1/rewriterules/length_gen_inv_160.smt2 b/test/regress/regress1/rewriterules/length_gen_inv_160.smt2 index 9c2a5c307..af134287d 100644 --- a/test/regress/regress1/rewriterules/length_gen_inv_160.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_inv_160.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/regress1/rewriterules/length_trick3.smt2 b/test/regress/regress1/rewriterules/length_trick3.smt2 index f6899541b..fce35d691 100644 --- a/test/regress/regress1/rewriterules/length_trick3.smt2 +++ b/test/regress/regress1/rewriterules/length_trick3.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/regress1/rewriterules/length_trick3_int.smt2 b/test/regress/regress1/rewriterules/length_trick3_int.smt2 index d58bf55fe..ec10ed6d3 100644 --- a/test/regress/regress1/rewriterules/length_trick3_int.smt2 +++ b/test/regress/regress1/rewriterules/length_trick3_int.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/regress1/rewriterules/reachability_back_to_the_future.smt2 b/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 index 13f7234e9..b73f1b2a4 100644 --- a/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 +++ b/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;; Back to the Future ... Shuvendu K.Lhiri, Shaz Qadeer (set-logic AUFLIA) (set-info :status unsat) diff --git a/test/regress/regress1/rewriterules/read5.smt2 b/test/regress/regress1/rewriterules/read5.smt2 index e66df7c7e..2cd6eb244 100644 --- a/test/regress/regress1/rewriterules/read5.smt2 +++ b/test/regress/regress1/rewriterules/read5.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules (set-logic AUF) (set-info :source | Translated from old SVC processor verification benchmarks. Contact Clark diff --git a/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2 b/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2 index 9bd49f714..7434f4257 100644 --- a/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2 +++ b/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.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/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 b/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 index 4d65ffac5..256c9bb11 100644 --- a/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 +++ b/test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.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 sat) diff --git a/test/regress/regress1/rewriterules/test_guards.smt2 b/test/regress/regress1/rewriterules/test_guards.smt2 index 98c845fb5..7344dfba5 100644 --- a/test/regress/regress1/rewriterules/test_guards.smt2 +++ b/test/regress/regress1/rewriterules/test_guards.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/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 b/test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 index 4d39e12bb..5646cd70b 100644 --- a/test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 +++ b/test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --rewrite-rules ;;; From a verification condition generated by why3. The original program ;; can be found at http://toccata.lri.fr/gallery/vstte10_max_sum.en.html . ;; The problem has been modified by doubling the size of the arrays |