From 85ba8a85a2398cdc752dcd503373614830206fdf Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 14 Jul 2021 19:29:50 -0300
Subject: [PATCH] Add option that exercises the previously buggy behavior
 (#6884)

---
 test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 | 1 +
 1 file changed, 1 insertion(+)

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