From e1dc39321cd4ab29b436025badfb05714f5649b3 Mon Sep 17 00:00:00 2001
From: makaimann <makaim@stanford.edu>
Date: Mon, 10 Dec 2018 08:37:11 -0800
Subject: BoolToBV modes (off, ite, all) (#2530)

---
 src/theory/bv/theory_bv.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/theory/bv')

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index e60d60456..949a3d738 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -740,7 +740,7 @@ Node TheoryBV::ppRewrite(TNode t)
 {
   Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n";
   Node res = t;
-  if (RewriteRule<BitwiseEq>::applies(t)) {
+  if (options::bitwiseEq() && RewriteRule<BitwiseEq>::applies(t)) {
     Node result = RewriteRule<BitwiseEq>::run<false>(t);
     res = Rewriter::rewrite(result);
   } else if (d_isCoreTheory && t.getKind() == kind::EQUAL) {
-- 
cgit v1.2.3