projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 6587cf5)
enable bug521 regression tests
authorMorgan Deters <mdeters@cs.nyu.edu>
Sat, 20 Jul 2013 01:13:24 +0000 (21:13 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Sat, 20 Jul 2013 02:24:26 +0000 (22:24 -0400)
test/regress/regress0/Makefile.am patch | blob | history
test/regress/regress0/bug521.smt2 patch | blob | history

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 92574d5a69e626140893af6316e0ea1c14506280..082662a1e34539429f7e5b894886d15c7c789e8d 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -147,13 +147,13 @@ BUG_TESTS = \
        bug516.smt2 \
        bug519.smt2 \
        bug520.smt2 \
+       bug521.smt2 \
+       bug521.minimized.smt2 \
        bug522.smt2
 
 TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
 EXTRA_DIST = $(TESTS) \
-       bug521.smt2 \
-       bug521.minimized.smt2 \
        simplification_bug4.smt2.expect \
        bug216.smt2.expect
 
diff --git a/test/regress/regress0/bug521.smt2 b/test/regress/regress0/bug521.smt2
index 47b73e8aa2ab46efa206b9f2babdf2d733156112..8f840a1f6bab061e80e071c9519d904c832c26a9 100644 (file)
--- a/test/regress/regress0/bug521.smt2
+++ b/test/regress/regress0/bug521.smt2
@@ -1,4 +1,5 @@
-(set-option :produce-unsat-cores true)
+;(set-option :produce-unsat-cores true)
+(set-option :incremental true)
 (set-option :print-success false)
 (set-info :smt-lib-version 2.0)
 (set-info :status sat)