Fix freeing nodes with maxed refcounts (#2903)

2 files changed, 31 insertions, 5 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index c9d772b26..66d597a36 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -363,7 +363,10 @@ void NodeManager::reclaimZombies() {
 std::vector<NodeValue*> NodeManager::TopologicalSort(
     const std::vector<NodeValue*>& roots) {
   std::vector<NodeValue*> order;
+  // The stack of nodes to visit. The Boolean value is false when visiting the
+  // node in preorder and true when visiting it in postorder.
   std::vector<std::pair<bool, NodeValue*> > stack;
+  // Nodes that have been visited in both pre- and postorder
   NodeValueIDSet visited;
   const NodeValueIDSet root_set(roots.begin(), roots.end());
 
@@ -382,17 +385,20 @@ std::vector<NodeValue*> NodeManager::TopologicalSort(
           order.push_back(current);
         }
         stack.pop_back();
-      } else {
+      }
+      else if (visited.find(current) == visited.end())
+      {
         stack.back().first = true;
-        Assert(visited.count(current) == 0);
         visited.insert(current);
         for (unsigned i = 0; i < current->getNumChildren(); ++i) {
           expr::NodeValue* child = current->getChild(i);
-          if (visited.find(child) == visited.end()) {
-            stack.push_back(std::make_pair(false, child));
-          }
+          stack.push_back(std::make_pair(false, child));
         }
       }
+      else
+      {
+        stack.pop_back();
+      }
     }
   }
   Assert(order.size() == roots.size());
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index 99ee171b7..0e5d550a9 100644
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -70,4 +70,24 @@ class NodeManagerWhite : public CxxTest::TestSuite {
     TS_ASSERT_THROWS(nb.realloc(67108863), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
   }
+
+  void testTopologicalSort()
+  {
+    TypeNode boolType = d_nm->booleanType();
+    Node i = d_nm->mkSkolem("i", boolType);
+    Node j = d_nm->mkSkolem("j", boolType);
+    Node n1 = d_nm->mkNode(kind::AND, j, j);
+    Node n2 = d_nm->mkNode(kind::AND, i, n1);
+
+    {
+      std::vector<NodeValue*> roots = {n1.d_nv};
+      TS_ASSERT_EQUALS(NodeManager::TopologicalSort(roots), roots);
+    }
+
+    {
+      std::vector<NodeValue*> roots = {n2.d_nv, n1.d_nv};
+      std::vector<NodeValue*> result = {n1.d_nv, n2.d_nv};
+      TS_ASSERT_EQUALS(NodeManager::TopologicalSort(roots), result);
+    }
+  }
 };