diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-25 15:57:54 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-28 11:52:33 -0500 |
| commit | db1bbaa13a0cba41e3176441d0b816088fd964ce (patch) | |
| tree | 4adc77f56fc3fe73aeb6eaebf3adc57026e02ca8 /test/regress | |
| parent | 79d4733d97dfed6c1198777df5f74f976c80aaf6 (diff) | |
Fix the regression test for bug 486, and enable it
(cherry-picked from master 23b4fd82d1ed326cd57e9bc57ef9fab98b0b1c87)
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 6 | ||||
| -rw-r--r-- | test/regress/regress0/bug486.cvc | 4 |
2 files changed, 7 insertions, 3 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index d5b35594f..99cd6dbe6 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -143,14 +143,14 @@ BUG_TESTS = \ bug421.smt2 \ bug421b.smt2 \ bug425.cvc \ - bug480.smt2 + bug480.smt2 \ + bug486.cvc TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) EXTRA_DIST = $(TESTS) \ simplification_bug4.smt2.expect \ - bug216.smt2.expect \ - bug486.cvc + bug216.smt2.expect if CVC4_BUILD_PROFILE_COMPETITION else diff --git a/test/regress/regress0/bug486.cvc b/test/regress/regress0/bug486.cvc index 6e8ee0018..9bcbc40fa 100644 --- a/test/regress/regress0/bug486.cvc +++ b/test/regress/regress0/bug486.cvc @@ -1,3 +1,7 @@ +% COMMAND-LINE: --finite-model-find -i +% EXPECT: invalid +% EXPECT: valid +% EXIT: 20 prin:TYPE; form:TYPE; |