summaryrefslogtreecommitdiff
path: root/test/regress
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress')
-rw-r--r--test/regress/regress0/Makefile.am3
-rw-r--r--test/regress/regress0/arrays/Makefile.am2
-rw-r--r--test/regress/regress0/auflia/Makefile.am2
-rw-r--r--test/regress/regress0/bug548a.smt217
-rw-r--r--test/regress/regress0/bv/bvsimple.cvc27
-rw-r--r--test/regress/regress0/bv/core/Makefile.am2
-rw-r--r--test/regress/regress0/fmf/Makefile.am3
-rw-r--r--test/regress/regress0/fmf/fmf-bound-int.smt27
-rw-r--r--test/regress/regress0/precedence/Makefile.am2
-rw-r--r--test/regress/regress0/rewriterules/Makefile.am21
-rw-r--r--test/regress/regress0/rewriterules/simulate_rewriting.smt22
-rw-r--r--test/regress/regress0/sets/Makefile.am4
-rw-r--r--test/regress/regress0/strings/Makefile.am5
-rw-r--r--test/regress/regress0/tptp/Makefile.am2
-rw-r--r--test/regress/regress0/uf/Makefile.am2
-rw-r--r--test/regress/regress0/unconstrained/Makefile.am2
-rwxr-xr-xtest/regress/run_regression10
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback