diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-04-11 16:31:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-04-11 16:31:03 +0000 |
commit | d01d291be3213368985f28d0072905c4f033d5ff (patch) | |
tree | 8524a2b6a00c012221ecca9266c3ab9fb11989ed /test | |
parent | 889853e225687dfef36b15ca1dccf74682e0fd66 (diff) |
merge from arrays-clark branch
Diffstat (limited to 'test')
-rw-r--r-- | test/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/arrays/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/arrays/x2.smt | 17 | ||||
-rw-r--r-- | test/regress/regress0/arrays/x3.smt | 46 | ||||
-rw-r--r-- | test/regress/regress0/aufbv/Makefile.am | 31 | ||||
-rw-r--r-- | test/regress/regress0/aufbv/bug00.smt | 35 |
7 files changed, 134 insertions, 2 deletions
diff --git a/test/Makefile.am b/test/Makefile.am index 2bcb283d7..a870ac44a 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -39,6 +39,7 @@ subdirs_to_check = \ regress/regress0/bv \ regress/regress0/bv/core \ regress/regress0/arrays \ + regress/regress0/aufbv \ regress/regress0/datatypes \ regress/regress0/lemmas \ regress/regress0/push-pop \ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 9245bb0af..3d68b73cb 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = . arith precedence uf uflra uflia bv arrays datatypes lemmas push-pop preprocess +SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv datatypes lemmas push-pop preprocess BINARY = cvc4 if PROOF_REGRESSIONS diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index b112d1129..5a18658d5 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -25,7 +25,9 @@ TESTS = \ incorrect8.minimized.smt \ incorrect9.smt \ incorrect10.smt \ - incorrect11.smt + incorrect11.smt \ + x2.smt \ + x3.smt EXTRA_DIST = $(TESTS) \ bug272.smt \ diff --git a/test/regress/regress0/arrays/x2.smt b/test/regress/regress0/arrays/x2.smt new file mode 100644 index 000000000..c043e88b9 --- /dev/null +++ b/test/regress/regress0/arrays/x2.smt @@ -0,0 +1,17 @@ +(benchmark read5.smt +:logic QF_AX +:status unsat +:extrafuns ((a Index)) +:extrafuns ((S Array)) +:extrafuns ((SS Array)) +:status unknown +:formula +(flet ($n1 (= S SS)) +(let (?n2 (select S a)) +(let (?n3 (store SS a ?n2)) +(flet ($n4 (= S ?n3)) +(flet ($n5 true) +(flet ($n6 (if_then_else $n1 $n4 $n5)) +(flet ($n7 (not $n6)) +$n7 +)))))))) diff --git a/test/regress/regress0/arrays/x3.smt b/test/regress/regress0/arrays/x3.smt new file mode 100644 index 000000000..ff070f142 --- /dev/null +++ b/test/regress/regress0/arrays/x3.smt @@ -0,0 +1,46 @@ +(benchmark fuzzsmt +:logic QF_AX +:status sat +:extrafuns ((v4 Index)) +:extrafuns ((v2 Index)) +:extrafuns ((v3 Index)) +:extrafuns ((v1 Array)) +:extrafuns ((v6 Element)) +:extrafuns ((v0 Array)) +:extrafuns ((v5 Element)) +:status unknown +:formula +(let (?n1 (store v1 v3 v6)) +(flet ($n2 (distinct ?n1 v0)) +(flet ($n3 (= v4 v2)) +(flet ($n4 true) +(let (?n5 (store v1 v4 v6)) +(let (?n6 (select ?n5 v2)) +(let (?n7 (ite $n4 ?n6 v6)) +(let (?n8 (select v1 v3)) +(let (?n9 (ite $n3 ?n7 ?n8)) +(flet ($n10 (distinct ?n8 ?n8)) +(let (?n11 (ite $n10 v6 ?n6)) +(let (?n12 (ite $n2 ?n9 ?n11)) +(flet ($n13 (= v6 ?n12)) +(flet ($n14 (distinct ?n8 v5)) +(let (?n15 (ite $n2 v1 v0)) +(let (?n16 (ite $n14 v1 ?n15)) +(flet ($n17 (distinct ?n5 ?n16)) +(flet ($n18 (and $n13 $n17)) +(flet ($n19 (distinct v0 ?n5)) +(let (?n20 (ite $n19 v2 v4)) +(flet ($n21 (= v3 v2)) +(flet ($n22 (= v0 v0)) +(flet ($n23 (= v6 ?n8)) +(flet ($n24 false) +(flet ($n25 (= ?n6 ?n8)) +(let (?n26 (ite $n25 v3 v2)) +(let (?n27 (ite $n24 v4 ?n26)) +(let (?n28 (ite $n23 v3 ?n27)) +(let (?n29 (ite $n22 ?n28 v4)) +(let (?n30 (ite $n21 v3 ?n29)) +(flet ($n31 (distinct ?n20 ?n30)) +(flet ($n32 (or $n18 $n31)) +$n32 +))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am new file mode 100644 index 000000000..9afa37e46 --- /dev/null +++ b/test/regress/regress0/aufbv/Makefile.am @@ -0,0 +1,31 @@ +if PROOF_REGRESSIONS +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/cvc4 +else +TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/cvc4 +endif + +# 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 = \ + bug00.smt + +EXTRA_DIST = $(TESTS) + +#if CVC4_BUILD_PROFILE_COMPETITION +#else +#TESTS += \ +# error.cvc +#endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc + +# synonyms for "check" +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/aufbv/bug00.smt b/test/regress/regress0/aufbv/bug00.smt new file mode 100644 index 000000000..d662207dd --- /dev/null +++ b/test/regress/regress0/aufbv/bug00.smt @@ -0,0 +1,35 @@ +(benchmark no_init_multi_member7.smt +:logic QF_AUFBV +:status unsat +:extrafuns ((member_6_curr_2 BitVec[32])) +:extrafuns ((arr_next_15 Array[32:32])) +:extrafuns ((member_3_curr_4 BitVec[32])) +:extrafuns ((main_0_x_3 BitVec[32])) +:extrafuns ((member_3_curr_5 BitVec[32])) +:extrafuns ((arr_val_8 Array[32:32])) +:status unknown +:formula +(flet ($n1 true) +(let (?n2 bv0[32]) +(let (?n3 bv1[32]) +(let (?n4 (select arr_val_8 member_6_curr_2)) +(flet ($n5 (= ?n3 ?n4)) +(let (?n6 (ite $n5 ?n3 ?n2)) +(flet ($n7 (= ?n2 ?n6)) +(let (?n8 (select arr_next_15 member_3_curr_5)) +(flet ($n9 (= ?n2 ?n8)) +(let (?n10 (select arr_next_15 ?n3)) +(flet ($n11 (= ?n10 member_3_curr_4)) +(let (?n12 (select arr_next_15 ?n2)) +(flet ($n13 (= ?n3 ?n12)) +(flet ($n14 (= ?n2 main_0_x_3)) +(flet ($n15 (= ?n3 member_3_curr_4)) +(flet ($n16 (and $n14 $n15)) +(let (?n17 (ite $n16 ?n2 member_3_curr_4)) +(flet ($n18 (= member_3_curr_5 ?n17)) +(flet ($n19 (= member_6_curr_2 ?n12)) +(let (?n20 (select arr_next_15 member_6_curr_2)) +(flet ($n21 (= ?n2 ?n20)) +(flet ($n22 (and $n7 $n9 $n11 $n13 $n18 $n19 $n1 $n21)) +$n22 +))))))))))))))))))))))) |