From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 17 Apr 2013 00:55:47 +0000 (-0400)
Subject: boolean flatten rewrite: dont re-rewrite
X-Git-Tag: cvc5-1.0.0~7320
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4e18e618039a4ae5a11ada2224b71d6700ec1f4c;p=cvc5.git

boolean flatten rewrite: dont re-rewrite
---

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) {