Rename test/unit/expr to test/unit/node. (#6156)

This is in preparation for renaming src/expr to src/node.

16 files changed, 3754 insertions, 0 deletions

diff --git a/test/unit/node/CMakeLists.txt b/test/unit/node/CMakeLists.txt
new file mode 100644
index 000000000..52e591aeb
--- /dev/null
+++ b/test/unit/node/CMakeLists.txt
@@ -0,0 +1,28 @@
+#####################
+## CMakeLists.txt
+## Top contributors (to current version):
+##   Aina Niemetz
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.
+##
+#-----------------------------------------------------------------------------#
+# Add unit tests
+
+cvc4_add_unit_test_black(attribute_black expr)
+cvc4_add_unit_test_white(attribute_white expr)
+cvc4_add_unit_test_black(kind_black expr)
+cvc4_add_unit_test_black(kind_map_black expr)
+cvc4_add_unit_test_black(node_black expr)
+cvc4_add_unit_test_black(node_algorithm_black expr)
+cvc4_add_unit_test_black(node_builder_black expr)
+cvc4_add_unit_test_black(node_manager_black expr)
+cvc4_add_unit_test_white(node_manager_white expr)
+cvc4_add_unit_test_black(node_self_iterator_black expr)
+cvc4_add_unit_test_black(node_traversal_black expr)
+cvc4_add_unit_test_white(node_white expr)
+cvc4_add_unit_test_black(symbol_table_black expr)
+cvc4_add_unit_test_black(type_cardinality_black expr)
+cvc4_add_unit_test_white(type_node_white expr)
diff --git a/test/unit/node/attribute_black.cpp b/test/unit/node/attribute_black.cpp
new file mode 100644
index 000000000..487798e49
--- /dev/null
+++ b/test/unit/node/attribute_black.cpp
@@ -0,0 +1,128 @@
+/*********************                                                        */
+/*! \file attribute_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Tim King, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::Attribute.
+ **
+ ** Black box testing of CVC4::Attribute.
+ **/
+
+#include <sstream>
+#include <vector>
+
+#include "expr/attribute.h"
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_value.h"
+#include "test_node.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace smt;
+
+namespace test {
+
+class TestNodeBlackAttribute : public TestNode
+{
+ protected:
+  struct PrimitiveIntAttributeId
+  {
+  };
+  using PrimitiveIntAttribute =
+      expr::Attribute<PrimitiveIntAttributeId, uint64_t>;
+  struct TNodeAttributeId
+  {
+  };
+  using TNodeAttribute = expr::Attribute<TNodeAttributeId, TNode>;
+  struct StringAttributeId
+  {
+  };
+  using StringAttribute = expr::Attribute<StringAttributeId, std::string>;
+  struct BoolAttributeId
+  {
+  };
+  using BoolAttribute = expr::Attribute<BoolAttributeId, bool>;
+};
+
+TEST_F(TestNodeBlackAttribute, ints)
+{
+  TypeNode booleanType = d_nodeManager->booleanType();
+  Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+  const uint64_t val = 63489;
+  uint64_t data0 = 0;
+  uint64_t data1 = 0;
+
+  PrimitiveIntAttribute attr;
+  ASSERT_FALSE(node->getAttribute(attr, data0));
+  node->setAttribute(attr, val);
+  ASSERT_TRUE(node->getAttribute(attr, data1));
+  ASSERT_EQ(data1, val);
+
+  delete node;
+}
+
+TEST_F(TestNodeBlackAttribute, tnodes)
+{
+  TypeNode booleanType = d_nodeManager->booleanType();
+  Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+
+  Node val(d_nodeManager->mkSkolem("b", booleanType));
+  TNode data0;
+  TNode data1;
+
+  TNodeAttribute attr;
+  ASSERT_FALSE(node->getAttribute(attr, data0));
+  node->setAttribute(attr, val);
+  ASSERT_TRUE(node->getAttribute(attr, data1));
+  ASSERT_EQ(data1, val);
+
+  delete node;
+}
+
+TEST_F(TestNodeBlackAttribute, strings)
+{
+  TypeNode booleanType = d_nodeManager->booleanType();
+  Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+
+  std::string val("63489");
+  std::string data0;
+  std::string data1;
+
+  StringAttribute attr;
+  ASSERT_FALSE(node->getAttribute(attr, data0));
+  node->setAttribute(attr, val);
+  ASSERT_TRUE(node->getAttribute(attr, data1));
+  ASSERT_EQ(data1, val);
+
+  delete node;
+}
+
+TEST_F(TestNodeBlackAttribute, bools)
+{
+  TypeNode booleanType = d_nodeManager->booleanType();
+  Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+
+  bool val = true;
+  bool data0 = false;
+  bool data1 = false;
+
+  BoolAttribute attr;
+  ASSERT_TRUE(node->getAttribute(attr, data0));
+  ASSERT_EQ(false, data0);
+  node->setAttribute(attr, val);
+  ASSERT_TRUE(node->getAttribute(attr, data1));
+  ASSERT_EQ(data1, val);
+
+  delete node;
+}
+
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/node/attribute_white.cpp b/test/unit/node/attribute_white.cpp
new file mode 100644
index 000000000..fccb587db
--- /dev/null
+++ b/test/unit/node/attribute_white.cpp
@@ -0,0 +1,448 @@
+/*********************                                                        */
+/*! \file attribute_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief White box testing of Node attributes.
+ **
+ ** White box testing of Node attributes.
+ **/
+
+#include <string>
+
+#include "base/check.h"
+#include "expr/attribute.h"
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_manager.h"
+#include "expr/node_manager_attributes.h"
+#include "expr/node_value.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "test_node.h"
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/theory_uf.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace smt;
+using namespace expr;
+using namespace expr::attr;
+
+namespace test {
+
+struct Test1;
+struct Test2;
+struct Test3;
+struct Test4;
+struct Test5;
+
+typedef Attribute<Test1, std::string> TestStringAttr1;
+typedef Attribute<Test2, std::string> TestStringAttr2;
+
+using TestFlag1 = Attribute<Test1, bool>;
+using TestFlag2 = Attribute<Test2, bool>;
+using TestFlag3 = Attribute<Test3, bool>;
+using TestFlag4 = Attribute<Test4, bool>;
+using TestFlag5 = Attribute<Test5, bool>;
+
+class TestNodeWhiteAttribute : public TestNode
+{
+ protected:
+  void SetUp() override
+  {
+    TestNode::SetUp();
+    d_booleanType.reset(new TypeNode(d_nodeManager->booleanType()));
+  }
+  std::unique_ptr<TypeNode> d_booleanType;
+};
+
+TEST_F(TestNodeWhiteAttribute, attribute_ids)
+{
+  // Test that IDs for (a subset of) attributes in the system are
+  // unique and that the LastAttributeId (which would be the next ID
+  // to assign) is greater than all attribute IDs.
+
+  // We used to check ID assignments explicitly.  However, between
+  // compilation modules, you don't get a strong guarantee
+  // (initialization order is somewhat implementation-specific, and
+  // anyway you'd have to change the tests anytime you add an
+  // attribute).  So we back off, and just test that they're unique
+  // and that the next ID to be assigned is strictly greater than
+  // those that have already been assigned.
+
+  unsigned lastId = attr::LastAttributeId<std::string, false>::getId();
+  ASSERT_LT(VarNameAttr::s_id, lastId);
+  ASSERT_LT(TestStringAttr1::s_id, lastId);
+  ASSERT_LT(TestStringAttr2::s_id, lastId);
+
+  ASSERT_NE(VarNameAttr::s_id, TestStringAttr1::s_id);
+  ASSERT_NE(VarNameAttr::s_id, TestStringAttr2::s_id);
+  ASSERT_NE(TestStringAttr1::s_id, TestStringAttr2::s_id);
+
+  lastId = attr::LastAttributeId<bool, false>::getId();
+  ASSERT_LT(TestFlag1::s_id, lastId);
+  ASSERT_LT(TestFlag2::s_id, lastId);
+  ASSERT_LT(TestFlag3::s_id, lastId);
+  ASSERT_LT(TestFlag4::s_id, lastId);
+  ASSERT_LT(TestFlag5::s_id, lastId);
+  ASSERT_NE(TestFlag1::s_id, TestFlag2::s_id);
+  ASSERT_NE(TestFlag1::s_id, TestFlag3::s_id);
+  ASSERT_NE(TestFlag1::s_id, TestFlag4::s_id);
+  ASSERT_NE(TestFlag1::s_id, TestFlag5::s_id);
+  ASSERT_NE(TestFlag2::s_id, TestFlag3::s_id);
+  ASSERT_NE(TestFlag2::s_id, TestFlag4::s_id);
+  ASSERT_NE(TestFlag2::s_id, TestFlag5::s_id);
+  ASSERT_NE(TestFlag3::s_id, TestFlag4::s_id);
+  ASSERT_NE(TestFlag3::s_id, TestFlag5::s_id);
+  ASSERT_NE(TestFlag4::s_id, TestFlag5::s_id);
+
+  lastId = attr::LastAttributeId<TypeNode, false>::getId();
+  ASSERT_LT(TypeAttr::s_id, lastId);
+}
+
+TEST_F(TestNodeWhiteAttribute, attributes)
+{
+  Node a = d_nodeManager->mkVar(*d_booleanType);
+  Node b = d_nodeManager->mkVar(*d_booleanType);
+  Node c = d_nodeManager->mkVar(*d_booleanType);
+  Node unnamed = d_nodeManager->mkVar(*d_booleanType);
+
+  a.setAttribute(VarNameAttr(), "a");
+  b.setAttribute(VarNameAttr(), "b");
+  c.setAttribute(VarNameAttr(), "c");
+
+  // test that all boolean flags are FALSE to start
+  Debug("boolattr") << "get flag 1 on a (should be F)\n";
+  ASSERT_FALSE(a.getAttribute(TestFlag1()));
+  Debug("boolattr") << "get flag 1 on b (should be F)\n";
+  ASSERT_FALSE(b.getAttribute(TestFlag1()));
+  Debug("boolattr") << "get flag 1 on c (should be F)\n";
+  ASSERT_FALSE(c.getAttribute(TestFlag1()));
+  Debug("boolattr") << "get flag 1 on unnamed (should be F)\n";
+  ASSERT_FALSE(unnamed.getAttribute(TestFlag1()));
+
+  Debug("boolattr") << "get flag 2 on a (should be F)\n";
+  ASSERT_FALSE(a.getAttribute(TestFlag2()));
+  Debug("boolattr") << "get flag 2 on b (should be F)\n";
+  ASSERT_FALSE(b.getAttribute(TestFlag2()));
+  Debug("boolattr") << "get flag 2 on c (should be F)\n";
+  ASSERT_FALSE(c.getAttribute(TestFlag2()));
+  Debug("boolattr") << "get flag 2 on unnamed (should be F)\n";
+  ASSERT_FALSE(unnamed.getAttribute(TestFlag2()));
+
+  Debug("boolattr") << "get flag 3 on a (should be F)\n";
+  ASSERT_FALSE(a.getAttribute(TestFlag3()));
+  Debug("boolattr") << "get flag 3 on b (should be F)\n";
+  ASSERT_FALSE(b.getAttribute(TestFlag3()));
+  Debug("boolattr") << "get flag 3 on c (should be F)\n";
+  ASSERT_FALSE(c.getAttribute(TestFlag3()));
+  Debug("boolattr") << "get flag 3 on unnamed (should be F)\n";
+  ASSERT_FALSE(unnamed.getAttribute(TestFlag3()));
+
+  Debug("boolattr") << "get flag 4 on a (should be F)\n";
+  ASSERT_FALSE(a.getAttribute(TestFlag4()));
+  Debug("boolattr") << "get flag 4 on b (should be F)\n";
+  ASSERT_FALSE(b.getAttribute(TestFlag4()));
+  Debug("boolattr") << "get flag 4 on c (should be F)\n";
+  ASSERT_FALSE(c.getAttribute(TestFlag4()));
+  Debug("boolattr") << "get flag 4 on unnamed (should be F)\n";
+  ASSERT_FALSE(unnamed.getAttribute(TestFlag4()));
+
+  Debug("boolattr") << "get flag 5 on a (should be F)\n";
+  ASSERT_FALSE(a.getAttribute(TestFlag5()));
+  Debug("boolattr") << "get flag 5 on b (should be F)\n";
+  ASSERT_FALSE(b.getAttribute(TestFlag5()));
+  Debug("boolattr") << "get flag 5 on c (should be F)\n";
+  ASSERT_FALSE(c.getAttribute(TestFlag5()));
+  Debug("boolattr") << "get flag 5 on unnamed (should be F)\n";
+  ASSERT_FALSE(unnamed.getAttribute(TestFlag5()));
+
+  // test that they all HAVE the boolean attributes
+  ASSERT_TRUE(a.hasAttribute(TestFlag1()));
+  ASSERT_TRUE(b.hasAttribute(TestFlag1()));
+  ASSERT_TRUE(c.hasAttribute(TestFlag1()));
+  ASSERT_TRUE(unnamed.hasAttribute(TestFlag1()));
+
+  ASSERT_TRUE(a.hasAttribute(TestFlag2()));
+  ASSERT_TRUE(b.hasAttribute(TestFlag2()));
+  ASSERT_TRUE(c.hasAttribute(TestFlag2()));
+  ASSERT_TRUE(unnamed.hasAttribute(TestFlag2()));
+
+  ASSERT_TRUE(a.hasAttribute(TestFlag3()));
+  ASSERT_TRUE(b.hasAttribute(TestFlag3()));
+  ASSERT_TRUE(c.hasAttribute(TestFlag3()));
+  ASSERT_TRUE(unnamed.hasAttribute(TestFlag3()));
+
+  ASSERT_TRUE(a.hasAttribute(TestFlag4()));
+  ASSERT_TRUE(b.hasAttribute(TestFlag4()));
+  ASSERT_TRUE(c.hasAttribute(TestFlag4()));
+  ASSERT_TRUE(unnamed.hasAttribute(TestFlag4()));
+
+  ASSERT_TRUE(a.hasAttribute(TestFlag5()));
+  ASSERT_TRUE(b.hasAttribute(TestFlag5()));
+  ASSERT_TRUE(c.hasAttribute(TestFlag5()));
+  ASSERT_TRUE(unnamed.hasAttribute(TestFlag5()));
+
+  // test two-arg version of hasAttribute()
+  bool bb = false;
+  Debug("boolattr") << "get flag 1 on a (should be F)\n";
+  ASSERT_TRUE(a.getAttribute(TestFlag1(), bb));
+  ASSERT_FALSE(bb);
+  Debug("boolattr") << "get flag 1 on b (should be F)\n";
+  ASSERT_TRUE(b.getAttribute(TestFlag1(), bb));
+  ASSERT_FALSE(bb);
+  Debug("boolattr") << "get flag 1 on c (should be F)\n";
+  ASSERT_TRUE(c.getAttribute(TestFlag1(), bb));
+  ASSERT_FALSE(bb);
+  Debug("boolattr") << "get flag 1 on unnamed (should be F)\n";
+  ASSERT_TRUE(unnamed.getAttribute(TestFlag1(), bb));
+  ASSERT_FALSE(bb);
+
+  Debug("boolattr") << "get flag 2 on a (should be F)\n";
+  ASSERT_TRUE(a.getAttribute(TestFlag2(), bb));
+  ASSERT_FALSE(bb);
+  Debug("boolattr") << "get flag 2 on b (should be F)\n";
+  ASSERT_TRUE(b.getAttribute(TestFlag2(), bb));
+  ASSERT_FALSE(bb);
+  Debug("boolattr") << "get flag 2 on c (should be F)\n";
+  ASSERT_TRUE(c.getAttribute(TestFlag2(), bb));
+  ASSERT_FALSE(bb);
+  Debug("boolattr") << "get flag 2 on unnamed (should be F)\n";
+  ASSERT_TRUE(unnamed.getAttribute(TestFlag2(), bb));
+  ASSERT_FALSE(bb);
+
+  Debug("boolattr") << "get flag 3 on a (should be F)\n";
+  ASSERT_TRUE(a.getAttribute(TestFlag3(), bb));
+  ASSERT_FALSE(bb);
+  Debug("boolattr") << "get flag 3 on b (should be F)\n";
+  ASSERT_TRUE(b.getAttribute(TestFlag3(), bb));
+  ASSERT_FALSE(bb);
+  Debug("boolattr") << "get flag 3 on c (should be F)\n";
+  ASSERT_TRUE(c.getAttribute(TestFlag3(), bb));
+  ASSERT_FALSE(bb);
+  Debug("boolattr") << "get flag 3 on unnamed (should be F)\n";
+  ASSERT_TRUE(unnamed.getAttribute(TestFlag3(), bb));
+  ASSERT_FALSE(bb);
+
+  Debug("boolattr") << "get flag 4 on a (should be F)\n";
+  ASSERT_TRUE(a.getAttribute(TestFlag4(), bb));
+  ASSERT_FALSE(bb);
+  Debug("boolattr") << "get flag 4 on b (should be F)\n";
+  ASSERT_TRUE(b.getAttribute(TestFlag4(), bb));
+  ASSERT_FALSE(bb);
+  Debug("boolattr") << "get flag 4 on c (should be F)\n";
+  ASSERT_TRUE(c.getAttribute(TestFlag4(), bb));
+  ASSERT_FALSE(bb);
+  Debug("boolattr") << "get flag 4 on unnamed (should be F)\n";
+  ASSERT_TRUE(unnamed.getAttribute(TestFlag4(), bb));
+  ASSERT_FALSE(bb);
+
+  Debug("boolattr") << "get flag 5 on a (should be F)\n";
+  ASSERT_TRUE(a.getAttribute(TestFlag5(), bb));
+  ASSERT_FALSE(bb);
+  Debug("boolattr") << "get flag 5 on b (should be F)\n";
+  ASSERT_TRUE(b.getAttribute(TestFlag5(), bb));
+  ASSERT_FALSE(bb);
+  Debug("boolattr") << "get flag 5 on c (should be F)\n";
+  ASSERT_TRUE(c.getAttribute(TestFlag5(), bb));
+  ASSERT_FALSE(bb);
+  Debug("boolattr") << "get flag 5 on unnamed (should be F)\n";
+  ASSERT_TRUE(unnamed.getAttribute(TestFlag5(), bb));
+  ASSERT_FALSE(bb);
+
+  // setting boolean flags
+  Debug("boolattr") << "set flag 1 on a to T\n";
+  a.setAttribute(TestFlag1(), true);
+  Debug("boolattr") << "set flag 1 on b to F\n";
+  b.setAttribute(TestFlag1(), false);
+  Debug("boolattr") << "set flag 1 on c to F\n";
+  c.setAttribute(TestFlag1(), false);
+  Debug("boolattr") << "set flag 1 on unnamed to T\n";
+  unnamed.setAttribute(TestFlag1(), true);
+
+  Debug("boolattr") << "set flag 2 on a to F\n";
+  a.setAttribute(TestFlag2(), false);
+  Debug("boolattr") << "set flag 2 on b to T\n";
+  b.setAttribute(TestFlag2(), true);
+  Debug("boolattr") << "set flag 2 on c to T\n";
+  c.setAttribute(TestFlag2(), true);
+  Debug("boolattr") << "set flag 2 on unnamed to F\n";
+  unnamed.setAttribute(TestFlag2(), false);
+
+  Debug("boolattr") << "set flag 3 on a to T\n";
+  a.setAttribute(TestFlag3(), true);
+  Debug("boolattr") << "set flag 3 on b to T\n";
+  b.setAttribute(TestFlag3(), true);
+  Debug("boolattr") << "set flag 3 on c to T\n";
+  c.setAttribute(TestFlag3(), true);
+  Debug("boolattr") << "set flag 3 on unnamed to T\n";
+  unnamed.setAttribute(TestFlag3(), true);
+
+  Debug("boolattr") << "set flag 4 on a to T\n";
+  a.setAttribute(TestFlag4(), true);
+  Debug("boolattr") << "set flag 4 on b to T\n";
+  b.setAttribute(TestFlag4(), true);
+  Debug("boolattr") << "set flag 4 on c to T\n";
+  c.setAttribute(TestFlag4(), true);
+  Debug("boolattr") << "set flag 4 on unnamed to T\n";
+  unnamed.setAttribute(TestFlag4(), true);
+
+  Debug("boolattr") << "set flag 5 on a to T\n";
+  a.setAttribute(TestFlag5(), true);
+  Debug("boolattr") << "set flag 5 on b to T\n";
+  b.setAttribute(TestFlag5(), true);
+  Debug("boolattr") << "set flag 5 on c to F\n";
+  c.setAttribute(TestFlag5(), false);
+  Debug("boolattr") << "set flag 5 on unnamed to T\n";
+  unnamed.setAttribute(TestFlag5(), true);
+
+  ASSERT_EQ(a.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "");
+
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "a");
+  ASSERT_EQ(b.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "");
+
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "b");
+  ASSERT_EQ(c.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "");
+
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c");
+  ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), "");
+
+  ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr()));
+
+  ASSERT_FALSE(a.hasAttribute(TestStringAttr1()));
+  ASSERT_FALSE(b.hasAttribute(TestStringAttr1()));
+  ASSERT_FALSE(c.hasAttribute(TestStringAttr1()));
+  ASSERT_FALSE(unnamed.hasAttribute(TestStringAttr1()));
+
+  ASSERT_FALSE(a.hasAttribute(TestStringAttr2()));
+  ASSERT_FALSE(b.hasAttribute(TestStringAttr2()));
+  ASSERT_FALSE(c.hasAttribute(TestStringAttr2()));
+  ASSERT_FALSE(unnamed.hasAttribute(TestStringAttr2()));
+
+  Debug("boolattr") << "get flag 1 on a (should be T)\n";
+  ASSERT_TRUE(a.getAttribute(TestFlag1()));
+  Debug("boolattr") << "get flag 1 on b (should be F)\n";
+  ASSERT_FALSE(b.getAttribute(TestFlag1()));
+  Debug("boolattr") << "get flag 1 on c (should be F)\n";
+  ASSERT_FALSE(c.getAttribute(TestFlag1()));
+  Debug("boolattr") << "get flag 1 on unnamed (should be T)\n";
+  ASSERT_TRUE(unnamed.getAttribute(TestFlag1()));
+
+  Debug("boolattr") << "get flag 2 on a (should be F)\n";
+  ASSERT_FALSE(a.getAttribute(TestFlag2()));
+  Debug("boolattr") << "get flag 2 on b (should be T)\n";
+  ASSERT_TRUE(b.getAttribute(TestFlag2()));
+  Debug("boolattr") << "get flag 2 on c (should be T)\n";
+  ASSERT_TRUE(c.getAttribute(TestFlag2()));
+  Debug("boolattr") << "get flag 2 on unnamed (should be F)\n";
+  ASSERT_FALSE(unnamed.getAttribute(TestFlag2()));
+
+  Debug("boolattr") << "get flag 3 on a (should be T)\n";
+  ASSERT_TRUE(a.getAttribute(TestFlag3()));
+  Debug("boolattr") << "get flag 3 on b (should be T)\n";
+  ASSERT_TRUE(b.getAttribute(TestFlag3()));
+  Debug("boolattr") << "get flag 3 on c (should be T)\n";
+  ASSERT_TRUE(c.getAttribute(TestFlag3()));
+  Debug("boolattr") << "get flag 3 on unnamed (should be T)\n";
+  ASSERT_TRUE(unnamed.getAttribute(TestFlag3()));
+
+  Debug("boolattr") << "get flag 4 on a (should be T)\n";
+  ASSERT_TRUE(a.getAttribute(TestFlag4()));
+  Debug("boolattr") << "get flag 4 on b (should be T)\n";
+  ASSERT_TRUE(b.getAttribute(TestFlag4()));
+  Debug("boolattr") << "get flag 4 on c (should be T)\n";
+  ASSERT_TRUE(c.getAttribute(TestFlag4()));
+  Debug("boolattr") << "get flag 4 on unnamed (should be T)\n";
+  ASSERT_TRUE(unnamed.getAttribute(TestFlag4()));
+
+  Debug("boolattr") << "get flag 5 on a (should be T)\n";
+  ASSERT_TRUE(a.getAttribute(TestFlag5()));
+  Debug("boolattr") << "get flag 5 on b (should be T)\n";
+  ASSERT_TRUE(b.getAttribute(TestFlag5()));
+  Debug("boolattr") << "get flag 5 on c (should be F)\n";
+  ASSERT_FALSE(c.getAttribute(TestFlag5()));
+  Debug("boolattr") << "get flag 5 on unnamed (should be T)\n";
+  ASSERT_TRUE(unnamed.getAttribute(TestFlag5()));
+
+  a.setAttribute(TestStringAttr1(), "foo");
+  b.setAttribute(TestStringAttr1(), "bar");
+  c.setAttribute(TestStringAttr1(), "baz");
+
+  ASSERT_EQ(a.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "");
+
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "a");
+  ASSERT_EQ(b.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "");
+
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "b");
+  ASSERT_EQ(c.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "");
+
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c");
+  ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), "");
+
+  ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr()));
+
+  ASSERT_TRUE(a.hasAttribute(TestStringAttr1()));
+  ASSERT_TRUE(b.hasAttribute(TestStringAttr1()));
+  ASSERT_TRUE(c.hasAttribute(TestStringAttr1()));
+  ASSERT_FALSE(unnamed.hasAttribute(TestStringAttr1()));
+
+  ASSERT_FALSE(a.hasAttribute(TestStringAttr2()));
+  ASSERT_FALSE(b.hasAttribute(TestStringAttr2()));
+  ASSERT_FALSE(c.hasAttribute(TestStringAttr2()));
+  ASSERT_FALSE(unnamed.hasAttribute(TestStringAttr2()));
+
+  a.setAttribute(VarNameAttr(), "b");
+  b.setAttribute(VarNameAttr(), "c");
+  c.setAttribute(VarNameAttr(), "a");
+
+  ASSERT_EQ(c.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "");
+
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "a");
+  ASSERT_EQ(a.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "");
+
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "b");
+  ASSERT_EQ(b.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "");
+
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c");
+  ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), "");
+
+  ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr()));
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/node/kind_black.cpp b/test/unit/node/kind_black.cpp
new file mode 100644
index 000000000..a33955152
--- /dev/null
+++ b/test/unit/node/kind_black.cpp
@@ -0,0 +1,90 @@
+/*********************                                                        */
+/*! \file kind_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::Kind.
+ **
+ ** Black box testing of CVC4::Kind.
+ **/
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#include "expr/kind.h"
+#include "test.h"
+
+namespace CVC4 {
+
+using namespace kind;
+
+namespace test {
+
+class TestNodeBlackKind : public TestInternal
+{
+ protected:
+  void SetUp() override
+  {
+    d_undefined = UNDEFINED_KIND;
+    d_null = NULL_EXPR;
+    d_last = LAST_KIND;
+    d_beyond = ((int32_t)LAST_KIND) + 1;
+    d_unknown = (Kind)d_beyond;
+  }
+
+  bool string_is_as_expected(Kind k, const char* s)
+  {
+    std::stringstream act;
+    std::stringstream exp;
+    act << k;
+    exp << s;
+    return act.str() == exp.str();
+  }
+
+  Kind d_undefined;
+  Kind d_unknown;
+  Kind d_null;
+  Kind d_last;
+  int32_t d_beyond;
+};
+
+TEST_F(TestNodeBlackKind, equality)
+{
+  ASSERT_EQ(d_undefined, UNDEFINED_KIND);
+  ASSERT_EQ(d_last, LAST_KIND);
+}
+
+TEST_F(TestNodeBlackKind, order)
+{
+  ASSERT_LT((int32_t)d_undefined, (int32_t)d_null);
+  ASSERT_LT((int32_t)d_null, (int32_t)d_last);
+  ASSERT_LT((int32_t)d_undefined, (int32_t)d_last);
+  ASSERT_LT((int32_t)d_last, (int32_t)d_unknown);
+}
+
+TEST_F(TestNodeBlackKind, output)
+{
+  ASSERT_TRUE(string_is_as_expected(d_undefined, "UNDEFINED_KIND"));
+  ASSERT_TRUE(string_is_as_expected(d_null, "NULL"));
+  ASSERT_TRUE(string_is_as_expected(d_last, "LAST_KIND"));
+}
+
+TEST_F(TestNodeBlackKind, output_concat)
+{
+  std::stringstream act, exp;
+  act << d_undefined << d_null << d_last << d_unknown;
+  exp << "UNDEFINED_KIND"
+      << "NULL"
+      << "LAST_KIND"
+      << "?";
+  ASSERT_EQ(act.str(), exp.str());
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/node/kind_map_black.cpp b/test/unit/node/kind_map_black.cpp
new file mode 100644
index 000000000..8e1c45d79
--- /dev/null
+++ b/test/unit/node/kind_map_black.cpp
@@ -0,0 +1,48 @@
+/*********************                                                        */
+/*! \file kind_map_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::KindMap
+ **
+ ** Black box testing of CVC4::KindMap.
+ **/
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#include "expr/kind_map.h"
+#include "test.h"
+
+namespace CVC4 {
+
+using namespace kind;
+
+namespace test {
+
+class TestNodeBlackKindMap : public TestInternal
+{
+};
+
+TEST_F(TestNodeBlackKindMap, simple)
+{
+  KindMap map;
+  ASSERT_FALSE(map.test(AND));
+  map.set(AND);
+  ASSERT_TRUE(map.test(AND));
+  map.reset(AND);
+  ASSERT_FALSE(map.test(AND));
+#ifdef CVC4_ASSERTIONS
+  ASSERT_THROW(map.set(LAST_KIND), AssertArgumentException);
+#endif
+}
+
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp
new file mode 100644
index 000000000..bd243e0fd
--- /dev/null
+++ b/test/unit/node/node_algorithm_black.cpp
@@ -0,0 +1,202 @@
+/*********************                                                        */
+/*! \file node_algorithm_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Yoni Zohar, Abdalrhman Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of utility functions in node_algorithm.{h,cpp}
+ **
+ ** Black box testing of node_algorithm.{h,cpp}
+ **/
+
+#include <string>
+#include <vector>
+
+#include "base/output.h"
+#include "expr/node_algorithm.h"
+#include "expr/node_manager.h"
+#include "test_node.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "util/integer.h"
+#include "util/rational.h"
+
+namespace CVC4 {
+
+using namespace expr;
+using namespace kind;
+
+namespace test {
+
+class TestNodeBlackNodeAlgorithm : public TestNode
+{
+};
+
+TEST_F(TestNodeBlackNodeAlgorithm, get_symbols1)
+{
+  // The only symbol in ~x (x is a boolean varible) should be x
+  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+  Node n = d_nodeManager->mkNode(NOT, x);
+  std::unordered_set<Node, NodeHashFunction> syms;
+  getSymbols(n, syms);
+  ASSERT_EQ(syms.size(), 1);
+  ASSERT_NE(syms.find(x), syms.end());
+}
+
+TEST_F(TestNodeBlackNodeAlgorithm, get_symbols2)
+{
+  // the only symbols in x=y ^ (exists var. var+var = x) are x and y, because
+  // "var" is bound.
+
+  // left conjunct
+  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
+  Node y = d_nodeManager->mkSkolem("y", d_nodeManager->integerType());
+  Node left = d_nodeManager->mkNode(EQUAL, x, y);
+
+  // right conjunct
+  Node var = d_nodeManager->mkBoundVar(*d_intTypeNode);
+  std::vector<Node> vars;
+  vars.push_back(var);
+  Node sum = d_nodeManager->mkNode(PLUS, var, var);
+  Node qeq = d_nodeManager->mkNode(EQUAL, x, sum);
+  Node bvl = d_nodeManager->mkNode(BOUND_VAR_LIST, vars);
+  Node right = d_nodeManager->mkNode(EXISTS, bvl, qeq);
+
+  // conjunction
+  Node res = d_nodeManager->mkNode(AND, left, right);
+
+  // symbols
+  std::unordered_set<Node, NodeHashFunction> syms;
+  getSymbols(res, syms);
+
+  // assertions
+  ASSERT_EQ(syms.size(), 2);
+  ASSERT_NE(syms.find(x), syms.end());
+  ASSERT_NE(syms.find(y), syms.end());
+  ASSERT_EQ(syms.find(var), syms.end());
+}
+
+TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map)
+{
+  // map to store result
+  std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > result =
+      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> >();
+
+  // create test formula
+  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
+  Node plus = d_nodeManager->mkNode(PLUS, x, x);
+  Node mul = d_nodeManager->mkNode(MULT, x, x);
+  Node eq1 = d_nodeManager->mkNode(EQUAL, plus, mul);
+
+  Node y = d_nodeManager->mkSkolem("y", d_nodeManager->mkBitVectorType(4));
+  Node ext1 = theory::bv::utils::mkExtract(y, 1, 0);
+  Node ext2 = theory::bv::utils::mkExtract(y, 3, 2);
+  Node eq2 = d_nodeManager->mkNode(EQUAL, ext1, ext2);
+
+  Node formula = d_nodeManager->mkNode(AND, eq1, eq2);
+
+  // call function
+  expr::getOperatorsMap(formula, result);
+
+  // Verify result
+  // We should have only integer, bv and boolean as types
+  ASSERT_EQ(result.size(), 3);
+  ASSERT_NE(result.find(*d_intTypeNode), result.end());
+  ASSERT_NE(result.find(*d_boolTypeNode), result.end());
+  ASSERT_NE(result.find(*d_bvTypeNode), result.end());
+
+  // in integers, we should only have plus and mult as operators
+  ASSERT_EQ(result[*d_intTypeNode].size(), 2);
+  ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(PLUS)),
+            result[*d_intTypeNode].end());
+  ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(MULT)),
+            result[*d_intTypeNode].end());
+
+  // in booleans, we should only have "=" and "and" as an operator.
+  ASSERT_EQ(result[*d_boolTypeNode].size(), 2);
+  ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(EQUAL)),
+            result[*d_boolTypeNode].end());
+  ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(AND)),
+            result[*d_boolTypeNode].end());
+
+  // in bv, we should only have "extract" as an operator.
+  ASSERT_EQ(result[*d_boolTypeNode].size(), 2);
+  Node extractOp1 =
+      d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(1, 0));
+  Node extractOp2 =
+      d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(3, 2));
+  ASSERT_NE(result[*d_bvTypeNode].find(extractOp1),
+            result[*d_bvTypeNode].end());
+  ASSERT_NE(result[*d_bvTypeNode].find(extractOp2),
+            result[*d_bvTypeNode].end());
+}
+
+TEST_F(TestNodeBlackNodeAlgorithm, match)
+{
+  TypeNode integer = d_nodeManager->integerType();
+
+  Node one = d_nodeManager->mkConst(Rational(1));
+  Node two = d_nodeManager->mkConst(Rational(2));
+
+  Node x = d_nodeManager->mkBoundVar(integer);
+  Node a = d_nodeManager->mkSkolem("a", integer);
+
+  Node n1 = d_nodeManager->mkNode(MULT, two, x);
+  std::unordered_map<Node, Node, NodeHashFunction> subs;
+
+  // check reflexivity
+  ASSERT_TRUE(match(n1, n1, subs));
+  ASSERT_EQ(subs.size(), 0);
+
+  Node n2 = d_nodeManager->mkNode(MULT, two, a);
+  subs.clear();
+
+  // check instance
+  ASSERT_TRUE(match(n1, n2, subs));
+  ASSERT_EQ(subs.size(), 1);
+  ASSERT_EQ(subs[x], a);
+
+  // should return false for flipped arguments (match is not symmetric)
+  ASSERT_FALSE(match(n2, n1, subs));
+
+  n2 = d_nodeManager->mkNode(MULT, one, a);
+
+  // should return false since n2 is not an instance of n1
+  ASSERT_FALSE(match(n1, n2, subs));
+
+  n2 = d_nodeManager->mkNode(NONLINEAR_MULT, two, a);
+
+  // should return false for similar operators
+  ASSERT_FALSE(match(n1, n2, subs));
+
+  n2 = d_nodeManager->mkNode(MULT, two, a, one);
+
+  // should return false for different number of arguments
+  ASSERT_FALSE(match(n1, n2, subs));
+
+  n1 = x;
+  n2 = d_nodeManager->mkConst(true);
+
+  // should return false for different types
+  ASSERT_FALSE(match(n1, n2, subs));
+
+  n1 = d_nodeManager->mkNode(MULT, x, x);
+  n2 = d_nodeManager->mkNode(MULT, two, a);
+
+  // should return false for contradictory substitutions
+  ASSERT_FALSE(match(n1, n2, subs));
+
+  n2 = d_nodeManager->mkNode(MULT, a, a);
+  subs.clear();
+
+  // implementation: check if the cache works correctly
+  ASSERT_TRUE(match(n1, n2, subs));
+  ASSERT_EQ(subs.size(), 1);
+  ASSERT_EQ(subs[x], a);
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
new file mode 100644
index 000000000..3c1651155
--- /dev/null
+++ b/test/unit/node/node_black.cpp
@@ -0,0 +1,787 @@
+/*********************                                                        */
+/*! \file node_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Morgan Deters, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::Node.
+ **
+ ** Black box testing of CVC4::Node.
+ **/
+
+#include <algorithm>
+#include <sstream>
+#include <string>
+#include <vector>
+
+#include "api/cvc4cpp.h"
+#include "expr/dtype.h"
+#include "expr/dtype_cons.h"
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_manager.h"
+#include "expr/node_value.h"
+#include "smt/smt_engine.h"
+#include "test_node.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+
+using namespace kind;
+
+namespace test {
+
+namespace {
+/** Returns N skolem nodes from 'nodeManager' with the same `type`. */
+std::vector<Node> makeNSkolemNodes(NodeManager* nodeManager,
+                                   uint32_t n,
+                                   TypeNode type)
+{
+  std::vector<Node> skolems;
+  for (uint32_t i = 0; i < n; i++)
+  {
+    skolems.push_back(nodeManager->mkSkolem(
+        "skolem_", type, "Created by makeNSkolemNodes()"));
+  }
+  return skolems;
+}
+}  // namespace
+
+class TestNodeBlackNode : public TestNode
+{
+ protected:
+  void SetUp() override
+  {
+    TestNode::SetUp();
+    // setup an SMT engine so that options are in scope
+    Options opts;
+    char* argv[2];
+    argv[0] = strdup("");
+    argv[1] = strdup("--output-lang=ast");
+    Options::parseOptions(&opts, 2, argv);
+    free(argv[0]);
+    free(argv[1]);
+    d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts));
+  }
+
+  std::unique_ptr<SmtEngine> d_smt;
+
+  bool imp(bool a, bool b) const { return (!a) || (b); }
+  bool iff(bool a, bool b) const { return (a && b) || ((!a) && (!b)); }
+
+  void testNaryExpForSize(Kind k, uint32_t n)
+  {
+    NodeBuilder<> nbz(k);
+    Node trueNode = d_nodeManager->mkConst(true);
+    for (uint32_t i = 0; i < n; ++i)
+    {
+      nbz << trueNode;
+    }
+    Node result = nbz;
+    ASSERT_EQ(n, result.getNumChildren());
+  }
+};
+
+TEST_F(TestNodeBlackNode, null) { Node::null(); }
+
+TEST_F(TestNodeBlackNode, is_null)
+{
+  Node a = Node::null();
+  ASSERT_TRUE(a.isNull());
+
+  Node b = Node();
+  ASSERT_TRUE(b.isNull());
+
+  Node c = b;
+  ASSERT_TRUE(c.isNull());
+}
+
+TEST_F(TestNodeBlackNode, copy_ctor) { Node e(Node::null()); }
+
+TEST_F(TestNodeBlackNode, dtor)
+{
+  /* No access to internals? Only test that this is crash free. */
+  Node* n = nullptr;
+  ASSERT_NO_FATAL_FAILURE(n = new Node());
+  if (n)
+  {
+    delete n;
+  }
+}
+
+/* operator== */
+TEST_F(TestNodeBlackNode, operator_equals)
+{
+  Node a, b, c;
+
+  b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+
+  a = b;
+  c = a;
+
+  Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
+
+  ASSERT_TRUE(a == a);
+  ASSERT_TRUE(a == b);
+  ASSERT_TRUE(a == c);
+
+  ASSERT_TRUE(b == a);
+  ASSERT_TRUE(b == b);
+  ASSERT_TRUE(b == c);
+
+  ASSERT_TRUE(c == a);
+  ASSERT_TRUE(c == b);
+  ASSERT_TRUE(c == c);
+
+  ASSERT_TRUE(d == d);
+
+  ASSERT_FALSE(d == a);
+  ASSERT_FALSE(d == b);
+  ASSERT_FALSE(d == c);
+
+  ASSERT_FALSE(a == d);
+  ASSERT_FALSE(b == d);
+  ASSERT_FALSE(c == d);
+}
+
+/* operator!= */
+TEST_F(TestNodeBlackNode, operator_not_equals)
+{
+  Node a, b, c;
+
+  b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+
+  a = b;
+  c = a;
+
+  Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
+
+  /*structed assuming operator == works */
+  ASSERT_TRUE(iff(a != a, !(a == a)));
+  ASSERT_TRUE(iff(a != b, !(a == b)));
+  ASSERT_TRUE(iff(a != c, !(a == c)));
+
+  ASSERT_TRUE(iff(b != a, !(b == a)));
+  ASSERT_TRUE(iff(b != b, !(b == b)));
+  ASSERT_TRUE(iff(b != c, !(b == c)));
+
+  ASSERT_TRUE(iff(c != a, !(c == a)));
+  ASSERT_TRUE(iff(c != b, !(c == b)));
+  ASSERT_TRUE(iff(c != c, !(c == c)));
+
+  ASSERT_TRUE(!(d != d));
+
+  ASSERT_TRUE(d != a);
+  ASSERT_TRUE(d != b);
+  ASSERT_TRUE(d != c);
+}
+
+/* operator[] */
+TEST_F(TestNodeBlackNode, operator_square)
+{
+#ifdef CVC4_ASSERTIONS
+  // Basic bounds check on a node w/out children
+  ASSERT_DEATH(Node::null()[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren");
+  ASSERT_DEATH(Node::null()[0], "i >= 0 && unsigned\\(i\\) < d_nchildren");
+#endif
+
+  // Basic access check
+  Node tb = d_nodeManager->mkConst(true);
+  Node eb = d_nodeManager->mkConst(false);
+  Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+  Node ite = cnd.iteNode(tb, eb);
+
+  ASSERT_EQ(tb, cnd[0]);
+  ASSERT_EQ(eb, cnd[1]);
+
+  ASSERT_EQ(cnd, ite[0]);
+  ASSERT_EQ(tb, ite[1]);
+  ASSERT_EQ(eb, ite[2]);
+
+#ifdef CVC4_ASSERTIONS
+  // Bounds check on a node with children
+  ASSERT_DEATH(ite == ite[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren");
+  ASSERT_DEATH(ite == ite[4], "i >= 0 && unsigned\\(i\\) < d_nchildren");
+#endif
+}
+
+/* operator= */
+TEST_F(TestNodeBlackNode, operator_assign)
+{
+  Node a, b;
+  Node c = d_nodeManager->mkNode(
+      NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType()));
+
+  b = c;
+  ASSERT_EQ(b, c);
+
+  a = b = c;
+
+  ASSERT_EQ(a, b);
+  ASSERT_EQ(a, c);
+}
+
+/* operator< */
+TEST_F(TestNodeBlackNode, operator_less_than)
+{
+  // We don't have access to the ids so we can't test the implementation
+  // in the black box tests.
+
+  Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+  Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+
+  ASSERT_TRUE(a < b || b < a);
+  ASSERT_TRUE(!(a < b && b < a));
+
+  Node c = d_nodeManager->mkNode(AND, a, b);
+  Node d = d_nodeManager->mkNode(AND, a, b);
+
+  ASSERT_FALSE(c < d);
+  ASSERT_FALSE(d < c);
+
+  // simple test of descending descendant property
+  Node child = d_nodeManager->mkConst(true);
+  Node parent = d_nodeManager->mkNode(NOT, child);
+
+  ASSERT_TRUE(child < parent);
+
+  // slightly less simple test of DD property
+  std::vector<Node> chain;
+  const int N = 500;
+  Node curr = d_nodeManager->mkNode(OR, a, b);
+  chain.push_back(curr);
+  for (int i = 0; i < N; ++i)
+  {
+    curr = d_nodeManager->mkNode(AND, curr, curr);
+    chain.push_back(curr);
+  }
+
+  for (int i = 0; i < N; ++i)
+  {
+    for (int j = i + 1; j < N; ++j)
+    {
+      Node chain_i = chain[i];
+      Node chain_j = chain[j];
+      ASSERT_TRUE(chain_i < chain_j);
+    }
+  }
+}
+
+TEST_F(TestNodeBlackNode, eqNode)
+{
+  TypeNode t = d_nodeManager->mkSort();
+  Node left = d_nodeManager->mkSkolem("left", t);
+  Node right = d_nodeManager->mkSkolem("right", t);
+  Node eq = left.eqNode(right);
+
+  ASSERT_EQ(EQUAL, eq.getKind());
+  ASSERT_EQ(2, eq.getNumChildren());
+
+  ASSERT_EQ(eq[0], left);
+  ASSERT_EQ(eq[1], right);
+}
+
+TEST_F(TestNodeBlackNode, notNode)
+{
+  Node child = d_nodeManager->mkConst(true);
+  Node parent = child.notNode();
+
+  ASSERT_EQ(NOT, parent.getKind());
+  ASSERT_EQ(1, parent.getNumChildren());
+
+  ASSERT_EQ(parent[0], child);
+}
+
+TEST_F(TestNodeBlackNode, andNode)
+{
+  Node left = d_nodeManager->mkConst(true);
+  Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
+  Node eq = left.andNode(right);
+
+  ASSERT_EQ(AND, eq.getKind());
+  ASSERT_EQ(2, eq.getNumChildren());
+
+  ASSERT_EQ(*(eq.begin()), left);
+  ASSERT_EQ(*(++eq.begin()), right);
+}
+
+TEST_F(TestNodeBlackNode, orNode)
+{
+  Node left = d_nodeManager->mkConst(true);
+  Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
+  Node eq = left.orNode(right);
+
+  ASSERT_EQ(OR, eq.getKind());
+  ASSERT_EQ(2, eq.getNumChildren());
+
+  ASSERT_EQ(*(eq.begin()), left);
+  ASSERT_EQ(*(++eq.begin()), right);
+}
+
+TEST_F(TestNodeBlackNode, iteNode)
+{
+  Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+  Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+
+  Node cnd = d_nodeManager->mkNode(OR, a, b);
+  Node thenBranch = d_nodeManager->mkConst(true);
+  Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false));
+  Node ite = cnd.iteNode(thenBranch, elseBranch);
+
+  ASSERT_EQ(ITE, ite.getKind());
+  ASSERT_EQ(3, ite.getNumChildren());
+
+  ASSERT_EQ(*(ite.begin()), cnd);
+  ASSERT_EQ(*(++ite.begin()), thenBranch);
+  ASSERT_EQ(*(++(++ite.begin())), elseBranch);
+}
+
+TEST_F(TestNodeBlackNode, iffNode)
+{
+  Node left = d_nodeManager->mkConst(true);
+  Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
+  Node eq = left.eqNode(right);
+
+  ASSERT_EQ(EQUAL, eq.getKind());
+  ASSERT_EQ(2, eq.getNumChildren());
+
+  ASSERT_EQ(*(eq.begin()), left);
+  ASSERT_EQ(*(++eq.begin()), right);
+}
+
+TEST_F(TestNodeBlackNode, impNode)
+{
+  Node left = d_nodeManager->mkConst(true);
+  Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
+  Node eq = left.impNode(right);
+
+  ASSERT_EQ(IMPLIES, eq.getKind());
+  ASSERT_EQ(2, eq.getNumChildren());
+
+  ASSERT_EQ(*(eq.begin()), left);
+  ASSERT_EQ(*(++eq.begin()), right);
+}
+
+TEST_F(TestNodeBlackNode, xorNode)
+{
+  Node left = d_nodeManager->mkConst(true);
+  Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
+  Node eq = left.xorNode(right);
+
+  ASSERT_EQ(XOR, eq.getKind());
+  ASSERT_EQ(2, eq.getNumChildren());
+
+  ASSERT_EQ(*(eq.begin()), left);
+  ASSERT_EQ(*(++eq.begin()), right);
+}
+
+TEST_F(TestNodeBlackNode, getKind)
+{
+  Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+  Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+
+  Node n = d_nodeManager->mkNode(NOT, a);
+  ASSERT_EQ(NOT, n.getKind());
+
+  n = d_nodeManager->mkNode(EQUAL, a, b);
+  ASSERT_EQ(EQUAL, n.getKind());
+
+  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType());
+  Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType());
+
+  n = d_nodeManager->mkNode(PLUS, x, y);
+  ASSERT_EQ(PLUS, n.getKind());
+
+  n = d_nodeManager->mkNode(UMINUS, x);
+  ASSERT_EQ(UMINUS, n.getKind());
+}
+
+TEST_F(TestNodeBlackNode, getOperator)
+{
+  TypeNode sort = d_nodeManager->mkSort("T");
+  TypeNode booleanType = d_nodeManager->booleanType();
+  TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
+
+  Node f = d_nodeManager->mkSkolem("f", predType);
+  Node a = d_nodeManager->mkSkolem("a", sort);
+  Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a);
+
+  ASSERT_TRUE(fa.hasOperator());
+  ASSERT_FALSE(f.hasOperator());
+  ASSERT_FALSE(a.hasOperator());
+
+  ASSERT_EQ(fa.getNumChildren(), 1);
+  ASSERT_EQ(f.getNumChildren(), 0);
+  ASSERT_EQ(a.getNumChildren(), 0);
+
+  ASSERT_EQ(f, fa.getOperator());
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(f.getOperator(), "mk == kind::metakind::PARAMETERIZED");
+  ASSERT_DEATH(a.getOperator(), "mk == kind::metakind::PARAMETERIZED");
+#endif
+}
+
+TEST_F(TestNodeBlackNode, getNumChildren)
+{
+  Node trueNode = d_nodeManager->mkConst(true);
+
+  ASSERT_EQ(0, (Node::null()).getNumChildren());
+  ASSERT_EQ(1, trueNode.notNode().getNumChildren());
+  ASSERT_EQ(2, trueNode.andNode(trueNode).getNumChildren());
+
+  srand(0);
+  for (uint32_t i = 0; i < 500; ++i)
+  {
+    uint32_t n = rand() % 1000 + 2;
+    testNaryExpForSize(AND, n);
+  }
+
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(testNaryExpForSize(AND, 0),
+               "getNumChildren\\(\\) >= "
+               "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)");
+  ASSERT_DEATH(testNaryExpForSize(AND, 1),
+               "getNumChildren\\(\\) >= "
+               "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)");
+  ASSERT_DEATH(testNaryExpForSize(NOT, 0),
+               "getNumChildren\\(\\) >= "
+               "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)");
+  ASSERT_DEATH(testNaryExpForSize(NOT, 2),
+               "getNumChildren\\(\\) <= "
+               "kind::metakind::getMaxArityForKind\\(getKind\\(\\)\\)");
+#endif /* CVC4_ASSERTIONS */
+}
+
+TEST_F(TestNodeBlackNode, iterator)
+{
+  NodeBuilder<> b;
+  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+  Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
+  Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType());
+  Node n = b << x << y << z << kind::AND;
+
+  {  // iterator
+    Node::iterator i = n.begin();
+    ASSERT_EQ(*i++, x);
+    ASSERT_EQ(*i++, y);
+    ASSERT_EQ(*i++, z);
+    ASSERT_EQ(i, n.end());
+  }
+
+  {  // same for const iterator
+    const Node& c = n;
+    Node::const_iterator i = c.begin();
+    ASSERT_EQ(*i++, x);
+    ASSERT_EQ(*i++, y);
+    ASSERT_EQ(*i++, z);
+    ASSERT_EQ(i, n.end());
+  }
+}
+
+TEST_F(TestNodeBlackNode, kinded_iterator)
+{
+  TypeNode integerType = d_nodeManager->integerType();
+
+  Node x = d_nodeManager->mkSkolem("x", integerType);
+  Node y = d_nodeManager->mkSkolem("y", integerType);
+  Node z = d_nodeManager->mkSkolem("z", integerType);
+  Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z);
+  Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y);
+
+  {  // iterator
+    Node::kinded_iterator i = plus_x_y_z.begin(PLUS);
+    ASSERT_EQ(*i++, x);
+    ASSERT_EQ(*i++, y);
+    ASSERT_EQ(*i++, z);
+    ASSERT_TRUE(i == plus_x_y_z.end(PLUS));
+
+    i = x.begin(PLUS);
+    ASSERT_EQ(*i++, x);
+    ASSERT_TRUE(i == x.end(PLUS));
+  }
+}
+
+TEST_F(TestNodeBlackNode, toString)
+{
+  TypeNode booleanType = d_nodeManager->booleanType();
+
+  Node w = d_nodeManager->mkSkolem(
+      "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node x = d_nodeManager->mkSkolem(
+      "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node y = d_nodeManager->mkSkolem(
+      "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node z = d_nodeManager->mkSkolem(
+      "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node m = NodeBuilder<>() << w << x << kind::OR;
+  Node n = NodeBuilder<>() << m << y << z << kind::AND;
+
+  ASSERT_EQ(n.toString(), "(AND (OR w x) y z)");
+}
+
+TEST_F(TestNodeBlackNode, toStream)
+{
+  TypeNode booleanType = d_nodeManager->booleanType();
+
+  Node w = d_nodeManager->mkSkolem(
+      "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node x = d_nodeManager->mkSkolem(
+      "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node y = d_nodeManager->mkSkolem(
+      "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node z = d_nodeManager->mkSkolem(
+      "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node m = NodeBuilder<>() << x << y << kind::OR;
+  Node n = NodeBuilder<>() << w << m << z << kind::AND;
+  Node o = NodeBuilder<>() << n << n << kind::XOR;
+
+  std::stringstream sstr;
+  sstr << Node::dag(false);
+  n.toStream(sstr);
+  ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
+
+  sstr.str(std::string());
+  o.toStream(sstr, -1, 0);
+  ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
+
+  sstr.str(std::string());
+  sstr << n;
+  ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
+
+  sstr.str(std::string());
+  sstr << o;
+  ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
+
+  sstr.str(std::string());
+  sstr << Node::setdepth(0) << n;
+  ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
+
+  sstr.str(std::string());
+  sstr << Node::setdepth(0) << o;
+  ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
+
+  sstr.str(std::string());
+  sstr << Node::setdepth(1) << n;
+  ASSERT_EQ(sstr.str(), "(AND w (OR (...) (...)) z)");
+
+  sstr.str(std::string());
+  sstr << Node::setdepth(1) << o;
+  ASSERT_EQ(sstr.str(),
+            "(XOR (AND (...) (...) (...)) (AND (...) (...) (...)))");
+
+  sstr.str(std::string());
+  sstr << Node::setdepth(2) << n;
+  ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
+
+  sstr.str(std::string());
+  sstr << Node::setdepth(2) << o;
+  ASSERT_EQ(sstr.str(),
+            "(XOR (AND w (OR (...) (...)) z) (AND w (OR (...) (...)) z))");
+
+  sstr.str(std::string());
+  sstr << Node::setdepth(3) << n;
+  ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
+
+  sstr.str(std::string());
+  sstr << Node::setdepth(3) << o;
+  ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
+}
+
+TEST_F(TestNodeBlackNode, dagifier)
+{
+  TypeNode intType = d_nodeManager->integerType();
+  TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType);
+
+  Node x =
+      d_nodeManager->mkSkolem("x", intType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node y =
+      d_nodeManager->mkSkolem("y", intType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node f =
+      d_nodeManager->mkSkolem("f", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node g =
+      d_nodeManager->mkSkolem("g", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node fx = d_nodeManager->mkNode(APPLY_UF, f, x);
+  Node fy = d_nodeManager->mkNode(APPLY_UF, f, y);
+  Node gx = d_nodeManager->mkNode(APPLY_UF, g, x);
+  Node gy = d_nodeManager->mkNode(APPLY_UF, g, y);
+  Node fgx = d_nodeManager->mkNode(APPLY_UF, f, gx);
+  Node ffx = d_nodeManager->mkNode(APPLY_UF, f, fx);
+  Node fffx = d_nodeManager->mkNode(APPLY_UF, f, ffx);
+  Node fffx_eq_x = d_nodeManager->mkNode(EQUAL, fffx, x);
+  Node fffx_eq_y = d_nodeManager->mkNode(EQUAL, fffx, y);
+  Node fx_eq_gx = d_nodeManager->mkNode(EQUAL, fx, gx);
+  Node x_eq_y = d_nodeManager->mkNode(EQUAL, x, y);
+  Node fgx_eq_gy = d_nodeManager->mkNode(EQUAL, fgx, gy);
+
+  Node n = d_nodeManager->mkNode(
+      OR, fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, fgx_eq_gy);
+
+  std::stringstream sstr;
+  sstr << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC4);
+  sstr << Node::dag(false) << n;  // never dagify
+  ASSERT_EQ(sstr.str(),
+            "(f(f(f(x))) = x) OR (f(f(f(x))) = y) OR (f(x) = g(x)) OR (x = "
+            "y) OR (f(g(x)) = g(y))");
+}
+
+TEST_F(TestNodeBlackNode, for_each_over_nodes_as_node)
+{
+  const std::vector<Node> skolems =
+      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+  Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
+  std::vector<Node> children;
+  for (Node child : add)
+  {
+    children.push_back(child);
+  }
+  ASSERT_TRUE(children.size() == skolems.size()
+              && std::equal(children.begin(), children.end(), skolems.begin()));
+}
+
+TEST_F(TestNodeBlackNode, for_each_over_nodes_as_tnode)
+{
+  const std::vector<Node> skolems =
+      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+  Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
+  std::vector<TNode> children;
+  for (TNode child : add)
+  {
+    children.push_back(child);
+  }
+  ASSERT_TRUE(children.size() == skolems.size()
+              && std::equal(children.begin(), children.end(), skolems.begin()));
+}
+
+TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_node)
+{
+  const std::vector<Node> skolems =
+      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+  Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
+  TNode add_tnode = add_node;
+  std::vector<Node> children;
+  for (Node child : add_tnode)
+  {
+    children.push_back(child);
+  }
+  ASSERT_TRUE(children.size() == skolems.size()
+              && std::equal(children.begin(), children.end(), skolems.begin()));
+}
+
+TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_tnode)
+{
+  const std::vector<Node> skolems =
+      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+  Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
+  TNode add_tnode = add_node;
+  std::vector<TNode> children;
+  for (TNode child : add_tnode)
+  {
+    children.push_back(child);
+  }
+  ASSERT_TRUE(children.size() == skolems.size()
+              && std::equal(children.begin(), children.end(), skolems.begin()));
+}
+
+TEST_F(TestNodeBlackNode, isConst)
+{
+  // more complicated "constants" exist in datatypes and arrays theories
+  DType list("list");
+  std::shared_ptr<DTypeConstructor> consC =
+      std::make_shared<DTypeConstructor>("cons");
+  consC->addArg("car", d_nodeManager->integerType());
+  consC->addArgSelf("cdr");
+  list.addConstructor(consC);
+  list.addConstructor(std::make_shared<DTypeConstructor>("nil"));
+  TypeNode listType = d_nodeManager->mkDatatypeType(list);
+  const std::vector<std::shared_ptr<DTypeConstructor> >& lcons =
+      listType.getDType().getConstructors();
+  Node cons = lcons[0]->getConstructor();
+  Node nil = lcons[1]->getConstructor();
+  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
+  Node cons_x_nil =
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
+                            cons,
+                            x,
+                            d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
+  Node cons_1_nil =
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
+                            cons,
+                            d_nodeManager->mkConst(Rational(1)),
+                            d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
+  Node cons_1_cons_2_nil = d_nodeManager->mkNode(
+      APPLY_CONSTRUCTOR,
+      cons,
+      d_nodeManager->mkConst(Rational(1)),
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
+                            cons,
+                            d_nodeManager->mkConst(Rational(2)),
+                            d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)));
+  ASSERT_TRUE(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst());
+  ASSERT_FALSE(cons_x_nil.isConst());
+  ASSERT_TRUE(cons_1_nil.isConst());
+  ASSERT_TRUE(cons_1_cons_2_nil.isConst());
+
+  TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+                                                d_nodeManager->integerType());
+  Node zero = d_nodeManager->mkConst(Rational(0));
+  Node one = d_nodeManager->mkConst(Rational(1));
+  Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
+  ASSERT_TRUE(storeAll.isConst());
+
+  Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
+  ASSERT_FALSE(arr.isConst());
+  arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
+  ASSERT_TRUE(arr.isConst());
+  Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
+  ASSERT_FALSE(arr2.isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
+  ASSERT_FALSE(arr2.isConst());
+
+  arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1),
+                                       d_nodeManager->mkBitVectorType(1));
+  zero = d_nodeManager->mkConst(BitVector(1, unsigned(0)));
+  one = d_nodeManager->mkConst(BitVector(1, unsigned(1)));
+  storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
+  ASSERT_TRUE(storeAll.isConst());
+
+  arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
+  ASSERT_FALSE(arr.isConst());
+  arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
+  ASSERT_TRUE(arr.isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
+  ASSERT_FALSE(arr2.isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr, one, one);
+  ASSERT_FALSE(arr2.isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
+  ASSERT_FALSE(arr2.isConst());
+}
+
+namespace {
+Node level0(NodeManager* nm)
+{
+  NodeBuilder<> nb(kind::AND);
+  Node x = nm->mkSkolem("x", nm->booleanType());
+  nb << x;
+  nb << x;
+  return Node(nb.constructNode());
+}
+TNode level1(NodeManager* nm) { return level0(nm); }
+}  // namespace
+
+/**
+ * This is for demonstrating what a certain type of user error looks like.
+ */
+TEST_F(TestNodeBlackNode, node_tnode_usage)
+{
+  Node n;
+  ASSERT_NO_FATAL_FAILURE(n = level0(d_nodeManager.get()));
+  ASSERT_DEATH(n = level1(d_nodeManager.get()), "d_nv->d_rc > 0");
+}
+
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp
new file mode 100644
index 000000000..7e38dd899
--- /dev/null
+++ b/test/unit/node/node_builder_black.cpp
@@ -0,0 +1,590 @@
+/*********************                                                        */
+/*! \file node_builder_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Tim King, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::NodeBuilder.
+ **
+ ** Black box testing of CVC4::NodeBuilder.
+ **/
+
+#include <limits.h>
+
+#include <sstream>
+#include <vector>
+
+#include "base/check.h"
+#include "expr/kind.h"
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_manager.h"
+#include "test_node.h"
+#include "util/rational.h"
+
+#define K 30u
+#define LARGE_K UINT_MAX / 40
+
+namespace CVC4 {
+
+using namespace kind;
+
+namespace test {
+
+class TestNodeBlackNodeBuilder : public TestNode
+{
+ protected:
+  template <unsigned N>
+  void push_back(NodeBuilder<N>& nb, uint32_t n)
+  {
+    for (uint32_t i = 0; i < n; ++i)
+    {
+      nb << d_nodeManager->mkConst(true);
+    }
+  }
+  Kind d_specKind = AND;
+};
+
+/** Tests just constructors. No modification is done to the node. */
+TEST_F(TestNodeBlackNodeBuilder, ctors)
+{
+  /* Default size tests. */
+  NodeBuilder<> def;
+  ASSERT_EQ(def.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(def.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(def.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(def.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+  NodeBuilder<> spec(d_specKind);
+  ASSERT_EQ(spec.getKind(), d_specKind);
+  ASSERT_EQ(spec.getNumChildren(), 0u);
+  ASSERT_EQ(spec.begin(), spec.end());
+
+  NodeBuilder<> from_nm(d_nodeManager.get());
+  ASSERT_EQ(from_nm.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(from_nm.getNumChildren(),
+               "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(from_nm.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(from_nm.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+  NodeBuilder<> from_nm_kind(d_nodeManager.get(), d_specKind);
+  ASSERT_EQ(from_nm_kind.getKind(), d_specKind);
+  ASSERT_EQ(from_nm_kind.getNumChildren(), 0u);
+  ASSERT_EQ(from_nm_kind.begin(), from_nm_kind.end());
+
+  /* Non-default size tests */
+  NodeBuilder<K> ws;
+  ASSERT_EQ(ws.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(ws.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(ws.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(ws.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+  NodeBuilder<K> ws_kind(d_specKind);
+  ASSERT_EQ(ws_kind.getKind(), d_specKind);
+  ASSERT_EQ(ws_kind.getNumChildren(), 0u);
+  ASSERT_EQ(ws_kind.begin(), ws_kind.end());
+
+  NodeBuilder<K> ws_from_nm(d_nodeManager.get());
+  ASSERT_EQ(ws_from_nm.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(ws_from_nm.getNumChildren(),
+               "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(ws_from_nm.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(ws_from_nm.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+  NodeBuilder<K> ws_from_nm_kind(d_nodeManager.get(), d_specKind);
+  ASSERT_EQ(ws_from_nm_kind.getKind(), d_specKind);
+  ASSERT_EQ(ws_from_nm_kind.getNumChildren(), 0u);
+  ASSERT_EQ(ws_from_nm_kind.begin(), ws_from_nm_kind.end());
+
+  /* Extreme size tests */
+  NodeBuilder<0> ws_size_0;
+
+  /* Allocating on the heap instead of the stack. */
+  NodeBuilder<LARGE_K>* ws_size_large = new NodeBuilder<LARGE_K>;
+  delete ws_size_large;
+
+  /* Copy constructors */
+  NodeBuilder<> copy(def);
+  ASSERT_EQ(copy.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(copy.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(copy.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(copy.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+  NodeBuilder<K> cp_ws(ws);
+  ASSERT_EQ(cp_ws.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(cp_ws.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(cp_ws.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(cp_ws.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+  NodeBuilder<K - 10> cp_from_larger(ws);
+  ASSERT_EQ(cp_from_larger.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(cp_from_larger.getNumChildren(),
+               "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(cp_from_larger.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(cp_from_larger.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+  NodeBuilder<K + 10> cp_from_smaller(ws);
+  ASSERT_EQ(cp_from_smaller.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(cp_from_smaller.getNumChildren(),
+               "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(cp_from_smaller.begin(),
+               "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(cp_from_smaller.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+}
+
+TEST_F(TestNodeBlackNodeBuilder, dtor)
+{
+  NodeBuilder<K>* nb = new NodeBuilder<K>();
+  delete nb;
+}
+
+TEST_F(TestNodeBlackNodeBuilder, begin_end)
+{
+  /* Test begin() and end() without resizing. */
+  NodeBuilder<K> ws(d_specKind);
+  ASSERT_EQ(ws.begin(), ws.end());
+
+  push_back(ws, K);
+  ASSERT_NE(ws.begin(), ws.end());
+
+  NodeBuilder<K>::iterator iter = ws.begin();
+  for (uint32_t i = 0; i < K; ++i)
+  {
+    ASSERT_NE(iter, ws.end());
+    ++iter;
+  }
+  ASSERT_EQ(iter, ws.end());
+
+  NodeBuilder<K>::const_iterator citer = ws.begin();
+  for (uint32_t i = 0; i < K; ++i)
+  {
+    ASSERT_NE(citer, ws.end());
+    ++citer;
+  }
+  ASSERT_EQ(citer, ws.end());
+
+  /* Repeat same tests and make sure that resizing occurs. */
+  NodeBuilder<> smaller(d_specKind);
+  ASSERT_EQ(smaller.begin(), smaller.end());
+
+  push_back(smaller, K);
+  ASSERT_NE(smaller.begin(), smaller.end());
+
+  NodeBuilder<>::iterator smaller_iter = smaller.begin();
+  for (uint32_t i = 0; i < K; ++i)
+  {
+    ASSERT_NE(smaller_iter, smaller.end());
+    ++smaller_iter;
+  }
+  ASSERT_EQ(iter, ws.end());
+
+  NodeBuilder<>::const_iterator smaller_citer = smaller.begin();
+  for (uint32_t i = 0; i < K; ++i)
+  {
+    ASSERT_NE(smaller_citer, smaller.end());
+    ++smaller_citer;
+  }
+  ASSERT_EQ(smaller_citer, smaller.end());
+}
+
+TEST_F(TestNodeBlackNodeBuilder, iterator)
+{
+  NodeBuilder<> b;
+  Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
+  Node y = d_nodeManager->mkSkolem("z", *d_boolTypeNode);
+  Node z = d_nodeManager->mkSkolem("y", *d_boolTypeNode);
+  b << x << y << z << AND;
+
+  {
+    NodeBuilder<>::iterator i = b.begin();
+    ASSERT_EQ(*i++, x);
+    ASSERT_EQ(*i++, y);
+    ASSERT_EQ(*i++, z);
+    ASSERT_EQ(i, b.end());
+  }
+
+  {
+    const NodeBuilder<>& c = b;
+    NodeBuilder<>::const_iterator i = c.begin();
+    ASSERT_EQ(*i++, x);
+    ASSERT_EQ(*i++, y);
+    ASSERT_EQ(*i++, z);
+    ASSERT_EQ(i, b.end());
+  }
+}
+
+TEST_F(TestNodeBlackNodeBuilder, getKind)
+{
+  NodeBuilder<> noKind;
+  ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
+
+  Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode));
+  noKind << x << x;
+  ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
+
+  noKind << PLUS;
+
+  ASSERT_EQ(noKind.getKind(), PLUS);
+
+  Node n = noKind;
+
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(noKind.getKind(), "!isUsed\\(\\)");
+#endif
+
+  NodeBuilder<> spec(PLUS);
+  ASSERT_EQ(spec.getKind(), PLUS);
+  spec << x << x;
+  ASSERT_EQ(spec.getKind(), PLUS);
+}
+
+TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
+{
+  Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode));
+
+  NodeBuilder<> nb;
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+  nb << PLUS << x << x;
+
+  ASSERT_EQ(nb.getNumChildren(), 2u);
+
+  nb << x << x;
+  ASSERT_EQ(nb.getNumChildren(), 4u);
+
+  nb.clear();
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+  nb.clear(PLUS);
+  ASSERT_EQ(nb.getNumChildren(), 0u);
+  nb << x << x << x;
+
+  ASSERT_EQ(nb.getNumChildren(), 3u);
+
+  nb << x << x << x;
+  ASSERT_EQ(nb.getNumChildren(), 6u);
+
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(nb << PLUS, "getKind\\(\\) == kind::UNDEFINED_KIND");
+  Node n = nb;
+  ASSERT_DEATH(nb.getNumChildren(), "!isUsed\\(\\)");
+#endif
+}
+
+TEST_F(TestNodeBlackNodeBuilder, operator_square)
+{
+  NodeBuilder<> arr(d_specKind);
+
+  Node i_0 = d_nodeManager->mkConst(false);
+  Node i_2 = d_nodeManager->mkConst(true);
+  Node i_K = d_nodeManager->mkNode(NOT, i_0);
+
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(arr[-1], "index out of range");
+  ASSERT_DEATH(arr[0], "index out of range");
+#endif
+
+  arr << i_0;
+
+  ASSERT_EQ(arr[0], i_0);
+
+  push_back(arr, 1);
+
+  arr << i_2;
+
+  ASSERT_EQ(arr[0], i_0);
+  ASSERT_EQ(arr[2], i_2);
+
+  push_back(arr, K - 3);
+
+  ASSERT_EQ(arr[0], i_0);
+  ASSERT_EQ(arr[2], i_2);
+  for (unsigned i = 3; i < K; ++i)
+  {
+    ASSERT_EQ(arr[i], d_nodeManager->mkConst(true));
+  }
+
+  arr << i_K;
+
+  ASSERT_EQ(arr[0], i_0);
+  ASSERT_EQ(arr[2], i_2);
+  for (unsigned i = 3; i < K; ++i)
+  {
+    ASSERT_EQ(arr[i], d_nodeManager->mkConst(true));
+  }
+  ASSERT_EQ(arr[K], i_K);
+
+#ifdef CVC4_ASSERTIONS
+  Node n = arr;
+  ASSERT_DEATH(arr[0], "!isUsed\\(\\)");
+#endif
+}
+
+TEST_F(TestNodeBlackNodeBuilder, clear)
+{
+  NodeBuilder<> nb;
+
+  ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+  nb << d_specKind;
+  push_back(nb, K);
+
+  ASSERT_EQ(nb.getKind(), d_specKind);
+  ASSERT_EQ(nb.getNumChildren(), K);
+  ASSERT_NE(nb.begin(), nb.end());
+
+  nb.clear();
+
+  ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+  nb << d_specKind;
+  push_back(nb, K);
+
+  ASSERT_EQ(nb.getKind(), d_specKind);
+  ASSERT_EQ(nb.getNumChildren(), K);
+  ASSERT_NE(nb.begin(), nb.end());
+
+  nb.clear(d_specKind);
+
+  ASSERT_EQ(nb.getKind(), d_specKind);
+  ASSERT_EQ(nb.getNumChildren(), 0u);
+  ASSERT_EQ(nb.begin(), nb.end());
+
+  push_back(nb, K);
+  nb.clear();
+
+  ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+  ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+}
+
+TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind)
+{
+#ifdef CVC4_ASSERTIONS
+  NodeBuilder<> spec(d_specKind);
+  ASSERT_DEATH(spec << PLUS, "can't redefine the Kind of a NodeBuilder");
+#endif
+
+  NodeBuilder<> noSpec;
+  noSpec << d_specKind;
+  ASSERT_EQ(noSpec.getKind(), d_specKind);
+
+  NodeBuilder<> modified;
+  push_back(modified, K);
+  modified << d_specKind;
+  ASSERT_EQ(modified.getKind(), d_specKind);
+
+  NodeBuilder<> nb(d_specKind);
+  nb << d_nodeManager->mkConst(true) << d_nodeManager->mkConst(false);
+  nb.clear(PLUS);
+
+#ifdef CVC4_ASSERTIONS
+  Node n;
+  ASSERT_DEATH(n = nb, "Nodes with kind PLUS must have at least 2 children");
+  nb.clear(PLUS);
+#endif
+
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(nb << PLUS, "can't redefine the Kind of a NodeBuilder");
+#endif
+
+  NodeBuilder<> testRef;
+  ASSERT_EQ((testRef << d_specKind).getKind(), d_specKind);
+
+#ifdef CVC4_ASSERTIONS
+  NodeBuilder<> testTwo;
+  ASSERT_DEATH(testTwo << d_specKind << PLUS,
+               "can't redefine the Kind of a NodeBuilder");
+#endif
+
+  NodeBuilder<> testMixOrder1;
+  ASSERT_EQ(
+      (testMixOrder1 << d_specKind << d_nodeManager->mkConst(true)).getKind(),
+      d_specKind);
+  NodeBuilder<> testMixOrder2;
+  ASSERT_EQ(
+      (testMixOrder2 << d_nodeManager->mkConst(true) << d_specKind).getKind(),
+      d_specKind);
+}
+
+TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_node)
+{
+  NodeBuilder<K> nb(d_specKind);
+  ASSERT_EQ(nb.getKind(), d_specKind);
+  ASSERT_EQ(nb.getNumChildren(), 0u);
+  ASSERT_EQ(nb.begin(), nb.end());
+  push_back(nb, K);
+  ASSERT_EQ(nb.getKind(), d_specKind);
+  ASSERT_EQ(nb.getNumChildren(), K);
+  ASSERT_NE(nb.begin(), nb.end());
+
+#ifdef CVC4_ASSERTIONS
+  Node n = nb;
+  ASSERT_DEATH(nb << n, "!isUsed\\(\\)");
+#endif
+
+  NodeBuilder<> overflow(d_specKind);
+  ASSERT_EQ(overflow.getKind(), d_specKind);
+  ASSERT_EQ(overflow.getNumChildren(), 0u);
+  ASSERT_EQ(overflow.begin(), overflow.end());
+
+  push_back(overflow, 5 * K + 1);
+
+  ASSERT_EQ(overflow.getKind(), d_specKind);
+  ASSERT_EQ(overflow.getNumChildren(), 5 * K + 1);
+  ASSERT_NE(overflow.begin(), overflow.end());
+}
+
+TEST_F(TestNodeBlackNodeBuilder, append)
+{
+  Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
+  Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode);
+  Node z = d_nodeManager->mkSkolem("z", *d_boolTypeNode);
+  Node m = d_nodeManager->mkNode(AND, y, z, x);
+  Node n = d_nodeManager->mkNode(OR, d_nodeManager->mkNode(NOT, x), y, z);
+  Node o = d_nodeManager->mkNode(XOR, y, x);
+
+  Node r = d_nodeManager->mkSkolem("r", *d_realTypeNode);
+  Node s = d_nodeManager->mkSkolem("s", *d_realTypeNode);
+  Node t = d_nodeManager->mkSkolem("t", *d_realTypeNode);
+
+  Node p = d_nodeManager->mkNode(
+      EQUAL,
+      d_nodeManager->mkConst<Rational>(0),
+      d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(UMINUS, s), t));
+  Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y));
+
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(d_nodeManager->mkNode(XOR, y, x, x),
+               "Nodes with kind XOR must have at most 2 children");
+#endif
+
+  NodeBuilder<> b(d_specKind);
+
+  /* test append(TNode) */
+  b.append(n).append(o).append(q);
+
+  ASSERT_EQ(b.getNumChildren(), 3);
+  ASSERT_EQ(b[0], n);
+  ASSERT_EQ(b[1], o);
+  ASSERT_EQ(b[2], q);
+
+  std::vector<Node> v;
+  v.push_back(m);
+  v.push_back(p);
+  v.push_back(q);
+
+  /* test append(vector<Node>) */
+  b.append(v);
+
+  ASSERT_EQ(b.getNumChildren(), 6);
+  ASSERT_EQ(b[0], n);
+  ASSERT_EQ(b[1], o);
+  ASSERT_EQ(b[2], q);
+  ASSERT_EQ(b[3], m);
+  ASSERT_EQ(b[4], p);
+  ASSERT_EQ(b[5], q);
+
+  /* test append(iterator, iterator) */
+  b.append(v.rbegin(), v.rend());
+
+  ASSERT_EQ(b.getNumChildren(), 9);
+  ASSERT_EQ(b[0], n);
+  ASSERT_EQ(b[1], o);
+  ASSERT_EQ(b[2], q);
+  ASSERT_EQ(b[3], m);
+  ASSERT_EQ(b[4], p);
+  ASSERT_EQ(b[5], q);
+  ASSERT_EQ(b[6], q);
+  ASSERT_EQ(b[7], p);
+  ASSERT_EQ(b[8], m);
+}
+
+TEST_F(TestNodeBlackNodeBuilder, operator_node_cast)
+{
+  NodeBuilder<K> implicit(d_specKind);
+  NodeBuilder<K> explic(d_specKind);
+
+  push_back(implicit, K);
+  push_back(explic, K);
+
+  Node nimpl = implicit;
+  Node nexplicit = (Node)explic;
+
+  ASSERT_EQ(nimpl.getKind(), d_specKind);
+  ASSERT_EQ(nimpl.getNumChildren(), K);
+
+  ASSERT_EQ(nexplicit.getKind(), d_specKind);
+  ASSERT_EQ(nexplicit.getNumChildren(), K);
+
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(Node blah = implicit, "!isUsed\\(\\)");
+#endif
+}
+
+TEST_F(TestNodeBlackNodeBuilder, leftist_building)
+{
+  NodeBuilder<> nb;
+
+  Node a = d_nodeManager->mkSkolem("a", *d_boolTypeNode);
+
+  Node b = d_nodeManager->mkSkolem("b", *d_boolTypeNode);
+  Node c = d_nodeManager->mkSkolem("c", *d_boolTypeNode);
+
+  Node d = d_nodeManager->mkSkolem("d", *d_realTypeNode);
+  Node e = d_nodeManager->mkSkolem("e", *d_realTypeNode);
+
+  nb << a << NOT << b << c << OR << c << a << AND << d << e << ITE;
+
+  Node n = nb;
+  ASSERT_EQ(n.getNumChildren(), 3u);
+  ASSERT_EQ(n.getType(), *d_realTypeNode);
+  ASSERT_EQ(n[0].getType(), *d_boolTypeNode);
+  ASSERT_EQ(n[1].getType(), *d_realTypeNode);
+  ASSERT_EQ(n[2].getType(), *d_realTypeNode);
+
+  Node nota = d_nodeManager->mkNode(NOT, a);
+  Node nota_or_b_or_c = d_nodeManager->mkNode(OR, nota, b, c);
+  Node n0 = d_nodeManager->mkNode(AND, nota_or_b_or_c, c, a);
+  Node nexpected = d_nodeManager->mkNode(ITE, n0, d, e);
+
+  ASSERT_EQ(nexpected, n);
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp
new file mode 100644
index 000000000..a2ede3ed0
--- /dev/null
+++ b/test/unit/node/node_manager_black.cpp
@@ -0,0 +1,333 @@
+/*********************                                                        */
+/*! \file node_manager_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Christopher L. Conway, Dejan Jovanovic
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::NodeManager.
+ **
+ ** Black box testing of CVC4::NodeManager.
+ **/
+
+#include <string>
+#include <vector>
+
+#include "base/output.h"
+#include "expr/node_manager.h"
+#include "expr/node_manager_attributes.h"
+#include "test_node.h"
+#include "util/integer.h"
+#include "util/rational.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace expr;
+
+namespace test {
+
+class TestNodeBlackNodeManager : public TestNode
+{
+};
+
+TEST_F(TestNodeBlackNodeManager, mkNode_not)
+{
+  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+  Node n = d_nodeManager->mkNode(NOT, x);
+  ASSERT_EQ(n.getNumChildren(), 1u);
+  ASSERT_EQ(n.getKind(), NOT);
+  ASSERT_EQ(n[0], x);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_binary)
+{
+  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+  Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
+  Node n = d_nodeManager->mkNode(IMPLIES, x, y);
+  ASSERT_EQ(n.getNumChildren(), 2u);
+  ASSERT_EQ(n.getKind(), IMPLIES);
+  ASSERT_EQ(n[0], x);
+  ASSERT_EQ(n[1], y);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_three_children)
+{
+  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+  Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
+  Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType());
+  Node n = d_nodeManager->mkNode(AND, x, y, z);
+  ASSERT_EQ(n.getNumChildren(), 3u);
+  ASSERT_EQ(n.getKind(), AND);
+  ASSERT_EQ(n[0], x);
+  ASSERT_EQ(n[1], y);
+  ASSERT_EQ(n[2], z);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_four_children)
+{
+  Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
+  Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
+  Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
+  Node x4 = d_nodeManager->mkSkolem("x4", d_nodeManager->booleanType());
+  Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4);
+  ASSERT_EQ(n.getNumChildren(), 4u);
+  ASSERT_EQ(n.getKind(), AND);
+  ASSERT_EQ(n[0], x1);
+  ASSERT_EQ(n[1], x2);
+  ASSERT_EQ(n[2], x3);
+  ASSERT_EQ(n[3], x4);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_five_children)
+{
+  Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
+  Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
+  Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
+  Node x4 = d_nodeManager->mkSkolem("x4", d_nodeManager->booleanType());
+  Node x5 = d_nodeManager->mkSkolem("x5", d_nodeManager->booleanType());
+  Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5);
+  ASSERT_EQ(n.getNumChildren(), 5u);
+  ASSERT_EQ(n.getKind(), AND);
+  ASSERT_EQ(n[0], x1);
+  ASSERT_EQ(n[1], x2);
+  ASSERT_EQ(n[2], x3);
+  ASSERT_EQ(n[3], x4);
+  ASSERT_EQ(n[4], x5);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node)
+{
+  Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
+  Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
+  Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
+  std::vector<Node> args;
+  args.push_back(x1);
+  args.push_back(x2);
+  args.push_back(x3);
+  Node n = d_nodeManager->mkNode(AND, args);
+  ASSERT_EQ(n.getNumChildren(), args.size());
+  ASSERT_EQ(n.getKind(), AND);
+  for (unsigned i = 0; i < args.size(); ++i)
+  {
+    ASSERT_EQ(n[i], args[i]);
+  }
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode)
+{
+  Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
+  Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
+  Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
+  std::vector<TNode> args;
+  args.push_back(x1);
+  args.push_back(x2);
+  args.push_back(x3);
+  Node n = d_nodeManager->mkNode(AND, args);
+  ASSERT_EQ(n.getNumChildren(), args.size());
+  ASSERT_EQ(n.getKind(), AND);
+  for (unsigned i = 0; i < args.size(); ++i)
+  {
+    ASSERT_EQ(n[i], args[i]);
+  }
+}
+
+TEST_F(TestNodeBlackNodeManager, mkSkolem_with_name)
+{
+  Node x = d_nodeManager->mkSkolem(
+      "x", *d_boolTypeNode, "", NodeManager::SKOLEM_EXACT_NAME);
+  ASSERT_EQ(x.getKind(), SKOLEM);
+  ASSERT_EQ(x.getNumChildren(), 0u);
+  ASSERT_EQ(x.getAttribute(VarNameAttr()), "x");
+  ASSERT_EQ(x.getType(), *d_boolTypeNode);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkConst_bool)
+{
+  Node tt = d_nodeManager->mkConst(true);
+  ASSERT_EQ(tt.getConst<bool>(), true);
+  Node ff = d_nodeManager->mkConst(false);
+  ASSERT_EQ(ff.getConst<bool>(), false);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkConst_rational)
+{
+  Rational r("3/2");
+  Node n = d_nodeManager->mkConst(r);
+  ASSERT_EQ(n.getConst<Rational>(), r);
+}
+
+TEST_F(TestNodeBlackNodeManager, hasOperator)
+{
+  ASSERT_TRUE(NodeManager::hasOperator(AND));
+  ASSERT_TRUE(NodeManager::hasOperator(OR));
+  ASSERT_TRUE(NodeManager::hasOperator(NOT));
+  ASSERT_TRUE(NodeManager::hasOperator(APPLY_UF));
+  ASSERT_TRUE(!NodeManager::hasOperator(VARIABLE));
+}
+
+TEST_F(TestNodeBlackNodeManager, booleanType)
+{
+  TypeNode t = d_nodeManager->booleanType();
+  TypeNode t2 = d_nodeManager->booleanType();
+  TypeNode t3 = d_nodeManager->mkSort("T");
+  ASSERT_TRUE(t.isBoolean());
+  ASSERT_FALSE(t.isFunction());
+  ASSERT_FALSE(t.isNull());
+  ASSERT_FALSE(t.isPredicate());
+  ASSERT_FALSE(t.isSort());
+  ASSERT_EQ(t, t2);
+  ASSERT_NE(t, t3);
+
+  TypeNode bt = t;
+  ASSERT_EQ(bt, t);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkFunctionType_bool_to_bool)
+{
+  TypeNode booleanType = d_nodeManager->booleanType();
+  TypeNode t = d_nodeManager->mkFunctionType(booleanType, booleanType);
+  TypeNode t2 = d_nodeManager->mkFunctionType(booleanType, booleanType);
+
+  ASSERT_FALSE(t.isBoolean());
+  ASSERT_TRUE(t.isFunction());
+  ASSERT_FALSE(t.isNull());
+  ASSERT_TRUE(t.isPredicate());
+  ASSERT_FALSE(t.isSort());
+
+  ASSERT_EQ(t, t2);
+
+  TypeNode ft = t;
+  ASSERT_EQ(ft, t);
+  ASSERT_EQ(ft.getArgTypes().size(), 1u);
+  ASSERT_EQ(ft.getArgTypes()[0], booleanType);
+  ASSERT_EQ(ft.getRangeType(), booleanType);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_args_with_return_type)
+{
+  TypeNode a = d_nodeManager->mkSort();
+  TypeNode b = d_nodeManager->mkSort();
+  TypeNode c = d_nodeManager->mkSort();
+
+  std::vector<TypeNode> argTypes;
+  argTypes.push_back(a);
+  argTypes.push_back(b);
+
+  TypeNode t = d_nodeManager->mkFunctionType(argTypes, c);
+  TypeNode t2 = d_nodeManager->mkFunctionType(argTypes, c);
+
+  ASSERT_FALSE(t.isBoolean());
+  ASSERT_TRUE(t.isFunction());
+  ASSERT_FALSE(t.isNull());
+  ASSERT_FALSE(t.isPredicate());
+  ASSERT_FALSE(t.isSort());
+
+  ASSERT_EQ(t, t2);
+
+  TypeNode ft = t;
+  ASSERT_EQ(ft, t);
+  ASSERT_EQ(ft.getArgTypes().size(), argTypes.size());
+  ASSERT_EQ(ft.getArgTypes()[0], a);
+  ASSERT_EQ(ft.getArgTypes()[1], b);
+  ASSERT_EQ(ft.getRangeType(), c);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_of_arguments)
+{
+  TypeNode a = d_nodeManager->mkSort();
+  TypeNode b = d_nodeManager->mkSort();
+  TypeNode c = d_nodeManager->mkSort();
+
+  std::vector<TypeNode> types;
+  types.push_back(a);
+  types.push_back(b);
+  types.push_back(c);
+
+  TypeNode t = d_nodeManager->mkFunctionType(types);
+  TypeNode t2 = d_nodeManager->mkFunctionType(types);
+
+  ASSERT_FALSE(t.isBoolean());
+  ASSERT_TRUE(t.isFunction());
+  ASSERT_FALSE(t.isNull());
+  ASSERT_FALSE(t.isPredicate());
+  ASSERT_FALSE(t.isSort());
+
+  ASSERT_EQ(t, t2);
+
+  TypeNode ft = t;
+  ASSERT_EQ(ft, t);
+  ASSERT_EQ(ft.getArgTypes().size(), types.size() - 1);
+  ASSERT_EQ(ft.getArgTypes()[0], a);
+  ASSERT_EQ(ft.getArgTypes()[1], b);
+  ASSERT_EQ(ft.getRangeType(), c);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkPredicateType)
+{
+  TypeNode a = d_nodeManager->mkSort("a");
+  TypeNode b = d_nodeManager->mkSort("b");
+  TypeNode c = d_nodeManager->mkSort("c");
+  TypeNode booleanType = d_nodeManager->booleanType();
+
+  std::vector<TypeNode> argTypes;
+  argTypes.push_back(a);
+  argTypes.push_back(b);
+  argTypes.push_back(c);
+
+  TypeNode t = d_nodeManager->mkPredicateType(argTypes);
+  TypeNode t2 = d_nodeManager->mkPredicateType(argTypes);
+
+  ASSERT_FALSE(t.isBoolean());
+  ASSERT_TRUE(t.isFunction());
+  ASSERT_FALSE(t.isNull());
+  ASSERT_TRUE(t.isPredicate());
+  ASSERT_FALSE(t.isSort());
+
+  ASSERT_EQ(t, t2);
+
+  TypeNode ft = t;
+  ASSERT_EQ(ft, t);
+  ASSERT_EQ(ft.getArgTypes().size(), argTypes.size());
+  ASSERT_EQ(ft.getArgTypes()[0], a);
+  ASSERT_EQ(ft.getArgTypes()[1], b);
+  ASSERT_EQ(ft.getArgTypes()[2], c);
+  ASSERT_EQ(ft.getRangeType(), booleanType);
+}
+
+/* This test is only valid if assertions are enabled. */
+TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children)
+{
+#ifdef CVC4_ASSERTIONS
+  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+  ASSERT_DEATH(d_nodeManager->mkNode(AND, x),
+               "Nodes with kind AND must have at least 2 children");
+#endif
+}
+
+/* This test is only valid if assertions are enabled. */
+TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children)
+{
+#ifdef CVC4_ASSERTIONS
+  std::vector<Node> vars;
+  const uint32_t max = metakind::getMaxArityForKind(AND);
+  TypeNode boolType = d_nodeManager->booleanType();
+  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);
+  }
+  ASSERT_DEATH(d_nodeManager->mkNode(AND, vars), "toSize > d_nvMaxChildren");
+#endif
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp
new file mode 100644
index 000000000..daf211b78
--- /dev/null
+++ b/test/unit/node/node_manager_white.cpp
@@ -0,0 +1,84 @@
+/*********************                                                        */
+/*! \file node_manager_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief White box testing of CVC4::NodeManager.
+ **
+ ** White box testing of CVC4::NodeManager.
+ **/
+
+#include <string>
+
+#include "expr/node_manager.h"
+#include "test_node.h"
+#include "util/integer.h"
+#include "util/rational.h"
+
+namespace CVC4 {
+
+using namespace CVC4::expr;
+
+namespace test {
+
+class TestNodeWhiteNodeManager : public TestNode
+{
+};
+
+TEST_F(TestNodeWhiteNodeManager, mkConst_rational)
+{
+  Rational i("3");
+  Node n = d_nodeManager->mkConst(i);
+  Node m = d_nodeManager->mkConst(i);
+  ASSERT_EQ(n.getId(), m.getId());
+}
+
+TEST_F(TestNodeWhiteNodeManager, oversized_node_builder)
+{
+  NodeBuilder<> nb;
+
+  ASSERT_NO_THROW(nb.realloc(15));
+  ASSERT_NO_THROW(nb.realloc(25));
+  ASSERT_NO_THROW(nb.realloc(256));
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(nb.realloc(100), "toSize > d_nvMaxChildren");
+#endif /* CVC4_ASSERTIONS */
+  ASSERT_NO_THROW(nb.realloc(257));
+  ASSERT_NO_THROW(nb.realloc(4000));
+  ASSERT_NO_THROW(nb.realloc(20000));
+  ASSERT_NO_THROW(nb.realloc(60000));
+  ASSERT_NO_THROW(nb.realloc(65535));
+  ASSERT_NO_THROW(nb.realloc(65536));
+  ASSERT_NO_THROW(nb.realloc(67108863));
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(nb.realloc(67108863), "toSize > d_nvMaxChildren");
+#endif /* CVC4_ASSERTIONS */
+}
+
+TEST_F(TestNodeWhiteNodeManager, topological_sort)
+{
+  TypeNode boolType = d_nodeManager->booleanType();
+  Node i = d_nodeManager->mkSkolem("i", boolType);
+  Node j = d_nodeManager->mkSkolem("j", boolType);
+  Node n1 = d_nodeManager->mkNode(kind::AND, j, j);
+  Node n2 = d_nodeManager->mkNode(kind::AND, i, n1);
+
+  {
+    std::vector<NodeValue*> roots = {n1.d_nv};
+    ASSERT_EQ(NodeManager::TopologicalSort(roots), roots);
+  }
+
+  {
+    std::vector<NodeValue*> roots = {n2.d_nv, n1.d_nv};
+    std::vector<NodeValue*> result = {n1.d_nv, n2.d_nv};
+    ASSERT_EQ(NodeManager::TopologicalSort(roots), result);
+  }
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/node/node_self_iterator_black.cpp b/test/unit/node/node_self_iterator_black.cpp
new file mode 100644
index 000000000..34ab5f09b
--- /dev/null
+++ b/test/unit/node/node_self_iterator_black.cpp
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file node_self_iterator_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Tim King, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::expr::NodeSelfIterator
+ **
+ ** Black box testing of CVC4::expr::NodeSelfIterator
+ **/
+
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_self_iterator.h"
+#include "test_node.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace expr;
+
+namespace test {
+
+class TestNodeBlackNodeSelfIterator : public TestNode
+{
+};
+
+TEST_F(TestNodeBlackNodeSelfIterator, iteration)
+{
+  Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
+  Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode);
+  Node x_and_y = x.andNode(y);
+  NodeSelfIterator i = x_and_y, j = NodeSelfIterator::self(x_and_y);
+  ASSERT_NE(i, x_and_y.end());
+  ASSERT_NE(j, x_and_y.end());
+  ASSERT_EQ(*i, x_and_y);
+  ASSERT_EQ(*j, x_and_y);
+  ASSERT_EQ(*i++, x_and_y);
+  ASSERT_EQ(*j++, x_and_y);
+  ASSERT_EQ(i, NodeSelfIterator::selfEnd(x_and_y));
+  ASSERT_EQ(j, NodeSelfIterator::selfEnd(x_and_y));
+  ASSERT_EQ(i, x_and_y.end());
+  ASSERT_EQ(j, x_and_y.end());
+
+  i = x_and_y.begin();
+  ASSERT_NE(i, x_and_y.end());
+  ASSERT_EQ(*i, x);
+  ASSERT_EQ(*++i, y);
+  ASSERT_EQ(++i, x_and_y.end());
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/node/node_traversal_black.cpp b/test/unit/node/node_traversal_black.cpp
new file mode 100644
index 000000000..e443ff685
--- /dev/null
+++ b/test/unit/node/node_traversal_black.cpp
@@ -0,0 +1,296 @@
+/*********************                                                        */
+/*! \file node_traversal_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Alex Ozdemir, Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of node traversal iterators.
+ **/
+
+#include <algorithm>
+#include <cstddef>
+#include <iterator>
+#include <sstream>
+#include <string>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_manager.h"
+#include "expr/node_traversal.h"
+#include "expr/node_value.h"
+#include "test_node.h"
+
+namespace CVC4 {
+
+using namespace kind;
+
+namespace test {
+
+class TestNodeBlackNodeTraversalPostorder : public TestNode
+{
+};
+
+class TestNodeBlackNodeTraversalPreorder : public TestNode
+{
+};
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, preincrement_iteration)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER);
+  NodeDfsIterator i = traversal.begin();
+  NodeDfsIterator end = traversal.end();
+  ASSERT_EQ(*i, tb);
+  ASSERT_FALSE(i == end);
+  ++i;
+  ASSERT_EQ(*i, eb);
+  ASSERT_FALSE(i == end);
+  ++i;
+  ASSERT_EQ(*i, cnd);
+  ASSERT_FALSE(i == end);
+  ++i;
+  ASSERT_TRUE(i == end);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, postincrement_iteration)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER);
+  NodeDfsIterator i = traversal.begin();
+  NodeDfsIterator end = traversal.end();
+  ASSERT_EQ(*(i++), tb);
+  ASSERT_EQ(*(i++), eb);
+  ASSERT_EQ(*(i++), cnd);
+  ASSERT_TRUE(i == end);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, postorder_is_default)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  auto traversal = NodeDfsIterable(cnd);
+  NodeDfsIterator i = traversal.begin();
+  NodeDfsIterator end = traversal.end();
+  ASSERT_EQ(*i, tb);
+  ASSERT_FALSE(i == end);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, range_for_loop)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  size_t count = 0;
+  for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER))
+  {
+    ++count;
+  }
+  ASSERT_EQ(count, 3);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, count_if_with_loop)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  size_t count = 0;
+  for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER))
+  {
+    if (i.isConst())
+    {
+      ++count;
+    }
+  }
+  ASSERT_EQ(count, 2);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, stl_count_if)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+  const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+
+  auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER);
+
+  size_t count = std::count_if(
+      traversal.begin(), traversal.end(), [](TNode n) { return n.isConst(); });
+  ASSERT_EQ(count, 2);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, stl_copy)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+  const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+  std::vector<TNode> expected = {tb, eb, cnd, top};
+
+  auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER);
+
+  std::vector<TNode> actual;
+  std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
+  ASSERT_EQ(actual, expected);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, skip_if)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+  const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+  std::vector<TNode> expected = {top};
+
+  auto traversal = NodeDfsIterable(
+      top, VisitOrder::POSTORDER, [&cnd](TNode n) { return n == cnd; });
+
+  std::vector<TNode> actual;
+  std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
+  ASSERT_EQ(actual, expected);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, skip_all)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+  const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+  std::vector<TNode> expected = {};
+
+  auto traversal =
+      NodeDfsIterable(top, VisitOrder::POSTORDER, [](TNode n) { return true; });
+
+  std::vector<TNode> actual;
+  std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
+  ASSERT_EQ(actual, expected);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, preincrement_iteration)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER);
+  NodeDfsIterator i = traversal.begin();
+  NodeDfsIterator end = traversal.end();
+  ASSERT_EQ(*i, cnd);
+  ASSERT_FALSE(i == end);
+  ++i;
+  ASSERT_EQ(*i, tb);
+  ASSERT_FALSE(i == end);
+  ++i;
+  ASSERT_EQ(*i, eb);
+  ASSERT_FALSE(i == end);
+  ++i;
+  ASSERT_TRUE(i == end);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, postincrement_iteration)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER);
+  NodeDfsIterator i = traversal.begin();
+  NodeDfsIterator end = traversal.end();
+  ASSERT_EQ(*(i++), cnd);
+  ASSERT_EQ(*(i++), tb);
+  ASSERT_EQ(*(i++), eb);
+  ASSERT_TRUE(i == end);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, range_for_loop)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  size_t count = 0;
+  for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER))
+  {
+    ++count;
+  }
+  ASSERT_EQ(count, 3);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, count_if_with_loop)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  size_t count = 0;
+  for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER))
+  {
+    if (i.isConst())
+    {
+      ++count;
+    }
+  }
+  ASSERT_EQ(count, 2);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, stl_count_if)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+  const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+
+  auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER);
+
+  size_t count = std::count_if(
+      traversal.begin(), traversal.end(), [](TNode n) { return n.isConst(); });
+  ASSERT_EQ(count, 2);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, stl_copy)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+  const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+  std::vector<TNode> expected = {top, cnd, tb, eb};
+
+  auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER);
+
+  std::vector<TNode> actual;
+  std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
+  ASSERT_EQ(actual, expected);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, skip_if)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+  const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+  std::vector<TNode> expected = {top, cnd, eb};
+
+  auto traversal = NodeDfsIterable(
+      top, VisitOrder::PREORDER, [&tb](TNode n) { return n == tb; });
+
+  std::vector<TNode> actual;
+  std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
+  ASSERT_EQ(actual, expected);
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp
new file mode 100644
index 000000000..651dd1990
--- /dev/null
+++ b/test/unit/node/node_white.cpp
@@ -0,0 +1,82 @@
+/*********************                                                        */
+/*! \file node_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief White box testing of CVC4::Node.
+ **
+ ** White box testing of CVC4::Node.
+ **/
+
+#include <string>
+
+#include "base/check.h"
+#include "test_node.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace expr;
+
+namespace test {
+
+class TestNodeWhiteNode : public TestNode
+{
+};
+
+TEST_F(TestNodeWhiteNode, null) { ASSERT_EQ(Node::null(), Node::s_null); }
+
+TEST_F(TestNodeWhiteNode, copy_ctor) { Node e(Node::s_null); }
+
+TEST_F(TestNodeWhiteNode, builder)
+{
+  NodeBuilder<> b;
+  ASSERT_TRUE(b.d_nv->getId() == 0);
+  ASSERT_TRUE(b.d_nv->getKind() == UNDEFINED_KIND);
+  ASSERT_EQ(b.d_nv->d_nchildren, 0u);
+  /* etc. */
+}
+
+TEST_F(TestNodeWhiteNode, iterators)
+{
+  Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType());
+  Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType());
+  Node x_plus_y = d_nodeManager->mkNode(PLUS, x, y);
+  Node two = d_nodeManager->mkConst(Rational(2));
+  Node x_times_2 = d_nodeManager->mkNode(MULT, x, two);
+
+  Node n = d_nodeManager->mkNode(PLUS, x_times_2, x_plus_y, y);
+
+  Node::iterator i;
+
+  i = std::find(n.begin(), n.end(), x_plus_y);
+  ASSERT_TRUE(i != n.end());
+  ASSERT_TRUE(*i == x_plus_y);
+
+  i = std::find(n.begin(), n.end(), x);
+  ASSERT_TRUE(i == n.end());
+
+  i = std::find(x_times_2.begin(), x_times_2.end(), two);
+  ASSERT_TRUE(i != x_times_2.end());
+  ASSERT_TRUE(*i == two);
+
+  i = std::find(n.begin(), n.end(), y);
+  ASSERT_TRUE(i != n.end());
+  ASSERT_TRUE(*i == y);
+
+  std::vector<Node> v;
+  copy(n.begin(), n.end(), back_inserter(v));
+  ASSERT_EQ(n.getNumChildren(), v.size());
+  ASSERT_EQ(3, v.size());
+  ASSERT_EQ(v[0], x_times_2);
+  ASSERT_EQ(v[1], x_plus_y);
+  ASSERT_EQ(v[2], y);
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/node/symbol_table_black.cpp b/test/unit/node/symbol_table_black.cpp
new file mode 100644
index 000000000..c1865eaa9
--- /dev/null
+++ b/test/unit/node/symbol_table_black.cpp
@@ -0,0 +1,149 @@
+/*********************                                                        */
+/*! \file symbol_table_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Morgan Deters, Christopher L. Conway
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::SymbolTable
+ **
+ ** Black box testing of CVC4::SymbolTable.
+ **/
+
+#include <sstream>
+#include <string>
+
+#include "base/check.h"
+#include "base/exception.h"
+#include "context/context.h"
+#include "expr/kind.h"
+#include "expr/symbol_table.h"
+#include "test_api.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace context;
+
+namespace test {
+
+class TestNodeBlackSymbolTable : public TestApi
+{
+};
+
+TEST_F(TestNodeBlackSymbolTable, bind1)
+{
+  SymbolTable symtab;
+  api::Sort booleanType = d_solver.getBooleanSort();
+  api::Term x = d_solver.mkConst(booleanType);
+  symtab.bind("x", x);
+  ASSERT_TRUE(symtab.isBound("x"));
+  ASSERT_EQ(symtab.lookup("x"), x);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind2)
+{
+  SymbolTable symtab;
+  api::Sort booleanType = d_solver.getBooleanSort();
+  // var name attribute shouldn't matter
+  api::Term y = d_solver.mkConst(booleanType, "y");
+  symtab.bind("x", y);
+  ASSERT_TRUE(symtab.isBound("x"));
+  ASSERT_EQ(symtab.lookup("x"), y);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind3)
+{
+  SymbolTable symtab;
+  api::Sort booleanType = d_solver.getBooleanSort();
+  api::Term x = d_solver.mkConst(booleanType);
+  symtab.bind("x", x);
+  api::Term y = d_solver.mkConst(booleanType);
+  // new binding covers old
+  symtab.bind("x", y);
+  ASSERT_TRUE(symtab.isBound("x"));
+  ASSERT_EQ(symtab.lookup("x"), y);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind4)
+{
+  SymbolTable symtab;
+  api::Sort booleanType = d_solver.getBooleanSort();
+  api::Term x = d_solver.mkConst(booleanType);
+  symtab.bind("x", x);
+
+  api::Sort t = d_solver.mkUninterpretedSort("T");
+  // duplicate binding for type is OK
+  symtab.bindType("x", t);
+
+  ASSERT_TRUE(symtab.isBound("x"));
+  ASSERT_EQ(symtab.lookup("x"), x);
+  ASSERT_TRUE(symtab.isBoundType("x"));
+  ASSERT_EQ(symtab.lookupType("x"), t);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind_type1)
+{
+  SymbolTable symtab;
+  api::Sort s = d_solver.mkUninterpretedSort("S");
+  symtab.bindType("S", s);
+  ASSERT_TRUE(symtab.isBoundType("S"));
+  ASSERT_EQ(symtab.lookupType("S"), s);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind_type2)
+{
+  SymbolTable symtab;
+  // type name attribute shouldn't matter
+  api::Sort s = d_solver.mkUninterpretedSort("S");
+  symtab.bindType("T", s);
+  ASSERT_TRUE(symtab.isBoundType("T"));
+  ASSERT_EQ(symtab.lookupType("T"), s);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind_type3)
+{
+  SymbolTable symtab;
+  api::Sort s = d_solver.mkUninterpretedSort("S");
+  symtab.bindType("S", s);
+  api::Sort t = d_solver.mkUninterpretedSort("T");
+  // new binding covers old
+  symtab.bindType("S", t);
+  ASSERT_TRUE(symtab.isBoundType("S"));
+  ASSERT_EQ(symtab.lookupType("S"), t);
+}
+
+TEST_F(TestNodeBlackSymbolTable, push_scope)
+{
+  SymbolTable symtab;
+  api::Sort booleanType = d_solver.getBooleanSort();
+  api::Term x = d_solver.mkConst(booleanType);
+  symtab.bind("x", x);
+  symtab.pushScope();
+
+  ASSERT_TRUE(symtab.isBound("x"));
+  ASSERT_EQ(symtab.lookup("x"), x);
+
+  api::Term y = d_solver.mkConst(booleanType);
+  symtab.bind("x", y);
+
+  ASSERT_TRUE(symtab.isBound("x"));
+  ASSERT_EQ(symtab.lookup("x"), y);
+
+  symtab.popScope();
+  ASSERT_TRUE(symtab.isBound("x"));
+  ASSERT_EQ(symtab.lookup("x"), x);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bad_pop)
+{
+  SymbolTable symtab;
+  ASSERT_THROW(symtab.popScope(), ScopeException);
+}
+
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/node/type_cardinality_black.cpp b/test/unit/node/type_cardinality_black.cpp
new file mode 100644
index 000000000..55936df0d
--- /dev/null
+++ b/test/unit/node/type_cardinality_black.cpp
@@ -0,0 +1,335 @@
+/*********************                                                        */
+/*! \file type_cardinality_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Public box testing of Type::getCardinality() for various Types
+ **
+ ** Public box testing of Type::getCardinality() for various Types.
+ **/
+
+#include <string>
+
+#include "expr/kind.h"
+#include "expr/node_manager.h"
+#include "test_node.h"
+#include "util/cardinality.h"
+
+namespace CVC4 {
+
+using namespace kind;
+
+namespace test {
+
+class TestNodeBlackTypeCardinality : public TestNode
+{
+};
+
+TEST_F(TestNodeBlackTypeCardinality, basics)
+{
+  ASSERT_EQ(d_nodeManager->booleanType().getCardinality().compare(2),
+            Cardinality::EQUAL);
+  ASSERT_EQ(d_nodeManager->integerType().getCardinality().compare(
+                Cardinality::INTEGERS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(
+      d_nodeManager->realType().getCardinality().compare(Cardinality::REALS),
+      Cardinality::EQUAL);
+}
+
+TEST_F(TestNodeBlackTypeCardinality, arrays)
+{
+  TypeNode intToInt = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+                                                 d_nodeManager->integerType());
+  TypeNode realToReal = d_nodeManager->mkArrayType(d_nodeManager->realType(),
+                                                   d_nodeManager->realType());
+  TypeNode realToInt = d_nodeManager->mkArrayType(d_nodeManager->realType(),
+                                                  d_nodeManager->integerType());
+  TypeNode intToReal = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+                                                  d_nodeManager->realType());
+  TypeNode intToBool = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+                                                  d_nodeManager->booleanType());
+  TypeNode realToBool = d_nodeManager->mkArrayType(
+      d_nodeManager->realType(), d_nodeManager->booleanType());
+  TypeNode boolToReal = d_nodeManager->mkArrayType(d_nodeManager->booleanType(),
+                                                   d_nodeManager->realType());
+  TypeNode boolToInt = d_nodeManager->mkArrayType(d_nodeManager->booleanType(),
+                                                  d_nodeManager->integerType());
+  TypeNode boolToBool = d_nodeManager->mkArrayType(
+      d_nodeManager->booleanType(), d_nodeManager->booleanType());
+
+  ASSERT_EQ(intToInt.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(realToReal.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+  ASSERT_EQ(realToInt.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+  ASSERT_EQ(intToReal.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(intToBool.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(realToBool.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+  ASSERT_EQ(boolToReal.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(boolToInt.getCardinality().compare(Cardinality::INTEGERS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(boolToBool.getCardinality().compare(4), Cardinality::EQUAL);
+}
+
+TEST_F(TestNodeBlackTypeCardinality, unary_functions)
+{
+  TypeNode intToInt = d_nodeManager->mkFunctionType(
+      d_nodeManager->integerType(), d_nodeManager->integerType());
+  TypeNode realToReal = d_nodeManager->mkFunctionType(
+      d_nodeManager->realType(), d_nodeManager->realType());
+  TypeNode realToInt = d_nodeManager->mkFunctionType(
+      d_nodeManager->realType(), d_nodeManager->integerType());
+  TypeNode intToReal = d_nodeManager->mkFunctionType(
+      d_nodeManager->integerType(), d_nodeManager->realType());
+  TypeNode intToBool = d_nodeManager->mkFunctionType(
+      d_nodeManager->integerType(), d_nodeManager->booleanType());
+  TypeNode realToBool = d_nodeManager->mkFunctionType(
+      d_nodeManager->realType(), d_nodeManager->booleanType());
+  TypeNode boolToReal = d_nodeManager->mkFunctionType(
+      d_nodeManager->booleanType(), d_nodeManager->realType());
+  TypeNode boolToInt = d_nodeManager->mkFunctionType(
+      d_nodeManager->booleanType(), d_nodeManager->integerType());
+  TypeNode boolToBool = d_nodeManager->mkFunctionType(
+      d_nodeManager->booleanType(), d_nodeManager->booleanType());
+
+  ASSERT_EQ(intToInt.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(realToReal.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+  ASSERT_EQ(realToInt.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+  ASSERT_EQ(intToReal.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(intToBool.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(realToBool.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+  ASSERT_EQ(boolToReal.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(boolToInt.getCardinality().compare(Cardinality::INTEGERS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(boolToBool.getCardinality().compare(4), Cardinality::EQUAL);
+}
+
+TEST_F(TestNodeBlackTypeCardinality, binary_functions)
+{
+  std::vector<TypeNode> boolbool;
+  boolbool.push_back(d_nodeManager->booleanType());
+  boolbool.push_back(d_nodeManager->booleanType());
+  std::vector<TypeNode> boolint;
+  boolint.push_back(d_nodeManager->booleanType());
+  boolint.push_back(d_nodeManager->integerType());
+  std::vector<TypeNode> intbool;
+  intbool.push_back(d_nodeManager->integerType());
+  intbool.push_back(d_nodeManager->booleanType());
+  std::vector<TypeNode> intint;
+  intint.push_back(d_nodeManager->integerType());
+  intint.push_back(d_nodeManager->integerType());
+  std::vector<TypeNode> intreal;
+  intreal.push_back(d_nodeManager->integerType());
+  intreal.push_back(d_nodeManager->realType());
+  std::vector<TypeNode> realint;
+  realint.push_back(d_nodeManager->realType());
+  realint.push_back(d_nodeManager->integerType());
+  std::vector<TypeNode> realreal;
+  realreal.push_back(d_nodeManager->realType());
+  realreal.push_back(d_nodeManager->realType());
+  std::vector<TypeNode> realbool;
+  realbool.push_back(d_nodeManager->realType());
+  realbool.push_back(d_nodeManager->booleanType());
+  std::vector<TypeNode> boolreal;
+  boolreal.push_back(d_nodeManager->booleanType());
+  boolreal.push_back(d_nodeManager->realType());
+
+  TypeNode boolboolToBool =
+      d_nodeManager->mkFunctionType(boolbool, d_nodeManager->booleanType());
+  TypeNode boolboolToInt =
+      d_nodeManager->mkFunctionType(boolbool, d_nodeManager->integerType());
+  TypeNode boolboolToReal =
+      d_nodeManager->mkFunctionType(boolbool, d_nodeManager->realType());
+
+  TypeNode boolintToBool =
+      d_nodeManager->mkFunctionType(boolint, d_nodeManager->booleanType());
+  TypeNode boolintToInt =
+      d_nodeManager->mkFunctionType(boolint, d_nodeManager->integerType());
+  TypeNode boolintToReal =
+      d_nodeManager->mkFunctionType(boolint, d_nodeManager->realType());
+
+  TypeNode intboolToBool =
+      d_nodeManager->mkFunctionType(intbool, d_nodeManager->booleanType());
+  TypeNode intboolToInt =
+      d_nodeManager->mkFunctionType(intbool, d_nodeManager->integerType());
+  TypeNode intboolToReal =
+      d_nodeManager->mkFunctionType(intbool, d_nodeManager->realType());
+
+  TypeNode intintToBool =
+      d_nodeManager->mkFunctionType(intint, d_nodeManager->booleanType());
+  TypeNode intintToInt =
+      d_nodeManager->mkFunctionType(intint, d_nodeManager->integerType());
+  TypeNode intintToReal =
+      d_nodeManager->mkFunctionType(intint, d_nodeManager->realType());
+
+  TypeNode intrealToBool =
+      d_nodeManager->mkFunctionType(intreal, d_nodeManager->booleanType());
+  TypeNode intrealToInt =
+      d_nodeManager->mkFunctionType(intreal, d_nodeManager->integerType());
+  TypeNode intrealToReal =
+      d_nodeManager->mkFunctionType(intreal, d_nodeManager->realType());
+
+  TypeNode realintToBool =
+      d_nodeManager->mkFunctionType(realint, d_nodeManager->booleanType());
+  TypeNode realintToInt =
+      d_nodeManager->mkFunctionType(realint, d_nodeManager->integerType());
+  TypeNode realintToReal =
+      d_nodeManager->mkFunctionType(realint, d_nodeManager->realType());
+
+  TypeNode realrealToBool =
+      d_nodeManager->mkFunctionType(realreal, d_nodeManager->booleanType());
+  TypeNode realrealToInt =
+      d_nodeManager->mkFunctionType(realreal, d_nodeManager->integerType());
+  TypeNode realrealToReal =
+      d_nodeManager->mkFunctionType(realreal, d_nodeManager->realType());
+
+  TypeNode realboolToBool =
+      d_nodeManager->mkFunctionType(realbool, d_nodeManager->booleanType());
+  TypeNode realboolToInt =
+      d_nodeManager->mkFunctionType(realbool, d_nodeManager->integerType());
+  TypeNode realboolToReal =
+      d_nodeManager->mkFunctionType(realbool, d_nodeManager->realType());
+
+  TypeNode boolrealToBool =
+      d_nodeManager->mkFunctionType(boolreal, d_nodeManager->booleanType());
+  TypeNode boolrealToInt =
+      d_nodeManager->mkFunctionType(boolreal, d_nodeManager->integerType());
+  TypeNode boolrealToReal =
+      d_nodeManager->mkFunctionType(boolreal, d_nodeManager->realType());
+
+  ASSERT_EQ(boolboolToBool.getCardinality().compare(16), Cardinality::EQUAL);
+  ASSERT_EQ(boolboolToInt.getCardinality().compare(Cardinality::INTEGERS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(boolboolToReal.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+
+  ASSERT_EQ(boolintToBool.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(boolintToInt.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(boolintToReal.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+
+  ASSERT_EQ(intboolToBool.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(intboolToInt.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(intboolToReal.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+
+  ASSERT_EQ(intintToBool.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(intintToInt.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+  ASSERT_EQ(intintToReal.getCardinality().compare(Cardinality::REALS),
+            Cardinality::EQUAL);
+
+  ASSERT_EQ(intrealToBool.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+  ASSERT_EQ(intrealToInt.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+  ASSERT_EQ(intrealToReal.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+
+  ASSERT_EQ(realintToBool.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+  ASSERT_EQ(realintToInt.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+  ASSERT_EQ(realintToReal.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+
+  ASSERT_EQ(realrealToBool.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+  ASSERT_EQ(realrealToInt.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+  ASSERT_EQ(realrealToReal.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+
+  ASSERT_EQ(realboolToBool.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+  ASSERT_EQ(realboolToInt.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+  ASSERT_EQ(realboolToReal.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+
+  ASSERT_EQ(boolrealToBool.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+  ASSERT_EQ(boolrealToInt.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+  ASSERT_EQ(boolrealToReal.getCardinality().compare(Cardinality::REALS),
+            Cardinality::GREATER);
+}
+
+TEST_F(TestNodeBlackTypeCardinality, ternary_functions)
+{
+  std::vector<TypeNode> boolbool;
+  boolbool.push_back(d_nodeManager->booleanType());
+  boolbool.push_back(d_nodeManager->booleanType());
+  std::vector<TypeNode> boolboolbool = boolbool;
+  boolboolbool.push_back(d_nodeManager->booleanType());
+
+  TypeNode boolboolTuple = d_nodeManager->mkTupleType(boolbool);
+  TypeNode boolboolboolTuple = d_nodeManager->mkTupleType(boolboolbool);
+
+  TypeNode boolboolboolToBool =
+      d_nodeManager->mkFunctionType(boolboolbool, d_nodeManager->booleanType());
+  TypeNode boolboolToBoolbool =
+      d_nodeManager->mkFunctionType(boolbool, boolboolTuple);
+  TypeNode boolToBoolboolbool = d_nodeManager->mkFunctionType(
+      d_nodeManager->booleanType(), boolboolboolTuple);
+
+  ASSERT_EQ(boolboolboolToBool.getCardinality().compare(/* 2 ^ 8 */ 1 << 8),
+            Cardinality::EQUAL);
+  ASSERT_EQ(
+      boolboolToBoolbool.getCardinality().compare(/* 4 ^ 4 */ 4 * 4 * 4 * 4),
+      Cardinality::EQUAL);
+  ASSERT_EQ(boolToBoolboolbool.getCardinality().compare(/* 8 ^ 2 */ 8 * 8),
+            Cardinality::EQUAL);
+}
+
+TEST_F(TestNodeBlackTypeCardinality, undefined_sorts)
+{
+  TypeNode foo = d_nodeManager->mkSort("foo", NodeManager::SORT_FLAG_NONE);
+  // We've currently assigned them a specific Beth number, which
+  // isn't really correct, but...
+  ASSERT_FALSE(foo.getCardinality().isFinite());
+}
+
+TEST_F(TestNodeBlackTypeCardinality, bitvectors)
+{
+  ASSERT_EQ(d_nodeManager->mkBitVectorType(0).getCardinality().compare(0),
+            Cardinality::EQUAL);
+  Cardinality lastCard = 0;
+  for (unsigned i = 1; i <= 65; ++i)
+  {
+    Cardinality card = Cardinality(2) ^ i;
+    Cardinality typeCard = d_nodeManager->mkBitVectorType(i).getCardinality();
+    ASSERT_TRUE(typeCard.compare(lastCard) == Cardinality::GREATER
+                || (typeCard.isLargeFinite() && lastCard.isLargeFinite()));
+    ASSERT_TRUE(typeCard.compare(card) == Cardinality::EQUAL
+                || typeCard.isLargeFinite());
+    lastCard = typeCard;
+  }
+}
+
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp
new file mode 100644
index 000000000..f364e40fc
--- /dev/null
+++ b/test/unit/node/type_node_white.cpp
@@ -0,0 +1,97 @@
+/*********************                                                        */
+/*! \file type_node_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief White box testing of TypeNode
+ **
+ ** White box testing of TypeNode.
+ **/
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#include "expr/node_manager.h"
+#include "expr/type_node.h"
+#include "smt/smt_engine.h"
+#include "test_node.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace context;
+
+namespace test {
+
+class TestNodeWhiteTypeNode : public TestNode
+{
+ protected:
+  void SetUp() override
+  {
+    TestNode::SetUp();
+    d_smt.reset(new SmtEngine(d_nodeManager.get()));
+  }
+  std::unique_ptr<SmtEngine> d_smt;
+};
+
+TEST_F(TestNodeWhiteTypeNode, sub_types)
+{
+  TypeNode realType = d_nodeManager->realType();
+  TypeNode integerType = d_nodeManager->realType();
+  TypeNode booleanType = d_nodeManager->booleanType();
+  TypeNode arrayType = d_nodeManager->mkArrayType(realType, integerType);
+  TypeNode bvType = d_nodeManager->mkBitVectorType(32);
+
+  Node x = d_nodeManager->mkBoundVar("x", realType);
+  Node xPos = d_nodeManager->mkNode(GT, x, d_nodeManager->mkConst(Rational(0)));
+  TypeNode funtype = d_nodeManager->mkFunctionType(integerType, booleanType);
+  Node lambda = d_nodeManager->mkVar("lambda", funtype);
+  std::vector<Node> formals;
+  formals.push_back(x);
+  d_smt->defineFunction(lambda, formals, xPos);
+
+  ASSERT_FALSE(realType.isComparableTo(booleanType));
+  ASSERT_TRUE(realType.isComparableTo(integerType));
+  ASSERT_TRUE(realType.isComparableTo(realType));
+  ASSERT_FALSE(realType.isComparableTo(arrayType));
+  ASSERT_FALSE(realType.isComparableTo(bvType));
+
+  ASSERT_FALSE(booleanType.isComparableTo(integerType));
+  ASSERT_FALSE(booleanType.isComparableTo(realType));
+  ASSERT_TRUE(booleanType.isComparableTo(booleanType));
+  ASSERT_FALSE(booleanType.isComparableTo(arrayType));
+  ASSERT_FALSE(booleanType.isComparableTo(bvType));
+
+  ASSERT_TRUE(integerType.isComparableTo(realType));
+  ASSERT_TRUE(integerType.isComparableTo(integerType));
+  ASSERT_FALSE(integerType.isComparableTo(booleanType));
+  ASSERT_FALSE(integerType.isComparableTo(arrayType));
+  ASSERT_FALSE(integerType.isComparableTo(bvType));
+
+  ASSERT_FALSE(arrayType.isComparableTo(booleanType));
+  ASSERT_FALSE(arrayType.isComparableTo(integerType));
+  ASSERT_FALSE(arrayType.isComparableTo(realType));
+  ASSERT_TRUE(arrayType.isComparableTo(arrayType));
+  ASSERT_FALSE(arrayType.isComparableTo(bvType));
+
+  ASSERT_FALSE(bvType.isComparableTo(booleanType));
+  ASSERT_FALSE(bvType.isComparableTo(integerType));
+  ASSERT_FALSE(bvType.isComparableTo(realType));
+  ASSERT_FALSE(bvType.isComparableTo(arrayType));
+  ASSERT_TRUE(bvType.isComparableTo(bvType));
+
+  ASSERT_TRUE(realType.getBaseType() == realType);
+  ASSERT_TRUE(integerType.getBaseType() == realType);
+  ASSERT_TRUE(booleanType.getBaseType() == booleanType);
+  ASSERT_TRUE(arrayType.getBaseType() == arrayType);
+  ASSERT_TRUE(bvType.getBaseType() == bvType);
+}
+}  // namespace test
+}  // namespace CVC4