diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-16 23:04:15 +0000 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-16 23:04:15 +0000 |
| commit | 94d13d40b27beb6e1ae8ec8221f6610d9d1a024d (patch) | |
| tree | 23923e2e838ffda91cf21800ca2c19505970b064 /test/regress/regress0/decision/Makefile.am | |
| parent | 4a45b80a981a875cb560876dee2eb7bfa9db1e08 (diff) | |
Adding the failing QF_AUFLIA regression mentioned in last commit.
pp-regfile.delta02.smt is the one to look at with
--decision=justificaiton, the delta minimized version of pp-regfile,
which also gives wrong answer. due to various commits/fixes, delta01
gives correct answer currently.
Diffstat (limited to 'test/regress/regress0/decision/Makefile.am')
| -rw-r--r-- | test/regress/regress0/decision/Makefile.am | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am index f40a65161..16020e9b3 100644 --- a/test/regress/regress0/decision/Makefile.am +++ b/test/regress/regress0/decision/Makefile.am @@ -29,9 +29,15 @@ TESTS = \ error122.smt \ error122.delta01.smt \ error3.smt \ - error3.delta01.smt + error3.delta01.smt \ + pp-regfile.delta01.smt # Incorrect answers: +# pp-regfile.delta02.smt +# Incorrect, and may take too long when fixed (currently don't): +# pp-regfile.smt \ +# +# Correct, but take too long: # EXTRA_DIST = $(TESTS) |