Fix for array bug with decision heuristic

Also fixed one bv rewrite failure (more to come)

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); 
   }
 }