summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorguykatzz <katz911@gmail.com>2017-03-09 12:13:12 -0800
committerguykatzz <katz911@gmail.com>2017-03-09 12:14:15 -0800
commit2f287a59e9c775d9087cddd8c72be5169c2706e1 (patch)
tree95a6664e3b013929d9190cff2d1889045e1a2af2 /test
parentab68adfc44049598ee79a3c8b4379694d786d9aa (diff)
better proof support for bools and formulas
Diffstat (limited to 'test')
-rw-r--r--test/regress/regress0/bt-test-00.smt21
-rw-r--r--test/regress/regress0/bt-test-01.smt21
-rw-r--r--test/regress/regress0/bug217.smt21
3 files changed, 0 insertions, 3 deletions
diff --git a/test/regress/regress0/bt-test-00.smt2 b/test/regress/regress0/bt-test-00.smt2
index cd3e1137e..517806542 100644
--- a/test/regress/regress0/bt-test-00.smt2
+++ b/test/regress/regress0/bt-test-00.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs
; EXPECT: unsat
(set-logic QF_UF)
(set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/bt-test-01.smt2 b/test/regress/regress0/bt-test-01.smt2
index 918dcf9ec..e17bd2d7a 100644
--- a/test/regress/regress0/bt-test-01.smt2
+++ b/test/regress/regress0/bt-test-01.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs
; EXPECT: unsat
(set-logic QF_UF)
(set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/bug217.smt2 b/test/regress/regress0/bug217.smt2
index 34cfcad33..4d2e828b5 100644
--- a/test/regress/regress0/bug217.smt2
+++ b/test/regress/regress0/bug217.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs
; EXPECT: unsat
(set-logic QF_UF)
(set-info :status unsat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback