diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-11 16:14:01 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-11 16:14:01 +0000 |
commit | 42794501e81c44dce5c2f7687af288af030ef63e (patch) | |
tree | 2f0c8b7f0ad93fe64ad877b46f1c449320de8513 /src/theory/bv | |
parent | 7fd544c108f9fc5a6b4842593597e8fa4a8d11d7 (diff) |
Fix for array bug with decision heuristic
Also fixed one bv rewrite failure (more to come)
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 47725444d..85ccbc787 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -521,10 +521,6 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) { >::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>, @@ -532,6 +528,12 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) { RewriteRule<ReflexivityEq>, RewriteRule<SolveEq> >::apply(node); + + if(RewriteRule<BitwiseEq>::applies(resultNode)) { + resultNode = RewriteRule<BitwiseEq>::run<false>(resultNode); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + return RewriteResponse(REWRITE_DONE, resultNode); } } |