summaryrefslogtreecommitdiff
path: root/test/regress
diff options
context:
space:
mode:
authorHaniel Barbosa <hanielbbarbosa@gmail.com>2021-07-14 19:29:50 -0300
committerGitHub <noreply@github.com>2021-07-14 22:29:50 +0000
commit85ba8a85a2398cdc752dcd503373614830206fdf (patch)
treec5bc46afde76d559653e3a6549539c2af8196977 /test/regress
parent35397d766e6cb991c0106aca56dcff865f525270 (diff)
Add option that exercises the previously buggy behavior (#6884)
Diffstat (limited to 'test/regress')
-rw-r--r--test/regress/regress0/proofs/open-pf-if-unordered-iff.smt21
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 b/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2
index b21c3f142..98d75d74f 100644
--- a/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2
+++ b/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --bv-solver=simple
; EXPECT: unsat
(set-logic ALL)
(declare-const __ (_ BitVec 3))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback