projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 8bde750)
boolean flatten rewrite: dont re-rewrite
authorKshitij Bansal <kshitij@cs.nyu.edu>
Wed, 17 Apr 2013 00:55:47 +0000 (20:55 -0400)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Wed, 17 Apr 2013 01:21:49 +0000 (21:21 -0400)
src/theory/booleans/theory_bool_rewriter.cpp patch | blob | history

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index b8a874209a6465c8602e488803beefbbdf7291dd..491c52eb37d4df6defa2039329396b48d59cb5fe 100644 (file)
--- 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) {