7 files changed, 249 insertions, 81 deletions

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
   ;