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:22:18 -0500 |
| commit | 23b4fd82d1ed326cd57e9bc57ef9fab98b0b1c87 (patch) | |
| tree | 89f7b6a14fa3ff74cbe2488248f4d3377e1f8632 /test | |
| parent | 31c768863403d50f7682ecbb7f72a4486de0e503 (diff) | |
Fix the regression test for bug 486, and enable it
Diffstat (limited to 'test')
| -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 3fd793b40..b81bcf799 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; |