summaryrefslogtreecommitdiff
path: root/test/regress/regress0/quantifiers/Makefile.am
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2015-10-31 10:00:52 +0100
committerajreynol <andrew.j.reynolds@gmail.com>2015-10-31 10:00:52 +0100
commit5bc200446b4165814db47e6e3639972af31ad0a6 (patch)
tree6a62e2f1296468b286b7bc513d448ca29ec353e1 /test/regress/regress0/quantifiers/Makefile.am
parentb035877b01e8b8c2ea902d9f3732cf84bfed0fdf (diff)
Improvements to handling of mixed Int/Real quantifiers.
Diffstat (limited to 'test/regress/regress0/quantifiers/Makefile.am')
-rw-r--r--test/regress/regress0/quantifiers/Makefile.am5
1 files changed, 4 insertions, 1 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 73fa07bf9..89dcc0a26 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -57,7 +57,10 @@ TESTS = \
cbqi-lia-dt-simp.smt2 \
is-int.smt2 \
floor.smt2 \
- array-unsat-simp3.smt2
+ array-unsat-simp3.smt2 \
+ mix-simp.smt2 \
+ mix-coeff.smt2 \
+ mix-match.smt2
# regression can be solved with --finite-model-find --fmf-inst-engine
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback