summaryrefslogtreecommitdiff
path: root/test/regress/regress0/rewriterules
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2014-03-07 10:24:04 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2014-03-07 23:48:49 -0500
commitd01269e2d5a02952fbda74dcd9629acfbf23dfd4 (patch)
treed8f2a90ddd94ade15edf84b48523e7ff76f78554 /test/regress/regress0/rewriterules
parent01cff049fac316d84ee05f747975a26b04e9c3a2 (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/regress/regress0/rewriterules')
-rw-r--r--test/regress/regress0/rewriterules/Makefile.am3
1 files changed, 2 insertions, 1 deletions
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback