From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 14 Jul 2021 22:29:50 +0000 (-0300)
Subject: Add option that exercises the previously buggy behavior (#6884)
X-Git-Tag: cvc5-1.0.0~1487
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=85ba8a85a2398cdc752dcd503373614830206fdf;p=cvc5.git

Add option that exercises the previously buggy behavior (#6884)
---

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))