summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/regress/regress0/bv/ackermann1.smt22
-rw-r--r--test/regress/regress0/bv/ackermann2.smt22
-rw-r--r--test/regress/regress1/bv/bug787.smt22
3 files changed, 3 insertions, 3 deletions
diff --git a/test/regress/regress0/bv/ackermann1.smt2 b/test/regress/regress0/bv/ackermann1.smt2
index 9b96b38c4..218fd746b 100644
--- a/test/regress/regress0/bv/ackermann1.smt2
+++ b/test/regress/regress0/bv/ackermann1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores
; EXPECT: sat
(set-logic QF_UFBV)
(set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/bv/ackermann2.smt2 b/test/regress/regress0/bv/ackermann2.smt2
index eeca505fe..b1aaa7d64 100644
--- a/test/regress/regress0/bv/ackermann2.smt2
+++ b/test/regress/regress0/bv/ackermann2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores
; EXPECT: unsat
(set-logic QF_UFBV)
(set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress1/bv/bug787.smt2 b/test/regress/regress1/bv/bug787.smt2
index 8e0ba0016..d732b9ff0 100644
--- a/test/regress/regress1/bv/bug787.smt2
+++ b/test/regress/regress1/bv/bug787.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bitblast=eager --no-check-proofs
+; COMMAND-LINE: --bitblast=eager
; EXPECT: unsat
(set-logic QF_BV)
(set-info :status unsat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback