boolean flatten: bug fix in dfs search

(this is not intended to (and doesn't) address the issue with
NodeBuilder limit)

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 491c52eb37d4df6defa2039329396b48d59cb5fe..e6b71474946bd042fb519003a70a00f9698baaad 100644 (file)
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -57,6 +57,7 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
       } else if(child == trivialNode) {
         return RewriteResponse(REWRITE_DONE, trivialNode);
       } else {
+        visited.insert(child);
         if(child.getKind() == k)
           toProcess.push_back(child);
         else

diff --git a/test/regress/regress0/preprocess/Makefile.am b/test/regress/regress0/preprocess/Makefile.am
index f8cd0fb9a86dfed1d9a956368931da845f698745..fe02b230eaf4c71ef383d539afd51b5560d619be 100644 (file)
--- a/test/regress/regress0/preprocess/Makefile.am
+++ b/test/regress/regress0/preprocess/Makefile.am
@@ -39,7 +39,8 @@ CVC_TESTS = \
        preprocess_11.cvc \
        preprocess_12.cvc \
        preprocess_13.cvc \
-       preprocess_14.cvc
+       preprocess_14.cvc \
+       preprocess_15.cvc
 
 # Regression tests derived from bug reports
 BUG_TESTS = 

diff --git a/test/regress/regress0/preprocess/preprocess_15.cvc b/test/regress/regress0/preprocess/preprocess_15.cvc
new file mode 100644 (file)
index 0000000..30df35e
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_15.cvc
@@ -0,0 +1,12 @@
+% EXPECT: sat
+
+a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN;
+
+ASSERT (a5);
+
+ASSERT (a0 OR (a1 AND (a2 OR (a3 AND (a4 AND (a5 AND (TRUE AND (a3 AND (a6 AND (a7 AND (a8 AND a9)))))))))));
+
+CHECKSAT;
+
+% EXIT: 10
+