summaryrefslogtreecommitdiff
path: root/test/regress/regress0/arith
diff options
context:
space:
mode:
authorLiana Hadarean <lianahady@gmail.com>2015-04-23 17:38:48 +0100
committerLiana Hadarean <lianahady@gmail.com>2015-04-23 17:38:48 +0100
commit0daf670d46ec2e781c2060b41449f2787b6e8f66 (patch)
tree7f1870bc621407a3c387ab6eb3dc77db529355dc /test/regress/regress0/arith
parentc604492260d0555bdb3cac5ba0863b7223f21777 (diff)
Added option for --check-unsat-cores and various core bug fixes (merge of Morgan's proof branch).
Diffstat (limited to 'test/regress/regress0/arith')
-rw-r--r--test/regress/regress0/arith/bug569.smt22
1 files changed, 2 insertions, 0 deletions
diff --git a/test/regress/regress0/arith/bug569.smt2 b/test/regress/regress0/arith/bug569.smt2
index acb6ffcdf..e1ca49ac5 100644
--- a/test/regress/regress0/arith/bug569.smt2
+++ b/test/regress/regress0/arith/bug569.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --no-check-unsat-cores
+; EXPECT: unsat
(set-logic QF_AUFLIRA)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback