diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-07 18:13:01 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-01 15:38:14 -0400 |
| commit | 994e6eb72e3475967a9a40a0566744ce1794f20a (patch) | |
| tree | fec05368ea52fbb00204ee3f3a168c2434610eae /test | |
| parent | bf7f728381bb27163f3e056d698ba4da6316b9c8 (diff) | |
Fix bug 491 and related issues with checkModel() and quantifiers. Enabling previously-failing testcase.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 96d07d7f3..48ac97294 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -145,6 +145,7 @@ BUG_TESTS = \ bug421b.smt2 \ bug425.cvc \ bug480.smt2 \ + bug484.smt2 \ bug486.cvc \ bug497.cvc @@ -152,8 +153,7 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) EXTRA_DIST = $(TESTS) \ simplification_bug4.smt2.expect \ - bug216.smt2.expect \ - bug484.smt2 + bug216.smt2.expect if CVC4_BUILD_PROFILE_COMPETITION else |