diff options
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/arrays/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/auflia/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/bug548a.smt2 | 17 | ||||
-rw-r--r-- | test/regress/regress0/bv/bvsimple.cvc | 27 | ||||
-rw-r--r-- | test/regress/regress0/bv/core/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/fmf/fmf-bound-int.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/precedence/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/rewriterules/Makefile.am | 21 | ||||
-rw-r--r-- | test/regress/regress0/rewriterules/simulate_rewriting.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/sets/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/strings/Makefile.am | 5 | ||||
-rw-r--r-- | test/regress/regress0/tptp/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/uf/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/unconstrained/Makefile.am | 2 | ||||
-rwxr-xr-x | test/regress/run_regression | 10 |
17 files changed, 79 insertions, 34 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index e2d6664cd..664958e5a 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -154,7 +154,8 @@ BUG_TESTS = \ bug522.smt2 \ bug528a.smt2 \ bug541.smt2 \ - bug544.smt2 + bug544.smt2 \ + bug548a.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index 62877ddf3..345856d85 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -13,6 +13,8 @@ TESTS_ENVIRONMENT = \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif +MAKEFLAGS = -k + # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am index 31d9c0797..d182539bc 100644 --- a/test/regress/regress0/auflia/Makefile.am +++ b/test/regress/regress0/auflia/Makefile.am @@ -13,6 +13,8 @@ TESTS_ENVIRONMENT = \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif +MAKEFLAGS = -k + # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" diff --git a/test/regress/regress0/bug548a.smt2 b/test/regress/regress0/bug548a.smt2 new file mode 100644 index 000000000..75d82d98f --- /dev/null +++ b/test/regress/regress0/bug548a.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --rewrite-divk --tlimit 1000 +; EXPECT: unknown +(set-logic AUFLIA) +(declare-fun f (Int) Int) + + +; instantiated version : cvc4 answers sat +;(assert (= (f 1) (div 1 10))) +;(assert (= (f 11) (div 11 10))) + +; cvc4 answers unsat, should be "sat", cvc4 expected to timeout or answer "unknown" +(assert (forall ((x Int)) (= (f x) (div x 10)))) + +(assert (= (f 1) 0)) +(assert (= (f 11) 1)) + +(check-sat) diff --git a/test/regress/regress0/bv/bvsimple.cvc b/test/regress/regress0/bv/bvsimple.cvc index be5707554..dcacd643a 100644 --- a/test/regress/regress0/bv/bvsimple.cvc +++ b/test/regress/regress0/bv/bvsimple.cvc @@ -22,22 +22,19 @@ QUERY ( 0bin0011 << 3 = 0bin0011000 ) AND ( 0bin1000 >> 3 = 0bin0001 ) AND -% these not working yet.. -% -%( BVZEROEXTEND(0bin100, 2) = 0bin00100 ) AND -%( SX(0bin100, 5) = 0bin11100 ) AND -% -%( BVZEROEXTEND(0bin100, 0) = 0bin100 ) AND -%( SX(0bin100, 3) = 0bin100 ) AND -% -%( (BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11)))[8:4] = BVPLUS(5, x, ~(y[3:2])) ) AND -% -%( x4 = 0hex5 AND y4 = 0bin0101 ) => -%( ( BVMULT(8,x4,y4)=BVMULT(8,y4,x4) ) AND -% ( NOT(BVLT(x4,y4)) ) AND -% ( BVLE(BVSUB(8,x4,y4), BVPLUS(8, x4, BVUMINUS(x4))) ) AND -% ( x4 = BVSUB(4, BVUMINUS(x4), BVPLUS(4, x4,0hex1)) ) ) AND +( BVZEROEXTEND(0bin100, 2) = 0bin00100 ) AND +( SX(0bin100, 5) = 0bin11100 ) AND +( BVZEROEXTEND(0bin100, 0) = 0bin100 ) AND +( SX(0bin100, 3) = 0bin100 ) AND + +( (BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11)))[8:4] = BVPLUS(5, x, ~(y[3:2])) ) AND + +( x4 = 0hex5 AND y4 = 0bin0101 ) => +( ( BVMULT(8,x4,y4)=BVMULT(8,y4,x4) ) AND + ( NOT(BVLT(x4,y4)) ) AND + ( BVLE(BVSUB(8,x4,y4), BVPLUS(8, x4, BVUMINUS(x4))) ) AND + ( x4 = BVSUB(4, BVUMINUS(x4), BVPLUS(4, x4,0hex1)) ) ) AND ( 0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2] ) AND ( 0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF) = (IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0] ) AND diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am index 7c411121a..0e3133b32 100644 --- a/test/regress/regress0/bv/core/Makefile.am +++ b/test/regress/regress0/bv/core/Makefile.am @@ -13,6 +13,8 @@ TESTS_ENVIRONMENT = \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif +MAKEFLAGS = -k + # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 2633949c8..b9a87231f 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -30,7 +30,8 @@ TESTS = \ german73.smt2 \ PUZ001+1.smt2 \ refcount24.cvc.smt2 \ - bug0909.smt2 + bug0909.smt2 \ + fmf-bound-int.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/fmf-bound-int.smt2 b/test/regress/regress0/fmf/fmf-bound-int.smt2 new file mode 100644 index 000000000..fb3106bdf --- /dev/null +++ b/test/regress/regress0/fmf/fmf-bound-int.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --finite-model-find --fmf-bound-int +; EXPECT: sat +(set-logic UFLIA) +(declare-fun P (Int Int) Bool) +(declare-fun Q (Int) Bool) +(assert (forall ((x Int)) (=> (and (<= 0 x) (<= x (ite (P 0 0) 10 20))) (Q x)))) +(check-sat) diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am index 1d980997d..1afcc0293 100644 --- a/test/regress/regress0/precedence/Makefile.am +++ b/test/regress/regress0/precedence/Makefile.am @@ -13,6 +13,8 @@ TESTS_ENVIRONMENT = \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif +MAKEFLAGS = -k + # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am index 32f8a72ba..3a3a097bd 100644 --- a/test/regress/regress0/rewriterules/Makefile.am +++ b/test/regress/regress0/rewriterules/Makefile.am @@ -1,6 +1,3 @@ -CVC4_REGRESSION_ARGS ?= --efficient-e-matching -export CVC4_REGRESSION_ARGS - # don't override a BINARY imported from a personal.mk @mk_if@eq ($(BINARY),) @mk_empty@BINARY = cvc4 @@ -16,16 +13,26 @@ 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. # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ - length_trick.smt2 length_trick2.smt2 length_gen_020.smt2 \ - datatypes.smt2 datatypes_sat.smt2 set_A_new_fast_tableau-base.smt2 \ - set_A_new_fast_tableau-base_sat.smt2 relation.smt2 simulate_rewriting.smt2 \ - reachability_back_to_the_future.smt2 native_arrays.smt2 reachability_bbttf_eT_arrays.smt2 + length_trick.smt2 \ + length_trick2.smt2 \ + length_gen_020.smt2 \ + datatypes.smt2 \ + datatypes_sat.smt2 \ + reachability_back_to_the_future.smt2 \ + relation.smt2 \ + simulate_rewriting.smt2 \ + native_arrays.smt2 + +# reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/rewriterules/simulate_rewriting.smt2 b/test/regress/regress0/rewriterules/simulate_rewriting.smt2 index d1d88a549..838c0cd16 100644 --- a/test/regress/regress0/rewriterules/simulate_rewriting.smt2 +++ b/test/regress/regress0/rewriterules/simulate_rewriting.smt2 @@ -1,6 +1,6 @@ ;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba (set-logic AUFLIA) -(set-info :status sat) +(set-info :status unsat) (declare-sort elt1 0) (declare-sort elt2 0) diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 04d3433eb..fe53838be 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -9,10 +9,12 @@ AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif +MAKEFLAGS = -k + # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 705a7eadb..e82076520 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -32,7 +32,6 @@ TESTS = \ fmf001.smt2 \ fmf002.smt2 \ type001.smt2 \ - type002.smt2 \ type003.smt2 \ model001.smt2 \ substr001.smt2 \ @@ -51,8 +50,8 @@ TESTS = \ FAILING_TESTS = -EXTRA_DIST = $(TESTS) - +EXTRA_DIST = $(TESTS) \ + type002.smt2 # and make sure to distribute it EXTRA_DIST += diff --git a/test/regress/regress0/tptp/Makefile.am b/test/regress/regress0/tptp/Makefile.am index f8f106362..e0c8a2b48 100644 --- a/test/regress/regress0/tptp/Makefile.am +++ b/test/regress/regress0/tptp/Makefile.am @@ -13,6 +13,8 @@ TESTS_ENVIRONMENT = \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif +MAKEFLAGS = -k + # escape the `=' in file names equals = = diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index 98194413d..da992286e 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -13,6 +13,8 @@ TESTS_ENVIRONMENT = \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif +MAKEFLAGS = -k + # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am index ecf427fb5..fcae3196a 100644 --- a/test/regress/regress0/unconstrained/Makefile.am +++ b/test/regress/regress0/unconstrained/Makefile.am @@ -16,6 +16,8 @@ endif override CVC4_REGRESSION_ARGS += --unconstrained-simp export CVC4_REGRESSION_ARGS +MAKEFLAGS = -k + # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" diff --git a/test/regress/run_regression b/test/regress/run_regression index ec9e17057..bf4dcc6ef 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -197,8 +197,8 @@ fi check_models=false if grep '^sat$' "$expoutfile" &>/dev/null || grep '^invalid$' "$expoutfile" &>/dev/null || grep '^unknown$' "$expoptfile" &>/dev/null; then - if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-models\>' &>/dev/null && - ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-models\>' &>/dev/null; then + if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-models' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-models' &>/dev/null; then # later on, we'll run another test with --check-models on check_models=true fi @@ -207,9 +207,9 @@ check_proofs=false if [ "$proof" = yes ]; then # proofs not currently supported in incremental mode, turn it off if grep '^unsat$' "$expoutfile" &>/dev/null || grep '^valid$' "$expoutfile" &>/dev/null &>/dev/null; then - if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-proofs\>' &>/dev/null && - ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-proofs\>' &>/dev/null && - ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental\>' &>/dev/null && + if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-proofs' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-proofs' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental' &>/dev/null && ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null; then # later on, we'll run another test with --check-proofs on check_proofs=true |