diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2013-01-10 14:30:23 -0500 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2013-01-10 14:30:23 -0500 |
| commit | 590e7f438dacbee1c349f431316e918de43e5a8e (patch) | |
| tree | a929137ade5daf8bee54882ca9800801f7ebd66c /src/theory/bv/theory_bv.cpp | |
| parent | 9d4f5a26492a377e9b818cdfbbeb8fb5ef5b310b (diff) | |
minor bug fixes
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; } |