google test: expr: Migrate node_builder_black. (#5855)

4 files changed, 595 insertions, 629 deletions

diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
index aa7e06ef0..442b2c7d3 100644
--- a/test/unit/expr/CMakeLists.txt
+++ b/test/unit/expr/CMakeLists.txt
@@ -17,7 +17,7 @@ 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_cxx_unit_test_black(node_builder_black expr)
+cvc4_add_unit_test_black(node_builder_black expr)
 cvc4_add_cxx_unit_test_black(node_manager_black expr)
 cvc4_add_cxx_unit_test_white(node_manager_white expr)
 cvc4_add_cxx_unit_test_black(node_self_iterator_black expr)
diff --git a/test/unit/expr/node_builder_black.cpp b/test/unit/expr/node_builder_black.cpp
new file mode 100644
index 000000000..3ba78950b
--- /dev/null
+++ b/test/unit/expr/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-2020 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 CVC4::kind;
+
+namespace test {
+
+class TestNodeBuilderBlackNode : public TestNodeBlack
+{
+ 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(TestNodeBuilderBlackNode, 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(TestNodeBuilderBlackNode, dtor)
+{
+  NodeBuilder<K>* nb = new NodeBuilder<K>();
+  delete nb;
+}
+
+TEST_F(TestNodeBuilderBlackNode, 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(TestNodeBuilderBlackNode, 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(TestNodeBuilderBlackNode, 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(TestNodeBuilderBlackNode, 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(TestNodeBuilderBlackNode, 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(TestNodeBuilderBlackNode, 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(TestNodeBuilderBlackNode, 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(TestNodeBuilderBlackNode, 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(TestNodeBuilderBlackNode, 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(TestNodeBuilderBlackNode, 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(TestNodeBuilderBlackNode, 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/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
deleted file mode 100644
index 6c8fec461..000000000
--- a/test/unit/expr/node_builder_black.h
+++ /dev/null
@@ -1,626 +0,0 @@
-/*********************                                                        */
-/*! \file node_builder_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 <cxxtest/TestSuite.h>
-
-#include <vector>
-#include <limits.h>
-#include <sstream>
-
-#include "base/check.h"
-#include "expr/kind.h"
-#include "expr/node.h"
-#include "expr/node_builder.h"
-#include "expr/node_manager.h"
-#include "test_utils.h"
-#include "util/rational.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace std;
-
-class NodeBuilderBlack : public CxxTest::TestSuite {
-private:
-
-  NodeManager* d_nm;
-  NodeManagerScope* d_scope;
-  TypeNode* d_booleanType;
-  TypeNode* d_integerType;
-  TypeNode* d_realType;
-
- public:
-  void setUp() override
-  {
-    d_nm = new NodeManager(NULL);
-    d_scope = new NodeManagerScope(d_nm);
-
-    specKind = AND;
-    d_integerType = new TypeNode(d_nm->integerType());
-    d_booleanType = new TypeNode(d_nm->booleanType());
-    d_realType = new TypeNode(d_nm->realType());
-  }
-
-  void tearDown() override
-  {
-    delete d_integerType;
-    delete d_booleanType;
-    delete d_realType;
-    delete d_scope;
-    delete d_nm;
-  }
-
-
-  template <unsigned N>
-  void push_back(NodeBuilder<N>& nb, int n){
-    for(int i = 0; i < n; ++i){
-      nb << d_nm->mkConst(true);
-    }
-  }
-
-#define K 30u
-#define LARGE_K UINT_MAX / 40
-
-  Kind specKind;
-
-  /**
-   * Tests just constructors. No modification is done to the node.
-   */
-  void testNodeConstructors() {
-
-    //inline NodeBuilder();
-    //inline NodeBuilder(Kind k);
-    //inline NodeBuilder(const NodeBuilder<nchild_thresh>& nb);
-    //template <unsigned N> inline NodeBuilder(const NodeBuilder<N>& nb);
-    //inline NodeBuilder(NodeManager* nm);
-    //inline NodeBuilder(NodeManager* nm, Kind k);
-
-    /* default size tests */
-    NodeBuilder<> def;
-    TS_ASSERT_EQUALS(def.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(def.getNumChildren());
-    TS_UTILS_EXPECT_ABORT(def.begin());
-    TS_UTILS_EXPECT_ABORT(def.end());
-#endif /* CVC4_ASSERTIONS */
-
-    NodeBuilder<> spec(specKind);
-    TS_ASSERT_EQUALS(spec.getKind(), specKind);
-    TS_ASSERT_EQUALS(spec.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(spec.begin(), spec.end());
-
-
-    NodeBuilder<> from_nm(d_nm);
-    TS_ASSERT_EQUALS(from_nm.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(from_nm.getNumChildren());
-    TS_UTILS_EXPECT_ABORT(from_nm.begin());
-    TS_UTILS_EXPECT_ABORT(from_nm.end());
-#endif /* CVC4_ASSERTIONS */
-
-    NodeBuilder<> from_nm_kind(d_nm, specKind);
-    TS_ASSERT_EQUALS(from_nm_kind.getKind(), specKind);
-    TS_ASSERT_EQUALS(from_nm_kind.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(from_nm_kind.begin(), from_nm_kind.end());
-
-
-    /* Non-default size tests */
-
-    NodeBuilder<K> ws;
-    TS_ASSERT_EQUALS(ws.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(ws.getNumChildren());
-    TS_UTILS_EXPECT_ABORT(ws.begin());
-    TS_UTILS_EXPECT_ABORT(ws.end());
-#endif /* CVC4_ASSERTIONS */
-
-    NodeBuilder<K> ws_kind(specKind);
-    TS_ASSERT_EQUALS(ws_kind.getKind(), specKind);
-    TS_ASSERT_EQUALS(ws_kind.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(ws_kind.begin(), ws_kind.end());
-
-
-    NodeBuilder<K> ws_from_nm(d_nm);
-    TS_ASSERT_EQUALS(ws_from_nm.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(ws_from_nm.getNumChildren());
-    TS_UTILS_EXPECT_ABORT(ws_from_nm.begin());
-    TS_UTILS_EXPECT_ABORT(ws_from_nm.end());
-#endif /* CVC4_ASSERTIONS */
-
-    NodeBuilder<K> ws_from_nm_kind(d_nm, specKind);
-    TS_ASSERT_EQUALS(ws_from_nm_kind.getKind(), specKind);
-    TS_ASSERT_EQUALS(ws_from_nm_kind.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(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;
-
-    /* CopyConstructors */
-
-    NodeBuilder<> copy(def);
-    TS_ASSERT_EQUALS(copy.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(copy.getNumChildren());
-    TS_UTILS_EXPECT_ABORT(copy.begin());
-    TS_UTILS_EXPECT_ABORT(copy.end());
-#endif /* CVC4_ASSERTIONS */
-
-    NodeBuilder<K> cp_ws(ws);
-    TS_ASSERT_EQUALS(cp_ws.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(cp_ws.getNumChildren());
-    TS_UTILS_EXPECT_ABORT(cp_ws.begin());
-    TS_UTILS_EXPECT_ABORT(cp_ws.end());
-#endif /* CVC4_ASSERTIONS */
-
-    NodeBuilder<K-10> cp_from_larger(ws);
-    TS_ASSERT_EQUALS(cp_from_larger.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(cp_from_larger.getNumChildren());
-    TS_UTILS_EXPECT_ABORT(cp_from_larger.begin());
-    TS_UTILS_EXPECT_ABORT(cp_from_larger.end());
-#endif /* CVC4_ASSERTIONS */
-
-    NodeBuilder<K+10> cp_from_smaller(ws);
-    TS_ASSERT_EQUALS(cp_from_smaller.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(cp_from_smaller.getNumChildren());
-    TS_UTILS_EXPECT_ABORT(cp_from_smaller.begin());
-    TS_UTILS_EXPECT_ABORT(cp_from_smaller.end());
-#endif /* CVC4_ASSERTIONS */
-  }
-
-  void testDestructor() {
-    //inline ~NodeBuilder();
-    NodeBuilder<K>* nb = new NodeBuilder<K>();
-    delete nb;
-    //Not sure what to test other than survival
-  }
-
-  void testBeginEnd() {
-    /* Test begin and ends without resizing */
-    NodeBuilder<K> ws(specKind);
-    TS_ASSERT_EQUALS(ws.begin(), ws.end());
-
-    push_back(ws, K);
-    TS_ASSERT_DIFFERS(ws.begin(), ws.end());
-
-    NodeBuilder<K>::iterator iter = ws.begin();
-    for(unsigned i = 0; i < K; ++i){
-      TS_ASSERT_DIFFERS(iter, ws.end());
-      ++iter;
-    }
-    TS_ASSERT_EQUALS(iter, ws.end());
-
-    NodeBuilder<K>::const_iterator citer = ws.begin();
-    for(unsigned i = 0; i < K; ++i){
-      TS_ASSERT_DIFFERS(citer, ws.end());
-      ++citer;
-    }
-    TS_ASSERT_EQUALS(citer, ws.end());
-
-    /* Do the same tests and make sure that resizing occurs */
-
-    NodeBuilder<> smaller(specKind);
-    TS_ASSERT_EQUALS(smaller.begin(), smaller.end());
-
-    push_back(smaller, K);
-    TS_ASSERT_DIFFERS(smaller.begin(), smaller.end());
-
-    NodeBuilder<>::iterator smaller_iter = smaller.begin();
-    for(unsigned i = 0; i < K; ++i){
-      TS_ASSERT_DIFFERS(smaller_iter, smaller.end());
-      ++smaller_iter;
-    }
-    TS_ASSERT_EQUALS(iter, ws.end());
-
-    NodeBuilder<>::const_iterator smaller_citer = smaller.begin();
-    for(unsigned i = 0; i < K; ++i){
-      TS_ASSERT_DIFFERS(smaller_citer, smaller.end());
-      ++smaller_citer;
-    }
-    TS_ASSERT_EQUALS(smaller_citer, smaller.end());
-  }
-
-  void testIterator() {
-    NodeBuilder<> b;
-    Node x = d_nm->mkSkolem("x", *d_booleanType);
-    Node y = d_nm->mkSkolem("z", *d_booleanType);
-    Node z = d_nm->mkSkolem("y", *d_booleanType);
-    b << x << y << z << AND;
-
-    {
-      NodeBuilder<>::iterator i = b.begin();
-      TS_ASSERT(*i++ == x);
-      TS_ASSERT(*i++ == y);
-      TS_ASSERT(*i++ == z);
-      TS_ASSERT(i == b.end());
-    }
-
-    {
-      const NodeBuilder<>& c = b;
-      NodeBuilder<>::const_iterator i = c.begin();
-      TS_ASSERT(*i++ == x);
-      TS_ASSERT(*i++ == y);
-      TS_ASSERT(*i++ == z);
-      TS_ASSERT(i == b.end());
-    }
-  }
-
-  void testGetKind() {
-    /*  Kind getKind() const; */
-    NodeBuilder<> noKind;
-    TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND);
-
-    Node x( d_nm->mkSkolem( "x", *d_integerType ) );
-    noKind << x << x;
-    //     push_back(noKind, K);
-    TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND);
-
-    noKind << PLUS;
-
-    TS_ASSERT_EQUALS(noKind.getKind(), PLUS);
-
-    Node n = noKind;
-
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(noKind.getKind());
-#endif /* CVC4_ASSERTIONS */
-
-    NodeBuilder<> spec(PLUS);
-    TS_ASSERT_EQUALS(spec.getKind(), PLUS);
-    spec << x << x ;
-    TS_ASSERT_EQUALS(spec.getKind(), PLUS);
-  }
-
-  void testGetNumChildren() {
-    /* unsigned getNumChildren() const; */
-    Node x( d_nm->mkSkolem( "x", *d_integerType ) );
-
-    NodeBuilder<> nb;
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(nb.getNumChildren());
-#endif /* CVC4_ASSERTIONS */
-    nb << PLUS << x << x;
-
-    TS_ASSERT_EQUALS(nb.getNumChildren(), 2u);
-
-    nb << x << x;
-    TS_ASSERT_EQUALS(nb.getNumChildren(), 4u);
-
-    Node n = nb;// avoid warning on clear()
-    nb.clear();
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(nb.getNumChildren());
-#endif /* CVC4_ASSERTIONS */
-    nb.clear(PLUS);
-    TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
-    nb << x << x << x;
-
-    TS_ASSERT_EQUALS(nb.getNumChildren(), 3u);
-
-    nb << x << x << x;
-    TS_ASSERT_EQUALS(nb.getNumChildren(), 6u);
-
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(nb << PLUS);
-    n = nb;
-    TS_UTILS_EXPECT_ABORT(nb.getNumChildren());
-#endif /* CVC4_ASSERTIONS */
-  }
-
-  void testOperatorSquare() {
-    /*
-      Node operator[](int i) const {
-      TS_ASSERT(i >= 0 && i < d_ev->getNumChildren());
-      return Node(d_ev->d_children[i]);
-      }
-    */
-    NodeBuilder<> arr(specKind);
-
-    Node i_0 = d_nm->mkConst(false);
-    Node i_2 = d_nm->mkConst(true);
-    Node i_K = d_nm->mkNode(NOT, i_0);
-
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(arr[-1]);
-    TS_UTILS_EXPECT_ABORT(arr[0]);
-#endif /* CVC4_ASSERTIONS */
-
-    arr << i_0;
-
-    TS_ASSERT_EQUALS(arr[0], i_0);
-
-    push_back(arr,1);
-
-    arr << i_2;
-
-    TS_ASSERT_EQUALS(arr[0], i_0);
-    TS_ASSERT_EQUALS(arr[2], i_2);
-
-    push_back(arr, K - 3);
-
-    TS_ASSERT_EQUALS(arr[0], i_0);
-    TS_ASSERT_EQUALS(arr[2], i_2);
-    for(unsigned i = 3; i < K; ++i) {
-      TS_ASSERT_EQUALS(arr[i], d_nm->mkConst(true));
-    }
-
-    arr << i_K;
-
-    TS_ASSERT_EQUALS(arr[0], i_0);
-    TS_ASSERT_EQUALS(arr[2], i_2);
-    for(unsigned i = 3; i < K; ++i) {
-      TS_ASSERT_EQUALS(arr[i], d_nm->mkConst(true));
-    }
-    TS_ASSERT_EQUALS(arr[K], i_K);
-
-#ifdef CVC4_ASSERTIONS
-    Node n = arr;
-    TS_UTILS_EXPECT_ABORT(arr[0]);
-#endif /* CVC4_ASSERTIONS */
-  }
-
-  void testClear() {
-    /* void clear(Kind k = UNDEFINED_KIND); */
-    NodeBuilder<> nb;
-
-    TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(nb.getNumChildren());
-    TS_UTILS_EXPECT_ABORT(nb.begin());
-    TS_UTILS_EXPECT_ABORT(nb.end());
-#endif /* CVC4_ASSERTIONS */
-
-    nb << specKind;
-    push_back(nb, K);
-
-    TS_ASSERT_EQUALS(nb.getKind(), specKind);
-    TS_ASSERT_EQUALS(nb.getNumChildren(), K);
-    TS_ASSERT_DIFFERS(nb.begin(), nb.end());
-
-    Node n = nb;// avoid warning on clear()
-    nb.clear();
-
-    TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(nb.getNumChildren());
-    TS_UTILS_EXPECT_ABORT(nb.begin());
-    TS_UTILS_EXPECT_ABORT(nb.end());
-#endif /* CVC4_ASSERTIONS */
-
-    nb << specKind;
-    push_back(nb, K);
-
-    TS_ASSERT_EQUALS(nb.getKind(), specKind);
-    TS_ASSERT_EQUALS(nb.getNumChildren(), K);
-    TS_ASSERT_DIFFERS(nb.begin(), nb.end());
-
-    n = nb;// avoid warning on clear()
-    nb.clear(specKind);
-
-    TS_ASSERT_EQUALS(nb.getKind(), specKind);
-    TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(nb.begin(), nb.end());
-
-    push_back(nb, K);
-    n = nb;// avoid warning on clear()
-    nb.clear();
-
-    TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(nb.getNumChildren());
-    TS_UTILS_EXPECT_ABORT(nb.begin());
-    TS_UTILS_EXPECT_ABORT(nb.end());
-#endif /* CVC4_ASSERTIONS */
-  }
-
-  void testStreamInsertionKind() {
-    /* NodeBuilder& operator<<(const Kind& k); */
-
-#ifdef CVC4_ASSERTIONS
-    NodeBuilder<> spec(specKind);
-    TS_UTILS_EXPECT_ABORT(spec << PLUS);
-#endif /* CVC4_ASSERTIONS */
-
-    NodeBuilder<> noSpec;
-    noSpec << specKind;
-    TS_ASSERT_EQUALS(noSpec.getKind(), specKind);
-
-
-    NodeBuilder<> modified;
-    push_back(modified, K);
-    modified << specKind;
-    TS_ASSERT_EQUALS(modified.getKind(), specKind);
-
-    NodeBuilder<> nb(specKind);
-    nb << d_nm->mkConst(true) << d_nm->mkConst(false);
-    Node n = nb;// avoid warning on clear()
-    nb.clear(PLUS);
-
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(n = nb);
-    nb.clear(PLUS);
-#endif /* CVC4_ASSERTIONS */
-
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(nb << PLUS);
-#endif /* CVC4_ASSERTIONS */
-
-    NodeBuilder<> testRef;
-    TS_ASSERT_EQUALS((testRef << specKind).getKind(), specKind);
-
-#ifdef CVC4_ASSERTIONS
-    NodeBuilder<> testTwo;
-    TS_UTILS_EXPECT_ABORT(testTwo << specKind << PLUS);
-#endif /* CVC4_ASSERTIONS */
-
-    NodeBuilder<> testMixOrder1;
-    TS_ASSERT_EQUALS((testMixOrder1 << specKind << d_nm->mkConst(true)).getKind(),
-                     specKind);
-    NodeBuilder<> testMixOrder2;
-    TS_ASSERT_EQUALS((testMixOrder2 << d_nm->mkConst(true) << specKind).getKind(),
-                     specKind);
-  }
-
-  void testStreamInsertionNode() {
-    /* NodeBuilder& operator<<(const Node& n); */
-    NodeBuilder<K> nb(specKind);
-    TS_ASSERT_EQUALS(nb.getKind(), specKind);
-    TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(nb.begin(), nb.end());
-    push_back(nb,K);
-    TS_ASSERT_EQUALS(nb.getKind(), specKind);
-    TS_ASSERT_EQUALS(nb.getNumChildren(), K);
-    TS_ASSERT_DIFFERS(nb.begin(), nb.end());
-
-#ifdef CVC4_ASSERTIONS
-    Node n = nb;
-    TS_UTILS_EXPECT_ABORT(nb << n);
-#endif /* CVC4_ASSERTIONS */
-
-    NodeBuilder<> overflow(specKind);
-    TS_ASSERT_EQUALS(overflow.getKind(), specKind);
-    TS_ASSERT_EQUALS(overflow.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(overflow.begin(), overflow.end());
-
-    push_back(overflow,5*K+1);
-
-    TS_ASSERT_EQUALS(overflow.getKind(), specKind);
-    TS_ASSERT_EQUALS(overflow.getNumChildren(), 5 * K + 1);
-    TS_ASSERT_DIFFERS(overflow.begin(), overflow.end());
-
-  }
-
-  void testAppend() {
-    Node x = d_nm->mkSkolem("x", *d_booleanType);
-    Node y = d_nm->mkSkolem("y", *d_booleanType);
-    Node z = d_nm->mkSkolem("z", *d_booleanType);
-    Node m = d_nm->mkNode(AND, y, z, x);
-    Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z);
-    Node o = d_nm->mkNode(XOR, y, x);
-
-    Node r = d_nm->mkSkolem("r", *d_realType);
-    Node s = d_nm->mkSkolem("s", *d_realType);
-    Node t = d_nm->mkSkolem("t", *d_realType);
-
-    Node p = d_nm->mkNode(EQUAL, d_nm->mkConst<Rational>(0),
-                          d_nm->mkNode(PLUS, r, d_nm->mkNode(UMINUS, s), t));
-    Node q = d_nm->mkNode(AND, x, z, d_nm->mkNode(NOT, y));
-
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(d_nm->mkNode(XOR, y, x, x));
-#endif /* CVC4_ASSERTIONS */
-
-    NodeBuilder<> b(specKind);
-
-    // test append(TNode)
-    b.append(n).append(o).append(q);
-
-    TS_ASSERT(b.getNumChildren() == 3);
-    TS_ASSERT(b[0] == n);
-    TS_ASSERT(b[1] == o);
-    TS_ASSERT(b[2] == q);
-
-    vector<Node> v;
-    v.push_back(m);
-    v.push_back(p);
-    v.push_back(q);
-    // test append(vector<Node>)
-    b.append(v);
-
-    TS_ASSERT(b.getNumChildren() == 6);
-    TS_ASSERT(b[0] == n);
-    TS_ASSERT(b[1] == o);
-    TS_ASSERT(b[2] == q);
-    TS_ASSERT(b[3] == m);
-    TS_ASSERT(b[4] == p);
-    TS_ASSERT(b[5] == q);
-
-    // test append(iterator, iterator)
-    b.append(v.rbegin(), v.rend());
-
-    TS_ASSERT(b.getNumChildren() == 9);
-    TS_ASSERT(b[0] == n);
-    TS_ASSERT(b[1] == o);
-    TS_ASSERT(b[2] == q);
-    TS_ASSERT(b[3] == m);
-    TS_ASSERT(b[4] == p);
-    TS_ASSERT(b[5] == q);
-    TS_ASSERT(b[6] == q);
-    TS_ASSERT(b[7] == p);
-    TS_ASSERT(b[8] == m);
-  }
-
-  void testOperatorNodeCast() {
-    /* operator Node();*/
-    NodeBuilder<K> implicit(specKind);
-    NodeBuilder<K> explic(specKind);
-
-    push_back(implicit, K);
-    push_back(explic, K);
-
-    Node nimpl = implicit;
-    Node nexplicit = (Node) explic;
-
-    TS_ASSERT_EQUALS(nimpl.getKind(), specKind);
-    TS_ASSERT_EQUALS(nimpl.getNumChildren(), K);
-
-    TS_ASSERT_EQUALS(nexplicit.getKind(), specKind);
-    TS_ASSERT_EQUALS(nexplicit.getNumChildren(), K);
-
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(Node blah = implicit);
-#endif /* CVC4_ASSERTIONS */
-  }
-
-  void testLeftistBuilding() {
-    NodeBuilder<> nb;
-
-    Node a = d_nm->mkSkolem("a", *d_booleanType);
-
-    Node b = d_nm->mkSkolem("b", *d_booleanType);
-    Node c = d_nm->mkSkolem("c", *d_booleanType);
-
-    Node d = d_nm->mkSkolem("d", *d_realType);
-    Node e = d_nm->mkSkolem("e", *d_realType);
-
-    nb << a << NOT
-       << b << c << OR
-       << c << a << AND
-       << d << e << ITE;
-
-    Node n = nb;
-    TS_ASSERT_EQUALS(n.getNumChildren(), 3u);
-    TS_ASSERT_EQUALS(n.getType(), *d_realType);
-    TS_ASSERT_EQUALS(n[0].getType(), *d_booleanType);
-    TS_ASSERT_EQUALS(n[1].getType(), *d_realType);
-    TS_ASSERT_EQUALS(n[2].getType(), *d_realType);
-
-    Node nota = d_nm->mkNode(NOT, a);
-    Node nota_or_b_or_c = d_nm->mkNode(OR, nota, b, c);
-    Node n0 = d_nm->mkNode(AND, nota_or_b_or_c, c, a);
-    Node nexpected = d_nm->mkNode(ITE, n0, d, e);
-
-    TS_ASSERT_EQUALS(nexpected, n);
-  }
-};
diff --git a/test/unit/test_node.h b/test/unit/test_node.h
index 774c9e4d0..3f2bfcc32 100644
--- a/test/unit/test_node.h
+++ b/test/unit/test_node.h
@@ -31,16 +31,18 @@ class TestNodeBlack : public TestInternal
   {
     d_nodeManager.reset(new NodeManager(nullptr));
     d_scope.reset(new NodeManagerScope(d_nodeManager.get()));
-    d_intTypeNode.reset(new TypeNode(d_nodeManager->integerType()));
     d_boolTypeNode.reset(new TypeNode(d_nodeManager->booleanType()));
     d_bvTypeNode.reset(new TypeNode(d_nodeManager->mkBitVectorType(2)));
+    d_intTypeNode.reset(new TypeNode(d_nodeManager->integerType()));
+    d_realTypeNode.reset(new TypeNode(d_nodeManager->realType()));
   }
 
   std::unique_ptr<NodeManagerScope> d_scope;
   std::unique_ptr<NodeManager> d_nodeManager;
-  std::unique_ptr<TypeNode> d_intTypeNode;
   std::unique_ptr<TypeNode> d_boolTypeNode;
   std::unique_ptr<TypeNode> d_bvTypeNode;
+  std::unique_ptr<TypeNode> d_intTypeNode;
+  std::unique_ptr<TypeNode> d_realTypeNode;
 };
 
 }  // namespace test