diff options
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 107cb9672..638715ae4 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -767,6 +767,10 @@ Node TheoryBV::ppRewrite(TNode t) } else if (RewriteRule<ZeroExtendEqConst>::applies(t)) { res = RewriteRule<ZeroExtendEqConst>::run<false>(t); } + else if (RewriteRule<NormalizeEqPlusNeg>::applies(t)) + { + res = RewriteRule<NormalizeEqPlusNeg>::run<false>(t); + } // if(t.getKind() == kind::EQUAL && // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == |