From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 11 Jan 2019 20:06:03 +0000 (-0800)
Subject: New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)
X-Git-Tag: cvc5-1.0.0~4293
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=87f38648fe82b69b527a387bec9836455290cdba;p=cvc5.git

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

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 5321a90ec..123613797 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -29,6 +29,7 @@
 #include "options/options.h"
 #include "smt/model.h"
 #include "smt/smt_engine.h"
+#include "theory/logic_info.h"
 #include "util/random.h"
 #include "util/result.h"
 #include "util/utility.h"
@@ -3374,26 +3375,70 @@ void Solver::reset(void) const { d_smtEngine->reset(); }
  */
 void Solver::resetAssertions(void) const { d_smtEngine->resetAssertions(); }
 
+// TODO: issue #2781
+void Solver::setLogicHelper(const std::string& logic) const
+{
+  CVC4_API_CHECK(!d_smtEngine->isFullyInited())
+      << "Invalid call to 'setLogic', solver is already fully initialized";
+  try
+  {
+    CVC4::LogicInfo logic_info(logic);
+    d_smtEngine->setLogic(logic_info);
+  }
+  catch (CVC4::IllegalArgumentException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
+}
+
 /**
  *  ( set-info <attribute> )
  */
 void Solver::setInfo(const std::string& keyword, const std::string& value) const
 {
-  // CHECK:
-  // if keyword == "cvc4-logic": value must be string
-  // if keyword == "status": must be sat, unsat or unknown
-  // if keyword == "smt-lib-version": supported?
+  bool is_cvc4_keyword = false;
+
+  /* Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_") */
+  if (keyword.length() > 5)
+  {
+    std::string prefix = keyword.substr(0, 5);
+    if (prefix == "cvc4-" || prefix == "cvc4_")
+    {
+      is_cvc4_keyword = true;
+      std::string cvc4key = keyword.substr(5);
+      CVC4_API_ARG_CHECK_EXPECTED(cvc4key == "logic", keyword)
+          << "keyword 'cvc4-logic'";
+      setLogicHelper(value);
+    }
+  }
+  if (!is_cvc4_keyword)
+  {
+    CVC4_API_ARG_CHECK_EXPECTED(
+        keyword == "source" || keyword == "category" || keyword == "difficulty"
+            || keyword == "filename" || keyword == "license"
+            || keyword == "name" || keyword == "notes"
+            || keyword == "smt-lib-version" || keyword == "status",
+        keyword)
+        << "'source', 'category', 'difficulty', 'filename', 'license', 'name', "
+           "'notes', 'smt-lib-version' or 'status'";
+    CVC4_API_ARG_CHECK_EXPECTED(keyword != "smt-lib-version" || value == "2"
+                                    || value == "2.0" || value == "2.5"
+                                    || value == "2.6" || value == "2.6.1",
+                                value)
+        << "'2.0', '2.5', '2.6' or '2.6.1'";
+    CVC4_API_ARG_CHECK_EXPECTED(keyword != "status" || value == "sat"
+                                    || value == "unsat" || value == "unknown",
+                                value)
+        << "'sat', 'unsat' or 'unknown'";
+  }
+
   d_smtEngine->setInfo(keyword, value);
 }
 
 /**
  *  ( set-logic <symbol> )
  */
-void Solver::setLogic(const std::string& logic) const
-{
-  // CHECK: !d_smtEngine->d_fullyInited
-  d_smtEngine->setLogic(logic);
-}
+void Solver::setLogic(const std::string& logic) const { setLogicHelper(logic); }
 
 /**
  *  ( set-option <option> )
@@ -3401,9 +3446,16 @@ void Solver::setLogic(const std::string& logic) const
 void Solver::setOption(const std::string& option,
                        const std::string& value) const
 {
-  // CHECK: option exists?
-  // CHECK: !d_smtEngine->d_fullInited, else option can't be set
-  d_smtEngine->setOption(option, value);
+  CVC4_API_CHECK(!d_smtEngine->isFullyInited())
+      << "Invalid call to 'setOption', solver is already fully initialized";
+  try
+  {
+    d_smtEngine->setOption(option, value);
+  }
+  catch (CVC4::OptionException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 Term Solver::ensureTermSort(const Term& t, const Sort& s) const
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 1d98f127d..a06f2e415 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -24,8 +24,8 @@
 #include <map>
 #include <memory>
 #include <set>
-#include <string>
 #include <sstream>
+#include <string>
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>
@@ -53,9 +53,10 @@ class CVC4_PUBLIC CVC4ApiException : public std::exception
 {
  public:
   CVC4ApiException(const std::string& str) : d_msg(str) {}
-  CVC4ApiException(const std::stringstream& stream) :d_msg(stream.str()) {}
+  CVC4ApiException(const std::stringstream& stream) : d_msg(stream.str()) {}
   std::string getMessage() const { return d_msg; }
   const char* what() const noexcept override { return d_msg.c_str(); }
+
  private:
   std::string d_msg;
 };
@@ -2237,9 +2238,8 @@ class CVC4_PUBLIC Solver
    * @param ctors the constructor declarations of the datatype sort
    * @return the datatype sort
    */
-  Sort declareDatatype(
-      const std::string& symbol,
-      const std::vector<DatatypeConstructorDecl>& ctors) const;
+  Sort declareDatatype(const std::string& symbol,
+                       const std::vector<DatatypeConstructorDecl>& ctors) const;
 
   /**
    * Declare 0-arity function symbol.
@@ -2489,7 +2489,8 @@ class CVC4_PUBLIC Solver
   /* Helper to check for API misuse in mkOpTerm functions. */
   void checkMkTerm(Kind kind, uint32_t nchildren) const;
   /* Helper for mk-functions that call d_exprMgr->mkConst(). */
-  template <typename T> Term mkConstHelper(T t) const;
+  template <typename T>
+  Term mkConstHelper(T t) const;
   /* Helper for mkReal functions that take a string as argument. */
   Term mkRealFromStrHelper(std::string s) const;
   /* Helper for mkBitVector functions that take a string as argument. */
@@ -2499,6 +2500,8 @@ class CVC4_PUBLIC Solver
   Term mkBVFromStrHelper(uint32_t size, std::string s, uint32_t base) const;
   /* Helper for mkBitVector functions that take an integer as argument. */
   Term mkBVFromIntHelper(uint32_t size, uint64_t val) const;
+  /* Helper for setLogic. */
+  void setLogicHelper(const std::string& logic) const;
 
   /**
    * Helper function that ensures that a given term is of sort real (as opposed
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 5aa59fad7..e53d1eb55 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -217,8 +217,8 @@ class CVC4_PUBLIC SmtEngine {
   /**
    * Whether or not this SmtEngine is fully initialized (post-construction).
    * This post-construction initialization is automatically triggered by the
-   * use of the SmtEngine; e.g. when setLogic() is called, or the first
-   * assertion is made, etc.
+   * use of the SmtEngine; e.g. when the first formula is asserted, a call
+   * to simplify() is issued, a scope is pushed, etc.
    */
   bool d_fullyInited;
 
@@ -456,6 +456,14 @@ class CVC4_PUBLIC SmtEngine {
    */
   ~SmtEngine();
 
+  /**
+   * Return true if this SmtEngine is fully initialized (post-construction).
+   * This post-construction initialization is automatically triggered by the
+   * use of the SmtEngine; e.g. when the first formula is asserted, a call
+   * to simplify() is issued, a scope is pushed, etc.
+   */
+  bool isFullyInited() { return d_fullyInited; }
+
   /**
    * Set the logic of the script.
    */
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&);
 }