diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-07 10:24:04 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-07 23:48:49 -0500 |
commit | d01269e2d5a02952fbda74dcd9629acfbf23dfd4 (patch) | |
tree | d8f2a90ddd94ade15edf84b48523e7ff76f78554 /test | |
parent | 01cff049fac316d84ee05f747975a26b04e9c3a2 (diff) |
Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodies; fix bug 551, improper ITE removal under quantifiers.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/bug548a.smt2 | 17 | ||||
-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/rewriterules/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/strings/Makefile.am | 5 |
6 files changed, 32 insertions, 6 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/bug548a.smt2 b/test/regress/regress0/bug548a.smt2 new file mode 100644 index 000000000..12658e507 --- /dev/null +++ b/test/regress/regress0/bug548a.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --rewrite-divk --tlimit 1000 +; EXPECT: unknown +(set-logic LIA) +(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/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/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am index 32f8a72ba..b7eac2535 100644 --- a/test/regress/regress0/rewriterules/Makefile.am +++ b/test/regress/regress0/rewriterules/Makefile.am @@ -25,7 +25,8 @@ 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 + reachability_back_to_the_future.smt2 native_arrays.smt2 +# reachability_bbttf_eT_arrays.smt2 EXTRA_DIST = $(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 += |