From 4e18e618039a4ae5a11ada2224b71d6700ec1f4c Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 16 Apr 2013 20:55:47 -0400
Subject: [PATCH] boolean flatten rewrite: dont re-rewrite

---
 src/theory/booleans/theory_bool_rewriter.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index b8a874209..491c52eb3 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -66,7 +66,7 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
   }
   if (nb.getNumChildren() == 0) return RewriteResponse(REWRITE_DONE, skipNode);
   if (nb.getNumChildren() == 1) return RewriteResponse(REWRITE_AGAIN, nb.getChild(0));
-  return RewriteResponse(REWRITE_AGAIN, nb.constructNode());
+  return RewriteResponse(REWRITE_DONE, nb.constructNode());
 }
 
 RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
-- 
2.30.2