google test: api: Migrate solver_black. (#5570)

3 files changed, 2262 insertions, 2487 deletions

diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 056f9d891..f6408606d 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -15,6 +15,6 @@ cvc4_add_unit_test_black(datatype_api_black api)
 cvc4_add_unit_test_black(grammar_black api)
 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_unit_test_black(solver_black api)
 cvc4_add_cxx_unit_test_black(sort_black api)
-cvc4_add_unit_test_black(term_black api)
\ No newline at end of file
+cvc4_add_unit_test_black(term_black api)
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
new file mode 100644
index 000000000..e7610265e
--- /dev/null
+++ b/test/unit/api/solver_black.cpp
@@ -0,0 +1,2260 @@
+/*********************                                                        */
+/*! \file solver_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Andres Noetzli, Abdalrhman Mohamed
+ ** 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 Solver class of the  C++ API.
+ **
+ ** Black box testing of the Solver class of the  C++ API.
+ **/
+
+#include "base/configuration.h"
+#include "test_api.h"
+
+namespace CVC4 {
+
+using namespace api;
+
+namespace test {
+
+class TestApiSolverBlack : public TestApi
+{
+};
+
+TEST_F(TestApiSolverBlack, recoverableException)
+{
+  d_solver.setOption("produce-models", "true");
+  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+  d_solver.assertFormula(x.eqTerm(x).notTerm());
+  ASSERT_THROW(d_solver.getValue(x), CVC4ApiRecoverableException);
+}
+
+TEST_F(TestApiSolverBlack, supportsFloatingPoint)
+{
+  if (d_solver.supportsFloatingPoint())
+  {
+    ASSERT_NO_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN));
+  }
+  else
+  {
+    ASSERT_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN),
+                 CVC4ApiException);
+  }
+}
+
+TEST_F(TestApiSolverBlack, getBooleanSort)
+{
+  ASSERT_NO_THROW(d_solver.getBooleanSort());
+}
+
+TEST_F(TestApiSolverBlack, getIntegerSort)
+{
+  ASSERT_NO_THROW(d_solver.getIntegerSort());
+}
+
+TEST_F(TestApiSolverBlack, getNullSort)
+{
+  ASSERT_NO_THROW(d_solver.getNullSort());
+}
+
+TEST_F(TestApiSolverBlack, getRealSort)
+{
+  ASSERT_NO_THROW(d_solver.getRealSort());
+}
+
+TEST_F(TestApiSolverBlack, getRegExpSort)
+{
+  ASSERT_NO_THROW(d_solver.getRegExpSort());
+}
+
+TEST_F(TestApiSolverBlack, getStringSort)
+{
+  ASSERT_NO_THROW(d_solver.getStringSort());
+}
+
+TEST_F(TestApiSolverBlack, getRoundingModeSort)
+{
+  if (d_solver.supportsFloatingPoint())
+  {
+    ASSERT_NO_THROW(d_solver.getRoundingModeSort());
+  }
+  else
+  {
+    ASSERT_THROW(d_solver.getRoundingModeSort(), CVC4ApiException);
+  }
+}
+
+TEST_F(TestApiSolverBlack, mkArraySort)
+{
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort intSort = d_solver.getIntegerSort();
+  Sort realSort = d_solver.getRealSort();
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  ASSERT_NO_THROW(d_solver.mkArraySort(boolSort, boolSort));
+  ASSERT_NO_THROW(d_solver.mkArraySort(intSort, intSort));
+  ASSERT_NO_THROW(d_solver.mkArraySort(realSort, realSort));
+  ASSERT_NO_THROW(d_solver.mkArraySort(bvSort, bvSort));
+  ASSERT_NO_THROW(d_solver.mkArraySort(boolSort, intSort));
+  ASSERT_NO_THROW(d_solver.mkArraySort(realSort, bvSort));
+
+  if (d_solver.supportsFloatingPoint())
+  {
+    Sort fpSort = d_solver.mkFloatingPointSort(3, 5);
+    ASSERT_NO_THROW(d_solver.mkArraySort(fpSort, fpSort));
+    ASSERT_NO_THROW(d_solver.mkArraySort(bvSort, fpSort));
+  }
+
+  Solver slv;
+  ASSERT_THROW(slv.mkArraySort(boolSort, boolSort), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkBitVectorSort)
+{
+  ASSERT_NO_THROW(d_solver.mkBitVectorSort(32));
+  ASSERT_THROW(d_solver.mkBitVectorSort(0), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkFloatingPointSort)
+{
+  if (d_solver.supportsFloatingPoint())
+  {
+    ASSERT_NO_THROW(d_solver.mkFloatingPointSort(4, 8));
+    ASSERT_THROW(d_solver.mkFloatingPointSort(0, 8), CVC4ApiException);
+    ASSERT_THROW(d_solver.mkFloatingPointSort(4, 0), CVC4ApiException);
+  }
+  else
+  {
+    ASSERT_THROW(d_solver.mkFloatingPointSort(4, 8), CVC4ApiException);
+  }
+}
+
+TEST_F(TestApiSolverBlack, mkDatatypeSort)
+{
+  DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+  cons.addSelector("head", d_solver.getIntegerSort());
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+  dtypeSpec.addConstructor(nil);
+  ASSERT_NO_THROW(d_solver.mkDatatypeSort(dtypeSpec));
+
+  Solver slv;
+  ASSERT_THROW(slv.mkDatatypeSort(dtypeSpec), CVC4ApiException);
+
+  DatatypeDecl throwsDtypeSpec = d_solver.mkDatatypeDecl("list");
+  ASSERT_THROW(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkDatatypeSorts)
+{
+  Solver slv;
+
+  DatatypeDecl dtypeSpec1 = d_solver.mkDatatypeDecl("list1");
+  DatatypeConstructorDecl cons1 = d_solver.mkDatatypeConstructorDecl("cons1");
+  cons1.addSelector("head1", d_solver.getIntegerSort());
+  dtypeSpec1.addConstructor(cons1);
+  DatatypeConstructorDecl nil1 = d_solver.mkDatatypeConstructorDecl("nil1");
+  dtypeSpec1.addConstructor(nil1);
+  DatatypeDecl dtypeSpec2 = d_solver.mkDatatypeDecl("list2");
+  DatatypeConstructorDecl cons2 = d_solver.mkDatatypeConstructorDecl("cons2");
+  cons2.addSelector("head2", d_solver.getIntegerSort());
+  dtypeSpec2.addConstructor(cons2);
+  DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil2");
+  dtypeSpec2.addConstructor(nil2);
+  std::vector<DatatypeDecl> decls = {dtypeSpec1, dtypeSpec2};
+  ASSERT_NO_THROW(d_solver.mkDatatypeSorts(decls));
+
+  ASSERT_THROW(slv.mkDatatypeSorts(decls), CVC4ApiException);
+
+  DatatypeDecl throwsDtypeSpec = d_solver.mkDatatypeDecl("list");
+  std::vector<DatatypeDecl> throwsDecls = {throwsDtypeSpec};
+  ASSERT_THROW(d_solver.mkDatatypeSorts(throwsDecls), CVC4ApiException);
+
+  /* with unresolved sorts */
+  Sort unresList = d_solver.mkUninterpretedSort("ulist");
+  std::set<Sort> unresSorts = {unresList};
+  DatatypeDecl ulist = d_solver.mkDatatypeDecl("ulist");
+  DatatypeConstructorDecl ucons = d_solver.mkDatatypeConstructorDecl("ucons");
+  ucons.addSelector("car", unresList);
+  ucons.addSelector("cdr", unresList);
+  ulist.addConstructor(ucons);
+  DatatypeConstructorDecl unil = d_solver.mkDatatypeConstructorDecl("unil");
+  ulist.addConstructor(unil);
+  std::vector<DatatypeDecl> udecls = {ulist};
+  ASSERT_NO_THROW(d_solver.mkDatatypeSorts(udecls, unresSorts));
+
+  ASSERT_THROW(slv.mkDatatypeSorts(udecls, unresSorts), CVC4ApiException);
+
+  /* Note: More tests are in datatype_api_black. */
+}
+
+TEST_F(TestApiSolverBlack, mkFunctionSort)
+{
+  ASSERT_NO_THROW(d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                          d_solver.getIntegerSort()));
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  ASSERT_THROW(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort),
+               CVC4ApiException);
+  ASSERT_NO_THROW(d_solver.mkFunctionSort(
+      {d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()},
+      d_solver.getIntegerSort()));
+  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                          d_solver.getIntegerSort());
+  ASSERT_THROW(
+      d_solver.mkFunctionSort({funSort2, d_solver.mkUninterpretedSort("u")},
+                              d_solver.getIntegerSort()),
+      CVC4ApiException);
+  ASSERT_THROW(d_solver.mkFunctionSort({d_solver.getIntegerSort(),
+                                        d_solver.mkUninterpretedSort("u")},
+                                       funSort2),
+               CVC4ApiException);
+
+  Solver slv;
+  ASSERT_THROW(slv.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                  d_solver.getIntegerSort()),
+               CVC4ApiException);
+  ASSERT_THROW(slv.mkFunctionSort(slv.mkUninterpretedSort("u"),
+                                  d_solver.getIntegerSort()),
+               CVC4ApiException);
+  std::vector<Sort> sorts1 = {d_solver.getBooleanSort(),
+                              slv.getIntegerSort(),
+                              d_solver.getIntegerSort()};
+  std::vector<Sort> sorts2 = {slv.getBooleanSort(), slv.getIntegerSort()};
+  ASSERT_NO_THROW(slv.mkFunctionSort(sorts2, slv.getIntegerSort()));
+  ASSERT_THROW(slv.mkFunctionSort(sorts1, slv.getIntegerSort()),
+               CVC4ApiException);
+  ASSERT_THROW(slv.mkFunctionSort(sorts2, d_solver.getIntegerSort()),
+               CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkParamSort)
+{
+  ASSERT_NO_THROW(d_solver.mkParamSort("T"));
+  ASSERT_NO_THROW(d_solver.mkParamSort(""));
+}
+
+TEST_F(TestApiSolverBlack, mkPredicateSort)
+{
+  ASSERT_NO_THROW(d_solver.mkPredicateSort({d_solver.getIntegerSort()}));
+  ASSERT_THROW(d_solver.mkPredicateSort({}), CVC4ApiException);
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  ASSERT_THROW(d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort}),
+               CVC4ApiException);
+
+  Solver slv;
+  ASSERT_THROW(slv.mkPredicateSort({d_solver.getIntegerSort()}),
+               CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkRecordSort)
+{
+  std::vector<std::pair<std::string, Sort>> fields = {
+      std::make_pair("b", d_solver.getBooleanSort()),
+      std::make_pair("bv", d_solver.mkBitVectorSort(8)),
+      std::make_pair("i", d_solver.getIntegerSort())};
+  std::vector<std::pair<std::string, Sort>> empty;
+  ASSERT_NO_THROW(d_solver.mkRecordSort(fields));
+  ASSERT_NO_THROW(d_solver.mkRecordSort(empty));
+  Sort recSort = d_solver.mkRecordSort(fields);
+  ASSERT_NO_THROW(recSort.getDatatype());
+
+  Solver slv;
+  ASSERT_THROW(slv.mkRecordSort(fields), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkSetSort)
+{
+  ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.getBooleanSort()));
+  ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.getIntegerSort()));
+  ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.mkBitVectorSort(4)));
+  Solver slv;
+  ASSERT_THROW(slv.mkSetSort(d_solver.mkBitVectorSort(4)), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkBagSort)
+{
+  ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.getBooleanSort()));
+  ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.getIntegerSort()));
+  ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.mkBitVectorSort(4)));
+  Solver slv;
+  ASSERT_THROW(slv.mkBagSort(d_solver.mkBitVectorSort(4)), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkSequenceSort)
+{
+  ASSERT_NO_THROW(d_solver.mkSequenceSort(d_solver.getBooleanSort()));
+  ASSERT_NO_THROW(d_solver.mkSequenceSort(
+      d_solver.mkSequenceSort(d_solver.getIntegerSort())));
+  Solver slv;
+  ASSERT_THROW(slv.mkSequenceSort(d_solver.getIntegerSort()), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkUninterpretedSort)
+{
+  ASSERT_NO_THROW(d_solver.mkUninterpretedSort("u"));
+  ASSERT_NO_THROW(d_solver.mkUninterpretedSort(""));
+}
+
+TEST_F(TestApiSolverBlack, mkSortConstructorSort)
+{
+  ASSERT_NO_THROW(d_solver.mkSortConstructorSort("s", 2));
+  ASSERT_NO_THROW(d_solver.mkSortConstructorSort("", 2));
+  ASSERT_THROW(d_solver.mkSortConstructorSort("", 0), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkTupleSort)
+{
+  ASSERT_NO_THROW(d_solver.mkTupleSort({d_solver.getIntegerSort()}));
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  ASSERT_THROW(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}),
+               CVC4ApiException);
+
+  Solver slv;
+  ASSERT_THROW(slv.mkTupleSort({d_solver.getIntegerSort()}), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkBitVector)
+{
+  uint32_t size0 = 0, size1 = 8, size2 = 32, val1 = 2;
+  uint64_t val2 = 2;
+  ASSERT_NO_THROW(d_solver.mkBitVector(size1, val1));
+  ASSERT_NO_THROW(d_solver.mkBitVector(size2, val2));
+  ASSERT_NO_THROW(d_solver.mkBitVector("1010", 2));
+  ASSERT_NO_THROW(d_solver.mkBitVector("1010", 10));
+  ASSERT_NO_THROW(d_solver.mkBitVector("1234", 10));
+  ASSERT_NO_THROW(d_solver.mkBitVector("1010", 16));
+  ASSERT_NO_THROW(d_solver.mkBitVector("a09f", 16));
+  ASSERT_NO_THROW(d_solver.mkBitVector(8, "-127", 10));
+  ASSERT_THROW(d_solver.mkBitVector(size0, val1), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkBitVector(size0, val2), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkBitVector("", 2), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkBitVector("10", 3), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkBitVector("20", 2), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkBitVector(8, "101010101", 2), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkBitVector(8, "-256", 10), CVC4ApiException);
+  EXPECT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("10", 10));
+  EXPECT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("a", 16));
+  EXPECT_EQ(d_solver.mkBitVector(8, "01010101", 2).toString(), "#b01010101");
+  EXPECT_EQ(d_solver.mkBitVector(8, "F", 16).toString(), "#b00001111");
+  EXPECT_EQ(d_solver.mkBitVector(8, "-1", 10),
+            d_solver.mkBitVector(8, "FF", 16));
+}
+
+TEST_F(TestApiSolverBlack, mkVar)
+{
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort intSort = d_solver.getIntegerSort();
+  Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
+  ASSERT_NO_THROW(d_solver.mkVar(boolSort));
+  ASSERT_NO_THROW(d_solver.mkVar(funSort));
+  ASSERT_NO_THROW(d_solver.mkVar(boolSort, std::string("b")));
+  ASSERT_NO_THROW(d_solver.mkVar(funSort, ""));
+  ASSERT_THROW(d_solver.mkVar(Sort()), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkVar(Sort(), "a"), CVC4ApiException);
+  Solver slv;
+  ASSERT_THROW(slv.mkVar(boolSort, "x"), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkBoolean)
+{
+  ASSERT_NO_THROW(d_solver.mkBoolean(true));
+  ASSERT_NO_THROW(d_solver.mkBoolean(false));
+}
+
+TEST_F(TestApiSolverBlack, mkRoundingMode)
+{
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
+  }
+  else
+  {
+    ASSERT_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO),
+                 CVC4ApiException);
+  }
+}
+
+TEST_F(TestApiSolverBlack, mkUninterpretedConst)
+{
+  ASSERT_NO_THROW(d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
+  ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC4ApiException);
+  Solver slv;
+  ASSERT_THROW(slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1),
+               CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkAbstractValue)
+{
+  ASSERT_NO_THROW(d_solver.mkAbstractValue(std::string("1")));
+  ASSERT_THROW(d_solver.mkAbstractValue(std::string("0")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkAbstractValue(std::string("-1")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkAbstractValue(std::string("1.2")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkAbstractValue("1/2"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkAbstractValue("asdf"), CVC4ApiException);
+
+  ASSERT_NO_THROW(d_solver.mkAbstractValue((uint32_t)1));
+  ASSERT_NO_THROW(d_solver.mkAbstractValue((int32_t)1));
+  ASSERT_NO_THROW(d_solver.mkAbstractValue((uint64_t)1));
+  ASSERT_NO_THROW(d_solver.mkAbstractValue((int64_t)1));
+  ASSERT_NO_THROW(d_solver.mkAbstractValue((int32_t)-1));
+  ASSERT_NO_THROW(d_solver.mkAbstractValue((int64_t)-1));
+  ASSERT_THROW(d_solver.mkAbstractValue(0), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkFloatingPoint)
+{
+  Term t1 = d_solver.mkBitVector(8);
+  Term t2 = d_solver.mkBitVector(4);
+  Term t3 = d_solver.mkInteger(2);
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    ASSERT_NO_THROW(d_solver.mkFloatingPoint(3, 5, t1));
+  }
+  else
+  {
+    ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t1), CVC4ApiException);
+  }
+  ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, Term()), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, t1), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkFloatingPoint(3, 0, t1), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC4ApiException);
+
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    Solver slv;
+    ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC4ApiException);
+  }
+}
+
+TEST_F(TestApiSolverBlack, mkEmptySet)
+{
+  Solver slv;
+  Sort s = d_solver.mkSetSort(d_solver.getBooleanSort());
+  ASSERT_NO_THROW(d_solver.mkEmptySet(Sort()));
+  ASSERT_NO_THROW(d_solver.mkEmptySet(s));
+  ASSERT_THROW(d_solver.mkEmptySet(d_solver.getBooleanSort()),
+               CVC4ApiException);
+  ASSERT_THROW(slv.mkEmptySet(s), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkEmptyBag)
+{
+  Solver slv;
+  Sort s = d_solver.mkBagSort(d_solver.getBooleanSort());
+  ASSERT_NO_THROW(d_solver.mkEmptyBag(Sort()));
+  ASSERT_NO_THROW(d_solver.mkEmptyBag(s));
+  ASSERT_THROW(d_solver.mkEmptyBag(d_solver.getBooleanSort()),
+               CVC4ApiException);
+  ASSERT_THROW(slv.mkEmptyBag(s), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkEmptySequence)
+{
+  Solver slv;
+  Sort s = d_solver.mkSequenceSort(d_solver.getBooleanSort());
+  ASSERT_NO_THROW(d_solver.mkEmptySequence(s));
+  ASSERT_NO_THROW(d_solver.mkEmptySequence(d_solver.getBooleanSort()));
+  ASSERT_THROW(slv.mkEmptySequence(s), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkFalse)
+{
+  ASSERT_NO_THROW(d_solver.mkFalse());
+  ASSERT_NO_THROW(d_solver.mkFalse());
+}
+
+TEST_F(TestApiSolverBlack, mkNaN)
+{
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    ASSERT_NO_THROW(d_solver.mkNaN(3, 5));
+  }
+  else
+  {
+    ASSERT_THROW(d_solver.mkNaN(3, 5), CVC4ApiException);
+  }
+}
+
+TEST_F(TestApiSolverBlack, mkNegZero)
+{
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    ASSERT_NO_THROW(d_solver.mkNegZero(3, 5));
+  }
+  else
+  {
+    ASSERT_THROW(d_solver.mkNegZero(3, 5), CVC4ApiException);
+  }
+}
+
+TEST_F(TestApiSolverBlack, mkNegInf)
+{
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    ASSERT_NO_THROW(d_solver.mkNegInf(3, 5));
+  }
+  else
+  {
+    ASSERT_THROW(d_solver.mkNegInf(3, 5), CVC4ApiException);
+  }
+}
+
+TEST_F(TestApiSolverBlack, mkPosInf)
+{
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    ASSERT_NO_THROW(d_solver.mkPosInf(3, 5));
+  }
+  else
+  {
+    ASSERT_THROW(d_solver.mkPosInf(3, 5), CVC4ApiException);
+  }
+}
+
+TEST_F(TestApiSolverBlack, mkPosZero)
+{
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    ASSERT_NO_THROW(d_solver.mkPosZero(3, 5));
+  }
+  else
+  {
+    ASSERT_THROW(d_solver.mkPosZero(3, 5), CVC4ApiException);
+  }
+}
+
+TEST_F(TestApiSolverBlack, mkOp)
+{
+  // mkOp(Kind kind, Kind k)
+  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, EQUAL), CVC4ApiException);
+
+  // mkOp(Kind kind, const std::string& arg)
+  ASSERT_NO_THROW(d_solver.mkOp(RECORD_UPDATE, "asdf"));
+  ASSERT_NO_THROW(d_solver.mkOp(DIVISIBLE, "2147483648"));
+  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, "asdf"), CVC4ApiException);
+
+  // mkOp(Kind kind, uint32_t arg)
+  ASSERT_NO_THROW(d_solver.mkOp(DIVISIBLE, 1));
+  ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 1));
+  ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 1));
+  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, 1), CVC4ApiException);
+
+  // mkOp(Kind kind, uint32_t arg1, uint32_t arg2)
+  ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, 1, 1));
+  ASSERT_THROW(d_solver.mkOp(DIVISIBLE, 1, 2), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkPi) { ASSERT_NO_THROW(d_solver.mkPi()); }
+
+TEST_F(TestApiSolverBlack, mkInteger)
+{
+  ASSERT_NO_THROW(d_solver.mkInteger("123"));
+  ASSERT_THROW(d_solver.mkInteger("1.23"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger("1/23"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger("12/3"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger(".2"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger("2."), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger(""), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger("asdf"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger("1.2/3"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger("."), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger("/"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger("2/"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger("/2"), CVC4ApiException);
+
+  ASSERT_NO_THROW(d_solver.mkReal(std::string("123")));
+  ASSERT_THROW(d_solver.mkInteger(std::string("1.23")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("1/23")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("12/3")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string(".2")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("2.")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("asdf")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("1.2/3")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string(".")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("/")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("2/")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("/2")), CVC4ApiException);
+
+  int32_t val1 = 1;
+  int64_t val2 = -1;
+  uint32_t val3 = 1;
+  uint64_t val4 = -1;
+  ASSERT_NO_THROW(d_solver.mkInteger(val1));
+  ASSERT_NO_THROW(d_solver.mkInteger(val2));
+  ASSERT_NO_THROW(d_solver.mkInteger(val3));
+  ASSERT_NO_THROW(d_solver.mkInteger(val4));
+  ASSERT_NO_THROW(d_solver.mkInteger(val4));
+}
+
+TEST_F(TestApiSolverBlack, mkReal)
+{
+  ASSERT_NO_THROW(d_solver.mkReal("123"));
+  ASSERT_NO_THROW(d_solver.mkReal("1.23"));
+  ASSERT_NO_THROW(d_solver.mkReal("1/23"));
+  ASSERT_NO_THROW(d_solver.mkReal("12/3"));
+  ASSERT_NO_THROW(d_solver.mkReal(".2"));
+  ASSERT_NO_THROW(d_solver.mkReal("2."));
+  ASSERT_THROW(d_solver.mkReal(""), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkReal("asdf"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkReal("1.2/3"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkReal("."), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkReal("/"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkReal("2/"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkReal("/2"), CVC4ApiException);
+
+  ASSERT_NO_THROW(d_solver.mkReal(std::string("123")));
+  ASSERT_NO_THROW(d_solver.mkReal(std::string("1.23")));
+  ASSERT_NO_THROW(d_solver.mkReal(std::string("1/23")));
+  ASSERT_NO_THROW(d_solver.mkReal(std::string("12/3")));
+  ASSERT_NO_THROW(d_solver.mkReal(std::string(".2")));
+  ASSERT_NO_THROW(d_solver.mkReal(std::string("2.")));
+  ASSERT_THROW(d_solver.mkReal(std::string("")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkReal(std::string("asdf")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkReal(std::string("1.2/3")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkReal(std::string(".")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkReal(std::string("/")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkReal(std::string("2/")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkReal(std::string("/2")), CVC4ApiException);
+
+  int32_t val1 = 1;
+  int64_t val2 = -1;
+  uint32_t val3 = 1;
+  uint64_t val4 = -1;
+  ASSERT_NO_THROW(d_solver.mkReal(val1));
+  ASSERT_NO_THROW(d_solver.mkReal(val2));
+  ASSERT_NO_THROW(d_solver.mkReal(val3));
+  ASSERT_NO_THROW(d_solver.mkReal(val4));
+  ASSERT_NO_THROW(d_solver.mkReal(val4));
+  ASSERT_NO_THROW(d_solver.mkReal(val1, val1));
+  ASSERT_NO_THROW(d_solver.mkReal(val2, val2));
+  ASSERT_NO_THROW(d_solver.mkReal(val3, val3));
+  ASSERT_NO_THROW(d_solver.mkReal(val4, val4));
+}
+
+TEST_F(TestApiSolverBlack, mkRegexpEmpty)
+{
+  Sort strSort = d_solver.getStringSort();
+  Term s = d_solver.mkConst(strSort, "s");
+  ASSERT_NO_THROW(
+      d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty()));
+}
+
+TEST_F(TestApiSolverBlack, mkRegexpSigma)
+{
+  Sort strSort = d_solver.getStringSort();
+  Term s = d_solver.mkConst(strSort, "s");
+  ASSERT_NO_THROW(
+      d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
+}
+
+TEST_F(TestApiSolverBlack, mkSepNil)
+{
+  ASSERT_NO_THROW(d_solver.mkSepNil(d_solver.getBooleanSort()));
+  ASSERT_THROW(d_solver.mkSepNil(Sort()), CVC4ApiException);
+  Solver slv;
+  ASSERT_THROW(slv.mkSepNil(d_solver.getIntegerSort()), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkString)
+{
+  ASSERT_NO_THROW(d_solver.mkString(""));
+  ASSERT_NO_THROW(d_solver.mkString("asdfasdf"));
+  EXPECT_EQ(d_solver.mkString("asdf\\nasdf").toString(),
+            "\"asdf\\u{5c}nasdf\"");
+  EXPECT_EQ(d_solver.mkString("asdf\\u{005c}nasdf", true).toString(),
+            "\"asdf\\u{5c}nasdf\"");
+}
+
+TEST_F(TestApiSolverBlack, mkChar)
+{
+  ASSERT_NO_THROW(d_solver.mkChar(std::string("0123")));
+  ASSERT_NO_THROW(d_solver.mkChar("aA"));
+  ASSERT_THROW(d_solver.mkChar(""), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkChar("0g0"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkChar("100000"), CVC4ApiException);
+  EXPECT_EQ(d_solver.mkChar("abc"), d_solver.mkChar("ABC"));
+}
+
+TEST_F(TestApiSolverBlack, mkTerm)
+{
+  Sort bv32 = d_solver.mkBitVectorSort(32);
+  Term a = d_solver.mkConst(bv32, "a");
+  Term b = d_solver.mkConst(bv32, "b");
+  std::vector<Term> v1 = {a, b};
+  std::vector<Term> v2 = {a, Term()};
+  std::vector<Term> v3 = {a, d_solver.mkTrue()};
+  std::vector<Term> v4 = {d_solver.mkInteger(1), d_solver.mkInteger(2)};
+  std::vector<Term> v5 = {d_solver.mkInteger(1), Term()};
+  std::vector<Term> v6 = {};
+  Solver slv;
+
+  // mkTerm(Kind kind) const
+  ASSERT_NO_THROW(d_solver.mkTerm(PI));
+  ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_EMPTY));
+  ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_SIGMA));
+  ASSERT_THROW(d_solver.mkTerm(CONST_BITVECTOR), CVC4ApiException);
+
+  // mkTerm(Kind kind, Term child) const
+  ASSERT_NO_THROW(d_solver.mkTerm(NOT, d_solver.mkTrue()));
+  ASSERT_THROW(d_solver.mkTerm(NOT, Term()), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(NOT, a), CVC4ApiException);
+  ASSERT_THROW(slv.mkTerm(NOT, d_solver.mkTrue()), CVC4ApiException);
+
+  // mkTerm(Kind kind, Term child1, Term child2) const
+  ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, a, b));
+  ASSERT_THROW(d_solver.mkTerm(EQUAL, Term(), b), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(EQUAL, a, Term()), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(EQUAL, a, d_solver.mkTrue()), CVC4ApiException);
+  ASSERT_THROW(slv.mkTerm(EQUAL, a, b), CVC4ApiException);
+
+  // mkTerm(Kind kind, Term child1, Term child2, Term child3) const
+  ASSERT_NO_THROW(d_solver.mkTerm(
+      ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue()));
+  ASSERT_THROW(
+      d_solver.mkTerm(ITE, Term(), d_solver.mkTrue(), d_solver.mkTrue()),
+      CVC4ApiException);
+  ASSERT_THROW(
+      d_solver.mkTerm(ITE, d_solver.mkTrue(), Term(), d_solver.mkTrue()),
+      CVC4ApiException);
+  ASSERT_THROW(
+      d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), Term()),
+      CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), b),
+               CVC4ApiException);
+  ASSERT_THROW(
+      slv.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue()),
+      CVC4ApiException);
+
+  // mkTerm(Kind kind, const std::vector<Term>& children) const
+  ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, v1));
+  ASSERT_THROW(d_solver.mkTerm(EQUAL, v2), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(EQUAL, v3), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(DISTINCT, v6), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkTermFromOp)
+{
+  Sort bv32 = d_solver.mkBitVectorSort(32);
+  Term a = d_solver.mkConst(bv32, "a");
+  Term b = d_solver.mkConst(bv32, "b");
+  std::vector<Term> v1 = {d_solver.mkInteger(1), d_solver.mkInteger(2)};
+  std::vector<Term> v2 = {d_solver.mkInteger(1), Term()};
+  std::vector<Term> v3 = {};
+  std::vector<Term> v4 = {d_solver.mkInteger(5)};
+  Solver slv;
+
+  // simple operator terms
+  Op opterm1 = d_solver.mkOp(BITVECTOR_EXTRACT, 2, 1);
+  Op opterm2 = d_solver.mkOp(DIVISIBLE, 1);
+
+  // list datatype
+  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 consTerm1 = list.getConstructorTerm("cons");
+  Term consTerm2 = list.getConstructor("cons").getConstructorTerm();
+  Term nilTerm1 = list.getConstructorTerm("nil");
+  Term nilTerm2 = list.getConstructor("nil").getConstructorTerm();
+  Term headTerm1 = list["cons"].getSelectorTerm("head");
+  Term headTerm2 = list["cons"].getSelector("head").getSelectorTerm();
+  Term tailTerm1 = list["cons"].getSelectorTerm("tail");
+  Term tailTerm2 = list["cons"]["tail"].getSelectorTerm();
+
+  // mkTerm(Op op, Term term) const
+  ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1));
+  ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm2));
+  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, nilTerm1), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, consTerm1), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm2), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm1), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, headTerm1), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm1), CVC4ApiException);
+  ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm1), CVC4ApiException);
+
+  // mkTerm(Op op, Term child) const
+  ASSERT_NO_THROW(d_solver.mkTerm(opterm1, a));
+  ASSERT_NO_THROW(d_solver.mkTerm(opterm2, d_solver.mkInteger(1)));
+  ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, headTerm1, c));
+  ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, tailTerm2, c));
+  ASSERT_THROW(d_solver.mkTerm(opterm2, a), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm1, Term()), CVC4ApiException);
+  ASSERT_THROW(
+      d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver.mkInteger(0)),
+      CVC4ApiException);
+  ASSERT_THROW(slv.mkTerm(opterm1, a), CVC4ApiException);
+
+  // mkTerm(Op op, Term child1, Term child2) const
+  ASSERT_NO_THROW(
+      d_solver.mkTerm(APPLY_CONSTRUCTOR,
+                      consTerm1,
+                      d_solver.mkInteger(0),
+                      d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
+  ASSERT_THROW(
+      d_solver.mkTerm(opterm2, d_solver.mkInteger(1), d_solver.mkInteger(2)),
+      CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm1, a, b), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm2, d_solver.mkInteger(1), Term()),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm2, Term(), d_solver.mkInteger(1)),
+               CVC4ApiException);
+  ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR,
+                          consTerm1,
+                          d_solver.mkInteger(0),
+                          d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)),
+               CVC4ApiException);
+
+  // mkTerm(Op op, Term child1, Term child2, Term child3) const
+  ASSERT_THROW(d_solver.mkTerm(opterm1, a, b, a), CVC4ApiException);
+  ASSERT_THROW(
+      d_solver.mkTerm(
+          opterm2, d_solver.mkInteger(1), d_solver.mkInteger(1), Term()),
+      CVC4ApiException);
+
+  // mkTerm(Op op, const std::vector<Term>& children) const
+  ASSERT_NO_THROW(d_solver.mkTerm(opterm2, v4));
+  ASSERT_THROW(d_solver.mkTerm(opterm2, v1), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm2, v2), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm2, v3), CVC4ApiException);
+  ASSERT_THROW(slv.mkTerm(opterm2, v4), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkTrue)
+{
+  ASSERT_NO_THROW(d_solver.mkTrue());
+  ASSERT_NO_THROW(d_solver.mkTrue());
+}
+
+TEST_F(TestApiSolverBlack, mkTuple)
+{
+  ASSERT_NO_THROW(d_solver.mkTuple({d_solver.mkBitVectorSort(3)},
+                                   {d_solver.mkBitVector("101", 2)}));
+  ASSERT_NO_THROW(
+      d_solver.mkTuple({d_solver.getRealSort()}, {d_solver.mkInteger("5")}));
+
+  ASSERT_THROW(d_solver.mkTuple({}, {d_solver.mkBitVector("101", 2)}),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTuple({d_solver.mkBitVectorSort(4)},
+                                {d_solver.mkBitVector("101", 2)}),
+               CVC4ApiException);
+  ASSERT_THROW(
+      d_solver.mkTuple({d_solver.getIntegerSort()}, {d_solver.mkReal("5.3")}),
+      CVC4ApiException);
+  Solver slv;
+  ASSERT_THROW(
+      slv.mkTuple({d_solver.mkBitVectorSort(3)}, {slv.mkBitVector("101", 2)}),
+      CVC4ApiException);
+  ASSERT_THROW(
+      slv.mkTuple({slv.mkBitVectorSort(3)}, {d_solver.mkBitVector("101", 2)}),
+      CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkUniverseSet)
+{
+  ASSERT_NO_THROW(d_solver.mkUniverseSet(d_solver.getBooleanSort()));
+  ASSERT_THROW(d_solver.mkUniverseSet(Sort()), CVC4ApiException);
+  Solver slv;
+  ASSERT_THROW(slv.mkUniverseSet(d_solver.getBooleanSort()), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkConst)
+{
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort intSort = d_solver.getIntegerSort();
+  Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
+  ASSERT_NO_THROW(d_solver.mkConst(boolSort));
+  ASSERT_NO_THROW(d_solver.mkConst(funSort));
+  ASSERT_NO_THROW(d_solver.mkConst(boolSort, std::string("b")));
+  ASSERT_NO_THROW(d_solver.mkConst(intSort, std::string("i")));
+  ASSERT_NO_THROW(d_solver.mkConst(funSort, "f"));
+  ASSERT_NO_THROW(d_solver.mkConst(funSort, ""));
+  ASSERT_THROW(d_solver.mkConst(Sort()), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkConst(Sort(), "a"), CVC4ApiException);
+
+  Solver slv;
+  ASSERT_THROW(slv.mkConst(boolSort), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkConstArray)
+{
+  Sort intSort = d_solver.getIntegerSort();
+  Sort arrSort = d_solver.mkArraySort(intSort, intSort);
+  Term zero = d_solver.mkInteger(0);
+  Term constArr = d_solver.mkConstArray(arrSort, zero);
+
+  ASSERT_NO_THROW(d_solver.mkConstArray(arrSort, zero));
+  ASSERT_THROW(d_solver.mkConstArray(Sort(), zero), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkConstArray(arrSort, Term()), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkConstArray(arrSort, d_solver.mkBitVector(1, 1)),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.mkConstArray(intSort, zero), CVC4ApiException);
+  Solver slv;
+  Term zero2 = slv.mkInteger(0);
+  Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort());
+  ASSERT_THROW(slv.mkConstArray(arrSort2, zero), CVC4ApiException);
+  ASSERT_THROW(slv.mkConstArray(arrSort, zero2), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, declareDatatype)
+{
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+  std::vector<DatatypeConstructorDecl> ctors1 = {nil};
+  ASSERT_NO_THROW(d_solver.declareDatatype(std::string("a"), ctors1));
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil");
+  std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil2};
+  ASSERT_NO_THROW(d_solver.declareDatatype(std::string("b"), ctors2));
+  DatatypeConstructorDecl cons2 = d_solver.mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl nil3 = d_solver.mkDatatypeConstructorDecl("nil");
+  std::vector<DatatypeConstructorDecl> ctors3 = {cons2, nil3};
+  ASSERT_NO_THROW(d_solver.declareDatatype(std::string(""), ctors3));
+  std::vector<DatatypeConstructorDecl> ctors4;
+  ASSERT_THROW(d_solver.declareDatatype(std::string("c"), ctors4),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.declareDatatype(std::string(""), ctors4),
+               CVC4ApiException);
+  Solver slv;
+  ASSERT_THROW(slv.declareDatatype(std::string("a"), ctors1), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, declareFun)
+{
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  ASSERT_NO_THROW(d_solver.declareFun("f1", {}, bvSort));
+  ASSERT_NO_THROW(
+      d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort));
+  ASSERT_THROW(d_solver.declareFun("f2", {}, funSort), CVC4ApiException);
+  ASSERT_THROW(d_solver.declareFun("f4", {bvSort, funSort}, bvSort),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.declareFun("f5", {bvSort, bvSort}, funSort),
+               CVC4ApiException);
+  Solver slv;
+  ASSERT_THROW(slv.declareFun("f1", {}, bvSort), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, declareSort)
+{
+  ASSERT_NO_THROW(d_solver.declareSort("s", 0));
+  ASSERT_NO_THROW(d_solver.declareSort("s", 2));
+  ASSERT_NO_THROW(d_solver.declareSort("", 2));
+}
+
+TEST_F(TestApiSolverBlack, defineFun)
+{
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
+  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                          d_solver.getIntegerSort());
+  Term b1 = d_solver.mkVar(bvSort, "b1");
+  Term b11 = d_solver.mkVar(bvSort, "b1");
+  Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
+  Term b3 = d_solver.mkVar(funSort2, "b3");
+  Term v1 = d_solver.mkConst(bvSort, "v1");
+  Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
+  Term v3 = d_solver.mkConst(funSort2, "v3");
+  Term f1 = d_solver.mkConst(funSort1, "f1");
+  Term f2 = d_solver.mkConst(funSort2, "f2");
+  Term f3 = d_solver.mkConst(bvSort, "f3");
+  ASSERT_NO_THROW(d_solver.defineFun("f", {}, bvSort, v1));
+  ASSERT_NO_THROW(d_solver.defineFun("ff", {b1, b2}, bvSort, v1));
+  ASSERT_NO_THROW(d_solver.defineFun(f1, {b1, b11}, v1));
+  ASSERT_THROW(d_solver.defineFun("ff", {v1, b2}, bvSort, v1),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFun("fff", {b1}, bvSort, v3), CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFun("ffff", {b1}, funSort2, v3),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFun(f1, {v1, b11}, v1), CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFun(f1, {b1}, v1), CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFun(f1, {b1, b11}, v2), CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFun(f1, {b1, b11}, v3), CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFun(f2, {b1}, v2), CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFun(f3, {b1}, v1), CVC4ApiException);
+
+  Solver slv;
+  Sort bvSort2 = slv.mkBitVectorSort(32);
+  Term v12 = slv.mkConst(bvSort2, "v1");
+  Term b12 = slv.mkVar(bvSort2, "b1");
+  Term b22 = slv.mkVar(slv.getIntegerSort(), "b2");
+  ASSERT_THROW(slv.defineFun("f", {}, bvSort, v12), CVC4ApiException);
+  ASSERT_THROW(slv.defineFun("f", {}, bvSort2, v1), CVC4ApiException);
+  ASSERT_THROW(slv.defineFun("ff", {b1, b22}, bvSort2, v12), CVC4ApiException);
+  ASSERT_THROW(slv.defineFun("ff", {b12, b2}, bvSort2, v12), CVC4ApiException);
+  ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort, v12), CVC4ApiException);
+  ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort2, v1), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, defineFunGlobal)
+{
+  Sort bSort = d_solver.getBooleanSort();
+  Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
+
+  Term bTrue = d_solver.mkBoolean(true);
+  // (define-fun f () Bool true)
+  Term f = d_solver.defineFun("f", {}, bSort, bTrue, true);
+  Term b = d_solver.mkVar(bSort, "b");
+  Term gSym = d_solver.mkConst(fSort, "g");
+  // (define-fun g (b Bool) Bool b)
+  Term g = d_solver.defineFun(gSym, {b}, b, true);
+
+  // (assert (or (not f) (not (g true))))
+  d_solver.assertFormula(d_solver.mkTerm(
+      OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm()));
+  ASSERT_TRUE(d_solver.checkSat().isUnsat());
+  d_solver.resetAssertions();
+  // (assert (or (not f) (not (g true))))
+  d_solver.assertFormula(d_solver.mkTerm(
+      OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm()));
+  ASSERT_TRUE(d_solver.checkSat().isUnsat());
+}
+
+TEST_F(TestApiSolverBlack, defineFunRec)
+{
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
+  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                          d_solver.getIntegerSort());
+  Term b1 = d_solver.mkVar(bvSort, "b1");
+  Term b11 = d_solver.mkVar(bvSort, "b1");
+  Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
+  Term b3 = d_solver.mkVar(funSort2, "b3");
+  Term v1 = d_solver.mkConst(bvSort, "v1");
+  Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
+  Term v3 = d_solver.mkConst(funSort2, "v3");
+  Term f1 = d_solver.mkConst(funSort1, "f1");
+  Term f2 = d_solver.mkConst(funSort2, "f2");
+  Term f3 = d_solver.mkConst(bvSort, "f3");
+  ASSERT_NO_THROW(d_solver.defineFunRec("f", {}, bvSort, v1));
+  ASSERT_NO_THROW(d_solver.defineFunRec("ff", {b1, b2}, bvSort, v1));
+  ASSERT_NO_THROW(d_solver.defineFunRec(f1, {b1, b11}, v1));
+  ASSERT_THROW(d_solver.defineFunRec("fff", {b1}, bvSort, v3),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFunRec("ff", {b1, v2}, bvSort, v1),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFunRec("ffff", {b1}, funSort2, v3),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFunRec(f1, {b1}, v1), CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFunRec(f2, {b1}, v2), CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFunRec(f3, {b1}, v1), CVC4ApiException);
+
+  Solver slv;
+  Sort bvSort2 = slv.mkBitVectorSort(32);
+  Term v12 = slv.mkConst(bvSort2, "v1");
+  Term b12 = slv.mkVar(bvSort2, "b1");
+  Term b22 = slv.mkVar(slv.getIntegerSort(), "b2");
+  ASSERT_NO_THROW(slv.defineFunRec("f", {}, bvSort2, v12));
+  ASSERT_NO_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort2, v12));
+  ASSERT_THROW(slv.defineFunRec("f", {}, bvSort, v12), CVC4ApiException);
+  ASSERT_THROW(slv.defineFunRec("f", {}, bvSort2, v1), CVC4ApiException);
+  ASSERT_THROW(slv.defineFunRec("ff", {b1, b22}, bvSort2, v12),
+               CVC4ApiException);
+  ASSERT_THROW(slv.defineFunRec("ff", {b12, b2}, bvSort2, v12),
+               CVC4ApiException);
+  ASSERT_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort, v12),
+               CVC4ApiException);
+  ASSERT_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort2, v1),
+               CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, defineFunRecWrongLogic)
+{
+  d_solver.setLogic("QF_BV");
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort funSort = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
+  Term b = d_solver.mkVar(bvSort, "b");
+  Term v = d_solver.mkConst(bvSort, "v");
+  Term f = d_solver.mkConst(funSort, "f");
+  ASSERT_THROW(d_solver.defineFunRec("f", {}, bvSort, v), CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFunRec(f, {b, b}, v), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, defineFunRecGlobal)
+{
+  Sort bSort = d_solver.getBooleanSort();
+  Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
+
+  d_solver.push();
+  Term bTrue = d_solver.mkBoolean(true);
+  // (define-fun f () Bool true)
+  Term f = d_solver.defineFunRec("f", {}, bSort, bTrue, true);
+  Term b = d_solver.mkVar(bSort, "b");
+  Term gSym = d_solver.mkConst(fSort, "g");
+  // (define-fun g (b Bool) Bool b)
+  Term g = d_solver.defineFunRec(gSym, {b}, b, true);
+
+  // (assert (or (not f) (not (g true))))
+  d_solver.assertFormula(d_solver.mkTerm(
+      OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm()));
+  ASSERT_TRUE(d_solver.checkSat().isUnsat());
+  d_solver.pop();
+  // (assert (or (not f) (not (g true))))
+  d_solver.assertFormula(d_solver.mkTerm(
+      OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm()));
+  ASSERT_TRUE(d_solver.checkSat().isUnsat());
+}
+
+TEST_F(TestApiSolverBlack, defineFunsRec)
+{
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
+  Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
+  Term b1 = d_solver.mkVar(bvSort, "b1");
+  Term b11 = d_solver.mkVar(bvSort, "b1");
+  Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
+  Term b3 = d_solver.mkVar(funSort2, "b3");
+  Term b4 = d_solver.mkVar(uSort, "b4");
+  Term v1 = d_solver.mkConst(bvSort, "v1");
+  Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
+  Term v3 = d_solver.mkConst(funSort2, "v3");
+  Term v4 = d_solver.mkConst(uSort, "v4");
+  Term f1 = d_solver.mkConst(funSort1, "f1");
+  Term f2 = d_solver.mkConst(funSort2, "f2");
+  Term f3 = d_solver.mkConst(bvSort, "f3");
+  ASSERT_NO_THROW(
+      d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2}));
+  ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{v1, b11}, {b4}}, {v1, v2}),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}),
+               CVC4ApiException);
+
+  Solver slv;
+  Sort uSort2 = slv.mkUninterpretedSort("u");
+  Sort bvSort2 = slv.mkBitVectorSort(32);
+  Sort funSort12 = slv.mkFunctionSort({bvSort2, bvSort2}, bvSort2);
+  Sort funSort22 = slv.mkFunctionSort(uSort2, slv.getIntegerSort());
+  Term b12 = slv.mkVar(bvSort2, "b1");
+  Term b112 = slv.mkVar(bvSort2, "b1");
+  Term b42 = slv.mkVar(uSort2, "b4");
+  Term v12 = slv.mkConst(bvSort2, "v1");
+  Term v22 = slv.mkConst(slv.getIntegerSort(), "v2");
+  Term f12 = slv.mkConst(funSort12, "f1");
+  Term f22 = slv.mkConst(funSort22, "f2");
+  ASSERT_NO_THROW(
+      slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v22}));
+  ASSERT_THROW(slv.defineFunsRec({f1, f22}, {{b12, b112}, {b42}}, {v12, v22}),
+               CVC4ApiException);
+  ASSERT_THROW(slv.defineFunsRec({f12, f2}, {{b12, b112}, {b42}}, {v12, v22}),
+               CVC4ApiException);
+  ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b1, b112}, {b42}}, {v12, v22}),
+               CVC4ApiException);
+  ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b11}, {b42}}, {v12, v22}),
+               CVC4ApiException);
+  ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b4}}, {v12, v22}),
+               CVC4ApiException);
+  ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v1, v22}),
+               CVC4ApiException);
+  ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v2}),
+               CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, defineFunsRecWrongLogic)
+{
+  d_solver.setLogic("QF_BV");
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
+  Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
+  Term b = d_solver.mkVar(bvSort, "b");
+  Term u = d_solver.mkVar(uSort, "u");
+  Term v1 = d_solver.mkConst(bvSort, "v1");
+  Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
+  Term f1 = d_solver.mkConst(funSort1, "f1");
+  Term f2 = d_solver.mkConst(funSort2, "f2");
+  ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b, b}, {u}}, {v1, v2}),
+               CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, defineFunsRecGlobal)
+{
+  Sort bSort = d_solver.getBooleanSort();
+  Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
+
+  d_solver.push();
+  Term bTrue = d_solver.mkBoolean(true);
+  Term b = d_solver.mkVar(bSort, "b");
+  Term gSym = d_solver.mkConst(fSort, "g");
+  // (define-funs-rec ((g ((b Bool)) Bool)) (b))
+  d_solver.defineFunsRec({gSym}, {{b}}, {b}, true);
+
+  // (assert (not (g true)))
+  d_solver.assertFormula(d_solver.mkTerm(APPLY_UF, gSym, bTrue).notTerm());
+  ASSERT_TRUE(d_solver.checkSat().isUnsat());
+  d_solver.pop();
+  // (assert (not (g true)))
+  d_solver.assertFormula(d_solver.mkTerm(APPLY_UF, gSym, bTrue).notTerm());
+  ASSERT_TRUE(d_solver.checkSat().isUnsat());
+}
+
+TEST_F(TestApiSolverBlack, uFIteration)
+{
+  Sort intSort = d_solver.getIntegerSort();
+  Sort funSort = d_solver.mkFunctionSort({intSort, intSort}, intSort);
+  Term x = d_solver.mkConst(intSort, "x");
+  Term y = d_solver.mkConst(intSort, "y");
+  Term f = d_solver.mkConst(funSort, "f");
+  Term fxy = d_solver.mkTerm(APPLY_UF, f, x, y);
+
+  // Expecting the uninterpreted function to be one of the children
+  Term expected_children[3] = {f, x, y};
+  uint32_t idx = 0;
+  for (auto c : fxy)
+  {
+    EXPECT_LT(idx, 3);
+    EXPECT_EQ(c, expected_children[idx]);
+    idx++;
+  }
+}
+
+TEST_F(TestApiSolverBlack, getInfo)
+{
+  ASSERT_NO_THROW(d_solver.getInfo("name"));
+  ASSERT_THROW(d_solver.getInfo("asdf"), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, getInterpolant)
+{
+  // TODO issue #5593
+}
+
+TEST_F(TestApiSolverBlack, getOp)
+{
+  Sort bv32 = d_solver.mkBitVectorSort(32);
+  Term a = d_solver.mkConst(bv32, "a");
+  Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 2, 1);
+  Term exta = d_solver.mkTerm(ext, a);
+
+  ASSERT_FALSE(a.hasOp());
+  ASSERT_THROW(a.getOp(), CVC4ApiException);
+  ASSERT_TRUE(exta.hasOp());
+  EXPECT_EQ(exta.getOp(), ext);
+
+  // Test Datatypes -- more complicated
+  DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+  cons.addSelector("head", d_solver.getIntegerSort());
+  cons.addSelectorSelf("tail");
+  consListSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+  consListSpec.addConstructor(nil);
+  Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
+  Datatype consList = consListSort.getDatatype();
+
+  Term consTerm = consList.getConstructorTerm("cons");
+  Term nilTerm = consList.getConstructorTerm("nil");
+  Term headTerm = consList["cons"].getSelectorTerm("head");
+
+  Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm);
+  Term listcons1 = d_solver.mkTerm(
+      APPLY_CONSTRUCTOR, consTerm, d_solver.mkInteger(1), listnil);
+  Term listhead = d_solver.mkTerm(APPLY_SELECTOR, headTerm, listcons1);
+
+  ASSERT_TRUE(listnil.hasOp());
+  EXPECT_EQ(listnil.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+
+  ASSERT_TRUE(listcons1.hasOp());
+  EXPECT_EQ(listcons1.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+
+  ASSERT_TRUE(listhead.hasOp());
+  EXPECT_EQ(listhead.getOp(), Op(&d_solver, APPLY_SELECTOR));
+}
+
+TEST_F(TestApiSolverBlack, getOption)
+{
+  ASSERT_NO_THROW(d_solver.getOption("incremental"));
+  ASSERT_THROW(d_solver.getOption("asdf"), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, getUnsatAssumptions1)
+{
+#if IS_PROOFS_BUILD
+  d_solver.setOption("incremental", "false");
+  d_solver.checkSatAssuming(d_solver.mkFalse());
+  ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException);
+#endif
+}
+
+TEST_F(TestApiSolverBlack, getUnsatAssumptions2)
+{
+#if IS_PROOFS_BUILD
+  d_solver.setOption("incremental", "true");
+  d_solver.setOption("produce-unsat-assumptions", "false");
+  d_solver.checkSatAssuming(d_solver.mkFalse());
+  ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException);
+#endif
+}
+
+TEST_F(TestApiSolverBlack, getUnsatAssumptions3)
+{
+#if IS_PROOFS_BUILD
+  d_solver.setOption("incremental", "true");
+  d_solver.setOption("produce-unsat-assumptions", "true");
+  d_solver.checkSatAssuming(d_solver.mkFalse());
+  ASSERT_NO_THROW(d_solver.getUnsatAssumptions());
+  d_solver.checkSatAssuming(d_solver.mkTrue());
+  ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException);
+#endif
+}
+
+TEST_F(TestApiSolverBlack, getUnsatCore1)
+{
+#if IS_PROOFS_BUILD
+  d_solver.setOption("incremental", "false");
+  d_solver.assertFormula(d_solver.mkFalse());
+  d_solver.checkSat();
+  ASSERT_THROW(d_solver.getUnsatCore(), CVC4ApiException);
+#endif
+}
+
+TEST_F(TestApiSolverBlack, getUnsatCore2)
+{
+#if IS_PROOFS_BUILD
+  d_solver.setOption("incremental", "false");
+  d_solver.setOption("produce-unsat-cores", "false");
+  d_solver.assertFormula(d_solver.mkFalse());
+  d_solver.checkSat();
+  ASSERT_THROW(d_solver.getUnsatCore(), CVC4ApiException);
+#endif
+}
+
+TEST_F(TestApiSolverBlack, getUnsatCore3)
+{
+#if IS_PROOFS_BUILD
+  d_solver.setOption("incremental", "true");
+  d_solver.setOption("produce-unsat-cores", "true");
+
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
+  Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
+  std::vector<Term> unsat_core;
+
+  Term x = d_solver.mkConst(uSort, "x");
+  Term y = d_solver.mkConst(uSort, "y");
+  Term f = d_solver.mkConst(uToIntSort, "f");
+  Term p = d_solver.mkConst(intPredSort, "p");
+  Term zero = d_solver.mkInteger(0);
+  Term one = d_solver.mkInteger(1);
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
+  d_solver.assertFormula(d_solver.mkTerm(GT, zero, f_x));
+  d_solver.assertFormula(d_solver.mkTerm(GT, zero, f_y));
+  d_solver.assertFormula(d_solver.mkTerm(GT, sum, one));
+  d_solver.assertFormula(p_0);
+  d_solver.assertFormula(p_f_y.notTerm());
+  ASSERT_TRUE(d_solver.checkSat().isUnsat());
+
+  ASSERT_NO_THROW(unsat_core = d_solver.getUnsatCore());
+
+  d_solver.resetAssertions();
+  for (const auto& t : unsat_core)
+  {
+    d_solver.assertFormula(t);
+  }
+  Result res = d_solver.checkSat();
+  ASSERT_TRUE(res.isUnsat());
+#endif
+}
+
+TEST_F(TestApiSolverBlack, getValue1)
+{
+  d_solver.setOption("produce-models", "false");
+  Term t = d_solver.mkTrue();
+  d_solver.assertFormula(t);
+  d_solver.checkSat();
+  ASSERT_THROW(d_solver.getValue(t), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, getValue2)
+{
+  d_solver.setOption("produce-models", "true");
+  Term t = d_solver.mkFalse();
+  d_solver.assertFormula(t);
+  d_solver.checkSat();
+  ASSERT_THROW(d_solver.getValue(t), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, getValue3)
+{
+  d_solver.setOption("produce-models", "true");
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
+  Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
+  std::vector<Term> unsat_core;
+
+  Term x = d_solver.mkConst(uSort, "x");
+  Term y = d_solver.mkConst(uSort, "y");
+  Term z = d_solver.mkConst(uSort, "z");
+  Term f = d_solver.mkConst(uToIntSort, "f");
+  Term p = d_solver.mkConst(intPredSort, "p");
+  Term zero = d_solver.mkInteger(0);
+  Term one = d_solver.mkInteger(1);
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
+
+  d_solver.assertFormula(d_solver.mkTerm(LEQ, zero, f_x));
+  d_solver.assertFormula(d_solver.mkTerm(LEQ, zero, f_y));
+  d_solver.assertFormula(d_solver.mkTerm(LEQ, sum, one));
+  d_solver.assertFormula(p_0.notTerm());
+  d_solver.assertFormula(p_f_y);
+  ASSERT_TRUE(d_solver.checkSat().isSat());
+  ASSERT_NO_THROW(d_solver.getValue(x));
+  ASSERT_NO_THROW(d_solver.getValue(y));
+  ASSERT_NO_THROW(d_solver.getValue(z));
+  ASSERT_NO_THROW(d_solver.getValue(sum));
+  ASSERT_NO_THROW(d_solver.getValue(p_f_y));
+
+  Solver slv;
+  ASSERT_THROW(slv.getValue(x), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, getQuantifierElimination)
+{
+  Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
+  Term forall =
+      d_solver.mkTerm(FORALL,
+                      d_solver.mkTerm(BOUND_VAR_LIST, x),
+                      d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
+  ASSERT_THROW(d_solver.getQuantifierElimination(Term()), CVC4ApiException);
+  ASSERT_THROW(d_solver.getQuantifierElimination(Solver().mkBoolean(false)),
+               CVC4ApiException);
+  ASSERT_NO_THROW(d_solver.getQuantifierElimination(forall));
+}
+
+TEST_F(TestApiSolverBlack, getQuantifierEliminationDisjunct)
+{
+  Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
+  Term forall =
+      d_solver.mkTerm(FORALL,
+                      d_solver.mkTerm(BOUND_VAR_LIST, x),
+                      d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
+  ASSERT_THROW(d_solver.getQuantifierEliminationDisjunct(Term()),
+               CVC4ApiException);
+  ASSERT_THROW(
+      d_solver.getQuantifierEliminationDisjunct(Solver().mkBoolean(false)),
+      CVC4ApiException);
+  ASSERT_NO_THROW(d_solver.getQuantifierEliminationDisjunct(forall));
+}
+
+TEST_F(TestApiSolverBlack, declareSeparationHeap)
+{
+  d_solver.setLogic("ALL_SUPPORTED");
+  Sort integer = d_solver.getIntegerSort();
+  ASSERT_NO_THROW(d_solver.declareSeparationHeap(integer, integer));
+  // cannot declare separation logic heap more than once
+  ASSERT_THROW(d_solver.declareSeparationHeap(integer, integer),
+               CVC4ApiException);
+}
+
+namespace {
+/**
+ * Helper function for testGetSeparation{Heap,Nil}TermX. Asserts and checks
+ * some simple separation logic constraints.
+ */
+void checkSimpleSeparationConstraints(Solver* solver)
+{
+  Sort integer = solver->getIntegerSort();
+  // declare the separation heap
+  solver->declareSeparationHeap(integer, integer);
+  Term x = solver->mkConst(integer, "x");
+  Term p = solver->mkConst(integer, "p");
+  Term heap = solver->mkTerm(CVC4::api::Kind::SEP_PTO, p, x);
+  solver->assertFormula(heap);
+  Term nil = solver->mkSepNil(integer);
+  solver->assertFormula(nil.eqTerm(solver->mkReal(5)));
+  solver->checkSat();
+}
+}  // namespace
+
+TEST_F(TestApiSolverBlack, getSeparationHeapTerm1)
+{
+  d_solver.setLogic("QF_BV");
+  d_solver.setOption("incremental", "false");
+  d_solver.setOption("produce-models", "true");
+  Term t = d_solver.mkTrue();
+  d_solver.assertFormula(t);
+  ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, getSeparationHeapTerm2)
+{
+  d_solver.setLogic("ALL_SUPPORTED");
+  d_solver.setOption("incremental", "false");
+  d_solver.setOption("produce-models", "false");
+  checkSimpleSeparationConstraints(&d_solver);
+  ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, getSeparationHeapTerm3)
+{
+  d_solver.setLogic("ALL_SUPPORTED");
+  d_solver.setOption("incremental", "false");
+  d_solver.setOption("produce-models", "true");
+  Term t = d_solver.mkFalse();
+  d_solver.assertFormula(t);
+  d_solver.checkSat();
+  ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, getSeparationHeapTerm4)
+{
+  d_solver.setLogic("ALL_SUPPORTED");
+  d_solver.setOption("incremental", "false");
+  d_solver.setOption("produce-models", "true");
+  Term t = d_solver.mkTrue();
+  d_solver.assertFormula(t);
+  d_solver.checkSat();
+  ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, getSeparationHeapTerm5)
+{
+  d_solver.setLogic("ALL_SUPPORTED");
+  d_solver.setOption("incremental", "false");
+  d_solver.setOption("produce-models", "true");
+  checkSimpleSeparationConstraints(&d_solver);
+  ASSERT_NO_THROW(d_solver.getSeparationHeap());
+}
+
+TEST_F(TestApiSolverBlack, getSeparationNilTerm1)
+{
+  d_solver.setLogic("QF_BV");
+  d_solver.setOption("incremental", "false");
+  d_solver.setOption("produce-models", "true");
+  Term t = d_solver.mkTrue();
+  d_solver.assertFormula(t);
+  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, getSeparationNilTerm2)
+{
+  d_solver.setLogic("ALL_SUPPORTED");
+  d_solver.setOption("incremental", "false");
+  d_solver.setOption("produce-models", "false");
+  checkSimpleSeparationConstraints(&d_solver);
+  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, getSeparationNilTerm3)
+{
+  d_solver.setLogic("ALL_SUPPORTED");
+  d_solver.setOption("incremental", "false");
+  d_solver.setOption("produce-models", "true");
+  Term t = d_solver.mkFalse();
+  d_solver.assertFormula(t);
+  d_solver.checkSat();
+  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, getSeparationNilTerm4)
+{
+  d_solver.setLogic("ALL_SUPPORTED");
+  d_solver.setOption("incremental", "false");
+  d_solver.setOption("produce-models", "true");
+  Term t = d_solver.mkTrue();
+  d_solver.assertFormula(t);
+  d_solver.checkSat();
+  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, getSeparationNilTerm5)
+{
+  d_solver.setLogic("ALL_SUPPORTED");
+  d_solver.setOption("incremental", "false");
+  d_solver.setOption("produce-models", "true");
+  checkSimpleSeparationConstraints(&d_solver);
+  ASSERT_NO_THROW(d_solver.getSeparationNilTerm());
+}
+
+TEST_F(TestApiSolverBlack, push1)
+{
+  d_solver.setOption("incremental", "true");
+  ASSERT_NO_THROW(d_solver.push(1));
+  ASSERT_THROW(d_solver.setOption("incremental", "false"), CVC4ApiException);
+  ASSERT_THROW(d_solver.setOption("incremental", "true"), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, push2)
+{
+  d_solver.setOption("incremental", "false");
+  ASSERT_THROW(d_solver.push(1), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, pop1)
+{
+  d_solver.setOption("incremental", "false");
+  ASSERT_THROW(d_solver.pop(1), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, pop2)
+{
+  d_solver.setOption("incremental", "true");
+  ASSERT_THROW(d_solver.pop(1), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, pop3)
+{
+  d_solver.setOption("incremental", "true");
+  ASSERT_NO_THROW(d_solver.push(1));
+  ASSERT_NO_THROW(d_solver.pop(1));
+  ASSERT_THROW(d_solver.pop(1), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, blockModel1)
+{
+  d_solver.setOption("produce-models", "true");
+  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+  d_solver.assertFormula(x.eqTerm(x));
+  d_solver.checkSat();
+  ASSERT_THROW(d_solver.blockModel(), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, blockModel2)
+{
+  d_solver.setOption("block-models", "literals");
+  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+  d_solver.assertFormula(x.eqTerm(x));
+  d_solver.checkSat();
+  ASSERT_THROW(d_solver.blockModel(), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, blockModel3)
+{
+  d_solver.setOption("produce-models", "true");
+  d_solver.setOption("block-models", "literals");
+  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+  d_solver.assertFormula(x.eqTerm(x));
+  ASSERT_THROW(d_solver.blockModel(), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, blockModel4)
+{
+  d_solver.setOption("produce-models", "true");
+  d_solver.setOption("block-models", "literals");
+  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+  d_solver.assertFormula(x.eqTerm(x));
+  d_solver.checkSat();
+  ASSERT_NO_THROW(d_solver.blockModel());
+}
+
+TEST_F(TestApiSolverBlack, blockModelValues1)
+{
+  d_solver.setOption("produce-models", "true");
+  d_solver.setOption("block-models", "literals");
+  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+  d_solver.assertFormula(x.eqTerm(x));
+  d_solver.checkSat();
+  ASSERT_THROW(d_solver.blockModelValues({}), CVC4ApiException);
+  ASSERT_THROW(d_solver.blockModelValues({Term()}), CVC4ApiException);
+  ASSERT_THROW(d_solver.blockModelValues({Solver().mkBoolean(false)}),
+               CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, blockModelValues2)
+{
+  d_solver.setOption("produce-models", "true");
+  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+  d_solver.assertFormula(x.eqTerm(x));
+  d_solver.checkSat();
+  ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, blockModelValues3)
+{
+  d_solver.setOption("block-models", "literals");
+  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+  d_solver.assertFormula(x.eqTerm(x));
+  d_solver.checkSat();
+  ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, blockModelValues4)
+{
+  d_solver.setOption("produce-models", "true");
+  d_solver.setOption("block-models", "literals");
+  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+  d_solver.assertFormula(x.eqTerm(x));
+  ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, blockModelValues5)
+{
+  d_solver.setOption("produce-models", "true");
+  d_solver.setOption("block-models", "literals");
+  Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+  d_solver.assertFormula(x.eqTerm(x));
+  d_solver.checkSat();
+  ASSERT_NO_THROW(d_solver.blockModelValues({x}));
+}
+
+TEST_F(TestApiSolverBlack, setInfo)
+{
+  ASSERT_THROW(d_solver.setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException);
+  ASSERT_THROW(d_solver.setInfo("cvc2-logic", "QF_BV"), CVC4ApiException);
+  ASSERT_THROW(d_solver.setInfo("cvc4-logic", "asdf"), CVC4ApiException);
+
+  ASSERT_NO_THROW(d_solver.setInfo("source", "asdf"));
+  ASSERT_NO_THROW(d_solver.setInfo("category", "asdf"));
+  ASSERT_NO_THROW(d_solver.setInfo("difficulty", "asdf"));
+  ASSERT_NO_THROW(d_solver.setInfo("filename", "asdf"));
+  ASSERT_NO_THROW(d_solver.setInfo("license", "asdf"));
+  ASSERT_NO_THROW(d_solver.setInfo("name", "asdf"));
+  ASSERT_NO_THROW(d_solver.setInfo("notes", "asdf"));
+
+  ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2"));
+  ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2.0"));
+  ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2.5"));
+  ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2.6"));
+  ASSERT_THROW(d_solver.setInfo("smt-lib-version", ".0"), CVC4ApiException);
+
+  ASSERT_NO_THROW(d_solver.setInfo("status", "sat"));
+  ASSERT_NO_THROW(d_solver.setInfo("status", "unsat"));
+  ASSERT_NO_THROW(d_solver.setInfo("status", "unknown"));
+  ASSERT_THROW(d_solver.setInfo("status", "asdf"), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, simplify)
+{
+  ASSERT_THROW(d_solver.simplify(Term()), CVC4ApiException);
+
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
+  Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
+  DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+  cons.addSelector("head", d_solver.getIntegerSort());
+  cons.addSelectorSelf("tail");
+  consListSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+  consListSpec.addConstructor(nil);
+  Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
+
+  Term x = d_solver.mkConst(bvSort, "x");
+  ASSERT_NO_THROW(d_solver.simplify(x));
+  Term a = d_solver.mkConst(bvSort, "a");
+  ASSERT_NO_THROW(d_solver.simplify(a));
+  Term b = d_solver.mkConst(bvSort, "b");
+  ASSERT_NO_THROW(d_solver.simplify(b));
+  Term x_eq_x = d_solver.mkTerm(EQUAL, x, x);
+  ASSERT_NO_THROW(d_solver.simplify(x_eq_x));
+  EXPECT_NE(d_solver.mkTrue(), x_eq_x);
+  EXPECT_EQ(d_solver.mkTrue(), d_solver.simplify(x_eq_x));
+  Term x_eq_b = d_solver.mkTerm(EQUAL, x, b);
+  ASSERT_NO_THROW(d_solver.simplify(x_eq_b));
+  EXPECT_NE(d_solver.mkTrue(), x_eq_b);
+  EXPECT_NE(d_solver.mkTrue(), d_solver.simplify(x_eq_b));
+  Solver slv;
+  ASSERT_THROW(slv.simplify(x), CVC4ApiException);
+
+  Term i1 = d_solver.mkConst(d_solver.getIntegerSort(), "i1");
+  ASSERT_NO_THROW(d_solver.simplify(i1));
+  Term i2 = d_solver.mkTerm(MULT, i1, d_solver.mkInteger("23"));
+  ASSERT_NO_THROW(d_solver.simplify(i2));
+  EXPECT_NE(i1, i2);
+  EXPECT_NE(i1, d_solver.simplify(i2));
+  Term i3 = d_solver.mkTerm(PLUS, i1, d_solver.mkInteger(0));
+  ASSERT_NO_THROW(d_solver.simplify(i3));
+  EXPECT_NE(i1, i3);
+  EXPECT_EQ(i1, d_solver.simplify(i3));
+
+  Datatype consList = consListSort.getDatatype();
+  Term dt1 = d_solver.mkTerm(
+      APPLY_CONSTRUCTOR,
+      consList.getConstructorTerm("cons"),
+      d_solver.mkInteger(0),
+      d_solver.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
+  ASSERT_NO_THROW(d_solver.simplify(dt1));
+  Term dt2 = d_solver.mkTerm(
+      APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1);
+  ASSERT_NO_THROW(d_solver.simplify(dt2));
+
+  Term b1 = d_solver.mkVar(bvSort, "b1");
+  ASSERT_NO_THROW(d_solver.simplify(b1));
+  Term b2 = d_solver.mkVar(bvSort, "b1");
+  ASSERT_NO_THROW(d_solver.simplify(b2));
+  Term b3 = d_solver.mkVar(uSort, "b3");
+  ASSERT_NO_THROW(d_solver.simplify(b3));
+  Term v1 = d_solver.mkConst(bvSort, "v1");
+  ASSERT_NO_THROW(d_solver.simplify(v1));
+  Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
+  ASSERT_NO_THROW(d_solver.simplify(v2));
+  Term f1 = d_solver.mkConst(funSort1, "f1");
+  ASSERT_NO_THROW(d_solver.simplify(f1));
+  Term f2 = d_solver.mkConst(funSort2, "f2");
+  ASSERT_NO_THROW(d_solver.simplify(f2));
+  d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b3}}, {v1, v2});
+  ASSERT_NO_THROW(d_solver.simplify(f1));
+  ASSERT_NO_THROW(d_solver.simplify(f2));
+}
+
+TEST_F(TestApiSolverBlack, assertFormula)
+{
+  ASSERT_NO_THROW(d_solver.assertFormula(d_solver.mkTrue()));
+  ASSERT_THROW(d_solver.assertFormula(Term()), CVC4ApiException);
+  Solver slv;
+  ASSERT_THROW(slv.assertFormula(d_solver.mkTrue()), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, checkEntailed)
+{
+  d_solver.setOption("incremental", "false");
+  ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue()));
+  ASSERT_THROW(d_solver.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
+  Solver slv;
+  ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, checkEntailed1)
+{
+  Sort boolSort = d_solver.getBooleanSort();
+  Term x = d_solver.mkConst(boolSort, "x");
+  Term y = d_solver.mkConst(boolSort, "y");
+  Term z = d_solver.mkTerm(AND, x, y);
+  d_solver.setOption("incremental", "true");
+  ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue()));
+  ASSERT_THROW(d_solver.checkEntailed(Term()), CVC4ApiException);
+  ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue()));
+  ASSERT_NO_THROW(d_solver.checkEntailed(z));
+  Solver slv;
+  ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, checkEntailed2)
+{
+  d_solver.setOption("incremental", "true");
+
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
+  Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term n = Term();
+  // Constants
+  Term x = d_solver.mkConst(uSort, "x");
+  Term y = d_solver.mkConst(uSort, "y");
+  // Functions
+  Term f = d_solver.mkConst(uToIntSort, "f");
+  Term p = d_solver.mkConst(intPredSort, "p");
+  // Values
+  Term zero = d_solver.mkInteger(0);
+  Term one = d_solver.mkInteger(1);
+  // Terms
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
+  // Assertions
+  Term assertions =
+      d_solver.mkTerm(AND,
+                      std::vector<Term>{
+                          d_solver.mkTerm(LEQ, zero, f_x),  // 0 <= f(x)
+                          d_solver.mkTerm(LEQ, zero, f_y),  // 0 <= f(y)
+                          d_solver.mkTerm(LEQ, sum, one),   // f(x) + f(y) <= 1
+                          p_0.notTerm(),                    // not p(0)
+                          p_f_y                             // p(f(y))
+                      });
+
+  ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue()));
+  d_solver.assertFormula(assertions);
+  ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTerm(DISTINCT, x, y)));
+  ASSERT_NO_THROW(d_solver.checkEntailed(
+      {d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, x, y)}));
+  ASSERT_THROW(d_solver.checkEntailed(n), CVC4ApiException);
+  ASSERT_THROW(d_solver.checkEntailed({n, d_solver.mkTerm(DISTINCT, x, y)}),
+               CVC4ApiException);
+  Solver slv;
+  ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, checkSat)
+{
+  d_solver.setOption("incremental", "false");
+  ASSERT_NO_THROW(d_solver.checkSat());
+  ASSERT_THROW(d_solver.checkSat(), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, checkSatAssuming)
+{
+  d_solver.setOption("incremental", "false");
+  ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
+  ASSERT_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
+  Solver slv;
+  ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, checkSatAssuming1)
+{
+  Sort boolSort = d_solver.getBooleanSort();
+  Term x = d_solver.mkConst(boolSort, "x");
+  Term y = d_solver.mkConst(boolSort, "y");
+  Term z = d_solver.mkTerm(AND, x, y);
+  d_solver.setOption("incremental", "true");
+  ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
+  ASSERT_THROW(d_solver.checkSatAssuming(Term()), CVC4ApiException);
+  ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
+  ASSERT_NO_THROW(d_solver.checkSatAssuming(z));
+  Solver slv;
+  ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, checkSatAssuming2)
+{
+  d_solver.setOption("incremental", "true");
+
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
+  Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term n = Term();
+  // Constants
+  Term x = d_solver.mkConst(uSort, "x");
+  Term y = d_solver.mkConst(uSort, "y");
+  // Functions
+  Term f = d_solver.mkConst(uToIntSort, "f");
+  Term p = d_solver.mkConst(intPredSort, "p");
+  // Values
+  Term zero = d_solver.mkInteger(0);
+  Term one = d_solver.mkInteger(1);
+  // Terms
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
+  // Assertions
+  Term assertions =
+      d_solver.mkTerm(AND,
+                      std::vector<Term>{
+                          d_solver.mkTerm(LEQ, zero, f_x),  // 0 <= f(x)
+                          d_solver.mkTerm(LEQ, zero, f_y),  // 0 <= f(y)
+                          d_solver.mkTerm(LEQ, sum, one),   // f(x) + f(y) <= 1
+                          p_0.notTerm(),                    // not p(0)
+                          p_f_y                             // p(f(y))
+                      });
+
+  ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
+  d_solver.assertFormula(assertions);
+  ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTerm(DISTINCT, x, y)));
+  ASSERT_NO_THROW(d_solver.checkSatAssuming(
+      {d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, x, y)}));
+  ASSERT_THROW(d_solver.checkSatAssuming(n), CVC4ApiException);
+  ASSERT_THROW(d_solver.checkSatAssuming({n, d_solver.mkTerm(DISTINCT, x, y)}),
+               CVC4ApiException);
+  Solver slv;
+  ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, setLogic)
+{
+  ASSERT_NO_THROW(d_solver.setLogic("AUFLIRA"));
+  ASSERT_THROW(d_solver.setLogic("AF_BV"), CVC4ApiException);
+  d_solver.assertFormula(d_solver.mkTrue());
+  ASSERT_THROW(d_solver.setLogic("AUFLIRA"), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, setOption)
+{
+  ASSERT_NO_THROW(d_solver.setOption("bv-sat-solver", "minisat"));
+  ASSERT_THROW(d_solver.setOption("bv-sat-solver", "1"), CVC4ApiException);
+  d_solver.assertFormula(d_solver.mkTrue());
+  ASSERT_THROW(d_solver.setOption("bv-sat-solver", "minisat"),
+               CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, resetAssertions)
+{
+  d_solver.setOption("incremental", "true");
+
+  Sort bvSort = d_solver.mkBitVectorSort(4);
+  Term one = d_solver.mkBitVector(4, 1);
+  Term x = d_solver.mkConst(bvSort, "x");
+  Term ule = d_solver.mkTerm(BITVECTOR_ULE, x, one);
+  Term srem = d_solver.mkTerm(BITVECTOR_SREM, one, x);
+  d_solver.push(4);
+  Term slt = d_solver.mkTerm(BITVECTOR_SLT, srem, one);
+  d_solver.resetAssertions();
+  d_solver.checkSatAssuming({slt, ule});
+}
+
+TEST_F(TestApiSolverBlack, mkSygusVar)
+{
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort intSort = d_solver.getIntegerSort();
+  Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
+
+  ASSERT_NO_THROW(d_solver.mkSygusVar(boolSort));
+  ASSERT_NO_THROW(d_solver.mkSygusVar(funSort));
+  ASSERT_NO_THROW(d_solver.mkSygusVar(boolSort, std::string("b")));
+  ASSERT_NO_THROW(d_solver.mkSygusVar(funSort, ""));
+  ASSERT_THROW(d_solver.mkSygusVar(Sort()), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkSygusVar(d_solver.getNullSort(), "a"),
+               CVC4ApiException);
+  Solver slv;
+  ASSERT_THROW(slv.mkSygusVar(boolSort), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, mkSygusGrammar)
+{
+  Term nullTerm;
+  Term boolTerm = d_solver.mkBoolean(true);
+  Term boolVar = d_solver.mkVar(d_solver.getBooleanSort());
+  Term intVar = d_solver.mkVar(d_solver.getIntegerSort());
+
+  ASSERT_NO_THROW(d_solver.mkSygusGrammar({}, {intVar}));
+  ASSERT_NO_THROW(d_solver.mkSygusGrammar({boolVar}, {intVar}));
+  ASSERT_THROW(d_solver.mkSygusGrammar({}, {}), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkSygusGrammar({}, {nullTerm}), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkSygusGrammar({}, {boolTerm}), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkSygusGrammar({boolTerm}, {intVar}), CVC4ApiException);
+  Solver slv;
+  Term boolVar2 = slv.mkVar(slv.getBooleanSort());
+  Term intVar2 = slv.mkVar(slv.getIntegerSort());
+  ASSERT_NO_THROW(slv.mkSygusGrammar({boolVar2}, {intVar2}));
+  ASSERT_THROW(slv.mkSygusGrammar({boolVar}, {intVar2}), CVC4ApiException);
+  ASSERT_THROW(slv.mkSygusGrammar({boolVar2}, {intVar}), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, synthFun)
+{
+  Sort null = d_solver.getNullSort();
+  Sort boolean = d_solver.getBooleanSort();
+  Sort integer = d_solver.getIntegerSort();
+
+  Term nullTerm;
+  Term x = d_solver.mkVar(boolean);
+
+  Term start1 = d_solver.mkVar(boolean);
+  Term start2 = d_solver.mkVar(integer);
+
+  Grammar g1 = d_solver.mkSygusGrammar({x}, {start1});
+  g1.addRule(start1, d_solver.mkBoolean(false));
+
+  Grammar g2 = d_solver.mkSygusGrammar({x}, {start2});
+  g2.addRule(start2, d_solver.mkInteger(0));
+
+  ASSERT_NO_THROW(d_solver.synthFun("", {}, boolean));
+  ASSERT_NO_THROW(d_solver.synthFun("f1", {x}, boolean));
+  ASSERT_NO_THROW(d_solver.synthFun("f2", {x}, boolean, g1));
+
+  ASSERT_THROW(d_solver.synthFun("f3", {nullTerm}, boolean), CVC4ApiException);
+  ASSERT_THROW(d_solver.synthFun("f4", {}, null), CVC4ApiException);
+  ASSERT_THROW(d_solver.synthFun("f6", {x}, boolean, g2), CVC4ApiException);
+  Solver slv;
+  Term x2 = slv.mkVar(slv.getBooleanSort());
+  ASSERT_NO_THROW(slv.synthFun("f1", {x2}, slv.getBooleanSort()));
+  ASSERT_THROW(slv.synthFun("", {}, d_solver.getBooleanSort()),
+               CVC4ApiException);
+  ASSERT_THROW(slv.synthFun("f1", {x}, d_solver.getBooleanSort()),
+               CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, synthInv)
+{
+  Sort boolean = d_solver.getBooleanSort();
+  Sort integer = d_solver.getIntegerSort();
+
+  Term nullTerm;
+  Term x = d_solver.mkVar(boolean);
+
+  Term start1 = d_solver.mkVar(boolean);
+  Term start2 = d_solver.mkVar(integer);
+
+  Grammar g1 = d_solver.mkSygusGrammar({x}, {start1});
+  g1.addRule(start1, d_solver.mkBoolean(false));
+
+  Grammar g2 = d_solver.mkSygusGrammar({x}, {start2});
+  g2.addRule(start2, d_solver.mkInteger(0));
+
+  ASSERT_NO_THROW(d_solver.synthInv("", {}));
+  ASSERT_NO_THROW(d_solver.synthInv("i1", {x}));
+  ASSERT_NO_THROW(d_solver.synthInv("i2", {x}, g1));
+
+  ASSERT_THROW(d_solver.synthInv("i3", {nullTerm}), CVC4ApiException);
+  ASSERT_THROW(d_solver.synthInv("i4", {x}, g2), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, addSygusConstraint)
+{
+  Term nullTerm;
+  Term boolTerm = d_solver.mkBoolean(true);
+  Term intTerm = d_solver.mkInteger(1);
+
+  ASSERT_NO_THROW(d_solver.addSygusConstraint(boolTerm));
+  ASSERT_THROW(d_solver.addSygusConstraint(nullTerm), CVC4ApiException);
+  ASSERT_THROW(d_solver.addSygusConstraint(intTerm), CVC4ApiException);
+
+  Solver slv;
+  ASSERT_THROW(slv.addSygusConstraint(boolTerm), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, addSygusInvConstraint)
+{
+  Sort boolean = d_solver.getBooleanSort();
+  Sort real = d_solver.getRealSort();
+
+  Term nullTerm;
+  Term intTerm = d_solver.mkInteger(1);
+
+  Term inv = d_solver.declareFun("inv", {real}, boolean);
+  Term pre = d_solver.declareFun("pre", {real}, boolean);
+  Term trans = d_solver.declareFun("trans", {real, real}, boolean);
+  Term post = d_solver.declareFun("post", {real}, boolean);
+
+  Term inv1 = d_solver.declareFun("inv1", {real}, real);
+
+  Term trans1 = d_solver.declareFun("trans1", {boolean, real}, boolean);
+  Term trans2 = d_solver.declareFun("trans2", {real, boolean}, boolean);
+  Term trans3 = d_solver.declareFun("trans3", {real, real}, real);
+
+  ASSERT_NO_THROW(d_solver.addSygusInvConstraint(inv, pre, trans, post));
+
+  ASSERT_THROW(d_solver.addSygusInvConstraint(nullTerm, pre, trans, post),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, nullTerm, trans, post),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, nullTerm, post),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans, nullTerm),
+               CVC4ApiException);
+
+  ASSERT_THROW(d_solver.addSygusInvConstraint(intTerm, pre, trans, post),
+               CVC4ApiException);
+
+  ASSERT_THROW(d_solver.addSygusInvConstraint(inv1, pre, trans, post),
+               CVC4ApiException);
+
+  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, trans, trans, post),
+               CVC4ApiException);
+
+  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, intTerm, post),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, pre, post),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans1, post),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans2, post),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans3, post),
+               CVC4ApiException);
+
+  ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans, trans),
+               CVC4ApiException);
+  Solver slv;
+  Sort boolean2 = slv.getBooleanSort();
+  Sort real2 = slv.getRealSort();
+  Term inv22 = slv.declareFun("inv", {real2}, boolean2);
+  Term pre22 = slv.declareFun("pre", {real2}, boolean2);
+  Term trans22 = slv.declareFun("trans", {real2, real2}, boolean2);
+  Term post22 = slv.declareFun("post", {real2}, boolean2);
+  ASSERT_NO_THROW(slv.addSygusInvConstraint(inv22, pre22, trans22, post22));
+  ASSERT_THROW(slv.addSygusInvConstraint(inv, pre22, trans22, post22),
+               CVC4ApiException);
+  ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre, trans22, post22),
+               CVC4ApiException);
+  ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre22, trans, post22),
+               CVC4ApiException);
+  ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre22, trans22, post),
+               CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, getSynthSolution)
+{
+  d_solver.setOption("lang", "sygus2");
+  d_solver.setOption("incremental", "false");
+
+  Term nullTerm;
+  Term x = d_solver.mkBoolean(false);
+  Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
+
+  ASSERT_THROW(d_solver.getSynthSolution(f), CVC4ApiException);
+
+  d_solver.checkSynth();
+
+  ASSERT_NO_THROW(d_solver.getSynthSolution(f));
+  ASSERT_NO_THROW(d_solver.getSynthSolution(f));
+
+  ASSERT_THROW(d_solver.getSynthSolution(nullTerm), CVC4ApiException);
+  ASSERT_THROW(d_solver.getSynthSolution(x), CVC4ApiException);
+
+  Solver slv;
+  ASSERT_THROW(slv.getSynthSolution(f), CVC4ApiException);
+}
+
+TEST_F(TestApiSolverBlack, getSynthSolutions)
+{
+  d_solver.setOption("lang", "sygus2");
+  d_solver.setOption("incremental", "false");
+
+  Term nullTerm;
+  Term x = d_solver.mkBoolean(false);
+  Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
+
+  ASSERT_THROW(d_solver.getSynthSolutions({}), CVC4ApiException);
+  ASSERT_THROW(d_solver.getSynthSolutions({f}), CVC4ApiException);
+
+  d_solver.checkSynth();
+
+  ASSERT_NO_THROW(d_solver.getSynthSolutions({f}));
+  ASSERT_NO_THROW(d_solver.getSynthSolutions({f, f}));
+
+  ASSERT_THROW(d_solver.getSynthSolutions({}), CVC4ApiException);
+  ASSERT_THROW(d_solver.getSynthSolutions({nullTerm}), CVC4ApiException);
+  ASSERT_THROW(d_solver.getSynthSolutions({x}), CVC4ApiException);
+
+  Solver slv;
+  ASSERT_THROW(slv.getSynthSolutions({x}), CVC4ApiException);
+}
+
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
deleted file mode 100644
index b3af67a8c..000000000
--- a/test/unit/api/solver_black.h
+++ /dev/null
@@ -1,2485 +0,0 @@
-/*********************                                                        */
-/*! \file solver_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andres Noetzli, Abdalrhman Mohamed
- ** 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 Solver class of the  C++ API.
- **
- ** Black box testing of the Solver class of the  C++ API.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "api/cvc4cpp.h"
-#include "base/configuration.h"
-
-using namespace CVC4::api;
-
-class SolverBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() override;
-  void tearDown() override;
-
-  void testRecoverableException();
-
-  void testSupportsFloatingPoint();
-
-  void testGetBooleanSort();
-  void testGetIntegerSort();
-  void testGetNullSort();
-  void testGetRealSort();
-  void testGetRegExpSort();
-  void testGetRoundingModeSort();
-  void testGetStringSort();
-
-  void testMkArraySort();
-  void testMkBitVectorSort();
-  void testMkFloatingPointSort();
-  void testMkDatatypeSort();
-  void testMkDatatypeSorts();
-  void testMkFunctionSort();
-  void testMkOp();
-  void testMkParamSort();
-  void testMkPredicateSort();
-  void testMkRecordSort();
-  void testMkSetSort();
-  void testMkBagSort();
-  void testMkSequenceSort();
-  void testMkSortConstructorSort();
-  void testMkTupleSort();
-  void testMkUninterpretedSort();
-
-  void testMkAbstractValue();
-  void testMkBitVector();
-  void testMkBoolean();
-  void testMkConst();
-  void testMkConstArray();
-  void testMkEmptySet();
-  void testMkEmptyBag();
-  void testMkEmptySequence();
-  void testMkFalse();
-  void testMkFloatingPoint();
-  void testMkNaN();
-  void testMkNegInf();
-  void testMkNegZero();
-  void testMkPi();
-  void testMkPosInf();
-  void testMkPosZero();
-  void testMkInteger();
-  void testMkReal();
-  void testMkRegexpEmpty();
-  void testMkRegexpSigma();
-  void testMkRoundingMode();
-  void testMkSepNil();
-  void testMkString();
-  void testMkChar();
-  void testMkTerm();
-  void testMkTermFromOp();
-  void testMkTrue();
-  void testMkTuple();
-  void testMkUninterpretedConst();
-  void testMkUniverseSet();
-  void testMkVar();
-
-  void testDeclareDatatype();
-  void testDeclareFun();
-  void testDeclareSort();
-
-  void testDefineFun();
-  void testDefineFunGlobal();
-  void testDefineFunRec();
-  void testDefineFunRecWrongLogic();
-  void testDefineFunRecGlobal();
-  void testDefineFunsRec();
-  void testDefineFunsRecWrongLogic();
-  void testDefineFunsRecGlobal();
-
-  void testUFIteration();
-
-  void testGetInfo();
-  void testGetInterpolant();
-  void testGetOp();
-  void testGetOption();
-  void testGetUnsatAssumptions1();
-  void testGetUnsatAssumptions2();
-  void testGetUnsatAssumptions3();
-  void testGetUnsatCore1();
-  void testGetUnsatCore2();
-  void testGetUnsatCore3();
-  void testGetValue1();
-  void testGetValue2();
-  void testGetValue3();
-  void testGetQuantifierElimination();
-  void testGetQuantifierEliminationDisjunct();
-  void testDeclareSeparationHeap();
-  void testGetSeparationHeapTerm1();
-  void testGetSeparationHeapTerm2();
-  void testGetSeparationHeapTerm3();
-  void testGetSeparationHeapTerm4();
-  void testGetSeparationHeapTerm5();
-  void testGetSeparationNilTerm1();
-  void testGetSeparationNilTerm2();
-  void testGetSeparationNilTerm3();
-  void testGetSeparationNilTerm4();
-  void testGetSeparationNilTerm5();
-
-  /**
-   * When using separation logic, obtain the term for nil.
-   * @return The term for nil
-   */
-  Term getSeparationNilTerm() const;
-
-  void testPush1();
-  void testPush2();
-  void testPop1();
-  void testPop2();
-  void testPop3();
-
-  void testBlockModel1();
-  void testBlockModel2();
-  void testBlockModel3();
-  void testBlockModel4();
-  void testBlockModelValues1();
-  void testBlockModelValues2();
-  void testBlockModelValues3();
-  void testBlockModelValues4();
-  void testBlockModelValues5();
-
-  void testSimplify();
-
-  void testAssertFormula();
-  void testCheckEntailed();
-  void testCheckEntailed1();
-  void testCheckEntailed2();
-  void testCheckSat();
-  void testCheckSatAssuming();
-  void testCheckSatAssuming1();
-  void testCheckSatAssuming2();
-
-  void testSetInfo();
-  void testSetLogic();
-  void testSetOption();
-
-  void testResetAssertions();
-
-  void testMkSygusVar();
-  void testMkSygusGrammar();
-  void testSynthFun();
-  void testSynthInv();
-  void testAddSygusConstraint();
-  void testAddSygusInvConstraint();
-  void testGetSynthSolution();
-  void testGetSynthSolutions();
-
- private:
-  std::unique_ptr<Solver> d_solver;
-};
-
-void SolverBlack::setUp() { d_solver.reset(new Solver()); }
-
-void SolverBlack::tearDown() { d_solver.reset(nullptr); }
-
-void SolverBlack::testRecoverableException()
-{
-  d_solver->setOption("produce-models", "true");
-  Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
-  d_solver->assertFormula(x.eqTerm(x).notTerm());
-  TS_ASSERT_THROWS(d_solver->getValue(x),
-                   CVC4ApiRecoverableException&);
-}
-
-void SolverBlack::testSupportsFloatingPoint()
-{
-  if (d_solver->supportsFloatingPoint())
-  {
-    TS_ASSERT_THROWS_NOTHING(
-        d_solver->mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN));
-  }
-  else
-  {
-    TS_ASSERT_THROWS(d_solver->mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN),
-                     CVC4ApiException&);
-  }
-}
-
-void SolverBlack::testGetBooleanSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->getBooleanSort());
-}
-
-void SolverBlack::testGetIntegerSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->getIntegerSort());
-}
-
-void SolverBlack::testGetNullSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->getNullSort());
-}
-
-void SolverBlack::testGetRealSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->getRealSort());
-}
-
-void SolverBlack::testGetRegExpSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->getRegExpSort());
-}
-
-void SolverBlack::testGetStringSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->getStringSort());
-}
-
-void SolverBlack::testGetRoundingModeSort()
-{
-  if (d_solver->supportsFloatingPoint())
-  {
-    TS_ASSERT_THROWS_NOTHING(d_solver->getRoundingModeSort());
-  }
-  else
-  {
-    TS_ASSERT_THROWS(d_solver->getRoundingModeSort(), CVC4ApiException&);
-  }
-}
-
-void SolverBlack::testMkArraySort()
-{
-  Sort boolSort = d_solver->getBooleanSort();
-  Sort intSort = d_solver->getIntegerSort();
-  Sort realSort = d_solver->getRealSort();
-  Sort bvSort = d_solver->mkBitVectorSort(32);
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(boolSort, boolSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(intSort, intSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(realSort, realSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, bvSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(boolSort, intSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(realSort, bvSort));
-
-  if (d_solver->supportsFloatingPoint())
-  {
-    Sort fpSort = d_solver->mkFloatingPointSort(3, 5);
-    TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(fpSort, fpSort));
-    TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, fpSort));
-  }
-
-  Solver slv;
-  TS_ASSERT_THROWS(slv.mkArraySort(boolSort, boolSort), CVC4ApiException&);
-}
-
-void SolverBlack::testMkBitVectorSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVectorSort(32));
-  TS_ASSERT_THROWS(d_solver->mkBitVectorSort(0), CVC4ApiException&);
-}
-
-void SolverBlack::testMkFloatingPointSort()
-{
-  if (d_solver->supportsFloatingPoint())
-  {
-    TS_ASSERT_THROWS_NOTHING(d_solver->mkFloatingPointSort(4, 8));
-    TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(0, 8), CVC4ApiException&);
-    TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(4, 0), CVC4ApiException&);
-  }
-  else
-  {
-    TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(4, 8), CVC4ApiException&);
-  }
-}
-
-void SolverBlack::testMkDatatypeSort()
-{
-  DatatypeDecl dtypeSpec = d_solver->mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
-  cons.addSelector("head", d_solver->getIntegerSort());
-  dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
-  dtypeSpec.addConstructor(nil);
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSort(dtypeSpec));
-
-  Solver slv;
-  TS_ASSERT_THROWS(slv.mkDatatypeSort(dtypeSpec), CVC4ApiException&);
-
-  DatatypeDecl throwsDtypeSpec = d_solver->mkDatatypeDecl("list");
-  TS_ASSERT_THROWS(d_solver->mkDatatypeSort(throwsDtypeSpec),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testMkDatatypeSorts()
-{
-  Solver slv;
-
-  DatatypeDecl dtypeSpec1 = d_solver->mkDatatypeDecl("list1");
-  DatatypeConstructorDecl cons1 = d_solver->mkDatatypeConstructorDecl("cons1");
-  cons1.addSelector("head1", d_solver->getIntegerSort());
-  dtypeSpec1.addConstructor(cons1);
-  DatatypeConstructorDecl nil1 = d_solver->mkDatatypeConstructorDecl("nil1");
-  dtypeSpec1.addConstructor(nil1);
-  DatatypeDecl dtypeSpec2 = d_solver->mkDatatypeDecl("list2");
-  DatatypeConstructorDecl cons2 = d_solver->mkDatatypeConstructorDecl("cons2");
-  cons2.addSelector("head2", d_solver->getIntegerSort());
-  dtypeSpec2.addConstructor(cons2);
-  DatatypeConstructorDecl nil2 = d_solver->mkDatatypeConstructorDecl("nil2");
-  dtypeSpec2.addConstructor(nil2);
-  std::vector<DatatypeDecl> decls = {dtypeSpec1, dtypeSpec2};
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSorts(decls));
-
-  TS_ASSERT_THROWS(slv.mkDatatypeSorts(decls), CVC4ApiException&);
-
-  DatatypeDecl throwsDtypeSpec = d_solver->mkDatatypeDecl("list");
-  std::vector<DatatypeDecl> throwsDecls = {throwsDtypeSpec};
-  TS_ASSERT_THROWS(d_solver->mkDatatypeSorts(throwsDecls), CVC4ApiException&);
-
-  /* with unresolved sorts */
-  Sort unresList = d_solver->mkUninterpretedSort("ulist");
-  std::set<Sort> unresSorts = {unresList};
-  DatatypeDecl ulist = d_solver->mkDatatypeDecl("ulist");
-  DatatypeConstructorDecl ucons = d_solver->mkDatatypeConstructorDecl("ucons");
-  ucons.addSelector("car", unresList);
-  ucons.addSelector("cdr", unresList);
-  ulist.addConstructor(ucons);
-  DatatypeConstructorDecl unil = d_solver->mkDatatypeConstructorDecl("unil");
-  ulist.addConstructor(unil);
-  std::vector<DatatypeDecl> udecls = {ulist};
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSorts(udecls, unresSorts));
-
-  TS_ASSERT_THROWS(slv.mkDatatypeSorts(udecls, unresSorts), CVC4ApiException&);
-
-  /* Note: More tests are in datatype_api_black. */
-}
-
-void SolverBlack::testMkFunctionSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkFunctionSort(
-      d_solver->mkUninterpretedSort("u"), d_solver->getIntegerSort()));
-  Sort funSort = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"),
-                                          d_solver->getIntegerSort());
-  TS_ASSERT_THROWS(
-      d_solver->mkFunctionSort(funSort, d_solver->getIntegerSort()),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->mkFunctionSort(d_solver->getIntegerSort(), funSort),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkFunctionSort(
-      {d_solver->mkUninterpretedSort("u"), d_solver->getIntegerSort()},
-      d_solver->getIntegerSort()));
-  Sort funSort2 = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"),
-                                           d_solver->getIntegerSort());
-  TS_ASSERT_THROWS(
-      d_solver->mkFunctionSort({funSort2, d_solver->mkUninterpretedSort("u")},
-                               d_solver->getIntegerSort()),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->mkFunctionSort(
-          {d_solver->getIntegerSort(), d_solver->mkUninterpretedSort("u")},
-          funSort2),
-      CVC4ApiException&);
-
-  Solver slv;
-  TS_ASSERT_THROWS(slv.mkFunctionSort(d_solver->mkUninterpretedSort("u"),
-                                      d_solver->getIntegerSort()),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.mkFunctionSort(slv.mkUninterpretedSort("u"),
-                                      d_solver->getIntegerSort()),
-                   CVC4ApiException&);
-  std::vector<Sort> sorts1 = {d_solver->getBooleanSort(),
-                              slv.getIntegerSort(),
-                              d_solver->getIntegerSort()};
-  std::vector<Sort> sorts2 = {slv.getBooleanSort(), slv.getIntegerSort()};
-  TS_ASSERT_THROWS_NOTHING(slv.mkFunctionSort(sorts2, slv.getIntegerSort()));
-  TS_ASSERT_THROWS(slv.mkFunctionSort(sorts1, slv.getIntegerSort()),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.mkFunctionSort(sorts2, d_solver->getIntegerSort()),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testMkParamSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkParamSort("T"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkParamSort(""));
-}
-
-void SolverBlack::testMkPredicateSort()
-{
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->mkPredicateSort({d_solver->getIntegerSort()}));
-  TS_ASSERT_THROWS(d_solver->mkPredicateSort({}), CVC4ApiException&);
-  Sort funSort = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"),
-                                          d_solver->getIntegerSort());
-  TS_ASSERT_THROWS(
-      d_solver->mkPredicateSort({d_solver->getIntegerSort(), funSort}),
-      CVC4ApiException&);
-
-  Solver slv;
-  TS_ASSERT_THROWS(slv.mkPredicateSort({d_solver->getIntegerSort()}),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testMkRecordSort()
-{
-  std::vector<std::pair<std::string, Sort>> fields = {
-      std::make_pair("b", d_solver->getBooleanSort()),
-      std::make_pair("bv", d_solver->mkBitVectorSort(8)),
-      std::make_pair("i", d_solver->getIntegerSort())};
-  std::vector<std::pair<std::string, Sort>> empty;
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkRecordSort(fields));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkRecordSort(empty));
-  Sort recSort = d_solver->mkRecordSort(fields);
-  TS_ASSERT_THROWS_NOTHING(recSort.getDatatype());
-
-  Solver slv;
-  TS_ASSERT_THROWS(slv.mkRecordSort(fields), CVC4ApiException&);
-}
-
-void SolverBlack::testMkSetSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkSetSort(d_solver->getBooleanSort()));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkSetSort(d_solver->getIntegerSort()));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkSetSort(d_solver->mkBitVectorSort(4)));
-  Solver slv;
-  TS_ASSERT_THROWS(slv.mkSetSort(d_solver->mkBitVectorSort(4)),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testMkBagSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBagSort(d_solver->getBooleanSort()));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBagSort(d_solver->getIntegerSort()));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBagSort(d_solver->mkBitVectorSort(4)));
-  Solver slv;
-  TS_ASSERT_THROWS(slv.mkBagSort(d_solver->mkBitVectorSort(4)),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testMkSequenceSort()
-{
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->mkSequenceSort(d_solver->getBooleanSort()));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkSequenceSort(
-      d_solver->mkSequenceSort(d_solver->getIntegerSort())));
-  Solver slv;
-  TS_ASSERT_THROWS(slv.mkSequenceSort(d_solver->getIntegerSort()),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testMkUninterpretedSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkUninterpretedSort("u"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkUninterpretedSort(""));
-}
-
-void SolverBlack::testMkSortConstructorSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkSortConstructorSort("s", 2));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkSortConstructorSort("", 2));
-  TS_ASSERT_THROWS(d_solver->mkSortConstructorSort("", 0), CVC4ApiException&);
-}
-
-void SolverBlack::testMkTupleSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTupleSort({d_solver->getIntegerSort()}));
-  Sort funSort = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"),
-                                          d_solver->getIntegerSort());
-  TS_ASSERT_THROWS(d_solver->mkTupleSort({d_solver->getIntegerSort(), funSort}),
-                   CVC4ApiException&);
-
-  Solver slv;
-  TS_ASSERT_THROWS(slv.mkTupleSort({d_solver->getIntegerSort()}),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testMkBitVector()
-{
-  uint32_t size0 = 0, size1 = 8, size2 = 32, val1 = 2;
-  uint64_t val2 = 2;
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size1, val1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(size2, val2));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 2));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 10));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1234", 10));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("1010", 16));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector("a09f", 16));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVector(8, "-127", 10));
-  TS_ASSERT_THROWS(d_solver->mkBitVector(size0, val1), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkBitVector(size0, val2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkBitVector("", 2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkBitVector("10", 3), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkBitVector("20", 2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkBitVector(8, "101010101", 2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkBitVector(8, "-256", 10), CVC4ApiException&);
-  TS_ASSERT_EQUALS(d_solver->mkBitVector("1010", 2),
-                   d_solver->mkBitVector("10", 10));
-  TS_ASSERT_EQUALS(d_solver->mkBitVector("1010", 2),
-                   d_solver->mkBitVector("a", 16));
-  TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "01010101", 2).toString(),
-                   "#b01010101");
-  TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "F", 16).toString(), "#b00001111");
-  TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "-1", 10),
-                   d_solver->mkBitVector(8, "FF", 16));
-}
-
-void SolverBlack::testMkVar()
-{
-  Sort boolSort = d_solver->getBooleanSort();
-  Sort intSort = d_solver->getIntegerSort();
-  Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort, std::string("b")));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort, ""));
-  TS_ASSERT_THROWS(d_solver->mkVar(Sort()), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkVar(Sort(), "a"), CVC4ApiException&);
-  Solver slv;
-  TS_ASSERT_THROWS(slv.mkVar(boolSort, "x"), CVC4ApiException&);
-}
-
-void SolverBlack::testMkBoolean()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoolean(true));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoolean(false));
-}
-
-void SolverBlack::testMkRoundingMode()
-{
-  if (CVC4::Configuration::isBuiltWithSymFPU())
-  {
-    TS_ASSERT_THROWS_NOTHING(
-        d_solver->mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
-  }
-  else
-  {
-    TS_ASSERT_THROWS(d_solver->mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO),
-                     CVC4ApiException&);
-  }
-}
-
-void SolverBlack::testMkUninterpretedConst()
-{
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->mkUninterpretedConst(d_solver->getBooleanSort(), 1));
-  TS_ASSERT_THROWS(d_solver->mkUninterpretedConst(Sort(), 1),
-                   CVC4ApiException&);
-  Solver slv;
-  TS_ASSERT_THROWS(slv.mkUninterpretedConst(d_solver->getBooleanSort(), 1),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testMkAbstractValue()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkAbstractValue(std::string("1")));
-  TS_ASSERT_THROWS(d_solver->mkAbstractValue(std::string("0")),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkAbstractValue(std::string("-1")),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkAbstractValue(std::string("1.2")),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkAbstractValue("1/2"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkAbstractValue("asdf"), CVC4ApiException&);
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkAbstractValue((uint32_t)1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkAbstractValue((int32_t)1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkAbstractValue((uint64_t)1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkAbstractValue((int64_t)1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkAbstractValue((int32_t)-1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkAbstractValue((int64_t)-1));
-  TS_ASSERT_THROWS(d_solver->mkAbstractValue(0), CVC4ApiException&);
-}
-
-void SolverBlack::testMkFloatingPoint()
-{
-  Term t1 = d_solver->mkBitVector(8);
-  Term t2 = d_solver->mkBitVector(4);
-  Term t3 = d_solver->mkInteger(2);
-  if (CVC4::Configuration::isBuiltWithSymFPU())
-  {
-    TS_ASSERT_THROWS_NOTHING(d_solver->mkFloatingPoint(3, 5, t1));
-  }
-  else
-  {
-    TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 5, t1), CVC4ApiException&);
-  }
-  TS_ASSERT_THROWS(d_solver->mkFloatingPoint(0, 5, Term()), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkFloatingPoint(0, 5, t1), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 0, t1), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 5, t2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 5, t2), CVC4ApiException&);
-
-  if (CVC4::Configuration::isBuiltWithSymFPU())
-  {
-    Solver slv;
-    TS_ASSERT_THROWS(slv.mkFloatingPoint(3, 5, t1), CVC4ApiException&);
-  }
-}
-
-void SolverBlack::testMkEmptySet()
-{
-  Solver slv;
-  Sort s = d_solver->mkSetSort(d_solver->getBooleanSort());
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySet(Sort()));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySet(s));
-  TS_ASSERT_THROWS(d_solver->mkEmptySet(d_solver->getBooleanSort()),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.mkEmptySet(s), CVC4ApiException&);
-}
-
-void SolverBlack::testMkEmptyBag()
-{
-  Solver slv;
-  Sort s = d_solver->mkBagSort(d_solver->getBooleanSort());
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptyBag(Sort()));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptyBag(s));
-  TS_ASSERT_THROWS(d_solver->mkEmptyBag(d_solver->getBooleanSort()),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.mkEmptyBag(s), CVC4ApiException&);
-}
-
-void SolverBlack::testMkEmptySequence()
-{
-  Solver slv;
-  Sort s = d_solver->mkSequenceSort(d_solver->getBooleanSort());
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySequence(s));
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->mkEmptySequence(d_solver->getBooleanSort()));
-  TS_ASSERT_THROWS(slv.mkEmptySequence(s), CVC4ApiException&);
-}
-
-void SolverBlack::testMkFalse()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkFalse());
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkFalse());
-}
-
-void SolverBlack::testMkNaN()
-{
-  if (CVC4::Configuration::isBuiltWithSymFPU())
-  {
-    TS_ASSERT_THROWS_NOTHING(d_solver->mkNaN(3, 5));
-  }
-  else
-  {
-    TS_ASSERT_THROWS(d_solver->mkNaN(3, 5), CVC4ApiException&);
-  }
-}
-
-void SolverBlack::testMkNegZero()
-{
-  if (CVC4::Configuration::isBuiltWithSymFPU())
-  {
-    TS_ASSERT_THROWS_NOTHING(d_solver->mkNegZero(3, 5));
-  }
-  else
-  {
-    TS_ASSERT_THROWS(d_solver->mkNegZero(3, 5), CVC4ApiException&);
-  }
-}
-
-void SolverBlack::testMkNegInf()
-{
-  if (CVC4::Configuration::isBuiltWithSymFPU())
-  {
-    TS_ASSERT_THROWS_NOTHING(d_solver->mkNegInf(3, 5));
-  }
-  else
-  {
-    TS_ASSERT_THROWS(d_solver->mkNegInf(3, 5), CVC4ApiException&);
-  }
-}
-
-void SolverBlack::testMkPosInf()
-{
-  if (CVC4::Configuration::isBuiltWithSymFPU())
-  {
-    TS_ASSERT_THROWS_NOTHING(d_solver->mkPosInf(3, 5));
-  }
-  else
-  {
-    TS_ASSERT_THROWS(d_solver->mkPosInf(3, 5), CVC4ApiException&);
-  }
-}
-
-void SolverBlack::testMkPosZero()
-{
-  if (CVC4::Configuration::isBuiltWithSymFPU())
-  {
-    TS_ASSERT_THROWS_NOTHING(d_solver->mkPosZero(3, 5));
-  }
-  else
-  {
-    TS_ASSERT_THROWS(d_solver->mkPosZero(3, 5), CVC4ApiException&);
-  }
-}
-
-void SolverBlack::testMkOp()
-{
-  // mkOp(Kind kind, Kind k)
-  TS_ASSERT_THROWS(d_solver->mkOp(BITVECTOR_EXTRACT, EQUAL), CVC4ApiException&);
-
-  // mkOp(Kind kind, const std::string& arg)
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(RECORD_UPDATE, "asdf"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(DIVISIBLE, "2147483648"));
-  TS_ASSERT_THROWS(d_solver->mkOp(BITVECTOR_EXTRACT, "asdf"),
-                   CVC4ApiException&);
-
-  // mkOp(Kind kind, uint32_t arg)
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(DIVISIBLE, 1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(BITVECTOR_ROTATE_LEFT, 1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(BITVECTOR_ROTATE_RIGHT, 1));
-  TS_ASSERT_THROWS(d_solver->mkOp(BITVECTOR_EXTRACT, 1), CVC4ApiException&);
-
-  // mkOp(Kind kind, uint32_t arg1, uint32_t arg2)
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(BITVECTOR_EXTRACT, 1, 1));
-  TS_ASSERT_THROWS(d_solver->mkOp(DIVISIBLE, 1, 2), CVC4ApiException&);
-}
-
-void SolverBlack::testMkPi() { TS_ASSERT_THROWS_NOTHING(d_solver->mkPi()); }
-
-void SolverBlack::testMkInteger()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger("123"));
-  TS_ASSERT_THROWS(d_solver->mkInteger("1.23"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger("1/23"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger("12/3"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger(".2"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger("2."), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger(""), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger("asdf"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger("1.2/3"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger("."), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger("/"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger("2/"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger("/2"), CVC4ApiException&);
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string("123")));
-  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("1.23")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("1/23")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("12/3")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger(std::string(".2")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("2.")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("asdf")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("1.2/3")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger(std::string(".")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("/")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("2/")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkInteger(std::string("/2")), CVC4ApiException&);
-
-  int32_t val1 = 1;
-  int64_t val2 = -1;
-  uint32_t val3 = 1;
-  uint64_t val4 = -1;
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val2));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val3));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val4));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkInteger(val4));
-}
-
-void SolverBlack::testMkReal()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal("123"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal("1.23"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal("1/23"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal("12/3"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(".2"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal("2."));
-  TS_ASSERT_THROWS(d_solver->mkReal(""), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkReal("asdf"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkReal("1.2/3"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkReal("."), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkReal("/"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkReal("2/"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkReal("/2"), CVC4ApiException&);
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string("123")));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string("1.23")));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string("1/23")));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string("12/3")));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string(".2")));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(std::string("2.")));
-  TS_ASSERT_THROWS(d_solver->mkReal(std::string("")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkReal(std::string("asdf")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkReal(std::string("1.2/3")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkReal(std::string(".")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkReal(std::string("/")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkReal(std::string("2/")), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkReal(std::string("/2")), CVC4ApiException&);
-
-  int32_t val1 = 1;
-  int64_t val2 = -1;
-  uint32_t val3 = 1;
-  uint64_t val4 = -1;
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val2));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val3));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val4));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val4));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val1, val1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val2, val2));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val3, val3));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(val4, val4));
-}
-
-void SolverBlack::testMkRegexpEmpty()
-{
-  Sort strSort = d_solver->getStringSort();
-  Term s = d_solver->mkConst(strSort, "s");
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpEmpty()));
-}
-
-void SolverBlack::testMkRegexpSigma()
-{
-  Sort strSort = d_solver->getStringSort();
-  Term s = d_solver->mkConst(strSort, "s");
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpSigma()));
-}
-
-void SolverBlack::testMkSepNil()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkSepNil(d_solver->getBooleanSort()));
-  TS_ASSERT_THROWS(d_solver->mkSepNil(Sort()), CVC4ApiException&);
-  Solver slv;
-  TS_ASSERT_THROWS(slv.mkSepNil(d_solver->getIntegerSort()), CVC4ApiException&);
-}
-
-void SolverBlack::testMkString()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkString(""));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkString("asdfasdf"));
-  TS_ASSERT_EQUALS(d_solver->mkString("asdf\\nasdf").toString(),
-                   "\"asdf\\u{5c}nasdf\"");
-  TS_ASSERT_EQUALS(d_solver->mkString("asdf\\u{005c}nasdf", true).toString(),
-                   "\"asdf\\u{5c}nasdf\"");
-}
-
-void SolverBlack::testMkChar()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkChar(std::string("0123")));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkChar("aA"));
-  TS_ASSERT_THROWS(d_solver->mkChar(""), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkChar("0g0"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkChar("100000"), CVC4ApiException&);
-  TS_ASSERT_EQUALS(d_solver->mkChar("abc"), d_solver->mkChar("ABC"));
-}
-
-void SolverBlack::testMkTerm()
-{
-  Sort bv32 = d_solver->mkBitVectorSort(32);
-  Term a = d_solver->mkConst(bv32, "a");
-  Term b = d_solver->mkConst(bv32, "b");
-  std::vector<Term> v1 = {a, b};
-  std::vector<Term> v2 = {a, Term()};
-  std::vector<Term> v3 = {a, d_solver->mkTrue()};
-  std::vector<Term> v4 = {d_solver->mkInteger(1), d_solver->mkInteger(2)};
-  std::vector<Term> v5 = {d_solver->mkInteger(1), Term()};
-  std::vector<Term> v6 = {};
-  Solver slv;
-
-  // mkTerm(Kind kind) const
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(PI));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(REGEXP_EMPTY));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(REGEXP_SIGMA));
-  TS_ASSERT_THROWS(d_solver->mkTerm(CONST_BITVECTOR), CVC4ApiException&);
-
-  // mkTerm(Kind kind, Term child) const
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(NOT, d_solver->mkTrue()));
-  TS_ASSERT_THROWS(d_solver->mkTerm(NOT, Term()), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(NOT, a), CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.mkTerm(NOT, d_solver->mkTrue()), CVC4ApiException&);
-
-  // mkTerm(Kind kind, Term child1, Term child2) const
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(EQUAL, a, b));
-  TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, Term(), b), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, a, Term()), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, a, d_solver->mkTrue()),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.mkTerm(EQUAL, a, b), CVC4ApiException&);
-
-  // mkTerm(Kind kind, Term child1, Term child2, Term child3) const
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(
-      ITE, d_solver->mkTrue(), d_solver->mkTrue(), d_solver->mkTrue()));
-  TS_ASSERT_THROWS(
-      d_solver->mkTerm(ITE, Term(), d_solver->mkTrue(), d_solver->mkTrue()),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->mkTerm(ITE, d_solver->mkTrue(), Term(), d_solver->mkTrue()),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->mkTerm(ITE, d_solver->mkTrue(), d_solver->mkTrue(), Term()),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->mkTerm(ITE, d_solver->mkTrue(), d_solver->mkTrue(), b),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      slv.mkTerm(
-          ITE, d_solver->mkTrue(), d_solver->mkTrue(), d_solver->mkTrue()),
-      CVC4ApiException&);
-
-  // mkTerm(Kind kind, const std::vector<Term>& children) const
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(EQUAL, v1));
-  TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, v2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, v3), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(DISTINCT, v6), CVC4ApiException&);
-}
-
-void SolverBlack::testMkTermFromOp()
-{
-  Sort bv32 = d_solver->mkBitVectorSort(32);
-  Term a = d_solver->mkConst(bv32, "a");
-  Term b = d_solver->mkConst(bv32, "b");
-  std::vector<Term> v1 = {d_solver->mkInteger(1), d_solver->mkInteger(2)};
-  std::vector<Term> v2 = {d_solver->mkInteger(1), Term()};
-  std::vector<Term> v3 = {};
-  std::vector<Term> v4 = {d_solver->mkInteger(5)};
-  Solver slv;
-
-  // simple operator terms
-  Op opterm1 = d_solver->mkOp(BITVECTOR_EXTRACT, 2, 1);
-  Op opterm2 = d_solver->mkOp(DIVISIBLE, 1);
-
-  // list datatype
-  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 consTerm1 = list.getConstructorTerm("cons");
-  Term consTerm2 = list.getConstructor("cons").getConstructorTerm();
-  Term nilTerm1 = list.getConstructorTerm("nil");
-  Term nilTerm2 = list.getConstructor("nil").getConstructorTerm();
-  Term headTerm1 = list["cons"].getSelectorTerm("head");
-  Term headTerm2 = list["cons"].getSelector("head").getSelectorTerm();
-  Term tailTerm1 = list["cons"].getSelectorTerm("tail");
-  Term tailTerm2 = list["cons"]["tail"].getSelectorTerm();
-
-  // mkTerm(Op op, Term term) const
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm2));
-  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, nilTerm1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, consTerm1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm2),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, headTerm1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm1), CVC4ApiException&);
-
-  // mkTerm(Op op, Term child) const
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, d_solver->mkInteger(1)));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, headTerm1, c));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2, c));
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, a), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkInteger(0)),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.mkTerm(opterm1, a), CVC4ApiException&);
-
-  // mkTerm(Op op, Term child1, Term child2) const
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->mkTerm(APPLY_CONSTRUCTOR,
-                       consTerm1,
-                       d_solver->mkInteger(0),
-                       d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
-  TS_ASSERT_THROWS(
-      d_solver->mkTerm(opterm2, d_solver->mkInteger(1), d_solver->mkInteger(2)),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, d_solver->mkInteger(1), Term()),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, Term(), d_solver->mkInteger(1)),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.mkTerm(APPLY_CONSTRUCTOR,
-                              consTerm1,
-                              d_solver->mkInteger(0),
-                              d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)),
-                   CVC4ApiException&);
-
-  // mkTerm(Op op, Term child1, Term child2, Term child3) const
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->mkTerm(
-          opterm2, d_solver->mkInteger(1), d_solver->mkInteger(1), Term()),
-      CVC4ApiException&);
-
-  // mkTerm(Op op, const std::vector<Term>& children) const
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, v4));
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v1), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v3), CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.mkTerm(opterm2, v4), CVC4ApiException&);
-}
-
-void SolverBlack::testMkTrue()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTrue());
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTrue());
-}
-
-void SolverBlack::testMkTuple()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTuple(
-      {d_solver->mkBitVectorSort(3)}, {d_solver->mkBitVector("101", 2)}));
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->mkTuple({d_solver->getRealSort()}, {d_solver->mkInteger("5")}));
-
-  TS_ASSERT_THROWS(d_solver->mkTuple({}, {d_solver->mkBitVector("101", 2)}),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTuple({d_solver->mkBitVectorSort(4)},
-                                     {d_solver->mkBitVector("101", 2)}),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTuple({d_solver->getIntegerSort()},
-                                     {d_solver->mkReal("5.3")}),
-                   CVC4ApiException&);
-  Solver slv;
-  TS_ASSERT_THROWS(
-      slv.mkTuple({d_solver->mkBitVectorSort(3)}, {slv.mkBitVector("101", 2)}),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      slv.mkTuple({slv.mkBitVectorSort(3)}, {d_solver->mkBitVector("101", 2)}),
-      CVC4ApiException&);
-}
-
-void SolverBlack::testMkUniverseSet()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkUniverseSet(d_solver->getBooleanSort()));
-  TS_ASSERT_THROWS(d_solver->mkUniverseSet(Sort()), CVC4ApiException&);
-  Solver slv;
-  TS_ASSERT_THROWS(slv.mkUniverseSet(d_solver->getBooleanSort()),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testMkConst()
-{
-  Sort boolSort = d_solver->getBooleanSort();
-  Sort intSort = d_solver->getIntegerSort();
-  Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(boolSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(boolSort, std::string("b")));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(intSort, std::string("i")));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort, "f"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort, ""));
-  TS_ASSERT_THROWS(d_solver->mkConst(Sort()), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkConst(Sort(), "a"), CVC4ApiException&);
-
-  Solver slv;
-  TS_ASSERT_THROWS(slv.mkConst(boolSort), CVC4ApiException&);
-}
-
-void SolverBlack::testMkConstArray()
-{
-  Sort intSort = d_solver->getIntegerSort();
-  Sort arrSort = d_solver->mkArraySort(intSort, intSort);
-  Term zero = d_solver->mkInteger(0);
-  Term constArr = d_solver->mkConstArray(arrSort, zero);
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkConstArray(arrSort, zero));
-  TS_ASSERT_THROWS(d_solver->mkConstArray(Sort(), zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkConstArray(arrSort, Term()), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkConstArray(arrSort, d_solver->mkBitVector(1, 1)),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkConstArray(intSort, zero), CVC4ApiException&);
-  Solver slv;
-  Term zero2 = slv.mkInteger(0);
-  Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort());
-  TS_ASSERT_THROWS(slv.mkConstArray(arrSort2, zero), CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.mkConstArray(arrSort, zero2), CVC4ApiException&);
-}
-
-void SolverBlack::testDeclareDatatype()
-{
-  DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
-  std::vector<DatatypeConstructorDecl> ctors1 = {nil};
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("a"), ctors1));
-  DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
-  DatatypeConstructorDecl nil2 = d_solver->mkDatatypeConstructorDecl("nil");
-  std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil2};
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("b"), ctors2));
-  DatatypeConstructorDecl cons2 = d_solver->mkDatatypeConstructorDecl("cons");
-  DatatypeConstructorDecl nil3 = d_solver->mkDatatypeConstructorDecl("nil");
-  std::vector<DatatypeConstructorDecl> ctors3 = {cons2, nil3};
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors3));
-  std::vector<DatatypeConstructorDecl> ctors4;
-  TS_ASSERT_THROWS(d_solver->declareDatatype(std::string("c"), ctors4),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors4),
-                   CVC4ApiException&);
-  Solver slv;
-  TS_ASSERT_THROWS(slv.declareDatatype(std::string("a"), ctors1),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testDeclareFun()
-{
-  Sort bvSort = d_solver->mkBitVectorSort(32);
-  Sort funSort = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"),
-                                          d_solver->getIntegerSort());
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareFun("f1", {}, bvSort));
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->declareFun("f3", {bvSort, d_solver->getIntegerSort()}, bvSort));
-  TS_ASSERT_THROWS(d_solver->declareFun("f2", {}, funSort), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->declareFun("f4", {bvSort, funSort}, bvSort),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->declareFun("f5", {bvSort, bvSort}, funSort),
-                   CVC4ApiException&);
-  Solver slv;
-  TS_ASSERT_THROWS(slv.declareFun("f1", {}, bvSort), CVC4ApiException&);
-}
-
-void SolverBlack::testDeclareSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareSort("s", 0));
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareSort("s", 2));
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareSort("", 2));
-}
-
-void SolverBlack::testDefineFun()
-{
-  Sort bvSort = d_solver->mkBitVectorSort(32);
-  Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
-  Sort funSort2 = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"),
-                                           d_solver->getIntegerSort());
-  Term b1 = d_solver->mkVar(bvSort, "b1");
-  Term b11 = d_solver->mkVar(bvSort, "b1");
-  Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2");
-  Term b3 = d_solver->mkVar(funSort2, "b3");
-  Term v1 = d_solver->mkConst(bvSort, "v1");
-  Term v2 = d_solver->mkConst(d_solver->getIntegerSort(), "v2");
-  Term v3 = d_solver->mkConst(funSort2, "v3");
-  Term f1 = d_solver->mkConst(funSort1, "f1");
-  Term f2 = d_solver->mkConst(funSort2, "f2");
-  Term f3 = d_solver->mkConst(bvSort, "f3");
-  TS_ASSERT_THROWS_NOTHING(d_solver->defineFun("f", {}, bvSort, v1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->defineFun("ff", {b1, b2}, bvSort, v1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->defineFun(f1, {b1, b11}, v1));
-  TS_ASSERT_THROWS(d_solver->defineFun("ff", {v1, b2}, bvSort, v1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFun("fff", {b1}, bvSort, v3),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFun("ffff", {b1}, funSort2, v3),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFun("fffff", {b1, b3}, bvSort, v1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFun(f1, {v1, b11}, v1), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFun(f1, {b1}, v1), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFun(f1, {b1, b11}, v2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFun(f1, {b1, b11}, v3), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFun(f2, {b1}, v2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFun(f3, {b1}, v1), CVC4ApiException&);
-
-  Solver slv;
-  Sort bvSort2 = slv.mkBitVectorSort(32);
-  Term v12 = slv.mkConst(bvSort2, "v1");
-  Term b12 = slv.mkVar(bvSort2, "b1");
-  Term b22 = slv.mkVar(slv.getIntegerSort(), "b2");
-  TS_ASSERT_THROWS(slv.defineFun("f", {}, bvSort, v12), CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.defineFun("f", {}, bvSort2, v1), CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.defineFun("ff", {b1, b22}, bvSort2, v12),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.defineFun("ff", {b12, b2}, bvSort2, v12),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.defineFun("ff", {b12, b22}, bvSort, v12),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.defineFun("ff", {b12, b22}, bvSort2, v1),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testDefineFunGlobal()
-{
-  Sort bSort = d_solver->getBooleanSort();
-  Sort fSort = d_solver->mkFunctionSort(bSort, bSort);
-
-  Term bTrue = d_solver->mkBoolean(true);
-  // (define-fun f () Bool true)
-  Term f = d_solver->defineFun("f", {}, bSort, bTrue, true);
-  Term b = d_solver->mkVar(bSort, "b");
-  Term gSym = d_solver->mkConst(fSort, "g");
-  // (define-fun g (b Bool) Bool b)
-  Term g = d_solver->defineFun(gSym, {b}, b, true);
-
-  // (assert (or (not f) (not (g true))))
-  d_solver->assertFormula(d_solver->mkTerm(
-      OR, f.notTerm(), d_solver->mkTerm(APPLY_UF, g, bTrue).notTerm()));
-  TS_ASSERT(d_solver->checkSat().isUnsat());
-  d_solver->resetAssertions();
-  // (assert (or (not f) (not (g true))))
-  d_solver->assertFormula(d_solver->mkTerm(
-      OR, f.notTerm(), d_solver->mkTerm(APPLY_UF, g, bTrue).notTerm()));
-  TS_ASSERT(d_solver->checkSat().isUnsat());
-}
-
-void SolverBlack::testDefineFunRec()
-{
-  Sort bvSort = d_solver->mkBitVectorSort(32);
-  Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
-  Sort funSort2 = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"),
-                                           d_solver->getIntegerSort());
-  Term b1 = d_solver->mkVar(bvSort, "b1");
-  Term b11 = d_solver->mkVar(bvSort, "b1");
-  Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2");
-  Term b3 = d_solver->mkVar(funSort2, "b3");
-  Term v1 = d_solver->mkConst(bvSort, "v1");
-  Term v2 = d_solver->mkConst(d_solver->getIntegerSort(), "v2");
-  Term v3 = d_solver->mkConst(funSort2, "v3");
-  Term f1 = d_solver->mkConst(funSort1, "f1");
-  Term f2 = d_solver->mkConst(funSort2, "f2");
-  Term f3 = d_solver->mkConst(bvSort, "f3");
-  TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec("f", {}, bvSort, v1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec("ff", {b1, b2}, bvSort, v1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec(f1, {b1, b11}, v1));
-  TS_ASSERT_THROWS(d_solver->defineFunRec("fff", {b1}, bvSort, v3),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFunRec("ff", {b1, v2}, bvSort, v1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFunRec("ffff", {b1}, funSort2, v3),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFunRec("fffff", {b1, b3}, bvSort, v1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFunRec(f1, {b1}, v1), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFunRec(f1, {b1, b11}, v2),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFunRec(f1, {b1, b11}, v3),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFunRec(f2, {b1}, v2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFunRec(f3, {b1}, v1), CVC4ApiException&);
-
-  Solver slv;
-  Sort bvSort2 = slv.mkBitVectorSort(32);
-  Term v12 = slv.mkConst(bvSort2, "v1");
-  Term b12 = slv.mkVar(bvSort2, "b1");
-  Term b22 = slv.mkVar(slv.getIntegerSort(), "b2");
-  TS_ASSERT_THROWS_NOTHING(slv.defineFunRec("f", {}, bvSort2, v12));
-  TS_ASSERT_THROWS_NOTHING(slv.defineFunRec("ff", {b12, b22}, bvSort2, v12));
-  TS_ASSERT_THROWS(slv.defineFunRec("f", {}, bvSort, v12), CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.defineFunRec("f", {}, bvSort2, v1), CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.defineFunRec("ff", {b1, b22}, bvSort2, v12),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.defineFunRec("ff", {b12, b2}, bvSort2, v12),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.defineFunRec("ff", {b12, b22}, bvSort, v12),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.defineFunRec("ff", {b12, b22}, bvSort2, v1),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testDefineFunRecWrongLogic()
-{
-  d_solver->setLogic("QF_BV");
-  Sort bvSort = d_solver->mkBitVectorSort(32);
-  Sort funSort = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
-  Term b = d_solver->mkVar(bvSort, "b");
-  Term v = d_solver->mkConst(bvSort, "v");
-  Term f = d_solver->mkConst(funSort, "f");
-  TS_ASSERT_THROWS(d_solver->defineFunRec("f", {}, bvSort, v),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFunRec(f, {b, b}, v), CVC4ApiException&);
-}
-
-void SolverBlack::testDefineFunRecGlobal()
-{
-  Sort bSort = d_solver->getBooleanSort();
-  Sort fSort = d_solver->mkFunctionSort(bSort, bSort);
-
-  d_solver->push();
-  Term bTrue = d_solver->mkBoolean(true);
-  // (define-fun f () Bool true)
-  Term f = d_solver->defineFunRec("f", {}, bSort, bTrue, true);
-  Term b = d_solver->mkVar(bSort, "b");
-  Term gSym = d_solver->mkConst(fSort, "g");
-  // (define-fun g (b Bool) Bool b)
-  Term g = d_solver->defineFunRec(gSym, {b}, b, true);
-
-  // (assert (or (not f) (not (g true))))
-  d_solver->assertFormula(d_solver->mkTerm(
-      OR, f.notTerm(), d_solver->mkTerm(APPLY_UF, g, bTrue).notTerm()));
-  TS_ASSERT(d_solver->checkSat().isUnsat());
-  d_solver->pop();
-  // (assert (or (not f) (not (g true))))
-  d_solver->assertFormula(d_solver->mkTerm(
-      OR, f.notTerm(), d_solver->mkTerm(APPLY_UF, g, bTrue).notTerm()));
-  TS_ASSERT(d_solver->checkSat().isUnsat());
-}
-
-void SolverBlack::testDefineFunsRec()
-{
-  Sort uSort = d_solver->mkUninterpretedSort("u");
-  Sort bvSort = d_solver->mkBitVectorSort(32);
-  Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
-  Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort());
-  Term b1 = d_solver->mkVar(bvSort, "b1");
-  Term b11 = d_solver->mkVar(bvSort, "b1");
-  Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2");
-  Term b3 = d_solver->mkVar(funSort2, "b3");
-  Term b4 = d_solver->mkVar(uSort, "b4");
-  Term v1 = d_solver->mkConst(bvSort, "v1");
-  Term v2 = d_solver->mkConst(d_solver->getIntegerSort(), "v2");
-  Term v3 = d_solver->mkConst(funSort2, "v3");
-  Term v4 = d_solver->mkConst(uSort, "v4");
-  Term f1 = d_solver->mkConst(funSort1, "f1");
-  Term f2 = d_solver->mkConst(funSort2, "f2");
-  Term f3 = d_solver->mkConst(bvSort, "f3");
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2}));
-  TS_ASSERT_THROWS(
-      d_solver->defineFunsRec({f1, f2}, {{v1, b11}, {b4}}, {v1, v2}),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}),
-      CVC4ApiException&);
-
-  Solver slv;
-  Sort uSort2 = slv.mkUninterpretedSort("u");
-  Sort bvSort2 = slv.mkBitVectorSort(32);
-  Sort funSort12 = slv.mkFunctionSort({bvSort2, bvSort2}, bvSort2);
-  Sort funSort22 = slv.mkFunctionSort(uSort2, slv.getIntegerSort());
-  Term b12 = slv.mkVar(bvSort2, "b1");
-  Term b112 = slv.mkVar(bvSort2, "b1");
-  Term b42 = slv.mkVar(uSort2, "b4");
-  Term v12 = slv.mkConst(bvSort2, "v1");
-  Term v22 = slv.mkConst(slv.getIntegerSort(), "v2");
-  Term f12 = slv.mkConst(funSort12, "f1");
-  Term f22 = slv.mkConst(funSort22, "f2");
-  TS_ASSERT_THROWS_NOTHING(
-      slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v22}));
-  TS_ASSERT_THROWS(
-      slv.defineFunsRec({f1, f22}, {{b12, b112}, {b42}}, {v12, v22}),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      slv.defineFunsRec({f12, f2}, {{b12, b112}, {b42}}, {v12, v22}),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      slv.defineFunsRec({f12, f22}, {{b1, b112}, {b42}}, {v12, v22}),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      slv.defineFunsRec({f12, f22}, {{b12, b11}, {b42}}, {v12, v22}),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      slv.defineFunsRec({f12, f22}, {{b12, b112}, {b4}}, {v12, v22}),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v1, v22}),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v2}),
-      CVC4ApiException&);
-}
-
-void SolverBlack::testDefineFunsRecWrongLogic()
-{
-  d_solver->setLogic("QF_BV");
-  Sort uSort = d_solver->mkUninterpretedSort("u");
-  Sort bvSort = d_solver->mkBitVectorSort(32);
-  Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
-  Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort());
-  Term b = d_solver->mkVar(bvSort, "b");
-  Term u = d_solver->mkVar(uSort, "u");
-  Term v1 = d_solver->mkConst(bvSort, "v1");
-  Term v2 = d_solver->mkConst(d_solver->getIntegerSort(), "v2");
-  Term f1 = d_solver->mkConst(funSort1, "f1");
-  Term f2 = d_solver->mkConst(funSort2, "f2");
-  TS_ASSERT_THROWS(d_solver->defineFunsRec({f1, f2}, {{b, b}, {u}}, {v1, v2}),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testDefineFunsRecGlobal()
-{
-  Sort bSort = d_solver->getBooleanSort();
-  Sort fSort = d_solver->mkFunctionSort(bSort, bSort);
-
-  d_solver->push();
-  Term bTrue = d_solver->mkBoolean(true);
-  Term b = d_solver->mkVar(bSort, "b");
-  Term gSym = d_solver->mkConst(fSort, "g");
-  // (define-funs-rec ((g ((b Bool)) Bool)) (b))
-  d_solver->defineFunsRec({gSym}, {{b}}, {b}, true);
-
-  // (assert (not (g true)))
-  d_solver->assertFormula(d_solver->mkTerm(APPLY_UF, gSym, bTrue).notTerm());
-  TS_ASSERT(d_solver->checkSat().isUnsat());
-  d_solver->pop();
-  // (assert (not (g true)))
-  d_solver->assertFormula(d_solver->mkTerm(APPLY_UF, gSym, bTrue).notTerm());
-  TS_ASSERT(d_solver->checkSat().isUnsat());
-}
-
-void SolverBlack::testUFIteration()
-{
-  Sort intSort = d_solver->getIntegerSort();
-  Sort funSort = d_solver->mkFunctionSort({intSort, intSort}, intSort);
-  Term x = d_solver->mkConst(intSort, "x");
-  Term y = d_solver->mkConst(intSort, "y");
-  Term f = d_solver->mkConst(funSort, "f");
-  Term fxy = d_solver->mkTerm(APPLY_UF, f, x, y);
-
-  // Expecting the uninterpreted function to be one of the children
-  Term expected_children[3] = {f, x, y};
-  uint32_t idx = 0;
-  for (auto c : fxy)
-  {
-    TS_ASSERT(idx < 3);
-    TS_ASSERT(c == expected_children[idx]);
-    idx++;
-  }
-}
-
-void SolverBlack::testGetInfo()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->getInfo("name"));
-  TS_ASSERT_THROWS(d_solver->getInfo("asdf"), CVC4ApiException&);
-}
-
-void SolverBlack::testGetInterpolant()
-{
-  // TODO
-}
-
-void SolverBlack::testGetOp()
-{
-  Sort bv32 = d_solver->mkBitVectorSort(32);
-  Term a = d_solver->mkConst(bv32, "a");
-  Op ext = d_solver->mkOp(BITVECTOR_EXTRACT, 2, 1);
-  Term exta = d_solver->mkTerm(ext, a);
-
-  TS_ASSERT(!a.hasOp());
-  TS_ASSERT_THROWS(a.getOp(), CVC4ApiException&);
-  TS_ASSERT(exta.hasOp());
-  TS_ASSERT_EQUALS(exta.getOp(), ext);
-
-  // Test Datatypes -- more complicated
-  DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
-  cons.addSelector("head", d_solver->getIntegerSort());
-  cons.addSelectorSelf("tail");
-  consListSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
-  consListSpec.addConstructor(nil);
-  Sort consListSort = d_solver->mkDatatypeSort(consListSpec);
-  Datatype consList = consListSort.getDatatype();
-
-  Term consTerm = consList.getConstructorTerm("cons");
-  Term nilTerm = consList.getConstructorTerm("nil");
-  Term headTerm = consList["cons"].getSelectorTerm("head");
-
-  Term listnil = d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm);
-  Term listcons1 = d_solver->mkTerm(
-      APPLY_CONSTRUCTOR, consTerm, d_solver->mkInteger(1), listnil);
-  Term listhead = d_solver->mkTerm(APPLY_SELECTOR, headTerm, listcons1);
-
-  TS_ASSERT(listnil.hasOp());
-  TS_ASSERT_EQUALS(listnil.getOp(), Op(d_solver.get(), APPLY_CONSTRUCTOR));
-
-  TS_ASSERT(listcons1.hasOp());
-  TS_ASSERT_EQUALS(listcons1.getOp(), Op(d_solver.get(), APPLY_CONSTRUCTOR));
-
-  TS_ASSERT(listhead.hasOp());
-  TS_ASSERT_EQUALS(listhead.getOp(), Op(d_solver.get(), APPLY_SELECTOR));
-}
-
-void SolverBlack::testGetOption()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->getOption("incremental"));
-  TS_ASSERT_THROWS(d_solver->getOption("asdf"), CVC4ApiException&);
-}
-
-void SolverBlack::testGetUnsatAssumptions1()
-{
-#if IS_PROOFS_BUILD
-  d_solver->setOption("incremental", "false");
-  d_solver->checkSatAssuming(d_solver->mkFalse());
-  TS_ASSERT_THROWS(d_solver->getUnsatAssumptions(), CVC4ApiException&);
-#endif
-}
-
-void SolverBlack::testGetUnsatAssumptions2()
-{
-#if IS_PROOFS_BUILD
-  d_solver->setOption("incremental", "true");
-  d_solver->setOption("produce-unsat-assumptions", "false");
-  d_solver->checkSatAssuming(d_solver->mkFalse());
-  TS_ASSERT_THROWS(d_solver->getUnsatAssumptions(), CVC4ApiException&);
-#endif
-}
-
-void SolverBlack::testGetUnsatAssumptions3()
-{
-#if IS_PROOFS_BUILD
-  d_solver->setOption("incremental", "true");
-  d_solver->setOption("produce-unsat-assumptions", "true");
-  d_solver->checkSatAssuming(d_solver->mkFalse());
-  TS_ASSERT_THROWS_NOTHING(d_solver->getUnsatAssumptions());
-  d_solver->checkSatAssuming(d_solver->mkTrue());
-  TS_ASSERT_THROWS(d_solver->getUnsatAssumptions(), CVC4ApiException&);
-#endif
-}
-
-void SolverBlack::testGetUnsatCore1()
-{
-#if IS_PROOFS_BUILD
-  d_solver->setOption("incremental", "false");
-  d_solver->assertFormula(d_solver->mkFalse());
-  d_solver->checkSat();
-  TS_ASSERT_THROWS(d_solver->getUnsatCore(), CVC4ApiException&);
-#endif
-}
-
-void SolverBlack::testGetUnsatCore2()
-{
-#if IS_PROOFS_BUILD
-  d_solver->setOption("incremental", "false");
-  d_solver->setOption("produce-unsat-cores", "false");
-  d_solver->assertFormula(d_solver->mkFalse());
-  d_solver->checkSat();
-  TS_ASSERT_THROWS(d_solver->getUnsatCore(), CVC4ApiException&);
-#endif
-}
-
-void SolverBlack::testGetUnsatCore3()
-{
-#if IS_PROOFS_BUILD
-  d_solver->setOption("incremental", "true");
-  d_solver->setOption("produce-unsat-cores", "true");
-
-  Sort uSort = d_solver->mkUninterpretedSort("u");
-  Sort intSort = d_solver->getIntegerSort();
-  Sort boolSort = d_solver->getBooleanSort();
-  Sort uToIntSort = d_solver->mkFunctionSort(uSort, intSort);
-  Sort intPredSort = d_solver->mkFunctionSort(intSort, boolSort);
-  std::vector<Term> unsat_core;
-
-  Term x = d_solver->mkConst(uSort, "x");
-  Term y = d_solver->mkConst(uSort, "y");
-  Term f = d_solver->mkConst(uToIntSort, "f");
-  Term p = d_solver->mkConst(intPredSort, "p");
-  Term zero = d_solver->mkInteger(0);
-  Term one = d_solver->mkInteger(1);
-  Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
-  Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
-  Term sum = d_solver->mkTerm(PLUS, f_x, f_y);
-  Term p_0 = d_solver->mkTerm(APPLY_UF, p, zero);
-  Term p_f_y = d_solver->mkTerm(APPLY_UF, p, f_y);
-  d_solver->assertFormula(d_solver->mkTerm(GT, zero, f_x));
-  d_solver->assertFormula(d_solver->mkTerm(GT, zero, f_y));
-  d_solver->assertFormula(d_solver->mkTerm(GT, sum, one));
-  d_solver->assertFormula(p_0);
-  d_solver->assertFormula(p_f_y.notTerm());
-  TS_ASSERT(d_solver->checkSat().isUnsat());
-
-  TS_ASSERT_THROWS_NOTHING(unsat_core = d_solver->getUnsatCore());
-
-  d_solver->resetAssertions();
-  for (const auto& t : unsat_core)
-  {
-    d_solver->assertFormula(t);
-  }
-  Result res = d_solver->checkSat();
-  TS_ASSERT(res.isUnsat());
-#endif
-}
-
-void SolverBlack::testGetValue1()
-{
-  d_solver->setOption("produce-models", "false");
-  Term t = d_solver->mkTrue();
-  d_solver->assertFormula(t);
-  d_solver->checkSat();
-  TS_ASSERT_THROWS(d_solver->getValue(t), CVC4ApiException&);
-}
-
-void SolverBlack::testGetValue2()
-{
-  d_solver->setOption("produce-models", "true");
-  Term t = d_solver->mkFalse();
-  d_solver->assertFormula(t);
-  d_solver->checkSat();
-  TS_ASSERT_THROWS(d_solver->getValue(t), CVC4ApiException&);
-}
-
-void SolverBlack::testGetValue3()
-{
-  d_solver->setOption("produce-models", "true");
-  Sort uSort = d_solver->mkUninterpretedSort("u");
-  Sort intSort = d_solver->getIntegerSort();
-  Sort boolSort = d_solver->getBooleanSort();
-  Sort uToIntSort = d_solver->mkFunctionSort(uSort, intSort);
-  Sort intPredSort = d_solver->mkFunctionSort(intSort, boolSort);
-  std::vector<Term> unsat_core;
-
-  Term x = d_solver->mkConst(uSort, "x");
-  Term y = d_solver->mkConst(uSort, "y");
-  Term z = d_solver->mkConst(uSort, "z");
-  Term f = d_solver->mkConst(uToIntSort, "f");
-  Term p = d_solver->mkConst(intPredSort, "p");
-  Term zero = d_solver->mkInteger(0);
-  Term one = d_solver->mkInteger(1);
-  Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
-  Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
-  Term sum = d_solver->mkTerm(PLUS, f_x, f_y);
-  Term p_0 = d_solver->mkTerm(APPLY_UF, p, zero);
-  Term p_f_y = d_solver->mkTerm(APPLY_UF, p, f_y);
-
-  d_solver->assertFormula(d_solver->mkTerm(LEQ, zero, f_x));
-  d_solver->assertFormula(d_solver->mkTerm(LEQ, zero, f_y));
-  d_solver->assertFormula(d_solver->mkTerm(LEQ, sum, one));
-  d_solver->assertFormula(p_0.notTerm());
-  d_solver->assertFormula(p_f_y);
-  TS_ASSERT(d_solver->checkSat().isSat());
-  TS_ASSERT_THROWS_NOTHING(d_solver->getValue(x));
-  TS_ASSERT_THROWS_NOTHING(d_solver->getValue(y));
-  TS_ASSERT_THROWS_NOTHING(d_solver->getValue(z));
-  TS_ASSERT_THROWS_NOTHING(d_solver->getValue(sum));
-  TS_ASSERT_THROWS_NOTHING(d_solver->getValue(p_f_y));
-
-  Solver slv;
-  TS_ASSERT_THROWS(slv.getValue(x), CVC4ApiException&);
-}
-
-void SolverBlack::testGetQuantifierElimination()
-{
-  Term x = d_solver->mkVar(d_solver->getBooleanSort(), "x");
-  Term forall =
-      d_solver->mkTerm(FORALL,
-                       d_solver->mkTerm(BOUND_VAR_LIST, x),
-                       d_solver->mkTerm(OR, x, d_solver->mkTerm(NOT, x)));
-  TS_ASSERT_THROWS(d_solver->getQuantifierElimination(Term()),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->getQuantifierElimination(Solver().mkBoolean(false)),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver->getQuantifierElimination(forall));
-}
-
-void SolverBlack::testGetQuantifierEliminationDisjunct()
-{
-  Term x = d_solver->mkVar(d_solver->getBooleanSort(), "x");
-  Term forall =
-      d_solver->mkTerm(FORALL,
-                       d_solver->mkTerm(BOUND_VAR_LIST, x),
-                       d_solver->mkTerm(OR, x, d_solver->mkTerm(NOT, x)));
-  TS_ASSERT_THROWS(d_solver->getQuantifierEliminationDisjunct(Term()),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->getQuantifierEliminationDisjunct(Solver().mkBoolean(false)),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver->getQuantifierEliminationDisjunct(forall));
-}
-
-void SolverBlack::testDeclareSeparationHeap()
-{
-  d_solver->setLogic("ALL_SUPPORTED");
-  Sort integer = d_solver->getIntegerSort();
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareSeparationHeap(integer, integer));
-  // cannot declare separation logic heap more than once
-  TS_ASSERT_THROWS(d_solver->declareSeparationHeap(integer, integer),
-                   CVC4ApiException&);
-}
-
-namespace {
-/**
- * Helper function for testGetSeparation{Heap,Nil}TermX. Asserts and checks
- * some simple separation logic constraints.
- */
-void checkSimpleSeparationConstraints(Solver* solver)
-{
-  Sort integer = solver->getIntegerSort();
-  // declare the separation heap
-  solver->declareSeparationHeap(integer, integer);
-  Term x = solver->mkConst(integer, "x");
-  Term p = solver->mkConst(integer, "p");
-  Term heap = solver->mkTerm(Kind::SEP_PTO, p, x);
-  solver->assertFormula(heap);
-  Term nil = solver->mkSepNil(integer);
-  solver->assertFormula(nil.eqTerm(solver->mkReal(5)));
-  solver->checkSat();
-}
-}  // namespace
-
-void SolverBlack::testGetSeparationHeapTerm1()
-{
-  d_solver->setLogic("QF_BV");
-  d_solver->setOption("incremental", "false");
-  d_solver->setOption("produce-models", "true");
-  Term t = d_solver->mkTrue();
-  d_solver->assertFormula(t);
-  TS_ASSERT_THROWS(d_solver->getSeparationHeap(), CVC4ApiException&);
-}
-
-void SolverBlack::testGetSeparationHeapTerm2()
-{
-  d_solver->setLogic("ALL_SUPPORTED");
-  d_solver->setOption("incremental", "false");
-  d_solver->setOption("produce-models", "false");
-  checkSimpleSeparationConstraints(d_solver.get());
-  TS_ASSERT_THROWS(d_solver->getSeparationHeap(), CVC4ApiException&);
-}
-
-void SolverBlack::testGetSeparationHeapTerm3()
-{
-  d_solver->setLogic("ALL_SUPPORTED");
-  d_solver->setOption("incremental", "false");
-  d_solver->setOption("produce-models", "true");
-  Term t = d_solver->mkFalse();
-  d_solver->assertFormula(t);
-  d_solver->checkSat();
-  TS_ASSERT_THROWS(d_solver->getSeparationHeap(), CVC4ApiException&);
-}
-
-void SolverBlack::testGetSeparationHeapTerm4()
-{
-  d_solver->setLogic("ALL_SUPPORTED");
-  d_solver->setOption("incremental", "false");
-  d_solver->setOption("produce-models", "true");
-  Term t = d_solver->mkTrue();
-  d_solver->assertFormula(t);
-  d_solver->checkSat();
-  TS_ASSERT_THROWS(d_solver->getSeparationHeap(), CVC4ApiException&);
-}
-
-void SolverBlack::testGetSeparationHeapTerm5()
-{
-  d_solver->setLogic("ALL_SUPPORTED");
-  d_solver->setOption("incremental", "false");
-  d_solver->setOption("produce-models", "true");
-  checkSimpleSeparationConstraints(d_solver.get());
-  TS_ASSERT_THROWS_NOTHING(d_solver->getSeparationHeap());
-}
-
-void SolverBlack::testGetSeparationNilTerm1()
-{
-  d_solver->setLogic("QF_BV");
-  d_solver->setOption("incremental", "false");
-  d_solver->setOption("produce-models", "true");
-  Term t = d_solver->mkTrue();
-  d_solver->assertFormula(t);
-  TS_ASSERT_THROWS(d_solver->getSeparationNilTerm(), CVC4ApiException&);
-}
-
-void SolverBlack::testGetSeparationNilTerm2()
-{
-  d_solver->setLogic("ALL_SUPPORTED");
-  d_solver->setOption("incremental", "false");
-  d_solver->setOption("produce-models", "false");
-  checkSimpleSeparationConstraints(d_solver.get());
-  TS_ASSERT_THROWS(d_solver->getSeparationNilTerm(), CVC4ApiException&);
-}
-
-void SolverBlack::testGetSeparationNilTerm3()
-{
-  d_solver->setLogic("ALL_SUPPORTED");
-  d_solver->setOption("incremental", "false");
-  d_solver->setOption("produce-models", "true");
-  Term t = d_solver->mkFalse();
-  d_solver->assertFormula(t);
-  d_solver->checkSat();
-  TS_ASSERT_THROWS(d_solver->getSeparationNilTerm(), CVC4ApiException&);
-}
-
-void SolverBlack::testGetSeparationNilTerm4()
-{
-  d_solver->setLogic("ALL_SUPPORTED");
-  d_solver->setOption("incremental", "false");
-  d_solver->setOption("produce-models", "true");
-  Term t = d_solver->mkTrue();
-  d_solver->assertFormula(t);
-  d_solver->checkSat();
-  TS_ASSERT_THROWS(d_solver->getSeparationNilTerm(), CVC4ApiException&);
-}
-
-void SolverBlack::testGetSeparationNilTerm5()
-{
-  d_solver->setLogic("ALL_SUPPORTED");
-  d_solver->setOption("incremental", "false");
-  d_solver->setOption("produce-models", "true");
-  checkSimpleSeparationConstraints(d_solver.get());
-  TS_ASSERT_THROWS_NOTHING(d_solver->getSeparationNilTerm());
-}
-
-void SolverBlack::testPush1()
-{
-  d_solver->setOption("incremental", "true");
-  TS_ASSERT_THROWS_NOTHING(d_solver->push(1));
-  TS_ASSERT_THROWS(d_solver->setOption("incremental", "false"),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->setOption("incremental", "true"),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testPush2()
-{
-  d_solver->setOption("incremental", "false");
-  TS_ASSERT_THROWS(d_solver->push(1), CVC4ApiException&);
-}
-
-void SolverBlack::testPop1()
-{
-  d_solver->setOption("incremental", "false");
-  TS_ASSERT_THROWS(d_solver->pop(1), CVC4ApiException&);
-}
-
-void SolverBlack::testPop2()
-{
-  d_solver->setOption("incremental", "true");
-  TS_ASSERT_THROWS(d_solver->pop(1), CVC4ApiException&);
-}
-
-void SolverBlack::testPop3()
-{
-  d_solver->setOption("incremental", "true");
-  TS_ASSERT_THROWS_NOTHING(d_solver->push(1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->pop(1));
-  TS_ASSERT_THROWS(d_solver->pop(1), CVC4ApiException&);
-}
-
-void SolverBlack::testBlockModel1()
-{
-  d_solver->setOption("produce-models", "true");
-  Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  d_solver->checkSat();
-  TS_ASSERT_THROWS(d_solver->blockModel(), CVC4ApiException&);
-}
-
-void SolverBlack::testBlockModel2()
-{
-  d_solver->setOption("block-models", "literals");
-  Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  d_solver->checkSat();
-  TS_ASSERT_THROWS(d_solver->blockModel(), CVC4ApiException&);
-}
-
-void SolverBlack::testBlockModel3()
-{
-  d_solver->setOption("produce-models", "true");
-  d_solver->setOption("block-models", "literals");
-  Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  TS_ASSERT_THROWS(d_solver->blockModel(), CVC4ApiException&);
-}
-
-void SolverBlack::testBlockModel4()
-{
-  d_solver->setOption("produce-models", "true");
-  d_solver->setOption("block-models", "literals");
-  Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  d_solver->checkSat();
-  TS_ASSERT_THROWS_NOTHING(d_solver->blockModel());
-}
-
-void SolverBlack::testBlockModelValues1()
-{
-  d_solver->setOption("produce-models", "true");
-  d_solver->setOption("block-models", "literals");
-  Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  d_solver->checkSat();
-  TS_ASSERT_THROWS(d_solver->blockModelValues({}), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->blockModelValues({Term()}), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->blockModelValues({Solver().mkBoolean(false)}),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testBlockModelValues2()
-{
-  d_solver->setOption("produce-models", "true");
-  Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  d_solver->checkSat();
-  TS_ASSERT_THROWS(d_solver->blockModelValues({x}), CVC4ApiException&);
-}
-
-void SolverBlack::testBlockModelValues3()
-{
-  d_solver->setOption("block-models", "literals");
-  Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  d_solver->checkSat();
-  TS_ASSERT_THROWS(d_solver->blockModelValues({x}), CVC4ApiException&);
-}
-
-void SolverBlack::testBlockModelValues4()
-{
-  d_solver->setOption("produce-models", "true");
-  d_solver->setOption("block-models", "literals");
-  Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  TS_ASSERT_THROWS(d_solver->blockModelValues({x}), CVC4ApiException&);
-}
-
-void SolverBlack::testBlockModelValues5()
-{
-  d_solver->setOption("produce-models", "true");
-  d_solver->setOption("block-models", "literals");
-  Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  d_solver->checkSat();
-  TS_ASSERT_THROWS_NOTHING(d_solver->blockModelValues({x}));
-}
-
-void SolverBlack::testSetInfo()
-{
-  TS_ASSERT_THROWS(d_solver->setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->setInfo("cvc2-logic", "QF_BV"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->setInfo("cvc4-logic", "asdf"), CVC4ApiException&);
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("source", "asdf"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("category", "asdf"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("difficulty", "asdf"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("filename", "asdf"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("license", "asdf"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("name", "asdf"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("notes", "asdf"));
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("smt-lib-version", "2"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("smt-lib-version", "2.0"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("smt-lib-version", "2.5"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("smt-lib-version", "2.6"));
-  TS_ASSERT_THROWS(d_solver->setInfo("smt-lib-version", ".0"),
-                   CVC4ApiException&);
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("status", "sat"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("status", "unsat"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("status", "unknown"));
-  TS_ASSERT_THROWS(d_solver->setInfo("status", "asdf"), CVC4ApiException&);
-}
-
-void SolverBlack::testSimplify()
-{
-  TS_ASSERT_THROWS(d_solver->simplify(Term()), CVC4ApiException&);
-
-  Sort bvSort = d_solver->mkBitVectorSort(32);
-  Sort uSort = d_solver->mkUninterpretedSort("u");
-  Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
-  Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort());
-  DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
-  cons.addSelector("head", d_solver->getIntegerSort());
-  cons.addSelectorSelf("tail");
-  consListSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
-  consListSpec.addConstructor(nil);
-  Sort consListSort = d_solver->mkDatatypeSort(consListSpec);
-
-  Term x = d_solver->mkConst(bvSort, "x");
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(x));
-  Term a = d_solver->mkConst(bvSort, "a");
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(a));
-  Term b = d_solver->mkConst(bvSort, "b");
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(b));
-  Term x_eq_x = d_solver->mkTerm(EQUAL, x, x);
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(x_eq_x));
-  TS_ASSERT(d_solver->mkTrue() != x_eq_x);
-  TS_ASSERT(d_solver->mkTrue() == d_solver->simplify(x_eq_x));
-  Term x_eq_b = d_solver->mkTerm(EQUAL, x, b);
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(x_eq_b));
-  TS_ASSERT(d_solver->mkTrue() != x_eq_b);
-  TS_ASSERT(d_solver->mkTrue() != d_solver->simplify(x_eq_b));
-  Solver slv;
-  TS_ASSERT_THROWS(slv.simplify(x), CVC4ApiException&);
-
-  Term i1 = d_solver->mkConst(d_solver->getIntegerSort(), "i1");
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i1));
-  Term i2 = d_solver->mkTerm(MULT, i1, d_solver->mkInteger("23"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i2));
-  TS_ASSERT(i1 != i2);
-  TS_ASSERT(i1 != d_solver->simplify(i2));
-  Term i3 = d_solver->mkTerm(PLUS, i1, d_solver->mkInteger(0));
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i3));
-  TS_ASSERT(i1 != i3);
-  TS_ASSERT(i1 == d_solver->simplify(i3));
-
-  Datatype consList = consListSort.getDatatype();
-  Term dt1 = d_solver->mkTerm(
-      APPLY_CONSTRUCTOR,
-      consList.getConstructorTerm("cons"),
-      d_solver->mkInteger(0),
-      d_solver->mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt1));
-  Term dt2 = d_solver->mkTerm(
-      APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1);
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt2));
-
-  Term b1 = d_solver->mkVar(bvSort, "b1");
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(b1));
-  Term b2 = d_solver->mkVar(bvSort, "b1");
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(b2));
-  Term b3 = d_solver->mkVar(uSort, "b3");
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(b3));
-  Term v1 = d_solver->mkConst(bvSort, "v1");
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(v1));
-  Term v2 = d_solver->mkConst(d_solver->getIntegerSort(), "v2");
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(v2));
-  Term f1 = d_solver->mkConst(funSort1, "f1");
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f1));
-  Term f2 = d_solver->mkConst(funSort2, "f2");
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f2));
-  d_solver->defineFunsRec({f1, f2}, {{b1, b2}, {b3}}, {v1, v2});
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f2));
-}
-
-void SolverBlack::testAssertFormula()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->assertFormula(d_solver->mkTrue()));
-  TS_ASSERT_THROWS(d_solver->assertFormula(Term()), CVC4ApiException&);
-  Solver slv;
-  TS_ASSERT_THROWS(slv.assertFormula(d_solver->mkTrue()), CVC4ApiException&);
-}
-
-void SolverBlack::testCheckEntailed()
-{
-  d_solver->setOption("incremental", "false");
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
-  TS_ASSERT_THROWS(d_solver->checkEntailed(d_solver->mkTrue()),
-                   CVC4ApiException&);
-  Solver slv;
-  TS_ASSERT_THROWS(slv.checkEntailed(d_solver->mkTrue()), CVC4ApiException&);
-}
-
-void SolverBlack::testCheckEntailed1()
-{
-  Sort boolSort = d_solver->getBooleanSort();
-  Term x = d_solver->mkConst(boolSort, "x");
-  Term y = d_solver->mkConst(boolSort, "y");
-  Term z = d_solver->mkTerm(AND, x, y);
-  d_solver->setOption("incremental", "true");
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
-  TS_ASSERT_THROWS(d_solver->checkEntailed(Term()), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(z));
-  Solver slv;
-  TS_ASSERT_THROWS(slv.checkEntailed(d_solver->mkTrue()), CVC4ApiException&);
-}
-
-void SolverBlack::testCheckEntailed2()
-{
-  d_solver->setOption("incremental", "true");
-
-  Sort uSort = d_solver->mkUninterpretedSort("u");
-  Sort intSort = d_solver->getIntegerSort();
-  Sort boolSort = d_solver->getBooleanSort();
-  Sort uToIntSort = d_solver->mkFunctionSort(uSort, intSort);
-  Sort intPredSort = d_solver->mkFunctionSort(intSort, boolSort);
-
-  Term n = Term();
-  // Constants
-  Term x = d_solver->mkConst(uSort, "x");
-  Term y = d_solver->mkConst(uSort, "y");
-  // Functions
-  Term f = d_solver->mkConst(uToIntSort, "f");
-  Term p = d_solver->mkConst(intPredSort, "p");
-  // Values
-  Term zero = d_solver->mkInteger(0);
-  Term one = d_solver->mkInteger(1);
-  // Terms
-  Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
-  Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
-  Term sum = d_solver->mkTerm(PLUS, f_x, f_y);
-  Term p_0 = d_solver->mkTerm(APPLY_UF, p, zero);
-  Term p_f_y = d_solver->mkTerm(APPLY_UF, p, f_y);
-  // Assertions
-  Term assertions =
-      d_solver->mkTerm(AND,
-                       std::vector<Term>{
-                           d_solver->mkTerm(LEQ, zero, f_x),  // 0 <= f(x)
-                           d_solver->mkTerm(LEQ, zero, f_y),  // 0 <= f(y)
-                           d_solver->mkTerm(LEQ, sum, one),  // f(x) + f(y) <= 1
-                           p_0.notTerm(),                    // not p(0)
-                           p_f_y                             // p(f(y))
-                       });
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
-  d_solver->assertFormula(assertions);
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->checkEntailed(d_solver->mkTerm(DISTINCT, x, y)));
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(
-      {d_solver->mkFalse(), d_solver->mkTerm(DISTINCT, x, y)}));
-  TS_ASSERT_THROWS(d_solver->checkEntailed(n), CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->checkEntailed({n, d_solver->mkTerm(DISTINCT, x, y)}),
-      CVC4ApiException&);
-  Solver slv;
-  TS_ASSERT_THROWS(slv.checkEntailed(d_solver->mkTrue()), CVC4ApiException&);
-}
-
-void SolverBlack::testCheckSat()
-{
-  d_solver->setOption("incremental", "false");
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkSat());
-  TS_ASSERT_THROWS(d_solver->checkSat(), CVC4ApiException&);
-}
-
-void SolverBlack::testCheckSatAssuming()
-{
-  d_solver->setOption("incremental", "false");
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue()));
-  TS_ASSERT_THROWS(d_solver->checkSatAssuming(d_solver->mkTrue()),
-                   CVC4ApiException&);
-  Solver slv;
-  TS_ASSERT_THROWS(slv.checkSatAssuming(d_solver->mkTrue()), CVC4ApiException&);
-}
-
-void SolverBlack::testCheckSatAssuming1()
-{
-  Sort boolSort = d_solver->getBooleanSort();
-  Term x = d_solver->mkConst(boolSort, "x");
-  Term y = d_solver->mkConst(boolSort, "y");
-  Term z = d_solver->mkTerm(AND, x, y);
-  d_solver->setOption("incremental", "true");
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue()));
-  TS_ASSERT_THROWS(d_solver->checkSatAssuming(Term()), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue()));
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(z));
-  Solver slv;
-  TS_ASSERT_THROWS(slv.checkSatAssuming(d_solver->mkTrue()), CVC4ApiException&);
-}
-
-void SolverBlack::testCheckSatAssuming2()
-{
-  d_solver->setOption("incremental", "true");
-
-  Sort uSort = d_solver->mkUninterpretedSort("u");
-  Sort intSort = d_solver->getIntegerSort();
-  Sort boolSort = d_solver->getBooleanSort();
-  Sort uToIntSort = d_solver->mkFunctionSort(uSort, intSort);
-  Sort intPredSort = d_solver->mkFunctionSort(intSort, boolSort);
-
-  Term n = Term();
-  // Constants
-  Term x = d_solver->mkConst(uSort, "x");
-  Term y = d_solver->mkConst(uSort, "y");
-  // Functions
-  Term f = d_solver->mkConst(uToIntSort, "f");
-  Term p = d_solver->mkConst(intPredSort, "p");
-  // Values
-  Term zero = d_solver->mkInteger(0);
-  Term one = d_solver->mkInteger(1);
-  // Terms
-  Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
-  Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
-  Term sum = d_solver->mkTerm(PLUS, f_x, f_y);
-  Term p_0 = d_solver->mkTerm(APPLY_UF, p, zero);
-  Term p_f_y = d_solver->mkTerm(APPLY_UF, p, f_y);
-  // Assertions
-  Term assertions =
-      d_solver->mkTerm(AND,
-                       std::vector<Term>{
-                           d_solver->mkTerm(LEQ, zero, f_x),  // 0 <= f(x)
-                           d_solver->mkTerm(LEQ, zero, f_y),  // 0 <= f(y)
-                           d_solver->mkTerm(LEQ, sum, one),  // f(x) + f(y) <= 1
-                           p_0.notTerm(),                    // not p(0)
-                           p_f_y                             // p(f(y))
-                       });
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue()));
-  d_solver->assertFormula(assertions);
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->checkSatAssuming(d_solver->mkTerm(DISTINCT, x, y)));
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(
-      {d_solver->mkFalse(), d_solver->mkTerm(DISTINCT, x, y)}));
-  TS_ASSERT_THROWS(d_solver->checkSatAssuming(n), CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->checkSatAssuming({n, d_solver->mkTerm(DISTINCT, x, y)}),
-      CVC4ApiException&);
-  Solver slv;
-  TS_ASSERT_THROWS(slv.checkSatAssuming(d_solver->mkTrue()), CVC4ApiException&);
-}
-
-void SolverBlack::testSetLogic()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->setLogic("AUFLIRA"));
-  TS_ASSERT_THROWS(d_solver->setLogic("AF_BV"), CVC4ApiException&);
-  d_solver->assertFormula(d_solver->mkTrue());
-  TS_ASSERT_THROWS(d_solver->setLogic("AUFLIRA"), CVC4ApiException&);
-}
-
-void SolverBlack::testSetOption()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver->setOption("bv-sat-solver", "minisat"));
-  TS_ASSERT_THROWS(d_solver->setOption("bv-sat-solver", "1"),
-                   CVC4ApiException&);
-  d_solver->assertFormula(d_solver->mkTrue());
-  TS_ASSERT_THROWS(d_solver->setOption("bv-sat-solver", "minisat"),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testResetAssertions()
-{
-  d_solver->setOption("incremental", "true");
-
-  Sort bvSort = d_solver->mkBitVectorSort(4);
-  Term one = d_solver->mkBitVector(4, 1);
-  Term x = d_solver->mkConst(bvSort, "x");
-  Term ule = d_solver->mkTerm(BITVECTOR_ULE, x, one);
-  Term srem = d_solver->mkTerm(BITVECTOR_SREM, one, x);
-  d_solver->push(4);
-  Term slt = d_solver->mkTerm(BITVECTOR_SLT, srem, one);
-  d_solver->resetAssertions();
-  d_solver->checkSatAssuming({slt, ule});
-}
-
-void SolverBlack::testMkSygusVar()
-{
-  Sort boolSort = d_solver->getBooleanSort();
-  Sort intSort = d_solver->getIntegerSort();
-  Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusVar(boolSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusVar(funSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusVar(boolSort, std::string("b")));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusVar(funSort, ""));
-  TS_ASSERT_THROWS(d_solver->mkSygusVar(Sort()), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkSygusVar(d_solver->getNullSort(), "a"),
-                   CVC4ApiException&);
-  Solver slv;
-  TS_ASSERT_THROWS(slv.mkSygusVar(boolSort), CVC4ApiException&);
-}
-
-void SolverBlack::testMkSygusGrammar()
-{
-  Term nullTerm;
-  Term boolTerm = d_solver->mkBoolean(true);
-  Term boolVar = d_solver->mkVar(d_solver->getBooleanSort());
-  Term intVar = d_solver->mkVar(d_solver->getIntegerSort());
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusGrammar({}, {intVar}));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusGrammar({boolVar}, {intVar}));
-  TS_ASSERT_THROWS(d_solver->mkSygusGrammar({}, {}), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkSygusGrammar({}, {nullTerm}), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkSygusGrammar({}, {boolTerm}), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkSygusGrammar({boolTerm}, {intVar}),
-                   CVC4ApiException&);
-  Solver slv;
-  Term boolVar2 = slv.mkVar(slv.getBooleanSort());
-  Term intVar2 = slv.mkVar(slv.getIntegerSort());
-  TS_ASSERT_THROWS_NOTHING(slv.mkSygusGrammar({boolVar2}, {intVar2}));
-  TS_ASSERT_THROWS(slv.mkSygusGrammar({boolVar}, {intVar2}), CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.mkSygusGrammar({boolVar2}, {intVar}), CVC4ApiException&);
-}
-
-void SolverBlack::testSynthFun()
-{
-  Sort null = d_solver->getNullSort();
-  Sort boolean = d_solver->getBooleanSort();
-  Sort integer = d_solver->getIntegerSort();
-
-  Term nullTerm;
-  Term x = d_solver->mkVar(boolean);
-
-  Term start1 = d_solver->mkVar(boolean);
-  Term start2 = d_solver->mkVar(integer);
-
-  Grammar g1 = d_solver->mkSygusGrammar({x}, {start1});
-  g1.addRule(start1, d_solver->mkBoolean(false));
-
-  Grammar g2 = d_solver->mkSygusGrammar({x}, {start2});
-  g2.addRule(start2, d_solver->mkInteger(0));
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->synthFun("", {}, boolean));
-  TS_ASSERT_THROWS_NOTHING(d_solver->synthFun("f1", {x}, boolean));
-  TS_ASSERT_THROWS_NOTHING(d_solver->synthFun("f2", {x}, boolean, g1));
-
-  TS_ASSERT_THROWS(d_solver->synthFun("f3", {nullTerm}, boolean),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->synthFun("f4", {}, null), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->synthFun("f6", {x}, boolean, g2),
-                   CVC4ApiException&);
-  Solver slv;
-  Term x2 = slv.mkVar(slv.getBooleanSort());
-  TS_ASSERT_THROWS_NOTHING(slv.synthFun("f1", {x2}, slv.getBooleanSort()));
-  TS_ASSERT_THROWS(slv.synthFun("", {}, d_solver->getBooleanSort()),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.synthFun("f1", {x}, d_solver->getBooleanSort()),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testSynthInv()
-{
-  Sort boolean = d_solver->getBooleanSort();
-  Sort integer = d_solver->getIntegerSort();
-
-  Term nullTerm;
-  Term x = d_solver->mkVar(boolean);
-
-  Term start1 = d_solver->mkVar(boolean);
-  Term start2 = d_solver->mkVar(integer);
-
-  Grammar g1 = d_solver->mkSygusGrammar({x}, {start1});
-  g1.addRule(start1, d_solver->mkBoolean(false));
-
-  Grammar g2 = d_solver->mkSygusGrammar({x}, {start2});
-  g2.addRule(start2, d_solver->mkInteger(0));
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->synthInv("", {}));
-  TS_ASSERT_THROWS_NOTHING(d_solver->synthInv("i1", {x}));
-  TS_ASSERT_THROWS_NOTHING(d_solver->synthInv("i2", {x}, g1));
-
-  TS_ASSERT_THROWS(d_solver->synthInv("i3", {nullTerm}), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->synthInv("i4", {x}, g2), CVC4ApiException&);
-}
-
-void SolverBlack::testAddSygusConstraint()
-{
-  Term nullTerm;
-  Term boolTerm = d_solver->mkBoolean(true);
-  Term intTerm = d_solver->mkInteger(1);
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->addSygusConstraint(boolTerm));
-  TS_ASSERT_THROWS(d_solver->addSygusConstraint(nullTerm), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->addSygusConstraint(intTerm), CVC4ApiException&);
-
-  Solver slv;
-  TS_ASSERT_THROWS(slv.addSygusConstraint(boolTerm), CVC4ApiException&);
-}
-
-void SolverBlack::testAddSygusInvConstraint()
-{
-  Sort boolean = d_solver->getBooleanSort();
-  Sort real = d_solver->getRealSort();
-
-  Term nullTerm;
-  Term intTerm = d_solver->mkInteger(1);
-
-  Term inv = d_solver->declareFun("inv", {real}, boolean);
-  Term pre = d_solver->declareFun("pre", {real}, boolean);
-  Term trans = d_solver->declareFun("trans", {real, real}, boolean);
-  Term post = d_solver->declareFun("post", {real}, boolean);
-
-  Term inv1 = d_solver->declareFun("inv1", {real}, real);
-
-  Term trans1 = d_solver->declareFun("trans1", {boolean, real}, boolean);
-  Term trans2 = d_solver->declareFun("trans2", {real, boolean}, boolean);
-  Term trans3 = d_solver->declareFun("trans3", {real, real}, real);
-
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->addSygusInvConstraint(inv, pre, trans, post));
-
-  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(nullTerm, pre, trans, post),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, nullTerm, trans, post),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, nullTerm, post),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, trans, nullTerm),
-                   CVC4ApiException&);
-
-  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(intTerm, pre, trans, post),
-                   CVC4ApiException&);
-
-  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv1, pre, trans, post),
-                   CVC4ApiException&);
-
-  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, trans, trans, post),
-                   CVC4ApiException&);
-
-  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, intTerm, post),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, pre, post),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, trans1, post),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, trans2, post),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, trans3, post),
-                   CVC4ApiException&);
-
-  TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, trans, trans),
-                   CVC4ApiException&);
-  Solver slv;
-  Sort boolean2 = slv.getBooleanSort();
-  Sort real2 = slv.getRealSort();
-  Term inv22 = slv.declareFun("inv", {real2}, boolean2);
-  Term pre22 = slv.declareFun("pre", {real2}, boolean2);
-  Term trans22 = slv.declareFun("trans", {real2, real2}, boolean2);
-  Term post22 = slv.declareFun("post", {real2}, boolean2);
-  TS_ASSERT_THROWS_NOTHING(
-      slv.addSygusInvConstraint(inv22, pre22, trans22, post22));
-  TS_ASSERT_THROWS(slv.addSygusInvConstraint(inv, pre22, trans22, post22),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.addSygusInvConstraint(inv22, pre, trans22, post22),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.addSygusInvConstraint(inv22, pre22, trans, post22),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(slv.addSygusInvConstraint(inv22, pre22, trans22, post),
-                   CVC4ApiException&);
-}
-
-void SolverBlack::testGetSynthSolution()
-{
-  d_solver->setOption("lang", "sygus2");
-  d_solver->setOption("incremental", "false");
-
-  Term nullTerm;
-  Term x = d_solver->mkBoolean(false);
-  Term f = d_solver->synthFun("f", {}, d_solver->getBooleanSort());
-
-  TS_ASSERT_THROWS(d_solver->getSynthSolution(f), CVC4ApiException&);
-
-  d_solver->checkSynth();
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->getSynthSolution(f));
-  TS_ASSERT_THROWS_NOTHING(d_solver->getSynthSolution(f));
-
-  TS_ASSERT_THROWS(d_solver->getSynthSolution(nullTerm), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->getSynthSolution(x), CVC4ApiException&);
-
-  Solver slv;
-  TS_ASSERT_THROWS(slv.getSynthSolution(f), CVC4ApiException&);
-}
-
-void SolverBlack::testGetSynthSolutions()
-{
-  d_solver->setOption("lang", "sygus2");
-  d_solver->setOption("incremental", "false");
-
-  Term nullTerm;
-  Term x = d_solver->mkBoolean(false);
-  Term f = d_solver->synthFun("f", {}, d_solver->getBooleanSort());
-
-  TS_ASSERT_THROWS(d_solver->getSynthSolutions({}), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->getSynthSolutions({f}), CVC4ApiException&);
-
-  d_solver->checkSynth();
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->getSynthSolutions({f}));
-  TS_ASSERT_THROWS_NOTHING(d_solver->getSynthSolutions({f, f}));
-
-  TS_ASSERT_THROWS(d_solver->getSynthSolutions({}), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->getSynthSolutions({nullTerm}), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->getSynthSolutions({x}), CVC4ApiException&);
-
-  Solver slv;
-  TS_ASSERT_THROWS(slv.getSynthSolutions({x}), CVC4ApiException&);
-}