diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 567f9dc46..d6de6edbd 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -516,17 +516,20 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule<FailEq>, RewriteRule<SimplifyEq>, - RewriteRule<ReflexivityEq> + RewriteRule<ReflexivityEq>, + RewriteRule<BitwiseEq> >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); } - + else if(RewriteRule<BitwiseEq>::applies(node)) { + Node resultNode = RewriteRule<BitwiseEq>::run<false>(node); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } else { Node resultNode = LinearRewriteStrategy < RewriteRule<FailEq>, RewriteRule<SimplifyEq>, RewriteRule<ReflexivityEq>, - // ,RewriteRule<BitwiseEq>, RewriteRule<SolveEq> >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); |