summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/bv/theory_bv.cpp2
1 files changed, 1 insertions, 1 deletions
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) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback