New C++ Api: First batch of API guards. (#4557)

This is the first batch of API guards, mainly extending existing guards
in the Solver object with checks that Ops, Terms, Sorts, and datatype objects
are associated to this solver object.

This further changes how DatatypeConstructorDecl objects are created. Previously,
they were not created via the Solver object (while DatatypeDecl was). Now, they are
created via Solver::mkDatatypeConstructorDecl, consistent with how DatatypeDecl
objects are created.

13 files changed, 559 insertions, 144 deletions

diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index 9cfc7992c..500cb0710 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -91,8 +91,8 @@ void test(Solver& slv, Sort& consListSort)
   DatatypeDecl paramConsListSpec =
       slv.mkDatatypeDecl("paramlist",
                          sort);  // give the datatype a name
-  DatatypeConstructorDecl paramCons("cons");
-  DatatypeConstructorDecl paramNil("nil");
+  DatatypeConstructorDecl paramCons = slv.mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl paramNil = slv.mkDatatypeConstructorDecl("nil");
   paramCons.addSelector("head", sort);
   paramCons.addSelectorSelf("tail");
   paramConsListSpec.addConstructor(paramCons);
@@ -144,11 +144,11 @@ int main()
 
   DatatypeDecl consListSpec =
       slv.mkDatatypeDecl("list");  // give the datatype a name
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = slv.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", slv.getIntegerSort());
   cons.addSelectorSelf("tail");
   consListSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = slv.mkDatatypeConstructorDecl("nil");
   consListSpec.addConstructor(nil);
 
   std::cout << "spec is:" << std::endl << consListSpec << std::endl;
@@ -167,10 +167,10 @@ int main()
             << ">>> Alternatively, use declareDatatype" << std::endl;
   std::cout << std::endl;
 
-  DatatypeConstructorDecl cons2("cons");
+  DatatypeConstructorDecl cons2 = slv.mkDatatypeConstructorDecl("cons");
   cons2.addSelector("head", slv.getIntegerSort());
   cons2.addSelectorSelf("tail");
-  DatatypeConstructorDecl nil2("nil");
+  DatatypeConstructorDecl nil2 = slv.mkDatatypeConstructorDecl("nil");
   std::vector<DatatypeConstructorDecl> ctors = {cons2, nil2};
   Sort consListSort2 = slv.declareDatatype("list2", ctors);
   test(slv, consListSort2);
diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py
index ded268d69..1a67f5661 100755
--- a/examples/api/python/datatypes.py
+++ b/examples/api/python/datatypes.py
@@ -65,8 +65,8 @@ def test(slv, consListSort):
     # constructor "cons".
     sort = slv.mkParamSort("T")
     paramConsListSpec = slv.mkDatatypeDecl("paramlist", sort)
-    paramCons = pycvc4.DatatypeConstructorDecl("cons")
-    paramNil = pycvc4.DatatypeConstructorDecl("nil")
+    paramCons = slv.mkDatatypeConstructorDecl("cons")
+    paramNil = slv.mkDatatypeConstructorDecl("nil")
     paramCons.addSelector("head", sort)
     paramCons.addSelectorSelf("tail")
     paramConsListSpec.addConstructor(paramCons)
@@ -102,11 +102,11 @@ if __name__ == "__main__":
     # symbols are assigned to its constructors, selectors, and testers.
 
     consListSpec = slv.mkDatatypeDecl("list") # give the datatype a name
-    cons = pycvc4.DatatypeConstructorDecl("cons")
+    cons = slv.mkDatatypeConstructorDecl("cons")
     cons.addSelector("head", slv.getIntegerSort())
     cons.addSelectorSelf("tail")
     consListSpec.addConstructor(cons)
-    nil = pycvc4.DatatypeConstructorDecl("nil")
+    nil = slv.mkDatatypeConstructorDecl("nil")
     consListSpec.addConstructor(nil)
 
     print("spec is {}".format(consListSpec))
@@ -122,10 +122,10 @@ if __name__ == "__main__":
 
     print("### Alternatively, use declareDatatype")
 
-    cons2 = pycvc4.DatatypeConstructorDecl("cons")
+    cons2 = slv.mkDatatypeConstructorDecl("cons")
     cons2.addSelector("head", slv.getIntegerSort())
     cons2.addSelectorSelf("tail")
-    nil2 = pycvc4.DatatypeConstructorDecl("nil")
+    nil2 = slv.mkDatatypeConstructorDecl("nil")
     ctors = [cons2, nil2]
     consListSort2 = slv.declareDatatype("list2", ctors)
     test(slv, consListSort2)
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 0bfb9a325..f225da333 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -702,8 +702,6 @@ class CVC4ApiExceptionStream
   CVC4_API_CHECK(isDefinedKind(kind)) \
       << "Invalid kind '" << kindToString(kind) << "'";
 
-#define CVC4_API_SORT_CHECK_SOLVER(sort)
-
 #define CVC4_API_KIND_CHECK_EXPECTED(cond, kind) \
   CVC4_PREDICT_TRUE(cond)                        \
   ? (void)0                                      \
@@ -726,12 +724,12 @@ class CVC4ApiExceptionStream
           & CVC4ApiExceptionStream().ostream()      \
                 << "Invalid size of argument '" << #arg << "', expected "
 
-#define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, arg, idx)          \
-  CVC4_PREDICT_TRUE(cond)                                                   \
-  ? (void)0                                                                 \
-  : OstreamVoider()                                                         \
-          & CVC4ApiExceptionStream().ostream()                              \
-                << "Invalid " << what << " '" << arg << "' at index" << idx \
+#define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, arg, idx)           \
+  CVC4_PREDICT_TRUE(cond)                                                    \
+  ? (void)0                                                                  \
+  : OstreamVoider()                                                          \
+          & CVC4ApiExceptionStream().ostream()                               \
+                << "Invalid " << what << " '" << arg << "' at index " << idx \
                 << ", expected "
 
 #define CVC4_API_SOLVER_TRY_CATCH_BEGIN \
@@ -741,6 +739,19 @@ class CVC4ApiExceptionStream
   }                                                                            \
   catch (const CVC4::Exception& e) { throw CVC4ApiException(e.getMessage()); } \
   catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); }
+
+#define CVC4_API_SOLVER_CHECK_SORT(sort) \
+  CVC4_API_CHECK(this == sort.d_solver)  \
+      << "Given sort is not associated with this solver";
+
+#define CVC4_API_SOLVER_CHECK_TERM(term) \
+  CVC4_API_CHECK(this == term.d_solver)  \
+      << "Given term is not associated with this solver";
+
+#define CVC4_API_SOLVER_CHECK_OP(op)  \
+  CVC4_API_CHECK(this == op.d_solver) \
+      << "Given operator is not associated with this solver";
+
 }  // namespace
 
 /* -------------------------------------------------------------------------- */
@@ -1612,6 +1623,7 @@ Term::const_iterator::const_iterator(const const_iterator& it)
 {
   if (it.d_orig_expr != nullptr)
   {
+    d_solver = it.d_solver;
     d_orig_expr = it.d_orig_expr;
     d_pos = it.d_pos;
   }
@@ -1619,6 +1631,7 @@ Term::const_iterator::const_iterator(const const_iterator& it)
 
 Term::const_iterator& Term::const_iterator::operator=(const const_iterator& it)
 {
+  d_solver = it.d_solver;
   d_orig_expr = it.d_orig_expr;
   d_pos = it.d_pos;
   return *this;
@@ -1630,7 +1643,8 @@ bool Term::const_iterator::operator==(const const_iterator& it) const
   {
     return false;
   }
-  return (*d_orig_expr == *it.d_orig_expr) && (d_pos == it.d_pos);
+  return (d_solver == it.d_solver && *d_orig_expr == *it.d_orig_expr)
+         && (d_pos == it.d_pos);
 }
 
 bool Term::const_iterator::operator!=(const const_iterator& it) const
@@ -1756,8 +1770,14 @@ size_t TermHashFunction::operator()(const Term& t) const
 
 /* DatatypeConstructorDecl -------------------------------------------------- */
 
-DatatypeConstructorDecl::DatatypeConstructorDecl(const std::string& name)
-    : d_ctor(new CVC4::DatatypeConstructor(name))
+DatatypeConstructorDecl::DatatypeConstructorDecl()
+    : d_solver(nullptr), d_ctor(nullptr)
+{
+}
+
+DatatypeConstructorDecl::DatatypeConstructorDecl(const Solver* slv,
+                                                 const std::string& name)
+    : d_solver(slv), d_ctor(new CVC4::DatatypeConstructor(name))
 {
 }
 
@@ -1804,10 +1824,13 @@ std::ostream& operator<<(std::ostream& out,
 
 /* DatatypeDecl ------------------------------------------------------------- */
 
+DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {}
+
 DatatypeDecl::DatatypeDecl(const Solver* slv,
                            const std::string& name,
                            bool isCoDatatype)
-    : d_dtype(new CVC4::Datatype(slv->getExprManager(), name, isCoDatatype))
+    : d_solver(slv),
+      d_dtype(new CVC4::Datatype(slv->getExprManager(), name, isCoDatatype))
 {
 }
 
@@ -1815,7 +1838,8 @@ DatatypeDecl::DatatypeDecl(const Solver* slv,
                            const std::string& name,
                            Sort param,
                            bool isCoDatatype)
-    : d_dtype(new CVC4::Datatype(slv->getExprManager(),
+    : d_solver(slv),
+      d_dtype(new CVC4::Datatype(slv->getExprManager(),
                                  name,
                                  std::vector<Type>{*param.d_type},
                                  isCoDatatype))
@@ -1826,6 +1850,7 @@ DatatypeDecl::DatatypeDecl(const Solver* slv,
                            const std::string& name,
                            const std::vector<Sort>& params,
                            bool isCoDatatype)
+    : d_solver(slv)
 {
   std::vector<Type> tparams;
   for (const Sort& p : params)
@@ -1838,8 +1863,6 @@ DatatypeDecl::DatatypeDecl(const Solver* slv,
 
 bool DatatypeDecl::isNullHelper() const { return !d_dtype; }
 
-DatatypeDecl::DatatypeDecl() {}
-
 DatatypeDecl::~DatatypeDecl() {}
 
 void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor)
@@ -2683,8 +2706,11 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
   for (size_t i = 0, size = children.size(); i < size; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !children[i].isNull(), "parameter term", children[i], i)
+        !children[i].isNull(), "child term", children[i], i)
         << "non-null term";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == children[i].d_solver, "child term", children[i], i)
+        << "a child term associated to this solver object";
   }
 
   std::vector<Expr> echildren = termVectorToExprs(children);
@@ -2749,13 +2775,24 @@ std::vector<Sort> Solver::mkDatatypeSortsInternal(
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
 
   std::vector<CVC4::Datatype> datatypes;
-  for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; i++)
-  {
-    CVC4_API_ARG_CHECK_EXPECTED(dtypedecls[i].getNumConstructors() > 0,
-                                dtypedecls[i])
+  for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i)
+  {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == dtypedecls[i].d_solver,
+                                         "datatype declaration",
+                                         dtypedecls[i],
+                                         i)
+        << "a datatype declaration associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(dtypedecls[i].getNumConstructors() > 0,
+                                         "datatype declaration",
+                                         dtypedecls[i],
+                                         i)
         << "a datatype declaration with at least one constructor";
     datatypes.push_back(dtypedecls[i].getDatatype());
   }
+  for (auto& sort : unresolvedSorts)
+  {
+    CVC4_API_SOLVER_CHECK_SORT(sort);
+  }
   std::set<Type> utypes = sortSetToTypes(unresolvedSorts);
   std::vector<CVC4::DatatypeType> dtypes =
       d_exprMgr->mkMutualDatatypeTypes(datatypes, utypes);
@@ -2778,6 +2815,7 @@ std::vector<Type> Solver::sortVectorToTypes(
   std::vector<Type> res;
   for (const Sort& s : sorts)
   {
+    CVC4_API_SOLVER_CHECK_SORT(s);
     res.push_back(*s.d_type);
   }
   return res;
@@ -2789,6 +2827,7 @@ std::vector<Expr> Solver::termVectorToExprs(
   std::vector<Expr> res;
   for (const Term& t : terms)
   {
+    CVC4_API_SOLVER_CHECK_TERM(t);
     res.push_back(*t.d_expr);
   }
   return res;
@@ -2877,6 +2916,8 @@ Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const
       << "non-null index sort";
   CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
       << "non-null element sort";
+  CVC4_API_SOLVER_CHECK_SORT(indexSort);
+  CVC4_API_SOLVER_CHECK_SORT(elemSort);
 
   return Sort(this,
               d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type));
@@ -2908,6 +2949,8 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
 Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK(this == dtypedecl.d_solver)
+      << "Given datatype declaration is not associated with this solver";
   CVC4_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl)
       << "a datatype declaration with at least one constructor";
 
@@ -2934,6 +2977,8 @@ Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain)
       << "non-null codomain sort";
+  CVC4_API_SOLVER_CHECK_SORT(domain);
+  CVC4_API_SOLVER_CHECK_SORT(codomain);
   CVC4_API_ARG_CHECK_EXPECTED(domain.isFirstClass(), domain)
       << "first-class sort as domain sort for function sort";
   CVC4_API_ARG_CHECK_EXPECTED(codomain.isFirstClass(), codomain)
@@ -2957,11 +3002,15 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const
         !sorts[i].isNull(), "parameter sort", sorts[i], i)
         << "non-null sort";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == sorts[i].d_solver, "parameter sort", sorts[i], i)
+        << "sort associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
         << "first-class sort as parameter sort for function sort";
   }
   CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain)
       << "non-null codomain sort";
+  CVC4_API_SOLVER_CHECK_SORT(codomain);
   CVC4_API_ARG_CHECK_EXPECTED(codomain.isFirstClass(), codomain)
       << "first-class sort as codomain sort for function sort";
   Assert(!codomain.isFunction()); /* A function sort is not first-class. */
@@ -2991,6 +3040,9 @@ Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const
         !sorts[i].isNull(), "parameter sort", sorts[i], i)
         << "non-null sort";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == sorts[i].d_solver, "parameter sort", sorts[i], i)
+        << "sort associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
         << "first-class sort as parameter sort for predicate sort";
   }
@@ -3012,6 +3064,9 @@ Sort Solver::mkRecordSort(
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         !p.second.isNull(), "parameter sort", p.second, i)
         << "non-null sort";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == p.second.d_solver, "parameter sort", p.second, i)
+        << "sort associated to this solver object";
     i += 1;
     f.emplace_back(p.first, *p.second.d_type);
   }
@@ -3026,6 +3081,7 @@ Sort Solver::mkSetSort(Sort elemSort) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
       << "non-null element sort";
+  CVC4_API_SOLVER_CHECK_SORT(elemSort);
 
   return Sort(this, d_exprMgr->mkSetType(*elemSort.d_type));
 
@@ -3059,6 +3115,9 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
         !sorts[i].isNull(), "parameter sort", sorts[i], i)
         << "non-null sort";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == sorts[i].d_solver, "parameter sort", sorts[i], i)
+        << "sort associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         !sorts[i].isFunctionLike(), "parameter sort", sorts[i], i)
         << "non-function-like sort as parameter sort for tuple sort";
   }
@@ -3207,6 +3266,8 @@ Term Solver::mkEmptySet(Sort s) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isSet(), s)
       << "null sort or set sort";
+  CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || this == s.d_solver, s)
+      << "set sort associated to this solver object";
 
   return mkValHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type));
 
@@ -3217,6 +3278,7 @@ Term Solver::mkSepNil(Sort sort) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+  CVC4_API_SOLVER_CHECK_SORT(sort);
 
   Expr res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL);
   (void)res.getType(true); /* kick off type checking */
@@ -3272,6 +3334,7 @@ Term Solver::mkUniverseSet(Sort sort) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+  CVC4_API_SOLVER_CHECK_SORT(sort);
 
   Expr res =
       d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET);
@@ -3324,7 +3387,10 @@ Term Solver::mkBitVector(uint32_t size, std::string& s, uint32_t base) const
 Term Solver::mkConstArray(Sort sort, Term val) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_ARG_CHECK_NOT_NULL(sort);
   CVC4_API_ARG_CHECK_NOT_NULL(val);
+  CVC4_API_SOLVER_CHECK_SORT(sort);
+  CVC4_API_SOLVER_CHECK_TERM(val);
   CVC4_API_CHECK(sort.isArray()) << "Not an array sort.";
   CVC4_API_CHECK(sort.getArrayElementSort().isComparableTo(val.getSort()))
       << "Value does not match element sort.";
@@ -3405,6 +3471,7 @@ Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+  CVC4_API_SOLVER_CHECK_SORT(sort);
 
   return mkValHelper<CVC4::UninterpretedConstant>(
       CVC4::UninterpretedConstant(*sort.d_type, index));
@@ -3448,6 +3515,7 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
   CVC4_API_ARG_CHECK_EXPECTED(bw == val.getSort().getBVSize(), val)
       << "a bit-vector constant with bit-width '" << bw << "'";
   CVC4_API_ARG_CHECK_EXPECTED(!val.isNull(), val) << "non-null term";
+  CVC4_API_SOLVER_CHECK_TERM(val);
   CVC4_API_ARG_CHECK_EXPECTED(
       val.getSort().isBitVector() && val.d_expr->isConst(), val)
       << "bit-vector constant";
@@ -3465,6 +3533,7 @@ Term Solver::mkConst(Sort sort, const std::string& symbol) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+  CVC4_API_SOLVER_CHECK_SORT(sort);
 
   Expr res = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type)
                             : d_exprMgr->mkVar(symbol, *sort.d_type);
@@ -3481,6 +3550,7 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+  CVC4_API_SOLVER_CHECK_SORT(sort);
 
   Expr res = symbol.empty() ? d_exprMgr->mkBoundVar(*sort.d_type)
                             : d_exprMgr->mkBoundVar(symbol, *sort.d_type);
@@ -3490,6 +3560,15 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+/* Create datatype constructor declarations                                   */
+/* -------------------------------------------------------------------------- */
+
+DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl(
+    const std::string& name)
+{
+  return DatatypeConstructorDecl(this, name);
+}
+
 /* Create datatype declarations                                               */
 /* -------------------------------------------------------------------------- */
 
@@ -3526,6 +3605,7 @@ Term Solver::mkTerm(Kind kind, Term child) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
+  CVC4_API_SOLVER_CHECK_TERM(child);
   checkMkTerm(kind, 1);
 
   Expr res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr);
@@ -3540,6 +3620,8 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
   CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
+  CVC4_API_SOLVER_CHECK_TERM(child1);
+  CVC4_API_SOLVER_CHECK_TERM(child2);
   checkMkTerm(kind, 2);
 
   Expr res =
@@ -3564,6 +3646,7 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
 Term Solver::mkTerm(Op op) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_SOLVER_CHECK_OP(op);
 
   Term res;
   if (op.isIndexedHelper())
@@ -3585,7 +3668,9 @@ Term Solver::mkTerm(Op op) const
 Term Solver::mkTerm(Op op, Term child) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_SOLVER_CHECK_OP(op);
   CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
+  CVC4_API_SOLVER_CHECK_TERM(child);
 
   const CVC4::Kind int_kind = extToIntKind(op.d_kind);
   Expr res;
@@ -3607,8 +3692,11 @@ Term Solver::mkTerm(Op op, Term child) const
 Term Solver::mkTerm(Op op, Term child1, Term child2) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_SOLVER_CHECK_OP(op);
   CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
   CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
+  CVC4_API_SOLVER_CHECK_TERM(child1);
+  CVC4_API_SOLVER_CHECK_TERM(child2);
 
   const CVC4::Kind int_kind = extToIntKind(op.d_kind);
   Expr res;
@@ -3630,9 +3718,13 @@ Term Solver::mkTerm(Op op, Term child1, Term child2) const
 Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_SOLVER_CHECK_OP(op);
   CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
   CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
   CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term";
+  CVC4_API_SOLVER_CHECK_TERM(child1);
+  CVC4_API_SOLVER_CHECK_TERM(child2);
+  CVC4_API_SOLVER_CHECK_TERM(child3);
 
   const CVC4::Kind int_kind = extToIntKind(op.d_kind);
   Expr res;
@@ -3656,11 +3748,15 @@ Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
 Term Solver::mkTerm(Op op, const std::vector<Term>& children) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_SOLVER_CHECK_OP(op);
   for (size_t i = 0, size = children.size(); i < size; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !children[i].isNull(), "parameter term", children[i], i)
+        !children[i].isNull(), "child term", children[i], i)
         << "non-null term";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == children[i].d_solver, "child term", children[i], i)
+        << "child term associated to this solver object";
   }
 
   const CVC4::Kind int_kind = extToIntKind(op.d_kind);
@@ -3690,6 +3786,12 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts,
   std::vector<CVC4::Expr> args;
   for (size_t i = 0, size = sorts.size(); i < size; i++)
   {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == terms[i].d_solver, "child term", terms[i], i)
+        << "child term associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == sorts[i].d_solver, "child sort", sorts[i], i)
+        << "child sort associated to this solver object";
     args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_expr);
   }
 
@@ -3913,12 +4015,13 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const
 /* Non-SMT-LIB commands                                                       */
 /* -------------------------------------------------------------------------- */
 
-Term Solver::simplify(const Term& t)
+Term Solver::simplify(const Term& term)
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_ARG_CHECK_NOT_NULL(t);
+  CVC4_API_ARG_CHECK_NOT_NULL(term);
+  CVC4_API_SOLVER_CHECK_TERM(term);
 
-  return Term(this, d_smtEngine->simplify(*t.d_expr));
+  return Term(this, d_smtEngine->simplify(*term.d_expr));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3932,6 +4035,7 @@ Result Solver::checkEntailed(Term term) const
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   CVC4_API_ARG_CHECK_NOT_NULL(term);
+  CVC4_API_SOLVER_CHECK_TERM(term);
 
   CVC4::Result r = d_smtEngine->checkEntailed(*term.d_expr);
   return Result(r);
@@ -3949,6 +4053,7 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const
          "(try --incremental)";
   for (const Term& term : terms)
   {
+    CVC4_API_SOLVER_CHECK_TERM(term);
     CVC4_API_ARG_CHECK_NOT_NULL(term);
   }
 
@@ -3967,10 +4072,11 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const
  */
 void Solver::assertFormula(Term term) const
 {
-  // CHECK:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(expr.getExprManager())
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_SOLVER_CHECK_TERM(term);
+  CVC4_API_ARG_CHECK_NOT_NULL(term);
   d_smtEngine->assertFormula(*term.d_expr);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -3978,10 +4084,15 @@ void Solver::assertFormula(Term term) const
  */
 Result Solver::checkSat(void) const
 {
-  // CHECK:
-  // if d_queryMade -> incremental enabled
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(!d_smtEngine->isQueryMade()
+                 || CVC4::options::incrementalSolving())
+      << "Cannot make multiple queries unless incremental solving is enabled "
+         "(try --incremental)";
   CVC4::Result r = d_smtEngine->checkSat();
   return Result(r);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -3989,10 +4100,16 @@ Result Solver::checkSat(void) const
  */
 Result Solver::checkSatAssuming(Term assumption) const
 {
-  // CHECK:
-  // if assumptions.size() > 0:  incremental enabled?
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(!d_smtEngine->isQueryMade()
+                 || CVC4::options::incrementalSolving())
+      << "Cannot make multiple queries unless incremental solving is enabled "
+         "(try --incremental)";
+  CVC4_API_SOLVER_CHECK_TERM(assumption);
   CVC4::Result r = d_smtEngine->checkSat(*assumption.d_expr);
   return Result(r);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4000,11 +4117,21 @@ Result Solver::checkSatAssuming(Term assumption) const
  */
 Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
 {
-  // CHECK:
-  // if assumptions.size() > 0:  incremental enabled?
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0
+                 || CVC4::options::incrementalSolving())
+      << "Cannot make multiple queries unless incremental solving is enabled "
+         "(try --incremental)";
+  for (const Term& term : assumptions)
+  {
+    CVC4_API_SOLVER_CHECK_TERM(term);
+    CVC4_API_ARG_CHECK_NOT_NULL(term);
+  }
   std::vector<Expr> eassumptions = termVectorToExprs(assumptions);
   CVC4::Result r = d_smtEngine->checkSat(eassumptions);
   return Result(r);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4014,14 +4141,21 @@ Sort Solver::declareDatatype(
     const std::string& symbol,
     const std::vector<DatatypeConstructorDecl>& ctors) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(ctors.size() > 0, ctors)
       << "a datatype declaration with at least one constructor";
   DatatypeDecl dtdecl(this, symbol);
-  for (const DatatypeConstructorDecl& ctor : ctors)
+  for (size_t i = 0, size = ctors.size(); i < size; i++)
   {
-    dtdecl.addConstructor(ctor);
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == ctors[i].d_solver,
+                                         "datatype constructor declaration",
+                                         ctors[i],
+                                         i)
+        << "datatype constructor declaration associated to this solver object";
+    dtdecl.addConstructor(ctors[i]);
   }
   return Sort(this, d_exprMgr->mkDatatypeType(*dtdecl.d_dtype));
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4031,14 +4165,19 @@ Term Solver::declareFun(const std::string& symbol,
                         const std::vector<Sort>& sorts,
                         Sort sort) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   for (size_t i = 0, size = sorts.size(); i < size; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == sorts[i].d_solver, "parameter sort", sorts[i], i)
+        << "parameter sort associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
         << "first-class sort as parameter sort for function sort";
   }
   CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
       << "first-class sort as function codomain sort";
+  CVC4_API_SOLVER_CHECK_SORT(sort);
   Assert(!sort.isFunction()); /* A function sort is not first-class. */
   Type type = *sort.d_type;
   if (!sorts.empty())
@@ -4047,6 +4186,7 @@ Term Solver::declareFun(const std::string& symbol,
     type = d_exprMgr->mkFunctionType(types, type);
   }
   return Term(this, d_exprMgr->mkVar(symbol, type));
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 87be7b74c..855ba4400 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -1167,14 +1167,13 @@ class DatatypeIterator;
 class CVC4_PUBLIC DatatypeConstructorDecl
 {
   friend class DatatypeDecl;
+  friend class Solver;
 
  public:
   /**
-   * Constructor.
-   * @param name the name of the datatype constructor
-   * @return the DatatypeConstructorDecl
+   * Nullary constructor for Cython.
    */
-  DatatypeConstructorDecl(const std::string& name);
+  DatatypeConstructorDecl();
 
   /**
    * Add datatype selector declaration.
@@ -1199,6 +1198,19 @@ class CVC4_PUBLIC DatatypeConstructorDecl
 
  private:
   /**
+   * Constructor.
+   * @param slv the associated solver object
+   * @param name the name of the datatype constructor
+   * @return the DatatypeConstructorDecl
+   */
+  DatatypeConstructorDecl(const Solver* slv, const std::string& name);
+
+  /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
+  /**
    * The internal (intermediate) datatype constructor wrapped by this
    * datatype constructor declaration.
    * This is a shared_ptr rather than a unique_ptr since
@@ -1219,7 +1231,7 @@ class CVC4_PUBLIC DatatypeDecl
 
  public:
   /**
-   * Nullary constructor for Cython
+   * Nullary constructor for Cython.
    */
   DatatypeDecl();
 
@@ -1240,6 +1252,9 @@ class CVC4_PUBLIC DatatypeDecl
   /** Is this Datatype declaration parametric? */
   bool isParametric() const;
 
+  /**
+   * @return true if this DatatypeDecl is a null object
+   */
   bool isNull() const;
 
   /**
@@ -1257,7 +1272,7 @@ class CVC4_PUBLIC DatatypeDecl
  private:
   /**
    * Constructor.
-   * @param slv the solver that created this datatype declaration
+   * @param slv the associated solver object
    * @param name the name of the datatype
    * @param isCoDatatype true if a codatatype is to be constructed
    * @return the DatatypeDecl
@@ -1269,7 +1284,7 @@ class CVC4_PUBLIC DatatypeDecl
   /**
    * Constructor for parameterized datatype declaration.
    * Create sorts parameter with Solver::mkParamSort().
-   * @param slv the solver that created this datatype declaration
+   * @param slv the associated solver object
    * @param name the name of the datatype
    * @param param the sort parameter
    * @param isCoDatatype true if a codatatype is to be constructed
@@ -1282,7 +1297,7 @@ class CVC4_PUBLIC DatatypeDecl
   /**
    * Constructor for parameterized datatype declaration.
    * Create sorts parameter with Solver::mkParamSort().
-   * @param slv the solver that created this datatype declaration
+   * @param slv the associated solver object
    * @param name the name of the datatype
    * @param params a list of sort parameters
    * @param isCoDatatype true if a codatatype is to be constructed
@@ -1292,9 +1307,17 @@ class CVC4_PUBLIC DatatypeDecl
                const std::vector<Sort>& params,
                bool isCoDatatype = false);
 
-  // helper for isNull() to avoid calling API functions from other API functions
+  /**
+   * Helper for isNull checks. This prevents calling an API function with
+   * CVC4_API_CHECK_NOT_NULL
+   */
   bool isNullHelper() const;
 
+  /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
   /* The internal (intermediate) datatype wrapped by this datatype
    * declaration
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -2680,6 +2703,12 @@ class CVC4_PUBLIC Solver
   Term mkVar(Sort sort, const std::string& symbol = std::string()) const;
 
   /* .................................................................... */
+  /* Create datatype constructor declarations                             */
+  /* .................................................................... */
+
+  DatatypeConstructorDecl mkDatatypeConstructorDecl(const std::string& name);
+
+  /* .................................................................... */
   /* Create datatype declarations                                         */
   /* .................................................................... */
 
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 1c7071958..2ca4b3645 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -54,7 +54,6 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
 
 
     cdef cppclass DatatypeConstructorDecl:
-        DatatypeConstructorDecl(const string& name) except +
         void addSelector(const string& name, Sort sort) except +
         void addSelectorSelf(const string& name) except +
         string toString() except +
@@ -160,6 +159,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         # default value for symbol defined in cvc4cpp.h
         Term mkConst(Sort sort) except +
         Term mkVar(Sort sort, const string& symbol) except +
+        DatatypeConstructorDecl mkDatatypeConstructorDecl(const string& name) except +
         DatatypeDecl mkDatatypeDecl(const string& name) except +
         DatatypeDecl mkDatatypeDecl(const string& name, bint isCoDatatype) except +
         DatatypeDecl mkDatatypeDecl(const string& name, Sort param) except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index fa5313f0e..e742e0061 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -134,12 +134,14 @@ cdef class DatatypeConstructor:
 
 
 cdef class DatatypeConstructorDecl:
-    cdef c_DatatypeConstructorDecl* cddc
-    def __cinit__(self, str name):
-        self.cddc = new c_DatatypeConstructorDecl(name.encode())
+    cdef c_DatatypeConstructorDecl cddc
+
+    def __cinit__(self):
+      pass
 
     def addSelector(self, str name, Sort sort):
         self.cddc.addSelector(name.encode(), sort.csort)
+
     def addSelectorSelf(self, str name):
         self.cddc.addSelectorSelf(name.encode())
 
@@ -156,7 +158,7 @@ cdef class DatatypeDecl:
         pass
 
     def addConstructor(self, DatatypeConstructorDecl ctor):
-        self.cdd.addConstructor(ctor.cddc[0])
+        self.cdd.addConstructor(ctor.cddc)
 
     def isParametric(self):
         return self.cdd.isParametric()
@@ -675,6 +677,11 @@ cdef class Solver:
                                             (<str?> symbol).encode())
         return term
 
+    def mkDatatypeConstructorDecl(self, str name):
+        cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl()
+        ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode())
+        return ddc
+
     def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None):
         cdef DatatypeDecl dd = DatatypeDecl()
         cdef vector[c_Sort] v
@@ -790,7 +797,7 @@ cdef class Solver:
         cdef vector[c_DatatypeConstructorDecl] v
 
         for c in ctors:
-            v.push_back((<DatatypeConstructorDecl?> c).cddc[0])
+            v.push_back((<DatatypeConstructorDecl?> c).cddc)
         sort.csort = self.csolver.declareDatatype(symbol.encode(), v)
         return sort
 
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index fdb6a081c..e604c7769 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1159,7 +1159,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t,
           PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
           api::Term func = PARSER_STATE->mkVar(
               *i,
-              api::Sort(PARSER_STATE->getSolver(), t.getType()),
+              api::Sort(SOLVER, t.getType()),
               ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
           PARSER_STATE->defineVar(*i, f);
           Command* decl =
@@ -1654,9 +1654,7 @@ tupleStore[CVC4::api::Term& f]
       }
       const Datatype & dt = ((DatatypeType)t.getType()).getDatatype();
       f2 = SOLVER->mkTerm(
-          api::APPLY_SELECTOR,
-          api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()),
-          f);
+          api::APPLY_SELECTOR, api::Term(SOLVER, dt[0][k].getSelector()), f);
     }
     ( ( arrayStore[f2]
       | DOT ( tupleStore[f2]
@@ -1689,9 +1687,7 @@ recordStore[CVC4::api::Term& f]
       }
       const Datatype & dt = ((DatatypeType)t.getType()).getDatatype();
       f2 = SOLVER->mkTerm(
-          api::APPLY_SELECTOR,
-          api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()),
-          f);
+          api::APPLY_SELECTOR, api::Term(SOLVER, dt[0][id].getSelector()), f);
     }
     ( ( arrayStore[f2]
       | DOT ( tupleStore[f2]
@@ -1835,10 +1831,9 @@ postfixTerm[CVC4::api::Term& f]
             PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
           }
           const Datatype & dt = ((DatatypeType)type.getType()).getDatatype();
-          f = SOLVER->mkTerm(
-              api::APPLY_SELECTOR,
-              api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()),
-              f);
+          f = SOLVER->mkTerm(api::APPLY_SELECTOR,
+                             api::Term(SOLVER, dt[0][id].getSelector()),
+                             f);
         }
       | k=numeral
         {
@@ -1853,10 +1848,9 @@ postfixTerm[CVC4::api::Term& f]
             PARSER_STATE->parseError(ss.str());
           }
           const Datatype & dt = ((DatatypeType)type.getType()).getDatatype();
-          f = SOLVER->mkTerm(
-              api::APPLY_SELECTOR,
-              api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()),
-              f);
+          f = SOLVER->mkTerm(api::APPLY_SELECTOR,
+                             api::Term(SOLVER, dt[0][k].getSelector()),
+                             f);
         }
       )
     )*
@@ -1896,8 +1890,7 @@ relationTerm[CVC4::api::Term& f]
       types.push_back(f.getSort());
       api::Sort t = SOLVER->mkTupleSort(types);
       const Datatype& dt = Datatype(((DatatypeType)t.getType()).getDatatype());
-      args.insert(args.begin(),
-                  api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+      args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor()));
       f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
     }
   | IDEN_TOK LPAREN formula[f] RPAREN
@@ -2147,9 +2140,7 @@ simpleTerm[CVC4::api::Term& f]
         }
         api::Sort dtype = SOLVER->mkTupleSort(types);
         const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
-        args.insert(
-            args.begin(),
-            api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+        args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor()));
         f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
       }
     }
@@ -2160,7 +2151,7 @@ simpleTerm[CVC4::api::Term& f]
       api::Sort dtype = SOLVER->mkTupleSort(types);
       const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
       f = MK_TERM(api::APPLY_CONSTRUCTOR,
-                  api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+                  api::Term(SOLVER, dt[0].getConstructor()));
     }
 
     /* empty record literal */
@@ -2170,7 +2161,7 @@ simpleTerm[CVC4::api::Term& f]
           std::vector<std::pair<std::string, api::Sort>>());
       const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
       f = MK_TERM(api::APPLY_CONSTRUCTOR,
-                  api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+                  api::Term(SOLVER, dt[0].getConstructor()));
     }
     /* empty set literal */
   | LBRACE RBRACE
@@ -2268,8 +2259,7 @@ simpleTerm[CVC4::api::Term& f]
       }
       api::Sort dtype = SOLVER->mkRecordSort(typeIds);
       const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
-      args.insert(args.begin(),
-                  api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+      args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor()));
       f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
     }
 
@@ -2377,8 +2367,9 @@ constructorDef[CVC4::api::DatatypeDecl& type]
   std::unique_ptr<CVC4::api::DatatypeConstructorDecl> ctor;
 }
   : identifier[id,CHECK_UNDECLARED,SYM_SORT]
-    { 
-      ctor.reset(new CVC4::api::DatatypeConstructorDecl(id));
+    {
+      ctor.reset(new CVC4::api::DatatypeConstructorDecl(
+          SOLVER->mkDatatypeConstructorDecl(id)));
     }
     ( LPAREN
       selector[&ctor]
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f29e03380..62bf7e974 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -800,7 +800,7 @@ sygusGrammarV1[CVC4::api::Sort & ret,
 
     PARSER_STATE->getUnresolvedSorts().clear();
 
-    ret = api::Sort(PARSER_STATE->getSolver(), datatypeTypes[0]);
+    ret = api::Sort(SOLVER, datatypeTypes[0]);
   };
 
 // SyGuS grammar term.
@@ -1798,7 +1798,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
           if (Datatype::datatypeOf(ef).isParametric())
           {
             type = api::Sort(
-                PARSER_STATE->getSolver(),
+                SOLVER,
                 Datatype::datatypeOf(ef)[Datatype::indexOf(ef)]
                     .getSpecializedConstructorType(expr.getSort().getType()));
           }
@@ -2521,7 +2521,8 @@ constructorDef[CVC4::api::DatatypeDecl& type]
 }
   : symbol[id,CHECK_NONE,SYM_VARIABLE]
     {
-      ctor = new api::DatatypeConstructorDecl(id);
+      ctor = new api::DatatypeConstructorDecl(
+          SOLVER->mkDatatypeConstructorDecl(id));
     }
     ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
     { // make the constructor
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index c1d60ca31..e26709595 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -1441,7 +1441,7 @@ tffLetTermBinding[std::vector<CVC4::api::Term> & bvlist,
     PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false);
     std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
     rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
-    lhs = api::Term(PARSER_STATE->getSolver(), lhs.getExpr().getOperator());
+    lhs = api::Term(SOLVER, lhs.getExpr().getOperator());
   }
   | LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK
   ;
@@ -1463,7 +1463,7 @@ tffLetFormulaBinding[std::vector<CVC4::api::Term> & bvlist,
     PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true);
     std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
     rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
-    lhs = api::Term(PARSER_STATE->getSolver(), lhs.getExpr().getOperator());
+    lhs = api::Term(SOLVER, lhs.getExpr().getOperator());
   }
   | LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK
   ;
diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h
index b404dfb13..c9eaf103e 100644
--- a/test/unit/api/datatype_api_black.h
+++ b/test/unit/api/datatype_api_black.h
@@ -43,10 +43,10 @@ void DatatypeBlack::tearDown() {}
 void DatatypeBlack::testMkDatatypeSort()
 {
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver.getIntegerSort());
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort listSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype d = listSort.getDatatype();
@@ -75,22 +75,22 @@ void DatatypeBlack::testMkDatatypeSorts()
   unresTypes.insert(unresList);
 
   DatatypeDecl tree = d_solver.mkDatatypeDecl("tree");
-  DatatypeConstructorDecl node("node");
+  DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node");
   node.addSelector("left", unresTree);
   node.addSelector("right", unresTree);
   tree.addConstructor(node);
 
-  DatatypeConstructorDecl leaf("leaf");
+  DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf");
   leaf.addSelector("data", unresList);
   tree.addConstructor(leaf);
 
   DatatypeDecl list = d_solver.mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("car", unresTree);
   cons.addSelector("cdr", unresTree);
   list.addConstructor(cons);
 
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   list.addConstructor(nil);
 
   std::vector<DatatypeDecl> dtdecls;
@@ -130,13 +130,13 @@ void DatatypeBlack::testDatatypeStructs()
 
   // create datatype sort to test
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", intSort);
   cons.addSelectorSelf("tail");
   Sort nullSort;
   TS_ASSERT_THROWS(cons.addSelector("null", nullSort), CVC4ApiException&);
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype dt = dtypeSort.getDatatype();
@@ -152,11 +152,11 @@ void DatatypeBlack::testDatatypeStructs()
 
   // create datatype sort to test
   DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum");
-  DatatypeConstructorDecl ca("A");
+  DatatypeConstructorDecl ca = d_solver.mkDatatypeConstructorDecl("A");
   dtypeSpecEnum.addConstructor(ca);
-  DatatypeConstructorDecl cb("B");
+  DatatypeConstructorDecl cb = d_solver.mkDatatypeConstructorDecl("B");
   dtypeSpecEnum.addConstructor(cb);
-  DatatypeConstructorDecl cc("C");
+  DatatypeConstructorDecl cc = d_solver.mkDatatypeConstructorDecl("C");
   dtypeSpecEnum.addConstructor(cc);
   Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum);
   Datatype dtEnum = dtypeSortEnum.getDatatype();
@@ -165,7 +165,8 @@ void DatatypeBlack::testDatatypeStructs()
 
   // create codatatype
   DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true);
-  DatatypeConstructorDecl consStream("cons");
+  DatatypeConstructorDecl consStream =
+      d_solver.mkDatatypeConstructorDecl("cons");
   consStream.addSelector("head", intSort);
   consStream.addSelectorSelf("tail");
   dtypeSpecStream.addConstructor(consStream);
@@ -204,11 +205,11 @@ void DatatypeBlack::testDatatypeNames()
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
   TS_ASSERT_THROWS_NOTHING(dtypeSpec.getName());
   TS_ASSERT(dtypeSpec.getName() == std::string("list"));
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", intSort);
   cons.addSelectorSelf("tail");
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype dt = dtypeSort.getDatatype();
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 90d4c10c1..7e925df54 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -39,6 +39,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkBitVectorSort();
   void testMkFloatingPointSort();
   void testMkDatatypeSort();
+  void testMkDatatypeSorts();
   void testMkFunctionSort();
   void testMkOp();
   void testMkParamSort();
@@ -96,9 +97,15 @@ class SolverBlack : public CxxTest::TestSuite
   void testPop3();
 
   void testSimplify();
+
+  void testAssertFormula();
   void testCheckEntailed();
   void testCheckEntailed1();
   void testCheckEntailed2();
+  void testCheckSat();
+  void testCheckSatAssuming();
+  void testCheckSatAssuming1();
+  void testCheckSatAssuming2();
 
   void testSetInfo();
   void testSetLogic();
@@ -173,6 +180,8 @@ void SolverBlack::testMkArraySort()
   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));
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkArraySort(boolSort, boolSort), CVC4ApiException&);
 }
 
 void SolverBlack::testMkBitVectorSort()
@@ -191,17 +200,64 @@ void SolverBlack::testMkFloatingPointSort()
 void SolverBlack::testMkDatatypeSort()
 {
   DatatypeDecl dtypeSpec = d_solver->mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver->getIntegerSort());
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSort(dtypeSpec));
+
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkDatatypeSort(dtypeSpec), CVC4ApiException&);
+
   DatatypeDecl throwsDtypeSpec = d_solver->mkDatatypeDecl("list");
   TS_ASSERT_THROWS(d_solver->mkDatatypeSort(throwsDtypeSpec),
                    CVC4ApiException&);
 }
 
+void SolverBlack::testMkDatatypeSorts()
+{
+  Solver slv;
+
+  DatatypeDecl dtypeSpec1 = d_solver->mkDatatypeDecl("list1");
+  DatatypeConstructorDecl cons1 = d_solver->mkDatatypeConstructorDecl("cons1");
+  cons1.addSelector("head1", d_solver->getIntegerSort());
+  dtypeSpec1.addConstructor(cons1);
+  DatatypeConstructorDecl nil1 = d_solver->mkDatatypeConstructorDecl("nil1");
+  dtypeSpec1.addConstructor(nil1);
+  DatatypeDecl dtypeSpec2 = d_solver->mkDatatypeDecl("list2");
+  DatatypeConstructorDecl cons2 = d_solver->mkDatatypeConstructorDecl("cons2");
+  cons2.addSelector("head2", d_solver->getIntegerSort());
+  dtypeSpec2.addConstructor(cons2);
+  DatatypeConstructorDecl nil2 = d_solver->mkDatatypeConstructorDecl("nil2");
+  dtypeSpec2.addConstructor(nil2);
+  std::vector<DatatypeDecl> decls = {dtypeSpec1, dtypeSpec2};
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSorts(decls));
+
+  TS_ASSERT_THROWS(slv.mkDatatypeSorts(decls), CVC4ApiException&);
+
+  DatatypeDecl throwsDtypeSpec = d_solver->mkDatatypeDecl("list");
+  std::vector<DatatypeDecl> throwsDecls = {throwsDtypeSpec};
+  TS_ASSERT_THROWS(d_solver->mkDatatypeSorts(throwsDecls), CVC4ApiException&);
+
+  /* with unresolved sorts */
+  Sort unresList = d_solver->mkUninterpretedSort("ulist");
+  std::set<Sort> unresSorts = {unresList};
+  DatatypeDecl ulist = d_solver->mkDatatypeDecl("ulist");
+  DatatypeConstructorDecl ucons = d_solver->mkDatatypeConstructorDecl("ucons");
+  ucons.addSelector("car", unresList);
+  ucons.addSelector("cdr", unresList);
+  ulist.addConstructor(ucons);
+  DatatypeConstructorDecl unil = d_solver->mkDatatypeConstructorDecl("unil");
+  ulist.addConstructor(unil);
+  std::vector<DatatypeDecl> udecls = {ulist};
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSorts(udecls, unresSorts));
+
+  TS_ASSERT_THROWS(slv.mkDatatypeSorts(udecls, unresSorts), CVC4ApiException&);
+
+  /* Note: More tests are in datatype_api_black. */
+}
+
 void SolverBlack::testMkFunctionSort()
 {
   TS_ASSERT_THROWS_NOTHING(d_solver->mkFunctionSort(
@@ -228,6 +284,23 @@ void SolverBlack::testMkFunctionSort()
           {d_solver->getIntegerSort(), d_solver->mkUninterpretedSort("u")},
           funSort2),
       CVC4ApiException&);
+
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkFunctionSort(d_solver->mkUninterpretedSort("u"),
+                                      d_solver->getIntegerSort()),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkFunctionSort(slv.mkUninterpretedSort("u"),
+                                      d_solver->getIntegerSort()),
+                   CVC4ApiException&);
+  std::vector<Sort> sorts1 = {d_solver->getBooleanSort(),
+                              slv.getIntegerSort(),
+                              d_solver->getIntegerSort()};
+  std::vector<Sort> sorts2 = {slv.getBooleanSort(), slv.getIntegerSort()};
+  TS_ASSERT_THROWS_NOTHING(slv.mkFunctionSort(sorts2, slv.getIntegerSort()));
+  TS_ASSERT_THROWS(slv.mkFunctionSort(sorts1, slv.getIntegerSort()),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkFunctionSort(sorts2, d_solver->getIntegerSort()),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testMkParamSort()
@@ -246,6 +319,10 @@ void SolverBlack::testMkPredicateSort()
   TS_ASSERT_THROWS(
       d_solver->mkPredicateSort({d_solver->getIntegerSort(), funSort}),
       CVC4ApiException&);
+
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkPredicateSort({d_solver->getIntegerSort()}),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testMkRecordSort()
@@ -259,6 +336,9 @@ void SolverBlack::testMkRecordSort()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkRecordSort(empty));
   Sort recSort = d_solver->mkRecordSort(fields);
   TS_ASSERT_THROWS_NOTHING(recSort.getDatatype());
+
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkRecordSort(fields), CVC4ApiException&);
 }
 
 void SolverBlack::testMkSetSort()
@@ -266,6 +346,9 @@ void SolverBlack::testMkSetSort()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkSetSort(d_solver->getBooleanSort()));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkSetSort(d_solver->getIntegerSort()));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkSetSort(d_solver->mkBitVectorSort(4)));
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkSetSort(d_solver->mkBitVectorSort(4)),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testMkUninterpretedSort()
@@ -288,6 +371,10 @@ void SolverBlack::testMkTupleSort()
                                           d_solver->getIntegerSort());
   TS_ASSERT_THROWS(d_solver->mkTupleSort({d_solver->getIntegerSort(), funSort}),
                    CVC4ApiException&);
+
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkTupleSort({d_solver->getIntegerSort()}),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testMkBitVector()
@@ -332,6 +419,8 @@ void SolverBlack::testMkVar()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort, ""));
   TS_ASSERT_THROWS(d_solver->mkVar(Sort()), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkVar(Sort(), "a"), CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkVar(boolSort, "x"), CVC4ApiException&);
 }
 
 void SolverBlack::testMkBoolean()
@@ -352,6 +441,9 @@ void SolverBlack::testMkUninterpretedConst()
       d_solver->mkUninterpretedConst(d_solver->getBooleanSort(), 1));
   TS_ASSERT_THROWS(d_solver->mkUninterpretedConst(Sort(), 1),
                    CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkUninterpretedConst(d_solver->getBooleanSort(), 1),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testMkAbstractValue()
@@ -393,13 +485,23 @@ void SolverBlack::testMkFloatingPoint()
   TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 0, t1), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 5, t2), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 5, t2), CVC4ApiException&);
+
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    Solver slv;
+    TS_ASSERT_THROWS(slv.mkFloatingPoint(3, 5, t1), CVC4ApiException&);
+  }
 }
 
 void SolverBlack::testMkEmptySet()
 {
+  Solver slv;
+  Sort s = d_solver->mkSetSort(d_solver->getBooleanSort());
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySet(Sort()));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySet(s));
   TS_ASSERT_THROWS(d_solver->mkEmptySet(d_solver->getBooleanSort()),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySet(Sort()));
+  TS_ASSERT_THROWS(slv.mkEmptySet(s), CVC4ApiException&);
 }
 
 void SolverBlack::testMkFalse()
@@ -558,6 +660,8 @@ void SolverBlack::testMkSepNil()
 {
   TS_ASSERT_THROWS_NOTHING(d_solver->mkSepNil(d_solver->getBooleanSort()));
   TS_ASSERT_THROWS(d_solver->mkSepNil(Sort()), CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkSepNil(d_solver->getIntegerSort()), CVC4ApiException&);
 }
 
 void SolverBlack::testMkString()
@@ -592,6 +696,7 @@ void SolverBlack::testMkTerm()
   std::vector<Term> v4 = {d_solver->mkReal(1), d_solver->mkReal(2)};
   std::vector<Term> v5 = {d_solver->mkReal(1), Term()};
   std::vector<Term> v6 = {};
+  Solver slv;
 
   // mkTerm(Kind kind) const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(PI));
@@ -603,6 +708,7 @@ void SolverBlack::testMkTerm()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(NOT, d_solver->mkTrue()));
   TS_ASSERT_THROWS(d_solver->mkTerm(NOT, Term()), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(NOT, a), CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkTerm(NOT, d_solver->mkTrue()), CVC4ApiException&);
 
   // mkTerm(Kind kind, Term child1, Term child2) const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(EQUAL, a, b));
@@ -610,6 +716,7 @@ void SolverBlack::testMkTerm()
   TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, a, Term()), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, a, d_solver->mkTrue()),
                    CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkTerm(EQUAL, a, b), CVC4ApiException&);
 
   // mkTerm(Kind kind, Term child1, Term child2, Term child3) const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(
@@ -626,6 +733,10 @@ void SolverBlack::testMkTerm()
   TS_ASSERT_THROWS(
       d_solver->mkTerm(ITE, d_solver->mkTrue(), d_solver->mkTrue(), b),
       CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      slv.mkTerm(
+          ITE, d_solver->mkTrue(), d_solver->mkTrue(), d_solver->mkTrue()),
+      CVC4ApiException&);
 
   // mkTerm(Kind kind, const std::vector<Term>& children) const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(EQUAL, v1));
@@ -643,15 +754,17 @@ void SolverBlack::testMkTermFromOp()
   std::vector<Term> v2 = {d_solver->mkReal(1), Term()};
   std::vector<Term> v3 = {};
   std::vector<Term> v4 = {d_solver->mkReal(5)};
+  Solver slv;
+
   // simple operator terms
   Op opterm1 = d_solver->mkOp(BITVECTOR_EXTRACT, 2, 1);
   Op opterm2 = d_solver->mkOp(DIVISIBLE, 1);
-  // list datatype
 
+  // list datatype
   Sort sort = d_solver->mkParamSort("T");
   DatatypeDecl listDecl = d_solver->mkDatatypeDecl("paramlist", sort);
-  DatatypeConstructorDecl cons("cons");
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
   cons.addSelector("head", sort);
   cons.addSelectorSelf("tail");
   listDecl.addConstructor(cons);
@@ -661,6 +774,7 @@ void SolverBlack::testMkTermFromOp()
       listSort.instantiate(std::vector<Sort>{d_solver->getIntegerSort()});
   Term c = d_solver->mkConst(intListSort, "c");
   Datatype list = listSort.getDatatype();
+
   // list datatype constructor and selector operator terms
   Term consTerm1 = list.getConstructorTerm("cons");
   Term consTerm2 = list.getConstructor("cons").getConstructorTerm();
@@ -684,6 +798,7 @@ void SolverBlack::testMkTermFromOp()
   TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, headTerm1),
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm1), CVC4ApiException&);
 
   // mkTerm(Op op, Term child) const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a));
@@ -695,24 +810,29 @@ void SolverBlack::testMkTermFromOp()
   TS_ASSERT_THROWS(
       d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)),
       CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkTerm(opterm1, a), CVC4ApiException&);
 
   // mkTerm(Op op, Term child1, Term child2) const
-  TS_ASSERT_THROWS(
-      d_solver->mkTerm(opterm2, d_solver->mkReal(1), d_solver->mkReal(2)),
-      CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(
       d_solver->mkTerm(APPLY_CONSTRUCTOR,
                        consTerm1,
                        d_solver->mkReal(0),
                        d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
+  TS_ASSERT_THROWS(
+      d_solver->mkTerm(opterm2, d_solver->mkReal(1), d_solver->mkReal(2)),
+      CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, d_solver->mkReal(1), Term()),
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, Term(), d_solver->mkReal(1)),
                    CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkTerm(APPLY_CONSTRUCTOR,
+                              consTerm1,
+                              d_solver->mkReal(0),
+                              d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)),
+                   CVC4ApiException&);
 
-  // mkTerm(Op op, Term child1, Term child2, Term child3)
-  // const
+  // mkTerm(Op op, Term child1, Term child2, Term child3) const
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&);
   TS_ASSERT_THROWS(
       d_solver->mkTerm(
@@ -724,6 +844,7 @@ void SolverBlack::testMkTermFromOp()
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v1), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v2), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v3), CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkTerm(opterm2, v4), CVC4ApiException&);
 }
 
 void SolverBlack::testMkTrue()
@@ -747,12 +868,22 @@ void SolverBlack::testMkTuple()
   TS_ASSERT_THROWS(d_solver->mkTuple({d_solver->getIntegerSort()},
                                      {d_solver->mkReal("5.3")}),
                    CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(
+      slv.mkTuple({d_solver->mkBitVectorSort(3)}, {slv.mkBitVector("101", 2)}),
+      CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      slv.mkTuple({slv.mkBitVectorSort(3)}, {d_solver->mkBitVector("101", 2)}),
+      CVC4ApiException&);
 }
 
 void SolverBlack::testMkUniverseSet()
 {
-  TS_ASSERT_THROWS(d_solver->mkUniverseSet(Sort()), CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(d_solver->mkUniverseSet(d_solver->getBooleanSort()));
+  TS_ASSERT_THROWS(d_solver->mkUniverseSet(Sort()), CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkUniverseSet(d_solver->getBooleanSort()),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testMkConst()
@@ -768,6 +899,9 @@ void SolverBlack::testMkConst()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort, ""));
   TS_ASSERT_THROWS(d_solver->mkConst(Sort()), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkConst(Sort(), "a"), CVC4ApiException&);
+
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkConst(boolSort), CVC4ApiException&);
 }
 
 void SolverBlack::testMkConstArray()
@@ -778,23 +912,29 @@ void SolverBlack::testMkConstArray()
   Term constArr = d_solver->mkConstArray(arrSort, zero);
 
   TS_ASSERT_THROWS_NOTHING(d_solver->mkConstArray(arrSort, zero));
+  TS_ASSERT_THROWS(d_solver->mkConstArray(Sort(), zero), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkConstArray(arrSort, Term()), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkConstArray(arrSort, d_solver->mkBitVector(1, 1)),
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkConstArray(intSort, zero), CVC4ApiException&);
+  Solver slv;
+  Term zero2 = slv.mkReal(0);
+  Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort());
+  TS_ASSERT_THROWS(slv.mkConstArray(arrSort2, zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkConstArray(arrSort, zero2), CVC4ApiException&);
 }
 
 void SolverBlack::testDeclareDatatype()
 {
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
   std::vector<DatatypeConstructorDecl> ctors1 = {nil};
   TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("a"), ctors1));
-  DatatypeConstructorDecl cons("cons");
-  DatatypeConstructorDecl nil2("nil");
+  DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl nil2 = d_solver->mkDatatypeConstructorDecl("nil");
   std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil2};
   TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("b"), ctors2));
-  DatatypeConstructorDecl cons2("cons");
-  DatatypeConstructorDecl nil3("nil");
+  DatatypeConstructorDecl cons2 = d_solver->mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl nil3 = d_solver->mkDatatypeConstructorDecl("nil");
   std::vector<DatatypeConstructorDecl> ctors3 = {cons2, nil3};
   TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors3));
   std::vector<DatatypeConstructorDecl> ctors4;
@@ -802,6 +942,9 @@ void SolverBlack::testDeclareDatatype()
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors4),
                    CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.declareDatatype(std::string("a"), ctors1),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testDeclareFun()
@@ -817,6 +960,8 @@ void SolverBlack::testDeclareFun()
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->declareFun("f5", {bvSort, bvSort}, funSort),
                    CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.declareFun("f1", {}, bvSort), CVC4ApiException&);
 }
 
 void SolverBlack::testDeclareSort()
@@ -959,11 +1104,11 @@ void SolverBlack::testGetOp()
 
   // Test Datatypes -- more complicated
   DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver->getIntegerSort());
   cons.addSelectorSelf("tail");
   consListSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
   consListSpec.addConstructor(nil);
   Sort consListSort = d_solver->mkDatatypeSort(consListSpec);
   Datatype consList = consListSort.getDatatype();
@@ -1059,11 +1204,11 @@ void SolverBlack::testSimplify()
   Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
   Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort());
   DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver->getIntegerSort());
   cons.addSelectorSelf("tail");
   consListSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
   consListSpec.addConstructor(nil);
   Sort consListSort = d_solver->mkDatatypeSort(consListSpec);
 
@@ -1081,6 +1226,8 @@ void SolverBlack::testSimplify()
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(x_eq_b));
   TS_ASSERT(d_solver->mkTrue() != x_eq_b);
   TS_ASSERT(d_solver->mkTrue() != d_solver->simplify(x_eq_b));
+  Solver slv;
+  TS_ASSERT_THROWS(slv.simplify(x), CVC4ApiException&);
 
   Term i1 = d_solver->mkConst(d_solver->getIntegerSort(), "i1");
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i1));
@@ -1123,12 +1270,22 @@ void SolverBlack::testSimplify()
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f2));
 }
 
+void SolverBlack::testAssertFormula()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver->assertFormula(d_solver->mkTrue()));
+  TS_ASSERT_THROWS(d_solver->assertFormula(Term()), CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.assertFormula(d_solver->mkTrue()), CVC4ApiException&);
+}
+
 void SolverBlack::testCheckEntailed()
 {
   d_solver->setOption("incremental", "false");
   TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
   TS_ASSERT_THROWS(d_solver->checkEntailed(d_solver->mkTrue()),
                    CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.checkEntailed(d_solver->mkTrue()), CVC4ApiException&);
 }
 
 void SolverBlack::testCheckEntailed1()
@@ -1142,6 +1299,8 @@ void SolverBlack::testCheckEntailed1()
   TS_ASSERT_THROWS(d_solver->checkEntailed(Term()), CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
   TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(z));
+  Solver slv;
+  TS_ASSERT_THROWS(slv.checkEntailed(d_solver->mkTrue()), CVC4ApiException&);
 }
 
 void SolverBlack::testCheckEntailed2()
@@ -1191,6 +1350,91 @@ void SolverBlack::testCheckEntailed2()
   TS_ASSERT_THROWS(
       d_solver->checkEntailed({n, d_solver->mkTerm(DISTINCT, x, y)}),
       CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.checkEntailed(d_solver->mkTrue()), CVC4ApiException&);
+}
+
+void SolverBlack::testCheckSat()
+{
+  d_solver->setOption("incremental", "false");
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkSat());
+  TS_ASSERT_THROWS(d_solver->checkSat(), CVC4ApiException&);
+}
+
+void SolverBlack::testCheckSatAssuming()
+{
+  d_solver->setOption("incremental", "false");
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue()));
+  TS_ASSERT_THROWS(d_solver->checkSatAssuming(d_solver->mkTrue()),
+                   CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.checkSatAssuming(d_solver->mkTrue()), CVC4ApiException&);
+}
+
+void SolverBlack::testCheckSatAssuming1()
+{
+  Sort boolSort = d_solver->getBooleanSort();
+  Term x = d_solver->mkConst(boolSort, "x");
+  Term y = d_solver->mkConst(boolSort, "y");
+  Term z = d_solver->mkTerm(AND, x, y);
+  d_solver->setOption("incremental", "true");
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue()));
+  TS_ASSERT_THROWS(d_solver->checkSatAssuming(Term()), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue()));
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(z));
+  Solver slv;
+  TS_ASSERT_THROWS(slv.checkSatAssuming(d_solver->mkTrue()), CVC4ApiException&);
+}
+
+void SolverBlack::testCheckSatAssuming2()
+{
+  d_solver->setOption("incremental", "true");
+
+  Sort uSort = d_solver->mkUninterpretedSort("u");
+  Sort intSort = d_solver->getIntegerSort();
+  Sort boolSort = d_solver->getBooleanSort();
+  Sort uToIntSort = d_solver->mkFunctionSort(uSort, intSort);
+  Sort intPredSort = d_solver->mkFunctionSort(intSort, boolSort);
+
+  Term n = Term();
+  // Constants
+  Term x = d_solver->mkConst(uSort, "x");
+  Term y = d_solver->mkConst(uSort, "y");
+  // Functions
+  Term f = d_solver->mkConst(uToIntSort, "f");
+  Term p = d_solver->mkConst(intPredSort, "p");
+  // Values
+  Term zero = d_solver->mkReal(0);
+  Term one = d_solver->mkReal(1);
+  // Terms
+  Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
+  Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
+  Term sum = d_solver->mkTerm(PLUS, f_x, f_y);
+  Term p_0 = d_solver->mkTerm(APPLY_UF, p, zero);
+  Term p_f_y = d_solver->mkTerm(APPLY_UF, p, f_y);
+  // Assertions
+  Term assertions =
+      d_solver->mkTerm(AND,
+                       std::vector<Term>{
+                           d_solver->mkTerm(LEQ, zero, f_x),  // 0 <= f(x)
+                           d_solver->mkTerm(LEQ, zero, f_y),  // 0 <= f(y)
+                           d_solver->mkTerm(LEQ, sum, one),  // f(x) + f(y) <= 1
+                           p_0.notTerm(),                    // not p(0)
+                           p_f_y                             // p(f(y))
+                       });
+
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue()));
+  d_solver->assertFormula(assertions);
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver->checkSatAssuming(d_solver->mkTerm(DISTINCT, x, y)));
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(
+      {d_solver->mkFalse(), d_solver->mkTerm(DISTINCT, x, y)}));
+  TS_ASSERT_THROWS(d_solver->checkSatAssuming(n), CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      d_solver->checkSatAssuming({n, d_solver->mkTerm(DISTINCT, x, y)}),
+      CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.checkSatAssuming(d_solver->mkTrue()), CVC4ApiException&);
 }
 
 void SolverBlack::testSetLogic()
diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h
index 42d2dcb25..437b5cf26 100644
--- a/test/unit/api/sort_black.h
+++ b/test/unit/api/sort_black.h
@@ -63,10 +63,10 @@ void SortBlack::testGetDatatype()
 {
   // create datatype sort, check should not fail
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver.getIntegerSort());
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatype());
@@ -80,11 +80,11 @@ void SortBlack::testDatatypeSorts()
   Sort intSort = d_solver.getIntegerSort();
   // create datatype sort to test
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", intSort);
   cons.addSelectorSelf("tail");
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype dt = dtypeSort.getDatatype();
@@ -121,8 +121,9 @@ void SortBlack::testInstantiate()
   // instantiate parametric datatype, check should not fail
   Sort sort = d_solver.mkParamSort("T");
   DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort);
-  DatatypeConstructorDecl paramCons("cons");
-  DatatypeConstructorDecl paramNil("nil");
+  DatatypeConstructorDecl paramCons =
+      d_solver.mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil");
   paramCons.addSelector("head", sort);
   paramDtypeSpec.addConstructor(paramCons);
   paramDtypeSpec.addConstructor(paramNil);
@@ -131,10 +132,10 @@ void SortBlack::testInstantiate()
       paramDtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}));
   // instantiate non-parametric datatype sort, check should fail
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver.getIntegerSort());
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   TS_ASSERT_THROWS(
@@ -265,8 +266,9 @@ void SortBlack::testGetDatatypeParamSorts()
   // create parametric datatype, check should not fail
   Sort sort = d_solver.mkParamSort("T");
   DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort);
-  DatatypeConstructorDecl paramCons("cons");
-  DatatypeConstructorDecl paramNil("nil");
+  DatatypeConstructorDecl paramCons =
+      d_solver.mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil");
   paramCons.addSelector("head", sort);
   paramDtypeSpec.addConstructor(paramCons);
   paramDtypeSpec.addConstructor(paramNil);
@@ -274,10 +276,10 @@ void SortBlack::testGetDatatypeParamSorts()
   TS_ASSERT_THROWS_NOTHING(paramDtypeSort.getDatatypeParamSorts());
   // create non-parametric datatype sort, check should fail
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver.getIntegerSort());
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   TS_ASSERT_THROWS(dtypeSort.getDatatypeParamSorts(), CVC4ApiException&);
@@ -287,10 +289,10 @@ void SortBlack::testGetDatatypeArity()
 {
   // create datatype sort, check should not fail
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver.getIntegerSort());
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatypeArity());
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index d8f022201..a3cbd028f 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -197,8 +197,8 @@ void TermBlack::testGetOp()
   // Test Datatypes Ops
   Sort sort = d_solver.mkParamSort("T");
   DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
-  DatatypeConstructorDecl cons("cons");
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   cons.addSelector("head", sort);
   cons.addSelectorSelf("tail");
   listDecl.addConstructor(cons);