Adding garbage collection of nodes with maxed out reference counts.

2 files changed, 11 insertions, 6 deletions

diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index ed772a471..cfdee8d37 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -277,7 +277,7 @@ public:
     TS_ASSERT(a_bool->getType(true) == d_em->booleanType());
     TS_ASSERT(b_bool->getType(false) == d_em->booleanType());
     TS_ASSERT(b_bool->getType(true) == d_em->booleanType());
-    TS_ASSERT_THROWS(d_em->mkExpr(MULT,*a_bool,*b_bool).getType(true), 
+    TS_ASSERT_THROWS(d_em->mkExpr(MULT,*a_bool,*b_bool).getType(true),
                      TypeCheckingException);
 // These need better support for operators
 //    TS_ASSERT(and_op->getType().isNull());
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 3958e0f2c..13d8084fa 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -19,6 +19,7 @@
 #include <string>
 #include <vector>
 
+#include "base/output.h"
 #include "expr/node_manager.h"
 #include "expr/node_manager_attributes.h"
 #include "util/integer.h"
@@ -308,12 +309,16 @@ public:
     std::vector<Node> vars;
     const unsigned int max = metakind::getUpperBoundForKind(AND);
     TypeNode boolType = d_nodeManager->booleanType();
-    Node skolem = d_nodeManager->mkSkolem("i", boolType);
-    for( unsigned int i = 0; i <= max; ++i ) {
-      vars.push_back( skolem );
+    Node skolem_i = d_nodeManager->mkSkolem("i", boolType);
+    Node skolem_j = d_nodeManager->mkSkolem("j", boolType);
+    Node andNode = skolem_i.andNode(skolem_j);
+    Node orNode = skolem_i.orNode(skolem_j);
+    while (vars.size() <= max) {
+      vars.push_back(andNode);
+      vars.push_back(skolem_j);
+      vars.push_back(orNode);
     }
-    TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, vars), AssertionException );
+    TS_ASSERT_THROWS(d_nodeManager->mkNode(AND, vars), AssertionException);
 #endif
   }
-
 };