diff options
| author | lianah <lianahady@gmail.com> | 2013-04-21 19:00:09 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-04-21 19:00:09 -0400 |
| commit | 12f48b0a11207ddbd34b2b2b88362250e9692ac2 (patch) | |
| tree | b2ae4be17e97444f6d51f2bd2dd54c43366dc363 /src/theory/bv/theory_bv.cpp | |
| parent | c863478fd87b4ff7d97d00a4a63a4c5e9bac2b4b (diff) | |
added some bv rewrite rules
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index fd2946d24..7cb06ca15 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -250,7 +250,7 @@ Node TheoryBV::ppRewrite(TNode t) // return Rewriter::rewrite(result); // } - if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) { + if (/*options::bitvectorCoreSolver() && */t.getKind() == kind::EQUAL) { std::vector<Node> equalities; Slicer::splitEqualities(t, equalities); return utils::mkAnd(equalities); |