Fix for array bug with decision heuristic

Also fixed one bv rewrite failure (more to come)

1 files changed, 2 insertions, 0 deletions

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 18274e060..7d5f541c0 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -173,6 +173,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
 	  rewriteStackTop.node = response.node;
           break;
         }
+        // Check for trivial rewrite loop of size 2
+        Assert(Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, response.node).node != rewriteStackTop.node);
 	rewriteStackTop.node = response.node;
       }
       // We're done with the post rewrite, so we add to the cache