diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-04 17:53:30 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-04 17:53:38 +0200 |
| commit | d3c365a60c88e33a7d73f81484db2cff5ef69bbb (patch) | |
| tree | 0b2779b9a69b6f855a01a4f22e3082e2f5faabd8 /test | |
| parent | 711815d937db09aeb7e8fa568718768113ef7176 (diff) | |
Fix bugs 605 and 667.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 4 | ||||
| -rw-r--r-- | test/regress/regress0/bug605.cvc | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index f716b8b11..7d7690d22 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -173,9 +173,9 @@ BUG_TESTS = \ bug593.smt2 \ bug595.cvc \ bug596.cvc \ - bug596b.cvc + bug596b.cvc \ + bug605.cvc #bug590.smt2 -#bug605.cvc %% fixes 605, but disabling as it runs into a different assertion failure TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug605.cvc b/test/regress/regress0/bug605.cvc index 5217c2242..1ccf7fa9e 100644 --- a/test/regress/regress0/bug605.cvc +++ b/test/regress/regress0/bug605.cvc @@ -1,3 +1,4 @@ +% EXPECT: sat
OPTION "produce-models";
% GeoLocation
@@ -27,4 +28,3 @@ init: (A, INT, Facet) -> BOOLEAN ASSERT (init(a, 2, f0));
CHECKSAT TRUE;
-COUNTERMODEL;
\ No newline at end of file |