New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)

1 files changed, 407 insertions, 340 deletions

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 3bfb51200..d2226f278 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -80,173 +80,181 @@ class SolverBlack : public CxxTest::TestSuite
   void testDefineFunRec();
   void testDefineFunsRec();
 
+  void testSetInfo();
+  void testSetLogic();
+  void testSetOption();
+
  private:
-  Solver d_solver;
+  std::unique_ptr<Solver> d_solver;
 };
 
-void SolverBlack::setUp() {}
+void SolverBlack::setUp() { d_solver.reset(new Solver()); }
 
 void SolverBlack::tearDown() {}
 
 void SolverBlack::testGetBooleanSort()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver.getBooleanSort());
+  TS_ASSERT_THROWS_NOTHING(d_solver->getBooleanSort());
 }
 
 void SolverBlack::testGetIntegerSort()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver.getIntegerSort());
+  TS_ASSERT_THROWS_NOTHING(d_solver->getIntegerSort());
 }
 
 void SolverBlack::testGetNullSort()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver.getNullSort());
+  TS_ASSERT_THROWS_NOTHING(d_solver->getNullSort());
 }
 
 void SolverBlack::testGetRealSort()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver.getRealSort());
+  TS_ASSERT_THROWS_NOTHING(d_solver->getRealSort());
 }
 
 void SolverBlack::testGetRegExpSort()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver.getRegExpSort());
+  TS_ASSERT_THROWS_NOTHING(d_solver->getRegExpSort());
 }
 
 void SolverBlack::testGetStringSort()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver.getStringSort());
+  TS_ASSERT_THROWS_NOTHING(d_solver->getStringSort());
 }
 
 void SolverBlack::testGetRoundingmodeSort()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver.getRoundingmodeSort());
+  TS_ASSERT_THROWS_NOTHING(d_solver->getRoundingmodeSort());
 }
 
 void SolverBlack::testMkArraySort()
 {
-  Sort boolSort = d_solver.getBooleanSort();
-  Sort intSort = d_solver.getIntegerSort();
-  Sort realSort = d_solver.getRealSort();
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  Sort fpSort = d_solver.mkFloatingPointSort(3, 5);
-  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(fpSort, fpSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(boolSort, intSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(realSort, bvSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(bvSort, fpSort));
+  Sort boolSort = d_solver->getBooleanSort();
+  Sort intSort = d_solver->getIntegerSort();
+  Sort realSort = d_solver->getRealSort();
+  Sort bvSort = d_solver->mkBitVectorSort(32);
+  Sort fpSort = d_solver->mkFloatingPointSort(3, 5);
+  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(fpSort, fpSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(boolSort, intSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(realSort, bvSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, fpSort));
 }
 
 void SolverBlack::testMkBitVectorSort()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVectorSort(32));
-  TS_ASSERT_THROWS(d_solver.mkBitVectorSort(0), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBitVectorSort(32));
+  TS_ASSERT_THROWS(d_solver->mkBitVectorSort(0), CVC4ApiException&);
 }
 
 void SolverBlack::testMkFloatingPointSort()
 {
-  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&);
+  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&);
 }
 
 void SolverBlack::testMkDatatypeSort()
 {
   DatatypeDecl dtypeSpec("list");
   DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
+  DatatypeSelectorDecl head("head", d_solver->getIntegerSort());
   cons.addSelector(head);
   dtypeSpec.addConstructor(cons);
   DatatypeConstructorDecl nil("nil");
   dtypeSpec.addConstructor(nil);
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkDatatypeSort(dtypeSpec));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSort(dtypeSpec));
   DatatypeDecl throwsDtypeSpec("list");
-  TS_ASSERT_THROWS(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkDatatypeSort(throwsDtypeSpec),
+                   CVC4ApiException&);
 }
 
 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_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({funSort2, d_solver.mkUninterpretedSort("u")},
-                              d_solver.getIntegerSort()),
+      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&);
-  TS_ASSERT_THROWS(d_solver.mkFunctionSort({d_solver.getIntegerSort(),
-                                            d_solver.mkUninterpretedSort("u")},
-                                           funSort2),
-                   CVC4ApiException&);
 }
 
 void SolverBlack::testMkParamSort()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkParamSort("T"));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkParamSort(""));
+  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());
+      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}),
+      d_solver->mkPredicateSort({d_solver->getIntegerSort(), funSort}),
       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::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));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkRecordSort(fields));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkRecordSort(empty));
 }
 
 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)));
+  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)));
 }
 
 void SolverBlack::testMkUninterpretedSort()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkUninterpretedSort("u"));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkUninterpretedSort(""));
+  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&);
+  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}),
+  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&);
 }
 
@@ -254,116 +262,118 @@ void SolverBlack::testMkBitVector()
 {
   uint32_t size0 = 0, size1 = 8, size2 = 32, val1 = 2;
   uint64_t val2 = 2;
-  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_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", 16));
-  TS_ASSERT_THROWS(d_solver.mkBitVector(8, "101010101", 2), CVC4ApiException&);
-  TS_ASSERT_EQUALS(d_solver.mkBitVector(8, "01010101", 2).toString(),
+  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_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", 16));
+  TS_ASSERT_THROWS(d_solver->mkBitVector(8, "101010101", 2), CVC4ApiException&);
+  TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "01010101", 2).toString(),
                    "0bin01010101");
-  TS_ASSERT_EQUALS(d_solver.mkBitVector(8, "F", 16).toString(), "0bin00001111");
+  TS_ASSERT_EQUALS(d_solver->mkBitVector(8, "F", 16).toString(),
+                   "0bin00001111");
 }
 
 void SolverBlack::testMkBoundVar()
 {
-  Sort boolSort = d_solver.getBooleanSort();
-  Sort intSort = d_solver.getIntegerSort();
-  Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
-  TS_ASSERT_THROWS(d_solver.mkBoundVar(Sort()), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkBoundVar(boolSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkBoundVar(funSort));
-  TS_ASSERT_THROWS(d_solver.mkBoundVar("a", Sort()), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkBoundVar(std::string("b"), boolSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkBoundVar("", funSort));
+  Sort boolSort = d_solver->getBooleanSort();
+  Sort intSort = d_solver->getIntegerSort();
+  Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
+  TS_ASSERT_THROWS(d_solver->mkBoundVar(Sort()), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(boolSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(funSort));
+  TS_ASSERT_THROWS(d_solver->mkBoundVar("a", Sort()), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(std::string("b"), boolSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar("", funSort));
 }
 
 void SolverBlack::testMkBoolean()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkBoolean(true));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkBoolean(false));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoolean(true));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoolean(false));
 }
 
 void SolverBlack::testMkRoundingMode()
 {
   TS_ASSERT_THROWS_NOTHING(
-      d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
+      d_solver->mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
 }
 
 void SolverBlack::testMkUninterpretedConst()
 {
   TS_ASSERT_THROWS_NOTHING(
-      d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
-  TS_ASSERT_THROWS(d_solver.mkUninterpretedConst(Sort(), 1), CVC4ApiException&);
+      d_solver->mkUninterpretedConst(d_solver->getBooleanSort(), 1));
+  TS_ASSERT_THROWS(d_solver->mkUninterpretedConst(Sort(), 1),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testMkAbstractValue()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue(std::string("1")));
-  TS_ASSERT_THROWS(d_solver.mkAbstractValue(std::string("0")),
+  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")),
+  TS_ASSERT_THROWS(d_solver->mkAbstractValue(std::string("-1")),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkAbstractValue(std::string("1.2")),
+  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(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&);
+  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.mkReal(2);
+  Term t1 = d_solver->mkBitVector(8);
+  Term t2 = d_solver->mkBitVector(4);
+  Term t3 = d_solver->mkReal(2);
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
-    TS_ASSERT_THROWS_NOTHING(d_solver.mkFloatingPoint(3, 5, t1));
+    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(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&);
+  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&);
 }
 
 void SolverBlack::testMkEmptySet()
 {
-  TS_ASSERT_THROWS(d_solver.mkEmptySet(d_solver.getBooleanSort()),
+  TS_ASSERT_THROWS(d_solver->mkEmptySet(d_solver->getBooleanSort()),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkEmptySet(Sort()));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySet(Sort()));
 }
 
 void SolverBlack::testMkFalse()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkFalse());
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkFalse());
+  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));
+    TS_ASSERT_THROWS_NOTHING(d_solver->mkNaN(3, 5));
   }
   else
   {
-    TS_ASSERT_THROWS(d_solver.mkNaN(3, 5), CVC4ApiException&);
+    TS_ASSERT_THROWS(d_solver->mkNaN(3, 5), CVC4ApiException&);
   }
 }
 
@@ -371,11 +381,11 @@ void SolverBlack::testMkNegZero()
 {
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
-    TS_ASSERT_THROWS_NOTHING(d_solver.mkNegZero(3, 5));
+    TS_ASSERT_THROWS_NOTHING(d_solver->mkNegZero(3, 5));
   }
   else
   {
-    TS_ASSERT_THROWS(d_solver.mkNegZero(3, 5), CVC4ApiException&);
+    TS_ASSERT_THROWS(d_solver->mkNegZero(3, 5), CVC4ApiException&);
   }
 }
 
@@ -383,11 +393,11 @@ void SolverBlack::testMkNegInf()
 {
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
-    TS_ASSERT_THROWS_NOTHING(d_solver.mkNegInf(3, 5));
+    TS_ASSERT_THROWS_NOTHING(d_solver->mkNegInf(3, 5));
   }
   else
   {
-    TS_ASSERT_THROWS(d_solver.mkNegInf(3, 5), CVC4ApiException&);
+    TS_ASSERT_THROWS(d_solver->mkNegInf(3, 5), CVC4ApiException&);
   }
 }
 
@@ -395,11 +405,11 @@ void SolverBlack::testMkPosInf()
 {
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
-    TS_ASSERT_THROWS_NOTHING(d_solver.mkPosInf(3, 5));
+    TS_ASSERT_THROWS_NOTHING(d_solver->mkPosInf(3, 5));
   }
   else
   {
-    TS_ASSERT_THROWS(d_solver.mkPosInf(3, 5), CVC4ApiException&);
+    TS_ASSERT_THROWS(d_solver->mkPosInf(3, 5), CVC4ApiException&);
   }
 }
 
@@ -407,349 +417,406 @@ void SolverBlack::testMkPosZero()
 {
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
-    TS_ASSERT_THROWS_NOTHING(d_solver.mkPosZero(3, 5));
+    TS_ASSERT_THROWS_NOTHING(d_solver->mkPosZero(3, 5));
   }
   else
   {
-    TS_ASSERT_THROWS(d_solver.mkPosZero(3, 5), CVC4ApiException&);
+    TS_ASSERT_THROWS(d_solver->mkPosZero(3, 5), CVC4ApiException&);
   }
 }
 
 void SolverBlack::testMkOpTerm()
 {
   // mkOpTerm(Kind kind, Kind k)
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkOpTerm(CHAIN_OP, EQUAL));
-  TS_ASSERT_THROWS(d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, EQUAL),
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(CHAIN_OP, EQUAL));
+  TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, EQUAL),
                    CVC4ApiException&);
 
   // mkOpTerm(Kind kind, const std::string& arg)
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkOpTerm(RECORD_UPDATE_OP, "asdf"));
-  TS_ASSERT_THROWS(d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, "asdf"),
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(RECORD_UPDATE_OP, "asdf"));
+  TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, "asdf"),
                    CVC4ApiException&);
 
   // mkOpTerm(Kind kind, uint32_t arg)
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkOpTerm(DIVISIBLE_OP, 1));
-  TS_ASSERT_THROWS(d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 1),
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(DIVISIBLE_OP, 1));
+  TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 1),
                    CVC4ApiException&);
 
   // mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2)
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 1, 1));
-  TS_ASSERT_THROWS(d_solver.mkOpTerm(DIVISIBLE_OP, 1, 2), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 1, 1));
+  TS_ASSERT_THROWS(d_solver->mkOpTerm(DIVISIBLE_OP, 1, 2), CVC4ApiException&);
 }
 
-void SolverBlack::testMkPi() { TS_ASSERT_THROWS_NOTHING(d_solver.mkPi()); }
+void SolverBlack::testMkPi() { TS_ASSERT_THROWS_NOTHING(d_solver->mkPi()); }
 
 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(nullptr), CVC4ApiException&);
-  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&);
+  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(nullptr), CVC4ApiException&);
+  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));
+  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.mkVar("s", strSort);
+  Sort strSort = d_solver->getStringSort();
+  Term s = d_solver->mkVar("s", strSort);
   TS_ASSERT_THROWS_NOTHING(
-      d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty()));
+      d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpEmpty()));
 }
 
 void SolverBlack::testMkRegexpSigma()
 {
-  Sort strSort = d_solver.getStringSort();
-  Term s = d_solver.mkVar("s", strSort);
+  Sort strSort = d_solver->getStringSort();
+  Term s = d_solver->mkVar("s", strSort);
   TS_ASSERT_THROWS_NOTHING(
-      d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
+      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&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkSepNil(d_solver->getBooleanSort()));
+  TS_ASSERT_THROWS(d_solver->mkSepNil(Sort()), 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(),
+  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\\\\nasdf\"");
-  TS_ASSERT_EQUALS(d_solver.mkString("asdf\\nasdf", true).toString(),
+  TS_ASSERT_EQUALS(d_solver->mkString("asdf\\nasdf", true).toString(),
                    "\"asdf\\nasdf\"");
 }
 
 void SolverBlack::testMkTerm()
 {
-  Sort bv32 = d_solver.mkBitVectorSort(32);
-  Term a = d_solver.mkVar("a", bv32);
-  Term b = d_solver.mkVar("b", bv32);
+  Sort bv32 = d_solver->mkBitVectorSort(32);
+  Term a = d_solver->mkVar("a", bv32);
+  Term b = d_solver->mkVar("b", bv32);
   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.mkReal(1), d_solver.mkReal(2)};
-  std::vector<Term> v5 = {d_solver.mkReal(1), Term()};
-  OpTerm opterm1 = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 2, 1);
-  OpTerm opterm2 = d_solver.mkOpTerm(DIVISIBLE_OP, 1);
-  OpTerm opterm3 = d_solver.mkOpTerm(CHAIN_OP, EQUAL);
+  std::vector<Term> v3 = {a, d_solver->mkTrue()};
+  std::vector<Term> v4 = {d_solver->mkReal(1), d_solver->mkReal(2)};
+  std::vector<Term> v5 = {d_solver->mkReal(1), Term()};
+  OpTerm opterm1 = d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 2, 1);
+  OpTerm opterm2 = d_solver->mkOpTerm(DIVISIBLE_OP, 1);
+  OpTerm opterm3 = d_solver->mkOpTerm(CHAIN_OP, EQUAL);
 
   // 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&);
+  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, Sort sort) const
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(SEP_NIL, d_solver.getBooleanSort()));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(SEP_NIL, Sort()));
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver->mkTerm(SEP_NIL, d_solver->getBooleanSort()));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(SEP_NIL, Sort()));
 
   // 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_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&);
 
   // 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()),
+  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&);
 
   // 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_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()),
+      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()),
+      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()),
+      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),
+      d_solver->mkTerm(ITE, d_solver->mkTrue(), d_solver->mkTrue(), b),
       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_NOTHING(d_solver->mkTerm(EQUAL, v1));
+  TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, v2), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, v3), CVC4ApiException&);
 
   // mkTerm(OpTerm opTerm, Term child) const
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(opterm1, a));
-  TS_ASSERT_THROWS(d_solver.mkTerm(opterm2, a), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkTerm(opterm1, Term()), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a));
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, a), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&);
 
   // mkTerm(OpTerm opTerm, Term child1, Term child2) const
   TS_ASSERT_THROWS_NOTHING(
-      d_solver.mkTerm(opterm3, d_solver.mkReal(1), d_solver.mkReal(2)));
-  TS_ASSERT_THROWS(d_solver.mkTerm(opterm1, a, b), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkTerm(opterm3, d_solver.mkReal(1), Term()),
+      d_solver->mkTerm(opterm3, d_solver->mkReal(1), d_solver->mkReal(2)));
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, d_solver->mkReal(1), Term()),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkTerm(opterm3, Term(), d_solver.mkReal(1)),
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, Term(), d_solver->mkReal(1)),
                    CVC4ApiException&);
 
   // mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(
-      opterm3, d_solver.mkReal(1), d_solver.mkReal(1), d_solver.mkReal(2)));
-  TS_ASSERT_THROWS(d_solver.mkTerm(opterm1, a, b, a), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(
+      opterm3, d_solver->mkReal(1), d_solver->mkReal(1), d_solver->mkReal(2)));
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&);
   TS_ASSERT_THROWS(
-      d_solver.mkTerm(opterm3, d_solver.mkReal(1), d_solver.mkReal(1), Term()),
+      d_solver->mkTerm(
+          opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()),
       CVC4ApiException&);
 
   // mkTerm(OpTerm opTerm, const std::vector<Term>& children) const
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkTerm(opterm3, v4));
-  TS_ASSERT_THROWS(d_solver.mkTerm(opterm3, v5), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm3, v4));
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, v5), CVC4ApiException&);
 }
 
 void SolverBlack::testMkTrue()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkTrue());
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkTrue());
+  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->mkBitVectorSort(3)}, {d_solver->mkBitVector("101", 2)}));
   TS_ASSERT_THROWS_NOTHING(
-      d_solver.mkTuple({d_solver.getRealSort()}, {d_solver.mkReal("5")}));
+      d_solver->mkTuple({d_solver->getRealSort()}, {d_solver->mkReal("5")}));
 
-  TS_ASSERT_THROWS(d_solver.mkTuple({}, {d_solver.mkBitVector("101", 2)}),
+  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)}),
+  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&);
-  TS_ASSERT_THROWS(
-      d_solver.mkTuple({d_solver.getIntegerSort()}, {d_solver.mkReal("5.3")}),
-      CVC4ApiException&);
 }
 
 void SolverBlack::testMkUniverseSet()
 {
-  TS_ASSERT_THROWS(d_solver.mkUniverseSet(Sort()), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkUniverseSet(d_solver.getBooleanSort()));
+  TS_ASSERT_THROWS(d_solver->mkUniverseSet(Sort()), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkUniverseSet(d_solver->getBooleanSort()));
 }
 
 void SolverBlack::testMkVar()
 {
-  Sort boolSort = d_solver.getBooleanSort();
-  Sort intSort = d_solver.getIntegerSort();
-  Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
-  TS_ASSERT_THROWS(d_solver.mkVar(Sort()), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkVar(boolSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkVar(funSort));
-  TS_ASSERT_THROWS(d_solver.mkVar("a", Sort()), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkVar(std::string("b"), boolSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkVar("", funSort));
+  Sort boolSort = d_solver->getBooleanSort();
+  Sort intSort = d_solver->getIntegerSort();
+  Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
+  TS_ASSERT_THROWS(d_solver->mkVar(Sort()), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort));
+  TS_ASSERT_THROWS(d_solver->mkVar("a", Sort()), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(std::string("b"), boolSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar("", funSort));
 }
 
 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("f2", funSort));
+  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("f2", funSort));
   TS_ASSERT_THROWS_NOTHING(
-      d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort));
-  TS_ASSERT_THROWS(d_solver.declareFun("f4", {bvSort, funSort}, bvSort),
+      d_solver->declareFun("f3", {bvSort, d_solver->getIntegerSort()}, bvSort));
+  TS_ASSERT_THROWS(d_solver->declareFun("f4", {bvSort, funSort}, bvSort),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.declareFun("f5", {bvSort, bvSort}, funSort),
+  TS_ASSERT_THROWS(d_solver->declareFun("f5", {bvSort, bvSort}, funSort),
                    CVC4ApiException&);
 }
 
 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.mkBoundVar("b1", bvSort);
-  Term b11 = d_solver.mkBoundVar("b1", bvSort);
-  Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort());
-  Term b3 = d_solver.mkBoundVar("b3", funSort2);
-  Term v1 = d_solver.mkBoundVar("v1", bvSort);
-  Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort());
-  Term v3 = d_solver.mkVar("v3", funSort2);
-  Term f1 = d_solver.declareFun("f1", funSort1);
-  Term f2 = d_solver.declareFun("f2", funSort2);
-  Term f3 = d_solver.declareFun("f3", bvSort);
-  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("fff", {b1}, bvSort, v3),
+  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->mkBoundVar("b1", bvSort);
+  Term b11 = d_solver->mkBoundVar("b1", bvSort);
+  Term b2 = d_solver->mkBoundVar("b2", d_solver->getIntegerSort());
+  Term b3 = d_solver->mkBoundVar("b3", funSort2);
+  Term v1 = d_solver->mkBoundVar("v1", bvSort);
+  Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort());
+  Term v3 = d_solver->mkVar("v3", funSort2);
+  Term f1 = d_solver->declareFun("f1", funSort1);
+  Term f2 = d_solver->declareFun("f2", funSort2);
+  Term f3 = d_solver->declareFun("f3", bvSort);
+  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("fff", {b1}, bvSort, v3),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFun("ffff", {b1}, funSort2, v3),
+  TS_ASSERT_THROWS(d_solver->defineFun("ffff", {b1}, funSort2, v3),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1),
+  TS_ASSERT_THROWS(d_solver->defineFun("fffff", {b1, b3}, bvSort, 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&);
+  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&);
 }
 
 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.mkBoundVar("b1", bvSort);
-  Term b11 = d_solver.mkBoundVar("b1", bvSort);
-  Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort());
-  Term b3 = d_solver.mkBoundVar("b3", funSort2);
-  Term v1 = d_solver.mkBoundVar("v1", bvSort);
-  Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort());
-  Term v3 = d_solver.mkVar("v3", funSort2);
-  Term f1 = d_solver.declareFun("f1", funSort1);
-  Term f2 = d_solver.declareFun("f2", funSort2);
-  Term f3 = d_solver.declareFun("f3", bvSort);
-  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),
+  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->mkBoundVar("b1", bvSort);
+  Term b11 = d_solver->mkBoundVar("b1", bvSort);
+  Term b2 = d_solver->mkBoundVar("b2", d_solver->getIntegerSort());
+  Term b3 = d_solver->mkBoundVar("b3", funSort2);
+  Term v1 = d_solver->mkBoundVar("v1", bvSort);
+  Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort());
+  Term v3 = d_solver->mkVar("v3", funSort2);
+  Term f1 = d_solver->declareFun("f1", funSort1);
+  Term f2 = d_solver->declareFun("f2", funSort2);
+  Term f3 = d_solver->declareFun("f3", bvSort);
+  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("ffff", {b1}, funSort2, v3),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunRec("ffff", {b1}, funSort2, v3),
+  TS_ASSERT_THROWS(d_solver->defineFunRec("fffff", {b1, b3}, bvSort, v1),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1),
+  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}, 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&);
+  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&);
 }
 
 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.mkBoundVar("b1", bvSort);
-  Term b11 = d_solver.mkBoundVar("b1", bvSort);
-  Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort());
-  Term b3 = d_solver.mkBoundVar("b3", funSort2);
-  Term b4 = d_solver.mkBoundVar("b4", uSort);
-  Term v1 = d_solver.mkBoundVar("v1", bvSort);
-  Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort());
-  Term v3 = d_solver.mkVar("v3", funSort2);
-  Term v4 = d_solver.mkVar("v4", uSort);
-  Term f1 = d_solver.declareFun("f1", funSort1);
-  Term f2 = d_solver.declareFun("f2", funSort2);
-  Term f3 = d_solver.declareFun("f3", bvSort);
+  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->mkBoundVar("b1", bvSort);
+  Term b11 = d_solver->mkBoundVar("b1", bvSort);
+  Term b2 = d_solver->mkBoundVar("b2", d_solver->getIntegerSort());
+  Term b3 = d_solver->mkBoundVar("b3", funSort2);
+  Term b4 = d_solver->mkBoundVar("b4", uSort);
+  Term v1 = d_solver->mkBoundVar("v1", bvSort);
+  Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort());
+  Term v3 = d_solver->mkVar("v3", funSort2);
+  Term v4 = d_solver->mkVar("v4", uSort);
+  Term f1 = d_solver->declareFun("f1", funSort1);
+  Term f2 = d_solver->declareFun("f2", funSort2);
+  Term f3 = d_solver->declareFun("f3", bvSort);
   TS_ASSERT_THROWS_NOTHING(
-      d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2}));
+      d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2}));
   TS_ASSERT_THROWS(
-      d_solver.defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}),
+      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}),
+  TS_ASSERT_THROWS(d_solver->defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}),
                    CVC4ApiException&);
   TS_ASSERT_THROWS(
-      d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}),
+      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&);
+}
+
+void SolverBlack::testSetInfo()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("cvc4-logic", "QF_BV"));
+  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("cvc4_logic", "QF_BV"));
+  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_NOTHING(d_solver->setInfo("smt-lib-version", "2.6.1"));
+  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&);
+
+  d_solver->assertFormula(d_solver->mkTrue());
+  TS_ASSERT_THROWS(d_solver->setInfo("cvc4-logic", "QF_BV"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->setInfo("cvc4_logic", "QF_BV"), 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&);
 }