From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 2 Dec 2020 21:55:19 +0000 (-0800)
Subject: google test: api: Migrate term_black. (#5571)
X-Git-Tag: cvc5-1.0.0~2519
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e2c0a2d6a4627ac750f56004175eb24975aeaab7;p=cvc5.git

google test: api: Migrate term_black. (#5571)
---

diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 59d914931..c6c682365 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -17,5 +17,4 @@ cvc4_add_unit_test_black(op_black api)
 cvc4_add_unit_test_black(result_black api)
 cvc4_add_cxx_unit_test_black(solver_black api)
 cvc4_add_cxx_unit_test_black(sort_black api)
-cvc4_add_cxx_unit_test_black(term_black api)
-
+cvc4_add_unit_test_black(term_black api)
\ No newline at end of file
diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
new file mode 100644
index 000000000..71e1c7f6f
--- /dev/null
+++ b/test/unit/api/term_black.cpp
@@ -0,0 +1,768 @@
+/*********************                                                        */
+/*! \file term_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Andrew Reynolds, Makai Mann
+ ** 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 the Term class
+ **/
+
+#include "test_api.h"
+
+using namespace CVC4::api;
+
+class TestApiTermBlack : public TestApi
+{
+};
+
+TEST_F(TestApiTermBlack, eq)
+{
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  Term x = d_solver.mkVar(uSort, "x");
+  Term y = d_solver.mkVar(uSort, "y");
+  Term z;
+
+  ASSERT_TRUE(x == x);
+  ASSERT_FALSE(x != x);
+  ASSERT_FALSE(x == y);
+  ASSERT_TRUE(x != y);
+  ASSERT_FALSE((x == z));
+  ASSERT_TRUE(x != z);
+}
+
+TEST_F(TestApiTermBlack, getId)
+{
+  Term n;
+  ASSERT_THROW(n.getId(), CVC4ApiException);
+  Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x");
+  ASSERT_NO_THROW(x.getId());
+  Term y = x;
+  EXPECT_EQ(x.getId(), y.getId());
+
+  Term z = d_solver.mkVar(d_solver.getIntegerSort(), "z");
+  EXPECT_NE(x.getId(), z.getId());
+}
+
+TEST_F(TestApiTermBlack, getKind)
+{
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(uSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term n;
+  ASSERT_THROW(n.getKind(), CVC4ApiException);
+  Term x = d_solver.mkVar(uSort, "x");
+  ASSERT_NO_THROW(x.getKind());
+  Term y = d_solver.mkVar(uSort, "y");
+  ASSERT_NO_THROW(y.getKind());
+
+  Term f = d_solver.mkVar(funSort1, "f");
+  ASSERT_NO_THROW(f.getKind());
+  Term p = d_solver.mkVar(funSort2, "p");
+  ASSERT_NO_THROW(p.getKind());
+
+  Term zero = d_solver.mkInteger(0);
+  ASSERT_NO_THROW(zero.getKind());
+
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  ASSERT_NO_THROW(f_x.getKind());
+  Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
+  ASSERT_NO_THROW(f_y.getKind());
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+  ASSERT_NO_THROW(sum.getKind());
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  ASSERT_NO_THROW(p_0.getKind());
+  Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
+  ASSERT_NO_THROW(p_f_y.getKind());
+
+  // Sequence kinds do not exist internally, test that the API properly
+  // converts them back.
+  Sort seqSort = d_solver.mkSequenceSort(intSort);
+  Term s = d_solver.mkConst(seqSort, "s");
+  Term ss = d_solver.mkTerm(SEQ_CONCAT, s, s);
+  EXPECT_EQ(ss.getKind(), SEQ_CONCAT);
+}
+
+TEST_F(TestApiTermBlack, getSort)
+{
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term n;
+  ASSERT_THROW(n.getSort(), CVC4ApiException);
+  Term x = d_solver.mkVar(bvSort, "x");
+  ASSERT_NO_THROW(x.getSort());
+  EXPECT_EQ(x.getSort(), bvSort);
+  Term y = d_solver.mkVar(bvSort, "y");
+  ASSERT_NO_THROW(y.getSort());
+  EXPECT_EQ(y.getSort(), bvSort);
+
+  Term f = d_solver.mkVar(funSort1, "f");
+  ASSERT_NO_THROW(f.getSort());
+  EXPECT_EQ(f.getSort(), funSort1);
+  Term p = d_solver.mkVar(funSort2, "p");
+  ASSERT_NO_THROW(p.getSort());
+  EXPECT_EQ(p.getSort(), funSort2);
+
+  Term zero = d_solver.mkInteger(0);
+  ASSERT_NO_THROW(zero.getSort());
+  EXPECT_EQ(zero.getSort(), intSort);
+
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  ASSERT_NO_THROW(f_x.getSort());
+  EXPECT_EQ(f_x.getSort(), intSort);
+  Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
+  ASSERT_NO_THROW(f_y.getSort());
+  EXPECT_EQ(f_y.getSort(), intSort);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+  ASSERT_NO_THROW(sum.getSort());
+  EXPECT_EQ(sum.getSort(), intSort);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  ASSERT_NO_THROW(p_0.getSort());
+  EXPECT_EQ(p_0.getSort(), boolSort);
+  Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
+  ASSERT_NO_THROW(p_f_y.getSort());
+  EXPECT_EQ(p_f_y.getSort(), boolSort);
+}
+
+TEST_F(TestApiTermBlack, getOp)
+{
+  Sort intsort = d_solver.getIntegerSort();
+  Sort bvsort = d_solver.mkBitVectorSort(8);
+  Sort arrsort = d_solver.mkArraySort(bvsort, intsort);
+  Sort funsort = d_solver.mkFunctionSort(intsort, bvsort);
+
+  Term x = d_solver.mkConst(intsort, "x");
+  Term a = d_solver.mkConst(arrsort, "a");
+  Term b = d_solver.mkConst(bvsort, "b");
+
+  ASSERT_FALSE(x.hasOp());
+  ASSERT_THROW(x.getOp(), CVC4ApiException);
+
+  Term ab = d_solver.mkTerm(SELECT, a, b);
+  Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
+  Term extb = d_solver.mkTerm(ext, b);
+
+  ASSERT_TRUE(ab.hasOp());
+  EXPECT_EQ(ab.getOp(), Op(&d_solver, SELECT));
+  ASSERT_FALSE(ab.getOp().isIndexed());
+  // can compare directly to a Kind (will invoke Op constructor)
+  EXPECT_EQ(ab.getOp(), Op(&d_solver, SELECT));
+  ASSERT_TRUE(extb.hasOp());
+  ASSERT_TRUE(extb.getOp().isIndexed());
+  EXPECT_EQ(extb.getOp(), ext);
+
+  Term f = d_solver.mkConst(funsort, "f");
+  Term fx = d_solver.mkTerm(APPLY_UF, f, x);
+
+  ASSERT_FALSE(f.hasOp());
+  ASSERT_THROW(f.getOp(), CVC4ApiException);
+  ASSERT_TRUE(fx.hasOp());
+  EXPECT_EQ(fx.getOp(), Op(&d_solver, APPLY_UF));
+  std::vector<Term> children(fx.begin(), fx.end());
+  // testing rebuild from op and children
+  EXPECT_EQ(fx, d_solver.mkTerm(fx.getOp(), children));
+
+  // Test Datatypes Ops
+  Sort sort = d_solver.mkParamSort("T");
+  DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+  cons.addSelector("head", sort);
+  cons.addSelectorSelf("tail");
+  listDecl.addConstructor(cons);
+  listDecl.addConstructor(nil);
+  Sort listSort = d_solver.mkDatatypeSort(listDecl);
+  Sort intListSort =
+      listSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()});
+  Term c = d_solver.mkConst(intListSort, "c");
+  Datatype list = listSort.getDatatype();
+  // list datatype constructor and selector operator terms
+  Term consOpTerm = list.getConstructorTerm("cons");
+  Term nilOpTerm = list.getConstructorTerm("nil");
+  Term headOpTerm = list["cons"].getSelectorTerm("head");
+  Term tailOpTerm = list["cons"].getSelectorTerm("tail");
+
+  Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm);
+  Term consTerm = d_solver.mkTerm(
+      APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkInteger(0), nilTerm);
+  Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm);
+  Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm);
+
+  ASSERT_TRUE(nilTerm.hasOp());
+  ASSERT_TRUE(consTerm.hasOp());
+  ASSERT_TRUE(headTerm.hasOp());
+  ASSERT_TRUE(tailTerm.hasOp());
+
+  EXPECT_EQ(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+  EXPECT_EQ(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+  EXPECT_EQ(headTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
+  EXPECT_EQ(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
+
+  // Test rebuilding
+  children.clear();
+  children.insert(children.begin(), headTerm.begin(), headTerm.end());
+  EXPECT_EQ(headTerm, d_solver.mkTerm(headTerm.getOp(), children));
+}
+
+TEST_F(TestApiTermBlack, isNull)
+{
+  Term x;
+  ASSERT_TRUE(x.isNull());
+  x = d_solver.mkVar(d_solver.mkBitVectorSort(4), "x");
+  ASSERT_FALSE(x.isNull());
+}
+
+TEST_F(TestApiTermBlack, notTerm)
+{
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  ASSERT_THROW(Term().notTerm(), CVC4ApiException);
+  Term b = d_solver.mkTrue();
+  ASSERT_NO_THROW(b.notTerm());
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
+  ASSERT_THROW(x.notTerm(), CVC4ApiException);
+  Term f = d_solver.mkVar(funSort1, "f");
+  ASSERT_THROW(f.notTerm(), CVC4ApiException);
+  Term p = d_solver.mkVar(funSort2, "p");
+  ASSERT_THROW(p.notTerm(), CVC4ApiException);
+  Term zero = d_solver.mkInteger(0);
+  ASSERT_THROW(zero.notTerm(), CVC4ApiException);
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  ASSERT_THROW(f_x.notTerm(), CVC4ApiException);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+  ASSERT_THROW(sum.notTerm(), CVC4ApiException);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  ASSERT_NO_THROW(p_0.notTerm());
+  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+  ASSERT_NO_THROW(p_f_x.notTerm());
+}
+
+TEST_F(TestApiTermBlack, andTerm)
+{
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term b = d_solver.mkTrue();
+  ASSERT_THROW(Term().andTerm(b), CVC4ApiException);
+  ASSERT_THROW(b.andTerm(Term()), CVC4ApiException);
+  ASSERT_NO_THROW(b.andTerm(b));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
+  ASSERT_THROW(x.andTerm(b), CVC4ApiException);
+  ASSERT_THROW(x.andTerm(x), CVC4ApiException);
+  Term f = d_solver.mkVar(funSort1, "f");
+  ASSERT_THROW(f.andTerm(b), CVC4ApiException);
+  ASSERT_THROW(f.andTerm(x), CVC4ApiException);
+  ASSERT_THROW(f.andTerm(f), CVC4ApiException);
+  Term p = d_solver.mkVar(funSort2, "p");
+  ASSERT_THROW(p.andTerm(b), CVC4ApiException);
+  ASSERT_THROW(p.andTerm(x), CVC4ApiException);
+  ASSERT_THROW(p.andTerm(f), CVC4ApiException);
+  ASSERT_THROW(p.andTerm(p), CVC4ApiException);
+  Term zero = d_solver.mkInteger(0);
+  ASSERT_THROW(zero.andTerm(b), CVC4ApiException);
+  ASSERT_THROW(zero.andTerm(x), CVC4ApiException);
+  ASSERT_THROW(zero.andTerm(f), CVC4ApiException);
+  ASSERT_THROW(zero.andTerm(p), CVC4ApiException);
+  ASSERT_THROW(zero.andTerm(zero), CVC4ApiException);
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  ASSERT_THROW(f_x.andTerm(b), CVC4ApiException);
+  ASSERT_THROW(f_x.andTerm(x), CVC4ApiException);
+  ASSERT_THROW(f_x.andTerm(f), CVC4ApiException);
+  ASSERT_THROW(f_x.andTerm(p), CVC4ApiException);
+  ASSERT_THROW(f_x.andTerm(zero), CVC4ApiException);
+  ASSERT_THROW(f_x.andTerm(f_x), CVC4ApiException);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+  ASSERT_THROW(sum.andTerm(b), CVC4ApiException);
+  ASSERT_THROW(sum.andTerm(x), CVC4ApiException);
+  ASSERT_THROW(sum.andTerm(f), CVC4ApiException);
+  ASSERT_THROW(sum.andTerm(p), CVC4ApiException);
+  ASSERT_THROW(sum.andTerm(zero), CVC4ApiException);
+  ASSERT_THROW(sum.andTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(sum.andTerm(sum), CVC4ApiException);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  ASSERT_NO_THROW(p_0.andTerm(b));
+  ASSERT_THROW(p_0.andTerm(x), CVC4ApiException);
+  ASSERT_THROW(p_0.andTerm(f), CVC4ApiException);
+  ASSERT_THROW(p_0.andTerm(p), CVC4ApiException);
+  ASSERT_THROW(p_0.andTerm(zero), CVC4ApiException);
+  ASSERT_THROW(p_0.andTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(p_0.andTerm(sum), CVC4ApiException);
+  ASSERT_NO_THROW(p_0.andTerm(p_0));
+  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+  ASSERT_NO_THROW(p_f_x.andTerm(b));
+  ASSERT_THROW(p_f_x.andTerm(x), CVC4ApiException);
+  ASSERT_THROW(p_f_x.andTerm(f), CVC4ApiException);
+  ASSERT_THROW(p_f_x.andTerm(p), CVC4ApiException);
+  ASSERT_THROW(p_f_x.andTerm(zero), CVC4ApiException);
+  ASSERT_THROW(p_f_x.andTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(p_f_x.andTerm(sum), CVC4ApiException);
+  ASSERT_NO_THROW(p_f_x.andTerm(p_0));
+  ASSERT_NO_THROW(p_f_x.andTerm(p_f_x));
+}
+
+TEST_F(TestApiTermBlack, orTerm)
+{
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term b = d_solver.mkTrue();
+  ASSERT_THROW(Term().orTerm(b), CVC4ApiException);
+  ASSERT_THROW(b.orTerm(Term()), CVC4ApiException);
+  ASSERT_NO_THROW(b.orTerm(b));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
+  ASSERT_THROW(x.orTerm(b), CVC4ApiException);
+  ASSERT_THROW(x.orTerm(x), CVC4ApiException);
+  Term f = d_solver.mkVar(funSort1, "f");
+  ASSERT_THROW(f.orTerm(b), CVC4ApiException);
+  ASSERT_THROW(f.orTerm(x), CVC4ApiException);
+  ASSERT_THROW(f.orTerm(f), CVC4ApiException);
+  Term p = d_solver.mkVar(funSort2, "p");
+  ASSERT_THROW(p.orTerm(b), CVC4ApiException);
+  ASSERT_THROW(p.orTerm(x), CVC4ApiException);
+  ASSERT_THROW(p.orTerm(f), CVC4ApiException);
+  ASSERT_THROW(p.orTerm(p), CVC4ApiException);
+  Term zero = d_solver.mkInteger(0);
+  ASSERT_THROW(zero.orTerm(b), CVC4ApiException);
+  ASSERT_THROW(zero.orTerm(x), CVC4ApiException);
+  ASSERT_THROW(zero.orTerm(f), CVC4ApiException);
+  ASSERT_THROW(zero.orTerm(p), CVC4ApiException);
+  ASSERT_THROW(zero.orTerm(zero), CVC4ApiException);
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  ASSERT_THROW(f_x.orTerm(b), CVC4ApiException);
+  ASSERT_THROW(f_x.orTerm(x), CVC4ApiException);
+  ASSERT_THROW(f_x.orTerm(f), CVC4ApiException);
+  ASSERT_THROW(f_x.orTerm(p), CVC4ApiException);
+  ASSERT_THROW(f_x.orTerm(zero), CVC4ApiException);
+  ASSERT_THROW(f_x.orTerm(f_x), CVC4ApiException);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+  ASSERT_THROW(sum.orTerm(b), CVC4ApiException);
+  ASSERT_THROW(sum.orTerm(x), CVC4ApiException);
+  ASSERT_THROW(sum.orTerm(f), CVC4ApiException);
+  ASSERT_THROW(sum.orTerm(p), CVC4ApiException);
+  ASSERT_THROW(sum.orTerm(zero), CVC4ApiException);
+  ASSERT_THROW(sum.orTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(sum.orTerm(sum), CVC4ApiException);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  ASSERT_NO_THROW(p_0.orTerm(b));
+  ASSERT_THROW(p_0.orTerm(x), CVC4ApiException);
+  ASSERT_THROW(p_0.orTerm(f), CVC4ApiException);
+  ASSERT_THROW(p_0.orTerm(p), CVC4ApiException);
+  ASSERT_THROW(p_0.orTerm(zero), CVC4ApiException);
+  ASSERT_THROW(p_0.orTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(p_0.orTerm(sum), CVC4ApiException);
+  ASSERT_NO_THROW(p_0.orTerm(p_0));
+  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+  ASSERT_NO_THROW(p_f_x.orTerm(b));
+  ASSERT_THROW(p_f_x.orTerm(x), CVC4ApiException);
+  ASSERT_THROW(p_f_x.orTerm(f), CVC4ApiException);
+  ASSERT_THROW(p_f_x.orTerm(p), CVC4ApiException);
+  ASSERT_THROW(p_f_x.orTerm(zero), CVC4ApiException);
+  ASSERT_THROW(p_f_x.orTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(p_f_x.orTerm(sum), CVC4ApiException);
+  ASSERT_NO_THROW(p_f_x.orTerm(p_0));
+  ASSERT_NO_THROW(p_f_x.orTerm(p_f_x));
+}
+
+TEST_F(TestApiTermBlack, xorTerm)
+{
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term b = d_solver.mkTrue();
+  ASSERT_THROW(Term().xorTerm(b), CVC4ApiException);
+  ASSERT_THROW(b.xorTerm(Term()), CVC4ApiException);
+  ASSERT_NO_THROW(b.xorTerm(b));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
+  ASSERT_THROW(x.xorTerm(b), CVC4ApiException);
+  ASSERT_THROW(x.xorTerm(x), CVC4ApiException);
+  Term f = d_solver.mkVar(funSort1, "f");
+  ASSERT_THROW(f.xorTerm(b), CVC4ApiException);
+  ASSERT_THROW(f.xorTerm(x), CVC4ApiException);
+  ASSERT_THROW(f.xorTerm(f), CVC4ApiException);
+  Term p = d_solver.mkVar(funSort2, "p");
+  ASSERT_THROW(p.xorTerm(b), CVC4ApiException);
+  ASSERT_THROW(p.xorTerm(x), CVC4ApiException);
+  ASSERT_THROW(p.xorTerm(f), CVC4ApiException);
+  ASSERT_THROW(p.xorTerm(p), CVC4ApiException);
+  Term zero = d_solver.mkInteger(0);
+  ASSERT_THROW(zero.xorTerm(b), CVC4ApiException);
+  ASSERT_THROW(zero.xorTerm(x), CVC4ApiException);
+  ASSERT_THROW(zero.xorTerm(f), CVC4ApiException);
+  ASSERT_THROW(zero.xorTerm(p), CVC4ApiException);
+  ASSERT_THROW(zero.xorTerm(zero), CVC4ApiException);
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  ASSERT_THROW(f_x.xorTerm(b), CVC4ApiException);
+  ASSERT_THROW(f_x.xorTerm(x), CVC4ApiException);
+  ASSERT_THROW(f_x.xorTerm(f), CVC4ApiException);
+  ASSERT_THROW(f_x.xorTerm(p), CVC4ApiException);
+  ASSERT_THROW(f_x.xorTerm(zero), CVC4ApiException);
+  ASSERT_THROW(f_x.xorTerm(f_x), CVC4ApiException);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+  ASSERT_THROW(sum.xorTerm(b), CVC4ApiException);
+  ASSERT_THROW(sum.xorTerm(x), CVC4ApiException);
+  ASSERT_THROW(sum.xorTerm(f), CVC4ApiException);
+  ASSERT_THROW(sum.xorTerm(p), CVC4ApiException);
+  ASSERT_THROW(sum.xorTerm(zero), CVC4ApiException);
+  ASSERT_THROW(sum.xorTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(sum.xorTerm(sum), CVC4ApiException);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  ASSERT_NO_THROW(p_0.xorTerm(b));
+  ASSERT_THROW(p_0.xorTerm(x), CVC4ApiException);
+  ASSERT_THROW(p_0.xorTerm(f), CVC4ApiException);
+  ASSERT_THROW(p_0.xorTerm(p), CVC4ApiException);
+  ASSERT_THROW(p_0.xorTerm(zero), CVC4ApiException);
+  ASSERT_THROW(p_0.xorTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(p_0.xorTerm(sum), CVC4ApiException);
+  ASSERT_NO_THROW(p_0.xorTerm(p_0));
+  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+  ASSERT_NO_THROW(p_f_x.xorTerm(b));
+  ASSERT_THROW(p_f_x.xorTerm(x), CVC4ApiException);
+  ASSERT_THROW(p_f_x.xorTerm(f), CVC4ApiException);
+  ASSERT_THROW(p_f_x.xorTerm(p), CVC4ApiException);
+  ASSERT_THROW(p_f_x.xorTerm(zero), CVC4ApiException);
+  ASSERT_THROW(p_f_x.xorTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(p_f_x.xorTerm(sum), CVC4ApiException);
+  ASSERT_NO_THROW(p_f_x.xorTerm(p_0));
+  ASSERT_NO_THROW(p_f_x.xorTerm(p_f_x));
+}
+
+TEST_F(TestApiTermBlack, eqTerm)
+{
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term b = d_solver.mkTrue();
+  ASSERT_THROW(Term().eqTerm(b), CVC4ApiException);
+  ASSERT_THROW(b.eqTerm(Term()), CVC4ApiException);
+  ASSERT_NO_THROW(b.eqTerm(b));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
+  ASSERT_THROW(x.eqTerm(b), CVC4ApiException);
+  ASSERT_NO_THROW(x.eqTerm(x));
+  Term f = d_solver.mkVar(funSort1, "f");
+  ASSERT_THROW(f.eqTerm(b), CVC4ApiException);
+  ASSERT_THROW(f.eqTerm(x), CVC4ApiException);
+  ASSERT_NO_THROW(f.eqTerm(f));
+  Term p = d_solver.mkVar(funSort2, "p");
+  ASSERT_THROW(p.eqTerm(b), CVC4ApiException);
+  ASSERT_THROW(p.eqTerm(x), CVC4ApiException);
+  ASSERT_THROW(p.eqTerm(f), CVC4ApiException);
+  ASSERT_NO_THROW(p.eqTerm(p));
+  Term zero = d_solver.mkInteger(0);
+  ASSERT_THROW(zero.eqTerm(b), CVC4ApiException);
+  ASSERT_THROW(zero.eqTerm(x), CVC4ApiException);
+  ASSERT_THROW(zero.eqTerm(f), CVC4ApiException);
+  ASSERT_THROW(zero.eqTerm(p), CVC4ApiException);
+  ASSERT_NO_THROW(zero.eqTerm(zero));
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  ASSERT_THROW(f_x.eqTerm(b), CVC4ApiException);
+  ASSERT_THROW(f_x.eqTerm(x), CVC4ApiException);
+  ASSERT_THROW(f_x.eqTerm(f), CVC4ApiException);
+  ASSERT_THROW(f_x.eqTerm(p), CVC4ApiException);
+  ASSERT_NO_THROW(f_x.eqTerm(zero));
+  ASSERT_NO_THROW(f_x.eqTerm(f_x));
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+  ASSERT_THROW(sum.eqTerm(b), CVC4ApiException);
+  ASSERT_THROW(sum.eqTerm(x), CVC4ApiException);
+  ASSERT_THROW(sum.eqTerm(f), CVC4ApiException);
+  ASSERT_THROW(sum.eqTerm(p), CVC4ApiException);
+  ASSERT_NO_THROW(sum.eqTerm(zero));
+  ASSERT_NO_THROW(sum.eqTerm(f_x));
+  ASSERT_NO_THROW(sum.eqTerm(sum));
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  ASSERT_NO_THROW(p_0.eqTerm(b));
+  ASSERT_THROW(p_0.eqTerm(x), CVC4ApiException);
+  ASSERT_THROW(p_0.eqTerm(f), CVC4ApiException);
+  ASSERT_THROW(p_0.eqTerm(p), CVC4ApiException);
+  ASSERT_THROW(p_0.eqTerm(zero), CVC4ApiException);
+  ASSERT_THROW(p_0.eqTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(p_0.eqTerm(sum), CVC4ApiException);
+  ASSERT_NO_THROW(p_0.eqTerm(p_0));
+  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+  ASSERT_NO_THROW(p_f_x.eqTerm(b));
+  ASSERT_THROW(p_f_x.eqTerm(x), CVC4ApiException);
+  ASSERT_THROW(p_f_x.eqTerm(f), CVC4ApiException);
+  ASSERT_THROW(p_f_x.eqTerm(p), CVC4ApiException);
+  ASSERT_THROW(p_f_x.eqTerm(zero), CVC4ApiException);
+  ASSERT_THROW(p_f_x.eqTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(p_f_x.eqTerm(sum), CVC4ApiException);
+  ASSERT_NO_THROW(p_f_x.eqTerm(p_0));
+  ASSERT_NO_THROW(p_f_x.eqTerm(p_f_x));
+}
+
+TEST_F(TestApiTermBlack, impTerm)
+{
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term b = d_solver.mkTrue();
+  ASSERT_THROW(Term().impTerm(b), CVC4ApiException);
+  ASSERT_THROW(b.impTerm(Term()), CVC4ApiException);
+  ASSERT_NO_THROW(b.impTerm(b));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
+  ASSERT_THROW(x.impTerm(b), CVC4ApiException);
+  ASSERT_THROW(x.impTerm(x), CVC4ApiException);
+  Term f = d_solver.mkVar(funSort1, "f");
+  ASSERT_THROW(f.impTerm(b), CVC4ApiException);
+  ASSERT_THROW(f.impTerm(x), CVC4ApiException);
+  ASSERT_THROW(f.impTerm(f), CVC4ApiException);
+  Term p = d_solver.mkVar(funSort2, "p");
+  ASSERT_THROW(p.impTerm(b), CVC4ApiException);
+  ASSERT_THROW(p.impTerm(x), CVC4ApiException);
+  ASSERT_THROW(p.impTerm(f), CVC4ApiException);
+  ASSERT_THROW(p.impTerm(p), CVC4ApiException);
+  Term zero = d_solver.mkInteger(0);
+  ASSERT_THROW(zero.impTerm(b), CVC4ApiException);
+  ASSERT_THROW(zero.impTerm(x), CVC4ApiException);
+  ASSERT_THROW(zero.impTerm(f), CVC4ApiException);
+  ASSERT_THROW(zero.impTerm(p), CVC4ApiException);
+  ASSERT_THROW(zero.impTerm(zero), CVC4ApiException);
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  ASSERT_THROW(f_x.impTerm(b), CVC4ApiException);
+  ASSERT_THROW(f_x.impTerm(x), CVC4ApiException);
+  ASSERT_THROW(f_x.impTerm(f), CVC4ApiException);
+  ASSERT_THROW(f_x.impTerm(p), CVC4ApiException);
+  ASSERT_THROW(f_x.impTerm(zero), CVC4ApiException);
+  ASSERT_THROW(f_x.impTerm(f_x), CVC4ApiException);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+  ASSERT_THROW(sum.impTerm(b), CVC4ApiException);
+  ASSERT_THROW(sum.impTerm(x), CVC4ApiException);
+  ASSERT_THROW(sum.impTerm(f), CVC4ApiException);
+  ASSERT_THROW(sum.impTerm(p), CVC4ApiException);
+  ASSERT_THROW(sum.impTerm(zero), CVC4ApiException);
+  ASSERT_THROW(sum.impTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(sum.impTerm(sum), CVC4ApiException);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  ASSERT_NO_THROW(p_0.impTerm(b));
+  ASSERT_THROW(p_0.impTerm(x), CVC4ApiException);
+  ASSERT_THROW(p_0.impTerm(f), CVC4ApiException);
+  ASSERT_THROW(p_0.impTerm(p), CVC4ApiException);
+  ASSERT_THROW(p_0.impTerm(zero), CVC4ApiException);
+  ASSERT_THROW(p_0.impTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(p_0.impTerm(sum), CVC4ApiException);
+  ASSERT_NO_THROW(p_0.impTerm(p_0));
+  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+  ASSERT_NO_THROW(p_f_x.impTerm(b));
+  ASSERT_THROW(p_f_x.impTerm(x), CVC4ApiException);
+  ASSERT_THROW(p_f_x.impTerm(f), CVC4ApiException);
+  ASSERT_THROW(p_f_x.impTerm(p), CVC4ApiException);
+  ASSERT_THROW(p_f_x.impTerm(zero), CVC4ApiException);
+  ASSERT_THROW(p_f_x.impTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(p_f_x.impTerm(sum), CVC4ApiException);
+  ASSERT_NO_THROW(p_f_x.impTerm(p_0));
+  ASSERT_NO_THROW(p_f_x.impTerm(p_f_x));
+}
+
+TEST_F(TestApiTermBlack, iteTerm)
+{
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term b = d_solver.mkTrue();
+  ASSERT_THROW(Term().iteTerm(b, b), CVC4ApiException);
+  ASSERT_THROW(b.iteTerm(Term(), b), CVC4ApiException);
+  ASSERT_THROW(b.iteTerm(b, Term()), CVC4ApiException);
+  ASSERT_NO_THROW(b.iteTerm(b, b));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
+  ASSERT_NO_THROW(b.iteTerm(x, x));
+  ASSERT_NO_THROW(b.iteTerm(b, b));
+  ASSERT_THROW(b.iteTerm(x, b), CVC4ApiException);
+  ASSERT_THROW(x.iteTerm(x, x), CVC4ApiException);
+  ASSERT_THROW(x.iteTerm(x, b), CVC4ApiException);
+  Term f = d_solver.mkVar(funSort1, "f");
+  ASSERT_THROW(f.iteTerm(b, b), CVC4ApiException);
+  ASSERT_THROW(x.iteTerm(b, x), CVC4ApiException);
+  Term p = d_solver.mkVar(funSort2, "p");
+  ASSERT_THROW(p.iteTerm(b, b), CVC4ApiException);
+  ASSERT_THROW(p.iteTerm(x, b), CVC4ApiException);
+  Term zero = d_solver.mkInteger(0);
+  ASSERT_THROW(zero.iteTerm(x, x), CVC4ApiException);
+  ASSERT_THROW(zero.iteTerm(x, b), CVC4ApiException);
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  ASSERT_THROW(f_x.iteTerm(b, b), CVC4ApiException);
+  ASSERT_THROW(f_x.iteTerm(b, x), CVC4ApiException);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+  ASSERT_THROW(sum.iteTerm(x, x), CVC4ApiException);
+  ASSERT_THROW(sum.iteTerm(b, x), CVC4ApiException);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  ASSERT_NO_THROW(p_0.iteTerm(b, b));
+  ASSERT_NO_THROW(p_0.iteTerm(x, x));
+  ASSERT_THROW(p_0.iteTerm(x, b), CVC4ApiException);
+  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+  ASSERT_NO_THROW(p_f_x.iteTerm(b, b));
+  ASSERT_NO_THROW(p_f_x.iteTerm(x, x));
+  ASSERT_THROW(p_f_x.iteTerm(x, b), CVC4ApiException);
+}
+
+TEST_F(TestApiTermBlack, termAssignment)
+{
+  Term t1 = d_solver.mkInteger(1);
+  Term t2 = t1;
+  t2 = d_solver.mkInteger(2);
+  EXPECT_EQ(t1, d_solver.mkInteger(1));
+}
+
+TEST_F(TestApiTermBlack, termCompare)
+{
+  Term t1 = d_solver.mkInteger(1);
+  Term t2 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
+  Term t3 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
+  ASSERT_TRUE(t2 >= t3);
+  ASSERT_TRUE(t2 <= t3);
+  ASSERT_TRUE((t1 > t2) != (t1 < t2));
+  ASSERT_TRUE((t1 > t2 || t1 == t2) == (t1 >= t2));
+}
+
+TEST_F(TestApiTermBlack, termChildren)
+{
+  // simple term 2+3
+  Term two = d_solver.mkInteger(2);
+  Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3));
+  EXPECT_EQ(t1[0], two);
+  EXPECT_EQ(t1.getNumChildren(), 2);
+  Term tnull;
+  ASSERT_THROW(tnull.getNumChildren(), CVC4ApiException);
+
+  // apply term f(2)
+  Sort intSort = d_solver.getIntegerSort();
+  Sort fsort = d_solver.mkFunctionSort(intSort, intSort);
+  Term f = d_solver.mkConst(fsort, "f");
+  Term t2 = d_solver.mkTerm(APPLY_UF, f, two);
+  // due to our higher-order view of terms, we treat f as a child of APPLY_UF
+  ASSERT_EQ(t2.getNumChildren(), 2);
+  EXPECT_EQ(t2[0], f);
+  EXPECT_EQ(t2[1], two);
+  ASSERT_THROW(tnull[0], CVC4ApiException);
+}
+
+TEST_F(TestApiTermBlack, substitute)
+{
+  Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
+  Term one = d_solver.mkInteger(1);
+  Term ttrue = d_solver.mkTrue();
+  Term xpx = d_solver.mkTerm(PLUS, x, x);
+  Term onepone = d_solver.mkTerm(PLUS, one, one);
+
+  EXPECT_EQ(xpx.substitute(x, one), onepone);
+  EXPECT_EQ(onepone.substitute(one, x), xpx);
+  // incorrect due to type
+  ASSERT_THROW(xpx.substitute(one, ttrue), CVC4ApiException);
+
+  // simultaneous substitution
+  Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y");
+  Term xpy = d_solver.mkTerm(PLUS, x, y);
+  Term xpone = d_solver.mkTerm(PLUS, y, one);
+  std::vector<Term> es;
+  std::vector<Term> rs;
+  es.push_back(x);
+  rs.push_back(y);
+  es.push_back(y);
+  rs.push_back(one);
+  EXPECT_EQ(xpy.substitute(es, rs), xpone);
+
+  // incorrect substitution due to arity
+  rs.pop_back();
+  ASSERT_THROW(xpy.substitute(es, rs), CVC4ApiException);
+
+  // incorrect substitution due to types
+  rs.push_back(ttrue);
+  ASSERT_THROW(xpy.substitute(es, rs), CVC4ApiException);
+
+  // null cannot substitute
+  Term tnull;
+  ASSERT_THROW(tnull.substitute(one, x), CVC4ApiException);
+  ASSERT_THROW(xpx.substitute(tnull, x), CVC4ApiException);
+  ASSERT_THROW(xpx.substitute(x, tnull), CVC4ApiException);
+  rs.pop_back();
+  rs.push_back(tnull);
+  ASSERT_THROW(xpy.substitute(es, rs), CVC4ApiException);
+  es.clear();
+  rs.clear();
+  es.push_back(x);
+  rs.push_back(y);
+  ASSERT_THROW(tnull.substitute(es, rs), CVC4ApiException);
+  es.push_back(tnull);
+  rs.push_back(one);
+  ASSERT_THROW(xpx.substitute(es, rs), CVC4ApiException);
+}
+
+TEST_F(TestApiTermBlack, constArray)
+{
+  Sort intsort = d_solver.getIntegerSort();
+  Sort arrsort = d_solver.mkArraySort(intsort, intsort);
+  Term a = d_solver.mkConst(arrsort, "a");
+  Term one = d_solver.mkInteger(1);
+  Term constarr = d_solver.mkConstArray(arrsort, one);
+
+  EXPECT_EQ(constarr.getKind(), CONST_ARRAY);
+  EXPECT_EQ(constarr.getConstArrayBase(), one);
+  ASSERT_THROW(a.getConstArrayBase(), CVC4ApiException);
+
+  arrsort =
+      d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort());
+  Term zero_array = d_solver.mkConstArray(arrsort, d_solver.mkReal(0));
+  Term stores = d_solver.mkTerm(
+      STORE, zero_array, d_solver.mkReal(1), d_solver.mkReal(2));
+  stores =
+      d_solver.mkTerm(STORE, stores, d_solver.mkReal(2), d_solver.mkReal(3));
+  stores =
+      d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5));
+}
+
+TEST_F(TestApiTermBlack, constSequenceElements)
+{
+  Sort realsort = d_solver.getRealSort();
+  Sort seqsort = d_solver.mkSequenceSort(realsort);
+  Term s = d_solver.mkEmptySequence(seqsort);
+
+  EXPECT_EQ(s.getKind(), CONST_SEQUENCE);
+  // empty sequence has zero elements
+  std::vector<Term> cs = s.getConstSequenceElements();
+  ASSERT_TRUE(cs.empty());
+
+  // A seq.unit app is not a constant sequence (regardless of whether it is
+  // applied to a constant).
+  Term su = d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1));
+  ASSERT_THROW(su.getConstSequenceElements(), CVC4ApiException);
+}
+
+TEST_F(TestApiTermBlack, termScopedToString)
+{
+  Sort intsort = d_solver.getIntegerSort();
+  Term x = d_solver.mkConst(intsort, "x");
+  EXPECT_EQ(x.toString(), "x");
+  Solver solver2;
+  EXPECT_EQ(x.toString(), "x");
+}
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
deleted file mode 100644
index bebfc6e1f..000000000
--- a/test/unit/api/term_black.h
+++ /dev/null
@@ -1,800 +0,0 @@
-/*********************                                                        */
-/*! \file term_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds, Makai Mann
- ** 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 the Term class
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "api/cvc4cpp.h"
-
-using namespace CVC4::api;
-
-class TermBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() override {}
-  void tearDown() override {}
-
-  void testEq();
-  void testGetId();
-  void testGetKind();
-  void testGetSort();
-  void testGetOp();
-  void testIsNull();
-  void testNotTerm();
-  void testAndTerm();
-  void testOrTerm();
-  void testXorTerm();
-  void testEqTerm();
-  void testImpTerm();
-  void testIteTerm();
-
-  void testTermAssignment();
-  void testTermCompare();
-  void testTermChildren();
-  void testSubstitute();
-  void testConstArray();
-  void testConstSequenceElements();
-
-  void testTermScopedToString();
-
- private:
-  Solver d_solver;
-};
-
-void TermBlack::testEq()
-{
-  Sort uSort = d_solver.mkUninterpretedSort("u");
-  Term x = d_solver.mkVar(uSort, "x");
-  Term y = d_solver.mkVar(uSort, "y");
-  Term z;
-
-  TS_ASSERT(x == x);
-  TS_ASSERT(!(x != x));
-  TS_ASSERT(!(x == y));
-  TS_ASSERT(x != y);
-  TS_ASSERT(!(x == z));
-  TS_ASSERT(x != z);
-}
-
-void TermBlack::testGetId()
-{
-  Term n;
-  TS_ASSERT_THROWS(n.getId(), CVC4ApiException&);
-  Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x");
-  TS_ASSERT_THROWS_NOTHING(x.getId());
-  Term y = x;
-  TS_ASSERT_EQUALS(x.getId(), y.getId());
-
-  Term z = d_solver.mkVar(d_solver.getIntegerSort(), "z");
-  TS_ASSERT_DIFFERS(x.getId(), z.getId());
-}
-
-void TermBlack::testGetKind()
-{
-  Sort uSort = d_solver.mkUninterpretedSort("u");
-  Sort intSort = d_solver.getIntegerSort();
-  Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(uSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
-
-  Term n;
-  TS_ASSERT_THROWS(n.getKind(), CVC4ApiException&);
-  Term x = d_solver.mkVar(uSort, "x");
-  TS_ASSERT_THROWS_NOTHING(x.getKind());
-  Term y = d_solver.mkVar(uSort, "y");
-  TS_ASSERT_THROWS_NOTHING(y.getKind());
-
-  Term f = d_solver.mkVar(funSort1, "f");
-  TS_ASSERT_THROWS_NOTHING(f.getKind());
-  Term p = d_solver.mkVar(funSort2, "p");
-  TS_ASSERT_THROWS_NOTHING(p.getKind());
-
-  Term zero = d_solver.mkInteger(0);
-  TS_ASSERT_THROWS_NOTHING(zero.getKind());
-
-  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
-  TS_ASSERT_THROWS_NOTHING(f_x.getKind());
-  Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
-  TS_ASSERT_THROWS_NOTHING(f_y.getKind());
-  Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
-  TS_ASSERT_THROWS_NOTHING(sum.getKind());
-  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
-  TS_ASSERT_THROWS_NOTHING(p_0.getKind());
-  Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
-  TS_ASSERT_THROWS_NOTHING(p_f_y.getKind());
-
-  // Sequence kinds do not exist internally, test that the API properly
-  // converts them back.
-  Sort seqSort = d_solver.mkSequenceSort(intSort);
-  Term s = d_solver.mkConst(seqSort, "s");
-  Term ss = d_solver.mkTerm(SEQ_CONCAT, s, s);
-  TS_ASSERT(ss.getKind() == SEQ_CONCAT);
-}
-
-void TermBlack::testGetSort()
-{
-  Sort bvSort = d_solver.mkBitVectorSort(8);
-  Sort intSort = d_solver.getIntegerSort();
-  Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
-
-  Term n;
-  TS_ASSERT_THROWS(n.getSort(), CVC4ApiException&);
-  Term x = d_solver.mkVar(bvSort, "x");
-  TS_ASSERT_THROWS_NOTHING(x.getSort());
-  TS_ASSERT(x.getSort() == bvSort);
-  Term y = d_solver.mkVar(bvSort, "y");
-  TS_ASSERT_THROWS_NOTHING(y.getSort());
-  TS_ASSERT(y.getSort() == bvSort);
-
-  Term f = d_solver.mkVar(funSort1, "f");
-  TS_ASSERT_THROWS_NOTHING(f.getSort());
-  TS_ASSERT(f.getSort() == funSort1);
-  Term p = d_solver.mkVar(funSort2, "p");
-  TS_ASSERT_THROWS_NOTHING(p.getSort());
-  TS_ASSERT(p.getSort() == funSort2);
-
-  Term zero = d_solver.mkInteger(0);
-  TS_ASSERT_THROWS_NOTHING(zero.getSort());
-  TS_ASSERT(zero.getSort() == intSort);
-
-  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
-  TS_ASSERT_THROWS_NOTHING(f_x.getSort());
-  TS_ASSERT(f_x.getSort() == intSort);
-  Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
-  TS_ASSERT_THROWS_NOTHING(f_y.getSort());
-  TS_ASSERT(f_y.getSort() == intSort);
-  Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
-  TS_ASSERT_THROWS_NOTHING(sum.getSort());
-  TS_ASSERT(sum.getSort() == intSort);
-  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
-  TS_ASSERT_THROWS_NOTHING(p_0.getSort());
-  TS_ASSERT(p_0.getSort() == boolSort);
-  Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
-  TS_ASSERT_THROWS_NOTHING(p_f_y.getSort());
-  TS_ASSERT(p_f_y.getSort() == boolSort);
-}
-
-void TermBlack::testGetOp()
-{
-  Sort intsort = d_solver.getIntegerSort();
-  Sort bvsort = d_solver.mkBitVectorSort(8);
-  Sort arrsort = d_solver.mkArraySort(bvsort, intsort);
-  Sort funsort = d_solver.mkFunctionSort(intsort, bvsort);
-
-  Term x = d_solver.mkConst(intsort, "x");
-  Term a = d_solver.mkConst(arrsort, "a");
-  Term b = d_solver.mkConst(bvsort, "b");
-
-  TS_ASSERT(!x.hasOp());
-  TS_ASSERT_THROWS(x.getOp(), CVC4ApiException&);
-
-  Term ab = d_solver.mkTerm(SELECT, a, b);
-  Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
-  Term extb = d_solver.mkTerm(ext, b);
-
-  TS_ASSERT(ab.hasOp());
-  TS_ASSERT_EQUALS(ab.getOp(), Op(&d_solver, SELECT));
-  TS_ASSERT(!ab.getOp().isIndexed());
-  // can compare directly to a Kind (will invoke Op constructor)
-  TS_ASSERT_EQUALS(ab.getOp(), Op(&d_solver, SELECT));
-  TS_ASSERT(extb.hasOp());
-  TS_ASSERT(extb.getOp().isIndexed());
-  TS_ASSERT_EQUALS(extb.getOp(), ext);
-
-  Term f = d_solver.mkConst(funsort, "f");
-  Term fx = d_solver.mkTerm(APPLY_UF, f, x);
-
-  TS_ASSERT(!f.hasOp());
-  TS_ASSERT_THROWS(f.getOp(), CVC4ApiException&);
-  TS_ASSERT(fx.hasOp());
-  TS_ASSERT_EQUALS(fx.getOp(), Op(&d_solver, APPLY_UF));
-  std::vector<Term> children(fx.begin(), fx.end());
-  // testing rebuild from op and children
-  TS_ASSERT_EQUALS(fx, d_solver.mkTerm(fx.getOp(), children));
-
-  // Test Datatypes Ops
-  Sort sort = d_solver.mkParamSort("T");
-  DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
-  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
-  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
-  cons.addSelector("head", sort);
-  cons.addSelectorSelf("tail");
-  listDecl.addConstructor(cons);
-  listDecl.addConstructor(nil);
-  Sort listSort = d_solver.mkDatatypeSort(listDecl);
-  Sort intListSort =
-      listSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()});
-  Term c = d_solver.mkConst(intListSort, "c");
-  Datatype list = listSort.getDatatype();
-  // list datatype constructor and selector operator terms
-  Term consOpTerm = list.getConstructorTerm("cons");
-  Term nilOpTerm = list.getConstructorTerm("nil");
-  Term headOpTerm = list["cons"].getSelectorTerm("head");
-  Term tailOpTerm = list["cons"].getSelectorTerm("tail");
-
-  Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm);
-  Term consTerm = d_solver.mkTerm(
-      APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkInteger(0), nilTerm);
-  Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm);
-  Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm);
-
-  TS_ASSERT(nilTerm.hasOp());
-  TS_ASSERT(consTerm.hasOp());
-  TS_ASSERT(headTerm.hasOp());
-  TS_ASSERT(tailTerm.hasOp());
-
-  TS_ASSERT_EQUALS(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
-  TS_ASSERT_EQUALS(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
-  TS_ASSERT_EQUALS(headTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
-  TS_ASSERT_EQUALS(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
-
-  // Test rebuilding
-  children.clear();
-  children.insert(children.begin(), headTerm.begin(), headTerm.end());
-  TS_ASSERT_EQUALS(headTerm, d_solver.mkTerm(headTerm.getOp(), children));
-}
-
-void TermBlack::testIsNull()
-{
-  Term x;
-  TS_ASSERT(x.isNull());
-  x = d_solver.mkVar(d_solver.mkBitVectorSort(4), "x");
-  TS_ASSERT(!x.isNull());
-}
-
-void TermBlack::testNotTerm()
-{
-  Sort bvSort = d_solver.mkBitVectorSort(8);
-  Sort intSort = d_solver.getIntegerSort();
-  Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
-
-  TS_ASSERT_THROWS(Term().notTerm(), CVC4ApiException&);
-  Term b = d_solver.mkTrue();
-  TS_ASSERT_THROWS_NOTHING(b.notTerm());
-  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
-  TS_ASSERT_THROWS(x.notTerm(), CVC4ApiException&);
-  Term f = d_solver.mkVar(funSort1, "f");
-  TS_ASSERT_THROWS(f.notTerm(), CVC4ApiException&);
-  Term p = d_solver.mkVar(funSort2, "p");
-  TS_ASSERT_THROWS(p.notTerm(), CVC4ApiException&);
-  Term zero = d_solver.mkInteger(0);
-  TS_ASSERT_THROWS(zero.notTerm(), CVC4ApiException&);
-  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
-  TS_ASSERT_THROWS(f_x.notTerm(), CVC4ApiException&);
-  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
-  TS_ASSERT_THROWS(sum.notTerm(), CVC4ApiException&);
-  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
-  TS_ASSERT_THROWS_NOTHING(p_0.notTerm());
-  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
-  TS_ASSERT_THROWS_NOTHING(p_f_x.notTerm());
-}
-
-void TermBlack::testAndTerm()
-{
-  Sort bvSort = d_solver.mkBitVectorSort(8);
-  Sort intSort = d_solver.getIntegerSort();
-  Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
-
-  Term b = d_solver.mkTrue();
-  TS_ASSERT_THROWS(Term().andTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(b.andTerm(Term()), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(b.andTerm(b));
-  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
-  TS_ASSERT_THROWS(x.andTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(x.andTerm(x), CVC4ApiException&);
-  Term f = d_solver.mkVar(funSort1, "f");
-  TS_ASSERT_THROWS(f.andTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(f.andTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(f.andTerm(f), CVC4ApiException&);
-  Term p = d_solver.mkVar(funSort2, "p");
-  TS_ASSERT_THROWS(p.andTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(p.andTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p.andTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(p.andTerm(p), CVC4ApiException&);
-  Term zero = d_solver.mkInteger(0);
-  TS_ASSERT_THROWS(zero.andTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.andTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.andTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.andTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.andTerm(zero), CVC4ApiException&);
-  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
-  TS_ASSERT_THROWS(f_x.andTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.andTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.andTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.andTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.andTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.andTerm(f_x), CVC4ApiException&);
-  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
-  TS_ASSERT_THROWS(sum.andTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.andTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.andTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.andTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.andTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.andTerm(f_x), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.andTerm(sum), CVC4ApiException&);
-  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
-  TS_ASSERT_THROWS_NOTHING(p_0.andTerm(b));
-  TS_ASSERT_THROWS(p_0.andTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.andTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.andTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.andTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.andTerm(f_x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.andTerm(sum), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(p_0.andTerm(p_0));
-  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
-  TS_ASSERT_THROWS_NOTHING(p_f_x.andTerm(b));
-  TS_ASSERT_THROWS(p_f_x.andTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.andTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.andTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.andTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.andTerm(f_x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.andTerm(sum), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(p_f_x.andTerm(p_0));
-  TS_ASSERT_THROWS_NOTHING(p_f_x.andTerm(p_f_x));
-}
-
-void TermBlack::testOrTerm()
-{
-  Sort bvSort = d_solver.mkBitVectorSort(8);
-  Sort intSort = d_solver.getIntegerSort();
-  Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
-
-  Term b = d_solver.mkTrue();
-  TS_ASSERT_THROWS(Term().orTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(b.orTerm(Term()), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(b.orTerm(b));
-  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
-  TS_ASSERT_THROWS(x.orTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(x.orTerm(x), CVC4ApiException&);
-  Term f = d_solver.mkVar(funSort1, "f");
-  TS_ASSERT_THROWS(f.orTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(f.orTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(f.orTerm(f), CVC4ApiException&);
-  Term p = d_solver.mkVar(funSort2, "p");
-  TS_ASSERT_THROWS(p.orTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(p.orTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p.orTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(p.orTerm(p), CVC4ApiException&);
-  Term zero = d_solver.mkInteger(0);
-  TS_ASSERT_THROWS(zero.orTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.orTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.orTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.orTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.orTerm(zero), CVC4ApiException&);
-  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
-  TS_ASSERT_THROWS(f_x.orTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.orTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.orTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.orTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.orTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.orTerm(f_x), CVC4ApiException&);
-  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
-  TS_ASSERT_THROWS(sum.orTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.orTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.orTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.orTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.orTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.orTerm(f_x), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.orTerm(sum), CVC4ApiException&);
-  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
-  TS_ASSERT_THROWS_NOTHING(p_0.orTerm(b));
-  TS_ASSERT_THROWS(p_0.orTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.orTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.orTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.orTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.orTerm(f_x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.orTerm(sum), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(p_0.orTerm(p_0));
-  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
-  TS_ASSERT_THROWS_NOTHING(p_f_x.orTerm(b));
-  TS_ASSERT_THROWS(p_f_x.orTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.orTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.orTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.orTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.orTerm(f_x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.orTerm(sum), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(p_f_x.orTerm(p_0));
-  TS_ASSERT_THROWS_NOTHING(p_f_x.orTerm(p_f_x));
-}
-
-void TermBlack::testXorTerm()
-{
-  Sort bvSort = d_solver.mkBitVectorSort(8);
-  Sort intSort = d_solver.getIntegerSort();
-  Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
-
-  Term b = d_solver.mkTrue();
-  TS_ASSERT_THROWS(Term().xorTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(b.xorTerm(Term()), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(b.xorTerm(b));
-  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
-  TS_ASSERT_THROWS(x.xorTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(x.xorTerm(x), CVC4ApiException&);
-  Term f = d_solver.mkVar(funSort1, "f");
-  TS_ASSERT_THROWS(f.xorTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(f.xorTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(f.xorTerm(f), CVC4ApiException&);
-  Term p = d_solver.mkVar(funSort2, "p");
-  TS_ASSERT_THROWS(p.xorTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(p.xorTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p.xorTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(p.xorTerm(p), CVC4ApiException&);
-  Term zero = d_solver.mkInteger(0);
-  TS_ASSERT_THROWS(zero.xorTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.xorTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.xorTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.xorTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.xorTerm(zero), CVC4ApiException&);
-  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
-  TS_ASSERT_THROWS(f_x.xorTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.xorTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.xorTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.xorTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.xorTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.xorTerm(f_x), CVC4ApiException&);
-  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
-  TS_ASSERT_THROWS(sum.xorTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.xorTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.xorTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.xorTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.xorTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.xorTerm(f_x), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.xorTerm(sum), CVC4ApiException&);
-  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
-  TS_ASSERT_THROWS_NOTHING(p_0.xorTerm(b));
-  TS_ASSERT_THROWS(p_0.xorTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.xorTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.xorTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.xorTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.xorTerm(f_x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.xorTerm(sum), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(p_0.xorTerm(p_0));
-  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
-  TS_ASSERT_THROWS_NOTHING(p_f_x.xorTerm(b));
-  TS_ASSERT_THROWS(p_f_x.xorTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.xorTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.xorTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.xorTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.xorTerm(f_x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.xorTerm(sum), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(p_f_x.xorTerm(p_0));
-  TS_ASSERT_THROWS_NOTHING(p_f_x.xorTerm(p_f_x));
-}
-
-void TermBlack::testEqTerm()
-{
-  Sort bvSort = d_solver.mkBitVectorSort(8);
-  Sort intSort = d_solver.getIntegerSort();
-  Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
-
-  Term b = d_solver.mkTrue();
-  TS_ASSERT_THROWS(Term().eqTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(b.eqTerm(Term()), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(b.eqTerm(b));
-  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
-  TS_ASSERT_THROWS(x.eqTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(x.eqTerm(x));
-  Term f = d_solver.mkVar(funSort1, "f");
-  TS_ASSERT_THROWS(f.eqTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(f.eqTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(f.eqTerm(f));
-  Term p = d_solver.mkVar(funSort2, "p");
-  TS_ASSERT_THROWS(p.eqTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(p.eqTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p.eqTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(p.eqTerm(p));
-  Term zero = d_solver.mkInteger(0);
-  TS_ASSERT_THROWS(zero.eqTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.eqTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.eqTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.eqTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(zero.eqTerm(zero));
-  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
-  TS_ASSERT_THROWS(f_x.eqTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.eqTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.eqTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.eqTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(f_x.eqTerm(zero));
-  TS_ASSERT_THROWS_NOTHING(f_x.eqTerm(f_x));
-  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
-  TS_ASSERT_THROWS(sum.eqTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.eqTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.eqTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.eqTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(sum.eqTerm(zero));
-  TS_ASSERT_THROWS_NOTHING(sum.eqTerm(f_x));
-  TS_ASSERT_THROWS_NOTHING(sum.eqTerm(sum));
-  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
-  TS_ASSERT_THROWS_NOTHING(p_0.eqTerm(b));
-  TS_ASSERT_THROWS(p_0.eqTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.eqTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.eqTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.eqTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.eqTerm(f_x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.eqTerm(sum), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(p_0.eqTerm(p_0));
-  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
-  TS_ASSERT_THROWS_NOTHING(p_f_x.eqTerm(b));
-  TS_ASSERT_THROWS(p_f_x.eqTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.eqTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.eqTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.eqTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.eqTerm(f_x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.eqTerm(sum), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(p_f_x.eqTerm(p_0));
-  TS_ASSERT_THROWS_NOTHING(p_f_x.eqTerm(p_f_x));
-}
-
-void TermBlack::testImpTerm()
-{
-  Sort bvSort = d_solver.mkBitVectorSort(8);
-  Sort intSort = d_solver.getIntegerSort();
-  Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
-
-  Term b = d_solver.mkTrue();
-  TS_ASSERT_THROWS(Term().impTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(b.impTerm(Term()), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(b.impTerm(b));
-  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
-  TS_ASSERT_THROWS(x.impTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(x.impTerm(x), CVC4ApiException&);
-  Term f = d_solver.mkVar(funSort1, "f");
-  TS_ASSERT_THROWS(f.impTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(f.impTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(f.impTerm(f), CVC4ApiException&);
-  Term p = d_solver.mkVar(funSort2, "p");
-  TS_ASSERT_THROWS(p.impTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(p.impTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p.impTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(p.impTerm(p), CVC4ApiException&);
-  Term zero = d_solver.mkInteger(0);
-  TS_ASSERT_THROWS(zero.impTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.impTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.impTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.impTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.impTerm(zero), CVC4ApiException&);
-  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
-  TS_ASSERT_THROWS(f_x.impTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.impTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.impTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.impTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.impTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.impTerm(f_x), CVC4ApiException&);
-  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
-  TS_ASSERT_THROWS(sum.impTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.impTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.impTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.impTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.impTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.impTerm(f_x), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.impTerm(sum), CVC4ApiException&);
-  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
-  TS_ASSERT_THROWS_NOTHING(p_0.impTerm(b));
-  TS_ASSERT_THROWS(p_0.impTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.impTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.impTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.impTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.impTerm(f_x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_0.impTerm(sum), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(p_0.impTerm(p_0));
-  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
-  TS_ASSERT_THROWS_NOTHING(p_f_x.impTerm(b));
-  TS_ASSERT_THROWS(p_f_x.impTerm(x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.impTerm(f), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.impTerm(p), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.impTerm(zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.impTerm(f_x), CVC4ApiException&);
-  TS_ASSERT_THROWS(p_f_x.impTerm(sum), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(p_f_x.impTerm(p_0));
-  TS_ASSERT_THROWS_NOTHING(p_f_x.impTerm(p_f_x));
-}
-
-void TermBlack::testIteTerm()
-{
-  Sort bvSort = d_solver.mkBitVectorSort(8);
-  Sort intSort = d_solver.getIntegerSort();
-  Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
-
-  Term b = d_solver.mkTrue();
-  TS_ASSERT_THROWS(Term().iteTerm(b, b), CVC4ApiException&);
-  TS_ASSERT_THROWS(b.iteTerm(Term(), b), CVC4ApiException&);
-  TS_ASSERT_THROWS(b.iteTerm(b, Term()), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b));
-  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
-  TS_ASSERT_THROWS_NOTHING(b.iteTerm(x, x));
-  TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b));
-  TS_ASSERT_THROWS(b.iteTerm(x, b), CVC4ApiException&);
-  TS_ASSERT_THROWS(x.iteTerm(x, x), CVC4ApiException&);
-  TS_ASSERT_THROWS(x.iteTerm(x, b), CVC4ApiException&);
-  Term f = d_solver.mkVar(funSort1, "f");
-  TS_ASSERT_THROWS(f.iteTerm(b, b), CVC4ApiException&);
-  TS_ASSERT_THROWS(x.iteTerm(b, x), CVC4ApiException&);
-  Term p = d_solver.mkVar(funSort2, "p");
-  TS_ASSERT_THROWS(p.iteTerm(b, b), CVC4ApiException&);
-  TS_ASSERT_THROWS(p.iteTerm(x, b), CVC4ApiException&);
-  Term zero = d_solver.mkInteger(0);
-  TS_ASSERT_THROWS(zero.iteTerm(x, x), CVC4ApiException&);
-  TS_ASSERT_THROWS(zero.iteTerm(x, b), CVC4ApiException&);
-  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
-  TS_ASSERT_THROWS(f_x.iteTerm(b, b), CVC4ApiException&);
-  TS_ASSERT_THROWS(f_x.iteTerm(b, x), CVC4ApiException&);
-  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
-  TS_ASSERT_THROWS(sum.iteTerm(x, x), CVC4ApiException&);
-  TS_ASSERT_THROWS(sum.iteTerm(b, x), CVC4ApiException&);
-  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
-  TS_ASSERT_THROWS_NOTHING(p_0.iteTerm(b, b));
-  TS_ASSERT_THROWS_NOTHING(p_0.iteTerm(x, x));
-  TS_ASSERT_THROWS(p_0.iteTerm(x, b), CVC4ApiException&);
-  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
-  TS_ASSERT_THROWS_NOTHING(p_f_x.iteTerm(b, b));
-  TS_ASSERT_THROWS_NOTHING(p_f_x.iteTerm(x, x));
-  TS_ASSERT_THROWS(p_f_x.iteTerm(x, b), CVC4ApiException&);
-}
-
-void TermBlack::testTermAssignment()
-{
-  Term t1 = d_solver.mkInteger(1);
-  Term t2 = t1;
-  t2 = d_solver.mkInteger(2);
-  TS_ASSERT_EQUALS(t1, d_solver.mkInteger(1));
-}
-
-void TermBlack::testTermCompare()
-{
-  Term t1 = d_solver.mkInteger(1);
-  Term t2 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
-  Term t3 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
-  TS_ASSERT(t2 >= t3);
-  TS_ASSERT(t2 <= t3);
-  TS_ASSERT((t1 > t2) != (t1 < t2));
-  TS_ASSERT((t1 > t2 || t1 == t2) == (t1 >= t2));
-}
-
-void TermBlack::testTermChildren()
-{
-  // simple term 2+3
-  Term two = d_solver.mkInteger(2);
-  Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3));
-  TS_ASSERT(t1[0] == two);
-  TS_ASSERT(t1.getNumChildren() == 2);
-  Term tnull;
-  TS_ASSERT_THROWS(tnull.getNumChildren(), CVC4ApiException&);
-
-  // apply term f(2)
-  Sort intSort = d_solver.getIntegerSort();
-  Sort fsort = d_solver.mkFunctionSort(intSort, intSort);
-  Term f = d_solver.mkConst(fsort, "f");
-  Term t2 = d_solver.mkTerm(APPLY_UF, f, two);
-  // due to our higher-order view of terms, we treat f as a child of APPLY_UF
-  TS_ASSERT(t2.getNumChildren() == 2);
-  TS_ASSERT_EQUALS(t2[0], f);
-  TS_ASSERT_EQUALS(t2[1], two);
-  TS_ASSERT_THROWS(tnull[0], CVC4ApiException&);
-}
-
-void TermBlack::testSubstitute()
-{
-  Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
-  Term one = d_solver.mkInteger(1);
-  Term ttrue = d_solver.mkTrue();
-  Term xpx = d_solver.mkTerm(PLUS, x, x);
-  Term onepone = d_solver.mkTerm(PLUS, one, one);
-
-  TS_ASSERT_EQUALS(xpx.substitute(x, one), onepone);
-  TS_ASSERT_EQUALS(onepone.substitute(one, x), xpx);
-  // incorrect due to type
-  TS_ASSERT_THROWS(xpx.substitute(one, ttrue), CVC4ApiException&);
-
-  // simultaneous substitution
-  Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y");
-  Term xpy = d_solver.mkTerm(PLUS, x, y);
-  Term xpone = d_solver.mkTerm(PLUS, y, one);
-  std::vector<Term> es;
-  std::vector<Term> rs;
-  es.push_back(x);
-  rs.push_back(y);
-  es.push_back(y);
-  rs.push_back(one);
-  TS_ASSERT_EQUALS(xpy.substitute(es, rs), xpone);
-
-  // incorrect substitution due to arity
-  rs.pop_back();
-  TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&);
-
-  // incorrect substitution due to types
-  rs.push_back(ttrue);
-  TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&);
-
-  // null cannot substitute
-  Term tnull;
-  TS_ASSERT_THROWS(tnull.substitute(one, x), CVC4ApiException&);
-  TS_ASSERT_THROWS(xpx.substitute(tnull, x), CVC4ApiException&);
-  TS_ASSERT_THROWS(xpx.substitute(x, tnull), CVC4ApiException&);
-  rs.pop_back();
-  rs.push_back(tnull);
-  TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&);
-  es.clear();
-  rs.clear();
-  es.push_back(x);
-  rs.push_back(y);
-  TS_ASSERT_THROWS(tnull.substitute(es, rs), CVC4ApiException&);
-  es.push_back(tnull);
-  rs.push_back(one);
-  TS_ASSERT_THROWS(xpx.substitute(es, rs), CVC4ApiException&);
-}
-
-void TermBlack::testConstArray()
-{
-  Sort intsort = d_solver.getIntegerSort();
-  Sort arrsort = d_solver.mkArraySort(intsort, intsort);
-  Term a = d_solver.mkConst(arrsort, "a");
-  Term one = d_solver.mkInteger(1);
-  Term constarr = d_solver.mkConstArray(arrsort, one);
-
-  TS_ASSERT_EQUALS(constarr.getKind(), CONST_ARRAY);
-  TS_ASSERT_EQUALS(constarr.getConstArrayBase(), one);
-  TS_ASSERT_THROWS(a.getConstArrayBase(), CVC4ApiException&);
-
-  arrsort =
-      d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort());
-  Term zero_array = d_solver.mkConstArray(arrsort, d_solver.mkReal(0));
-  Term stores = d_solver.mkTerm(
-      STORE, zero_array, d_solver.mkReal(1), d_solver.mkReal(2));
-  stores =
-      d_solver.mkTerm(STORE, stores, d_solver.mkReal(2), d_solver.mkReal(3));
-  stores =
-      d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5));
-}
-
-void TermBlack::testConstSequenceElements()
-{
-  Sort realsort = d_solver.getRealSort();
-  Sort seqsort = d_solver.mkSequenceSort(realsort);
-  Term s = d_solver.mkEmptySequence(seqsort);
-
-
-  TS_ASSERT_EQUALS(s.getKind(), CONST_SEQUENCE);
-  // empty sequence has zero elements
-  std::vector<Term> cs = s.getConstSequenceElements();
-  TS_ASSERT(cs.empty());
-
-  // A seq.unit app is not a constant sequence (regardless of whether it is
-  // applied to a constant).
-  Term su = d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1));
-  TS_ASSERT_THROWS(su.getConstSequenceElements(), CVC4ApiException&);
-}
-
-void TermBlack::testTermScopedToString()
-{
-  Sort intsort = d_solver.getIntegerSort();
-  Term x = d_solver.mkConst(intsort, "x");
-  TS_ASSERT_EQUALS(x.toString(), "x");
-  Solver solver2;
-  TS_ASSERT_EQUALS(x.toString(), "x");
-}