summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorClark Barrett <barrett@cs.nyu.edu>2012-06-17 01:49:58 +0000
committerClark Barrett <barrett@cs.nyu.edu>2012-06-17 01:49:58 +0000
commit65c2efaaef8fbea0affa6216a0985f3f91d83462 (patch)
tree2e5a83597dd4689ccd971e2a647ad2a4e1e66d8e /test
parent3f94a7cacbdf22c26c406b411da3a220ef5520d1 (diff)
Fix array bug causing incorrect answers
Diffstat (limited to 'test')
-rw-r--r--test/regress/regress0/decision/Makefile.am9
-rw-r--r--test/regress/regress0/quantifiers/Makefile.am5
2 files changed, 7 insertions, 7 deletions
diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am
index 16020e9b3..d3ba458ee 100644
--- a/test/regress/regress0/decision/Makefile.am
+++ b/test/regress/regress0/decision/Makefile.am
@@ -30,15 +30,12 @@ TESTS = \
error122.delta01.smt \
error3.smt \
error3.delta01.smt \
- pp-regfile.delta01.smt
+ pp-regfile.delta01.smt \
+ pp-regfile.delta02.smt
-# Incorrect answers:
-# pp-regfile.delta02.smt
-# Incorrect, and may take too long when fixed (currently don't):
+# Correct, but takes too long:
# pp-regfile.smt \
#
-# Correct, but take too long:
-#
EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 19f74e42d..b72cad89e 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -33,9 +33,12 @@ TESTS = \
smtlibf957ea.smt2 \
gauss_init_0030.fof.smt2 \
piVC_5581bd.smt2 \
- symmetric_unsat_7.smt2 \
set3.smt2
+# removed because it now reports unknown
+# symmetric_unsat_7.smt2 \
+
+
# removed because they take more than 20s
# ex1.smt2 \
# ex6.smt2 \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback