1 files changed, 20 insertions, 0 deletions
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);
+    }
+  }
 };