summaryrefslogtreecommitdiff
path: root/test/regress/regress0/Makefile.am
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2017-03-02 14:45:21 -0600
committerajreynol <andrew.j.reynolds@gmail.com>2017-03-02 14:45:21 -0600
commit1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch)
treeea8734e89aa5fba170781c7148d3fd886c597d4e /test/regress/regress0/Makefile.am
parent21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff)
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
Diffstat (limited to 'test/regress/regress0/Makefile.am')
-rw-r--r--test/regress/regress0/Makefile.am4
1 files changed, 3 insertions, 1 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 20de7a97c..1e533cc61 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -177,7 +177,9 @@ BUG_TESTS = \
bug595.cvc \
bug596.cvc \
bug596b.cvc \
- bug605.cvc
+ bug605.cvc \
+ bt-test-00.smt2 \
+ bt-test-01.smt2
#bug590.smt2
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback