diff options
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index d537b8e60..bb16e00ce 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -210,6 +210,13 @@ Node TheoryBV::ppRewrite(TNode t) Node result = RewriteRule<BitwiseEq>::run<false>(t); return Rewriter::rewrite(result); } + + if (t.getKind() == kind::EQUAL) { + std::vector<Node> equalities; + Slicer::splitEqualities(t, equalities); + return utils::mkAnd(equalities); + } + return t; } |