From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 4 Jun 2020 18:07:41 +0000 (-0700)
Subject: New C++ Api: Second and last batch of API guards. (#4563)
X-Git-Tag: cvc5-1.0.0~3257
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f0169b253759632aee0d21db916fe68702c66116;p=cvc5.git

New C++ Api: Second and last batch of API guards. (#4563)

This adds the remaining API guards in the Solver object (incl. unit tests).
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index f225da333..734fcddae 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -4194,8 +4194,10 @@ Term Solver::declareFun(const std::string& symbol,
  */
 Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   if (arity == 0) return Sort(this, d_exprMgr->mkSort(symbol));
   return Sort(this, d_exprMgr->mkSortConstructor(symbol, arity));
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4206,26 +4208,28 @@ Term Solver::defineFun(const std::string& symbol,
                        Sort sort,
                        Term term) const
 {
-  // CHECK:
-  // for bv in bound_vars:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(bv.getExprManager())
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(expr.getExprManager())
-  // CHECK: not recursive
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
       << "first-class sort as codomain sort for function sort";
-  // CHECK:
-  // for v in bound_vars: is bound var
   std::vector<Type> domain_types;
   for (size_t i = 0, size = bound_vars.size(); i < size; ++i)
   {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
+        << "bound variable associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        "bound variable",
+        bound_vars[i],
+        i)
+        << "a bound variable";
     CVC4::Type t = bound_vars[i].d_expr->getType();
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         t.isFirstClass(), "sort of parameter", bound_vars[i], i)
         << "first-class sort of parameter of defined function";
     domain_types.push_back(t);
   }
+  CVC4_API_SOLVER_CHECK_SORT(sort);
   CVC4_API_CHECK(sort == term.getSort())
       << "Invalid sort of function body '" << term << "', expected '" << sort
       << "'";
@@ -4238,17 +4242,14 @@ Term Solver::defineFun(const std::string& symbol,
   std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
   d_smtEngine->defineFunction(fun, ebound_vars, *term.d_expr);
   return Term(this, fun);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::defineFun(Term fun,
                        const std::vector<Term>& bound_vars,
                        Term term) const
 {
-  // CHECK:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(bv.getExprManager())
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(expr.getExprManager())
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function";
   std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
   size_t size = bound_vars.size();
@@ -4256,6 +4257,15 @@ Term Solver::defineFun(Term fun,
       << "'" << domain_sorts.size() << "'";
   for (size_t i = 0; i < size; ++i)
   {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
+        << "bound variable associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        "bound variable",
+        bound_vars[i],
+        i)
+        << "a bound variable";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         domain_sorts[i] == bound_vars[i].getSort(),
         "sort of parameter",
@@ -4264,16 +4274,15 @@ Term Solver::defineFun(Term fun,
         << "'" << domain_sorts[i] << "'";
   }
   Sort codomain = fun.getSort().getFunctionCodomainSort();
+  CVC4_API_SOLVER_CHECK_TERM(term);
   CVC4_API_CHECK(codomain == term.getSort())
       << "Invalid sort of function body '" << term << "', expected '"
       << codomain << "'";
 
-  // CHECK: not recursive
-  // CHECK:
-  // for v in bound_vars: is bound var
   std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
   d_smtEngine->defineFunction(*fun.d_expr, ebound_vars, *term.d_expr);
   return fun;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4284,29 +4293,33 @@ Term Solver::defineFunRec(const std::string& symbol,
                           Sort sort,
                           Term term) const
 {
-  // CHECK:
-  // for bv in bound_vars:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(bv.getExprManager())
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(expr.getExprManager())
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
       << "first-class sort as function codomain sort";
   Assert(!sort.isFunction()); /* A function sort is not first-class. */
-  // CHECK:
-  // for v in bound_vars: is bound var
   std::vector<Type> domain_types;
   for (size_t i = 0, size = bound_vars.size(); i < size; ++i)
   {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
+        << "bound variable associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        "bound variable",
+        bound_vars[i],
+        i)
+        << "a bound variable";
     CVC4::Type t = bound_vars[i].d_expr->getType();
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         t.isFirstClass(), "sort of parameter", bound_vars[i], i)
         << "first-class sort of parameter of defined function";
     domain_types.push_back(t);
   }
+  CVC4_API_SOLVER_CHECK_SORT(sort);
   CVC4_API_CHECK(sort == term.getSort())
       << "Invalid sort of function body '" << term << "', expected '" << sort
       << "'";
+  CVC4_API_SOLVER_CHECK_TERM(term);
   Type type = *sort.d_type;
   if (!domain_types.empty())
   {
@@ -4316,18 +4329,14 @@ Term Solver::defineFunRec(const std::string& symbol,
   std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
   d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_expr);
   return Term(this, fun);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::defineFunRec(Term fun,
                           const std::vector<Term>& bound_vars,
                           Term term) const
 {
-  // CHECK:
-  // for bv in bound_vars:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(bv.getExprManager())
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(expr.getExprManager())
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function";
   std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
   size_t size = bound_vars.size();
@@ -4335,6 +4344,15 @@ Term Solver::defineFunRec(Term fun,
       << "'" << domain_sorts.size() << "'";
   for (size_t i = 0; i < size; ++i)
   {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
+        << "bound variable associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        "bound variable",
+        bound_vars[i],
+        i)
+        << "a bound variable";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         domain_sorts[i] == bound_vars[i].getSort(),
         "sort of parameter",
@@ -4342,15 +4360,15 @@ Term Solver::defineFunRec(Term fun,
         i)
         << "'" << domain_sorts[i] << "'";
   }
+  CVC4_API_SOLVER_CHECK_TERM(term);
   Sort codomain = fun.getSort().getFunctionCodomainSort();
   CVC4_API_CHECK(codomain == term.getSort())
       << "Invalid sort of function body '" << term << "', expected '"
       << codomain << "'";
-  // CHECK:
-  // for v in bound_vars: is bound var
   std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
   d_smtEngine->defineFunctionRec(*fun.d_expr, ebound_vars, *term.d_expr);
   return fun;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4360,15 +4378,7 @@ void Solver::defineFunsRec(const std::vector<Term>& funs,
                            const std::vector<std::vector<Term>>& bound_vars,
                            const std::vector<Term>& terms) const
 {
-  // CHECK:
-  // for f in funs:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(f.getExprManager())
-  // for bv in bound_vars:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(bv.getExprManager())
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(expr.getExprManager())
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   size_t funs_size = funs.size();
   CVC4_API_ARG_SIZE_CHECK_EXPECTED(funs_size == bound_vars.size(), bound_vars)
       << "'" << funs_size << "'";
@@ -4378,13 +4388,30 @@ void Solver::defineFunsRec(const std::vector<Term>& funs,
     const std::vector<Term>& bvars = bound_vars[j];
     const Term& term = terms[j];
 
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == fun.d_solver, "function", fun, j)
+        << "function associated to this solver object";
     CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function";
+    CVC4_API_SOLVER_CHECK_TERM(term);
+
     std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
     size_t size = bvars.size();
     CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bvars)
         << "'" << domain_sorts.size() << "'";
     for (size_t i = 0; i < size; ++i)
     {
+      for (size_t k = 0, nbvars = bvars.size(); k < nbvars; ++k)
+      {
+        CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+            this == bvars[k].d_solver, "bound variable", bvars[k], k)
+            << "bound variable associated to this solver object";
+        CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+            bvars[k].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+            "bound variable",
+            bvars[k],
+            k)
+            << "a bound variable";
+      }
       CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
           domain_sorts[i] == bvars[i].getSort(),
           "sort of parameter",
@@ -4397,8 +4424,6 @@ void Solver::defineFunsRec(const std::vector<Term>& funs,
         codomain == term.getSort(), "sort of function body", term, j)
         << "'" << codomain << "'";
   }
-  // CHECK:
-  // for bv in bound_vars (for v in bv): is bound var
   std::vector<Expr> efuns = termVectorToExprs(funs);
   std::vector<std::vector<Expr>> ebound_vars;
   for (const auto& v : bound_vars)
@@ -4407,6 +4432,7 @@ void Solver::defineFunsRec(const std::vector<Term>& funs,
   }
   std::vector<Expr> exprs = termVectorToExprs(terms);
   d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4422,6 +4448,7 @@ void Solver::echo(std::ostream& out, const std::string& str) const
  */
 std::vector<Term> Solver::getAssertions(void) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   std::vector<Expr> assertions = d_smtEngine->getAssertions();
   /* Can not use
    *   return std::vector<Term>(assertions.begin(), assertions.end());
@@ -4432,6 +4459,7 @@ std::vector<Term> Solver::getAssertions(void) const
     res.push_back(Term(this, e));
   }
   return res;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4439,8 +4467,11 @@ std::vector<Term> Solver::getAssertions(void) const
  */
 std::vector<std::pair<Term, Term>> Solver::getAssignment(void) const
 {
-  // CHECK: produce-models set
-  // CHECK: result sat
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(CVC4::options::produceAssignments())
+      << "Cannot get assignment unless assignment generation is enabled "
+         "(try --produce-assignments)";
   std::vector<std::pair<Expr, Expr>> assignment = d_smtEngine->getAssignment();
   std::vector<std::pair<Term, Term>> res;
   for (const auto& p : assignment)
@@ -4448,6 +4479,7 @@ std::vector<std::pair<Term, Term>> Solver::getAssignment(void) const
     res.emplace_back(Term(this, p.first), Term(this, p.second));
   }
   return res;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4455,8 +4487,12 @@ std::vector<std::pair<Term, Term>> Solver::getAssignment(void) const
  */
 std::string Solver::getInfo(const std::string& flag) const
 {
-  // CHECK: flag valid?
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK(d_smtEngine->isValidGetInfoFlag(flag))
+      << "Unrecognized flag for getInfo.";
+
   return d_smtEngine->getInfo(flag).toString();
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4464,9 +4500,10 @@ std::string Solver::getInfo(const std::string& flag) const
  */
 std::string Solver::getOption(const std::string& option) const
 {
-  // CHECK: option exists?
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   SExpr res = d_smtEngine->getOption(option);
   return res.toString();
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4474,9 +4511,18 @@ std::string Solver::getOption(const std::string& option) const
  */
 std::vector<Term> Solver::getUnsatAssumptions(void) const
 {
-  // CHECK: incremental?
-  // CHECK: option produce-unsat-assumptions set?
-  // CHECK: last check sat/valid result is unsat/invalid
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(CVC4::options::incrementalSolving())
+      << "Cannot get unsat assumptions unless incremental solving is enabled "
+         "(try --incremental)";
+  CVC4_API_CHECK(CVC4::options::unsatAssumptions())
+      << "Cannot get unsat assumptions unless explicitly enabled "
+         "(try --produce-unsat-assumptions)";
+  CVC4_API_CHECK(d_smtEngine->getSmtMode()
+                 == SmtEngine::SmtMode::SMT_MODE_UNSAT)
+      << "Cannot get unsat assumptions unless in unsat mode.";
+
   std::vector<Expr> uassumptions = d_smtEngine->getUnsatAssumptions();
   /* Can not use
    *   return std::vector<Term>(uassumptions.begin(), uassumptions.end());
@@ -4487,6 +4533,7 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const
     res.push_back(Term(this, e));
   }
   return res;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4494,7 +4541,14 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const
  */
 std::vector<Term> Solver::getUnsatCore(void) const
 {
-  // CHECK: result unsat?
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(CVC4::options::unsatCores())
+      << "Cannot get unsat core unless explicitly enabled "
+         "(try --produce-unsat-cores)";
+  CVC4_API_CHECK(d_smtEngine->getSmtMode()
+                 == SmtEngine::SmtMode::SMT_MODE_UNSAT)
+      << "Cannot get unsat core unless in unsat mode.";
   UnsatCore core = d_smtEngine->getUnsatCore();
   /* Can not use
    *   return std::vector<Term>(core.begin(), core.end());
@@ -4505,6 +4559,7 @@ std::vector<Term> Solver::getUnsatCore(void) const
     res.push_back(Term(this, e));
   }
   return res;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4512,10 +4567,10 @@ std::vector<Term> Solver::getUnsatCore(void) const
  */
 Term Solver::getValue(Term term) const
 {
-  // CHECK:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(expr.getExprManager())
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_SOLVER_CHECK_TERM(term);
   return Term(this, d_smtEngine->getValue(*term.d_expr));
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4523,17 +4578,25 @@ Term Solver::getValue(Term term) const
  */
 std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
 {
-  // CHECK:
-  // for e in exprs:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(e.getExprManager())
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(CVC4::options::produceModels())
+      << "Cannot get value unless model generation is enabled "
+         "(try --produce-models)";
+  CVC4_API_CHECK(d_smtEngine->getSmtMode()
+                 != SmtEngine::SmtMode::SMT_MODE_UNSAT)
+      << "Cannot get value when in unsat mode.";
   std::vector<Term> res;
-  for (const Term& t : terms)
+  for (size_t i = 0, n = terms.size(); i < n; ++i)
   {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == terms[i].d_solver, "term", terms[i], i)
+        << "term associated to this solver object";
     /* Can not use emplace_back here since constructor is private. */
-    res.push_back(Term(this, d_smtEngine->getValue(*t.d_expr)));
+    res.push_back(Term(this, d_smtEngine->getValue(*terms[i].d_expr)));
   }
   return res;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4558,8 +4621,16 @@ void Solver::pop(uint32_t nscopes) const
 
 void Solver::printModel(std::ostream& out) const
 {
-  // CHECK: produce-models?
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(CVC4::options::produceModels())
+      << "Cannot get value unless model generation is enabled "
+         "(try --produce-models)";
+  CVC4_API_CHECK(d_smtEngine->getSmtMode()
+                 != SmtEngine::SmtMode::SMT_MODE_UNSAT)
+      << "Cannot get value when in unsat mode.";
   out << *d_smtEngine->getModel();
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4583,22 +4654,11 @@ void Solver::push(uint32_t nscopes) const
 /**
  *  ( reset-assertions )
  */
-void Solver::resetAssertions(void) const { d_smtEngine->resetAssertions(); }
-
-// TODO: issue #2781
-void Solver::setLogicHelper(const std::string& logic) const
+void Solver::resetAssertions(void) const
 {
-  CVC4_API_CHECK(!d_smtEngine->isFullyInited())
-      << "Invalid call to 'setLogic', solver is already fully initialized";
-  try
-  {
-    CVC4::LogicInfo logic_info(logic);
-    d_smtEngine->setLogic(logic_info);
-  }
-  catch (CVC4::IllegalArgumentException& e)
-  {
-    throw CVC4ApiException(e.getMessage());
-  }
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  d_smtEngine->resetAssertions();
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4606,6 +4666,7 @@ void Solver::setLogicHelper(const std::string& logic) const
  */
 void Solver::setInfo(const std::string& keyword, const std::string& value) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(
       keyword == "source" || keyword == "category" || keyword == "difficulty"
           || keyword == "filename" || keyword == "license" || keyword == "name"
@@ -4625,12 +4686,21 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const
       << "'sat', 'unsat' or 'unknown'";
 
   d_smtEngine->setInfo(keyword, value);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
  *  ( set-logic <symbol> )
  */
-void Solver::setLogic(const std::string& logic) const { setLogicHelper(logic); }
+void Solver::setLogic(const std::string& logic) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK(!d_smtEngine->isFullyInited())
+      << "Invalid call to 'setLogic', solver is already fully initialized";
+  CVC4::LogicInfo logic_info(logic);
+  d_smtEngine->setLogic(logic_info);
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
 
 /**
  *  ( set-option <option> )
@@ -4638,16 +4708,11 @@ void Solver::setLogic(const std::string& logic) const { setLogicHelper(logic); }
 void Solver::setOption(const std::string& option,
                        const std::string& value) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_CHECK(!d_smtEngine->isFullyInited())
       << "Invalid call to 'setOption', solver is already fully initialized";
-  try
-  {
-    d_smtEngine->setOption(option, value);
-  }
-  catch (CVC4::OptionException& e)
-  {
-    throw CVC4ApiException(e.getMessage());
-  }
+  d_smtEngine->setOption(option, value);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::ensureTermSort(const Term& term, const Sort& sort) const
@@ -4684,6 +4749,7 @@ Term Solver::mkSygusVar(Sort sort, const std::string& symbol) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_NOT_NULL(sort);
+  CVC4_API_SOLVER_CHECK_SORT(sort);
 
   Expr res = d_exprMgr->mkBoundVar(symbol, *sort.d_type);
   (void)res.getType(true); /* kick off type checking */
@@ -4698,11 +4764,21 @@ Term Solver::mkSygusVar(Sort sort, const std::string& symbol) const
 Grammar Solver::mkSygusGrammar(const std::vector<Term>& boundVars,
                                const std::vector<Term>& ntSymbols) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols.empty(), ntSymbols)
       << "non-empty vector";
 
   for (size_t i = 0, n = boundVars.size(); i < n; ++i)
   {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == boundVars[i].d_solver, "bound variable", boundVars[i], i)
+        << "bound variable associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        boundVars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        "bound variable",
+        boundVars[i],
+        i)
+        << "a bound variable";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         !boundVars[i].isNull(), "parameter term", boundVars[i], i)
         << "non-null term";
@@ -4710,12 +4786,22 @@ Grammar Solver::mkSygusGrammar(const std::vector<Term>& boundVars,
 
   for (size_t i = 0, n = ntSymbols.size(); i < n; ++i)
   {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == ntSymbols[i].d_solver, "term", ntSymbols[i], i)
+        << "term associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        ntSymbols[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        "bound variable",
+        ntSymbols[i],
+        i)
+        << "a bound variable";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         !ntSymbols[i].isNull(), "parameter term", ntSymbols[i], i)
         << "non-null term";
   }
 
   return Grammar(this, boundVars, ntSymbols);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::synthFun(const std::string& symbol,
@@ -4763,11 +4849,21 @@ Term Solver::synthFunHelper(const std::string& symbol,
   std::vector<Type> varTypes;
   for (size_t i = 0, n = boundVars.size(); i < n; ++i)
   {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == boundVars[i].d_solver, "bound variable", boundVars[i], i)
+        << "bound variable associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        boundVars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        "bound variable",
+        boundVars[i],
+        i)
+        << "a bound variable";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         !boundVars[i].isNull(), "parameter term", boundVars[i], i)
         << "non-null term";
     varTypes.push_back(boundVars[i].d_expr->getType());
   }
+  CVC4_API_SOLVER_CHECK_SORT(sort);
 
   if (g != nullptr)
   {
@@ -4796,12 +4892,15 @@ Term Solver::synthFunHelper(const std::string& symbol,
 
 void Solver::addSygusConstraint(Term term) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_NOT_NULL(term);
+  CVC4_API_SOLVER_CHECK_TERM(term);
   CVC4_API_ARG_CHECK_EXPECTED(
       term.d_expr->getType() == d_exprMgr->booleanType(), term)
       << "boolean term";
 
   d_smtEngine->assertSygusConstraint(*term.d_expr);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 void Solver::addSygusInvConstraint(Term inv,
@@ -4809,10 +4908,15 @@ void Solver::addSygusInvConstraint(Term inv,
                                    Term trans,
                                    Term post) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_NOT_NULL(inv);
+  CVC4_API_SOLVER_CHECK_TERM(inv);
   CVC4_API_ARG_CHECK_NOT_NULL(pre);
+  CVC4_API_SOLVER_CHECK_TERM(pre);
   CVC4_API_ARG_CHECK_NOT_NULL(trans);
+  CVC4_API_SOLVER_CHECK_TERM(trans);
   CVC4_API_ARG_CHECK_NOT_NULL(post);
+  CVC4_API_SOLVER_CHECK_TERM(post);
 
   CVC4_API_ARG_CHECK_EXPECTED(inv.d_expr->getType().isFunction(), inv)
       << "a function";
@@ -4847,13 +4951,21 @@ void Solver::addSygusInvConstraint(Term inv,
 
   d_smtEngine->assertSygusInvConstraint(
       *inv.d_expr, *pre.d_expr, *trans.d_expr, *post.d_expr);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-Result Solver::checkSynth() const { return d_smtEngine->checkSynth(); }
+Result Solver::checkSynth() const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  return d_smtEngine->checkSynth();
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
 
 Term Solver::getSynthSolution(Term term) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_NOT_NULL(term);
+  CVC4_API_SOLVER_CHECK_TERM(term);
 
   std::map<CVC4::Expr, CVC4::Expr> map;
   CVC4_API_CHECK(d_smtEngine->getSynthSolutions(map))
@@ -4865,15 +4977,20 @@ Term Solver::getSynthSolution(Term term) const
   CVC4_API_CHECK(it != map.cend()) << "Synth solution not found for given term";
 
   return Term(this, it->second);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 std::vector<Term> Solver::getSynthSolutions(
     const std::vector<Term>& terms) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) << "non-empty vector";
 
   for (size_t i = 0, n = terms.size(); i < n; ++i)
   {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == terms[i].d_solver, "parameter term", terms[i], i)
+        << "parameter term associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         !terms[i].isNull(), "parameter term", terms[i], i)
         << "non-null term";
@@ -4899,11 +5016,14 @@ std::vector<Term> Solver::getSynthSolutions(
   }
 
   return synthSolution;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 void Solver::printSynthSolution(std::ostream& out) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   d_smtEngine->printSynthSolution(out);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3c0a2cd8f..9e382cdcf 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1022,72 +1022,110 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
   throw UnrecognizedOptionException();
 }
 
-CVC4::SExpr SmtEngine::getInfo(const std::string& key) const {
+bool SmtEngine::isValidGetInfoFlag(const std::string& key) const
+{
+  if (key == "all-statistics" || key == "error-behavior" || key == "name"
+      || key == "version" || key == "authors" || key == "status"
+      || key == "reason-unknown" || key == "assertion-stack-levels"
+      || key == "all-options")
+  {
+    return true;
+  }
+  return false;
+}
 
+CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
+{
   SmtScope smts(this);
 
   Trace("smt") << "SMT getInfo(" << key << ")" << endl;
-  if(key == "all-statistics") {
+  if (!isValidGetInfoFlag(key))
+  {
+    throw UnrecognizedOptionException();
+  }
+  if (key == "all-statistics")
+  {
     vector<SExpr> stats;
-    for(StatisticsRegistry::const_iterator i = NodeManager::fromExprManager(d_exprManager)->getStatisticsRegistry()->begin();
-        i != NodeManager::fromExprManager(d_exprManager)->getStatisticsRegistry()->end();
-        ++i) {
+    for (StatisticsRegistry::const_iterator i =
+             NodeManager::fromExprManager(d_exprManager)
+                 ->getStatisticsRegistry()
+                 ->begin();
+         i
+         != NodeManager::fromExprManager(d_exprManager)
+                ->getStatisticsRegistry()
+                ->end();
+         ++i)
+    {
       vector<SExpr> v;
       v.push_back((*i).first);
       v.push_back((*i).second);
       stats.push_back(v);
     }
-    for(StatisticsRegistry::const_iterator i = d_statisticsRegistry->begin();
-        i != d_statisticsRegistry->end();
-        ++i) {
+    for (StatisticsRegistry::const_iterator i = d_statisticsRegistry->begin();
+         i != d_statisticsRegistry->end();
+         ++i)
+    {
       vector<SExpr> v;
       v.push_back((*i).first);
       v.push_back((*i).second);
       stats.push_back(v);
     }
     return SExpr(stats);
-  } else if(key == "error-behavior") {
+  }
+  if (key == "error-behavior")
+  {
     return SExpr(SExpr::Keyword("immediate-exit"));
-  } else if(key == "name") {
+  }
+  if (key == "name")
+  {
     return SExpr(Configuration::getName());
-  } else if(key == "version") {
+  }
+  if (key == "version")
+  {
     return SExpr(Configuration::getVersionString());
-  } else if(key == "authors") {
+  }
+  if (key == "authors")
+  {
     return SExpr(Configuration::about());
-  } else if(key == "status") {
+  }
+  if (key == "status")
+  {
     // sat | unsat | unknown
-    switch(d_status.asSatisfiabilityResult().isSat()) {
-    case Result::SAT:
-      return SExpr(SExpr::Keyword("sat"));
-    case Result::UNSAT:
-      return SExpr(SExpr::Keyword("unsat"));
-    default:
-      return SExpr(SExpr::Keyword("unknown"));
-    }
-  } else if(key == "reason-unknown") {
-    if(!d_status.isNull() && d_status.isUnknown()) {
+    switch (d_status.asSatisfiabilityResult().isSat())
+    {
+      case Result::SAT: return SExpr(SExpr::Keyword("sat"));
+      case Result::UNSAT: return SExpr(SExpr::Keyword("unsat"));
+      default: return SExpr(SExpr::Keyword("unknown"));
+    }
+  }
+  if (key == "reason-unknown")
+  {
+    if (!d_status.isNull() && d_status.isUnknown())
+    {
       stringstream ss;
       ss << d_status.whyUnknown();
       string s = ss.str();
       transform(s.begin(), s.end(), s.begin(), ::tolower);
       return SExpr(SExpr::Keyword(s));
-    } else {
+    }
+    else
+    {
       throw RecoverableModalException(
           "Can't get-info :reason-unknown when the "
           "last result wasn't unknown!");
     }
-  } else if(key == "assertion-stack-levels") {
+  }
+  if (key == "assertion-stack-levels")
+  {
     AlwaysAssert(d_userLevels.size()
                  <= std::numeric_limits<unsigned long int>::max());
     return SExpr(static_cast<unsigned long int>(d_userLevels.size()));
-  } else if(key == "all-options") {
-    // get the options, like all-statistics
-    std::vector< std::vector<std::string> > current_options =
-      Options::current()->getOptions();
-    return SExpr::parseListOfListOfAtoms(current_options);
-  } else {
-    throw UnrecognizedOptionException();
   }
+  Assert(key == "all-options");
+  // get the options, like all-statistics
+  std::vector<std::vector<std::string>> current_options =
+      Options::current()->getOptions();
+  return SExpr::parseListOfListOfAtoms(current_options);
 }
 
 void SmtEngine::debugCheckFormals(const std::vector<Expr>& formals, Expr func)
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 672bec821..75737b603 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -141,6 +141,27 @@ class CVC4_PUBLIC SmtEngine
  public:
   /* .......................................................................  */
 
+  /**
+   * The current mode of the solver, which is an extension of Figure 4.1 on
+   * page 52 of the SMT-LIB version 2.6 standard
+   * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
+   */
+  enum SmtMode
+  {
+    // the initial state of the solver
+    SMT_MODE_START,
+    // normal state of the solver, after assert/push/pop/declare/define
+    SMT_MODE_ASSERT,
+    // immediately after a check-sat returning "sat"
+    SMT_MODE_SAT,
+    // immediately after a check-sat returning "unknown"
+    SMT_MODE_SAT_UNKNOWN,
+    // immediately after a check-sat returning "unsat"
+    SMT_MODE_UNSAT,
+    // immediately after a successful call to get-abduct
+    SMT_MODE_ABDUCT
+  };
+
   /** Construct an SmtEngine with the given expression manager.  */
   SmtEngine(ExprManager* em);
   /** Destruct the SMT engine.  */
@@ -162,6 +183,9 @@ class CVC4_PUBLIC SmtEngine
   /** Return the user context level.  */
   size_t getNumUserLevels() { return d_userLevels.size(); }
 
+  /** Return the current mode of the solver. */
+  SmtMode getSmtMode() { return d_smtMode; }
+
   /**
    * Set the logic of the script.
    * @throw ModalException, LogicException
@@ -189,6 +213,9 @@ class CVC4_PUBLIC SmtEngine
    */
   void setInfo(const std::string& key, const CVC4::SExpr& value);
 
+  /** Return true if given keyword is a valid SMT-LIB v2 get-info flag. */
+  bool isValidGetInfoFlag(const std::string& key) const;
+
   /** Query information about the SMT environment.  */
   CVC4::SExpr getInfo(const std::string& key) const;
 
@@ -838,27 +865,6 @@ class CVC4_PUBLIC SmtEngine
   /** The types for the recursive function definitions */
   typedef context::CDList<Node> NodeList;
 
-  /**
-   * The current mode of the solver, which is an extension of Figure 4.1 on
-   * page 52 of the SMT-LIB version 2.6 standard
-   * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
-   */
-  enum SmtMode
-  {
-    // the initial state of the solver
-    SMT_MODE_START,
-    // normal state of the solver, after assert/push/pop/declare/define
-    SMT_MODE_ASSERT,
-    // immediately after a check-sat returning "sat"
-    SMT_MODE_SAT,
-    // immediately after a check-sat returning "unknown"
-    SMT_MODE_SAT_UNKNOWN,
-    // immediately after a check-sat returning "unsat"
-    SMT_MODE_UNSAT,
-    // immediately after a successful call to get-abduct
-    SMT_MODE_ABDUCT
-  };
-
   // disallow copy/assignment
   SmtEngine(const SmtEngine&) = delete;
   SmtEngine& operator=(const SmtEngine&) = delete;
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 7e925df54..43554088f 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -88,13 +88,28 @@ class SolverBlack : public CxxTest::TestSuite
   void testDefineFunsRec();
 
   void testUFIteration();
+
+  void testGetInfo();
   void testGetOp();
+  void testGetOption();
+  void testGetUnsatAssumptions1();
+  void testGetUnsatAssumptions2();
+  void testGetUnsatAssumptions3();
+  void testGetUnsatCore1();
+  void testGetUnsatCore2();
+  void testGetUnsatCore3();
+  void testGetValue1();
+  void testGetValue2();
+  void testGetValue3();
 
   void testPush1();
   void testPush2();
   void testPop1();
   void testPop2();
   void testPop3();
+  void testPrintModel1();
+  void testPrintModel2();
+  void testPrintModel3();
 
   void testSimplify();
 
@@ -990,17 +1005,36 @@ void SolverBlack::testDefineFun()
   TS_ASSERT_THROWS_NOTHING(d_solver->defineFun("f", {}, bvSort, v1));
   TS_ASSERT_THROWS_NOTHING(d_solver->defineFun("ff", {b1, b2}, bvSort, v1));
   TS_ASSERT_THROWS_NOTHING(d_solver->defineFun(f1, {b1, b11}, v1));
+  TS_ASSERT_THROWS(d_solver->defineFun("ff", {v1, b2}, bvSort, v1),
+                   CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->defineFun("fff", {b1}, bvSort, v3),
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->defineFun("ffff", {b1}, funSort2, v3),
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->defineFun("fffff", {b1, b3}, bvSort, v1),
                    CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->defineFun(f1, {v1, b11}, v1), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->defineFun(f1, {b1}, v1), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->defineFun(f1, {b1, b11}, v2), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->defineFun(f1, {b1, b11}, v3), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->defineFun(f2, {b1}, v2), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->defineFun(f3, {b1}, v1), CVC4ApiException&);
+
+  Solver slv;
+  Sort bvSort2 = slv.mkBitVectorSort(32);
+  Term v12 = slv.mkConst(bvSort2, "v1");
+  Term b12 = slv.mkVar(bvSort2, "b1");
+  Term b22 = slv.mkVar(slv.getIntegerSort(), "b2");
+  TS_ASSERT_THROWS(slv.defineFun("f", {}, bvSort, v12), CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.defineFun("f", {}, bvSort2, v1), CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.defineFun("ff", {b1, b22}, bvSort2, v12),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.defineFun("ff", {b12, b2}, bvSort2, v12),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.defineFun("ff", {b12, b22}, bvSort, v12),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.defineFun("ff", {b12, b22}, bvSort2, v1),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testDefineFunRec()
@@ -1024,6 +1058,8 @@ void SolverBlack::testDefineFunRec()
   TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec(f1, {b1, b11}, v1));
   TS_ASSERT_THROWS(d_solver->defineFunRec("fff", {b1}, bvSort, v3),
                    CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->defineFunRec("ff", {b1, v2}, bvSort, v1),
+                   CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->defineFunRec("ffff", {b1}, funSort2, v3),
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->defineFunRec("fffff", {b1, b3}, bvSort, v1),
@@ -1035,6 +1071,24 @@ void SolverBlack::testDefineFunRec()
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->defineFunRec(f2, {b1}, v2), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->defineFunRec(f3, {b1}, v1), CVC4ApiException&);
+
+  Solver slv;
+  Sort bvSort2 = slv.mkBitVectorSort(32);
+  Term v12 = slv.mkConst(bvSort2, "v1");
+  Term b12 = slv.mkVar(bvSort2, "b1");
+  Term b22 = slv.mkVar(slv.getIntegerSort(), "b2");
+  TS_ASSERT_THROWS_NOTHING(slv.defineFunRec("f", {}, bvSort2, v12));
+  TS_ASSERT_THROWS_NOTHING(slv.defineFunRec("ff", {b12, b22}, bvSort2, v12));
+  TS_ASSERT_THROWS(slv.defineFunRec("f", {}, bvSort, v12), CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.defineFunRec("f", {}, bvSort2, v1), CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.defineFunRec("ff", {b1, b22}, bvSort2, v12),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.defineFunRec("ff", {b12, b2}, bvSort2, v12),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.defineFunRec("ff", {b12, b22}, bvSort, v12),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.defineFunRec("ff", {b12, b22}, bvSort2, v1),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testDefineFunsRec()
@@ -1057,6 +1111,9 @@ void SolverBlack::testDefineFunsRec()
   Term f3 = d_solver->mkConst(bvSort, "f3");
   TS_ASSERT_THROWS_NOTHING(
       d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2}));
+  TS_ASSERT_THROWS(
+      d_solver->defineFunsRec({f1, f2}, {{v1, b11}, {b4}}, {v1, v2}),
+      CVC4ApiException&);
   TS_ASSERT_THROWS(
       d_solver->defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}),
       CVC4ApiException&);
@@ -1068,6 +1125,42 @@ void SolverBlack::testDefineFunsRec()
   TS_ASSERT_THROWS(
       d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}),
       CVC4ApiException&);
+
+  Solver slv;
+  Sort uSort2 = slv.mkUninterpretedSort("u");
+  Sort bvSort2 = slv.mkBitVectorSort(32);
+  Sort funSort12 = slv.mkFunctionSort({bvSort2, bvSort2}, bvSort2);
+  Sort funSort22 = slv.mkFunctionSort(uSort2, slv.getIntegerSort());
+  Term b12 = slv.mkVar(bvSort2, "b1");
+  Term b112 = slv.mkVar(bvSort2, "b1");
+  Term b42 = slv.mkVar(uSort2, "b4");
+  Term v12 = slv.mkConst(bvSort2, "v1");
+  Term v22 = slv.mkConst(slv.getIntegerSort(), "v2");
+  Term f12 = slv.mkConst(funSort12, "f1");
+  Term f22 = slv.mkConst(funSort22, "f2");
+  TS_ASSERT_THROWS_NOTHING(
+      slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v22}));
+  TS_ASSERT_THROWS(
+      slv.defineFunsRec({f1, f22}, {{b12, b112}, {b42}}, {v12, v22}),
+      CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      slv.defineFunsRec({f12, f2}, {{b12, b112}, {b42}}, {v12, v22}),
+      CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      slv.defineFunsRec({f12, f22}, {{b1, b112}, {b42}}, {v12, v22}),
+      CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      slv.defineFunsRec({f12, f22}, {{b12, b11}, {b42}}, {v12, v22}),
+      CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      slv.defineFunsRec({f12, f22}, {{b12, b112}, {b4}}, {v12, v22}),
+      CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v1, v22}),
+      CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v2}),
+      CVC4ApiException&);
 }
 
 void SolverBlack::testUFIteration()
@@ -1090,6 +1183,12 @@ void SolverBlack::testUFIteration()
   }
 }
 
+void SolverBlack::testGetInfo()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver->getInfo("name"));
+  TS_ASSERT_THROWS(d_solver->getInfo("asdf"), CVC4ApiException&);
+}
+
 void SolverBlack::testGetOp()
 {
   Sort bv32 = d_solver->mkBitVectorSort(32);
@@ -1132,6 +1231,164 @@ void SolverBlack::testGetOp()
   TS_ASSERT_EQUALS(listhead.getOp(), Op(d_solver.get(), APPLY_SELECTOR));
 }
 
+void SolverBlack::testGetOption()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver->getOption("incremental"));
+  TS_ASSERT_THROWS(d_solver->getOption("asdf"), CVC4ApiException&);
+}
+
+void SolverBlack::testGetUnsatAssumptions1()
+{
+#if IS_PROOFS_BUILD
+  d_solver->setOption("incremental", "false");
+  d_solver->checkSatAssuming(d_solver->mkFalse());
+  TS_ASSERT_THROWS(d_solver->getUnsatAssumptions(), CVC4ApiException&);
+#endif
+}
+
+void SolverBlack::testGetUnsatAssumptions2()
+{
+#if IS_PROOFS_BUILD
+  d_solver->setOption("incremental", "true");
+  d_solver->setOption("produce-unsat-assumptions", "false");
+  d_solver->checkSatAssuming(d_solver->mkFalse());
+  TS_ASSERT_THROWS(d_solver->getUnsatAssumptions(), CVC4ApiException&);
+#endif
+}
+
+void SolverBlack::testGetUnsatAssumptions3()
+{
+#if IS_PROOFS_BUILD
+  d_solver->setOption("incremental", "true");
+  d_solver->setOption("produce-unsat-assumptions", "true");
+  d_solver->checkSatAssuming(d_solver->mkFalse());
+  TS_ASSERT_THROWS_NOTHING(d_solver->getUnsatAssumptions());
+  d_solver->checkSatAssuming(d_solver->mkTrue());
+  TS_ASSERT_THROWS(d_solver->getUnsatAssumptions(), CVC4ApiException&);
+#endif
+}
+
+void SolverBlack::testGetUnsatCore1()
+{
+#if IS_PROOFS_BUILD
+  d_solver->setOption("incremental", "false");
+  d_solver->assertFormula(d_solver->mkFalse());
+  d_solver->checkSat();
+  TS_ASSERT_THROWS(d_solver->getUnsatCore(), CVC4ApiException&);
+#endif
+}
+
+void SolverBlack::testGetUnsatCore2()
+{
+#if IS_PROOFS_BUILD
+  d_solver->setOption("incremental", "false");
+  d_solver->setOption("produce-unsat-cores", "false");
+  d_solver->assertFormula(d_solver->mkFalse());
+  d_solver->checkSat();
+  TS_ASSERT_THROWS(d_solver->getUnsatCore(), CVC4ApiException&);
+#endif
+}
+
+void SolverBlack::testGetUnsatCore3()
+{
+#if IS_PROOFS_BUILD
+  d_solver->setOption("incremental", "true");
+  d_solver->setOption("produce-unsat-cores", "true");
+
+  Sort uSort = d_solver->mkUninterpretedSort("u");
+  Sort intSort = d_solver->getIntegerSort();
+  Sort boolSort = d_solver->getBooleanSort();
+  Sort uToIntSort = d_solver->mkFunctionSort(uSort, intSort);
+  Sort intPredSort = d_solver->mkFunctionSort(intSort, boolSort);
+  std::vector<Term> unsat_core;
+
+  Term x = d_solver->mkConst(uSort, "x");
+  Term y = d_solver->mkConst(uSort, "y");
+  Term f = d_solver->mkConst(uToIntSort, "f");
+  Term p = d_solver->mkConst(intPredSort, "p");
+  Term zero = d_solver->mkReal(0);
+  Term one = d_solver->mkReal(1);
+  Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
+  Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
+  Term sum = d_solver->mkTerm(PLUS, f_x, f_y);
+  Term p_0 = d_solver->mkTerm(APPLY_UF, p, zero);
+  Term p_f_y = d_solver->mkTerm(APPLY_UF, p, f_y);
+  d_solver->assertFormula(d_solver->mkTerm(GT, zero, f_x));
+  d_solver->assertFormula(d_solver->mkTerm(GT, zero, f_y));
+  d_solver->assertFormula(d_solver->mkTerm(GT, sum, one));
+  d_solver->assertFormula(p_0);
+  d_solver->assertFormula(p_f_y.notTerm());
+  TS_ASSERT(d_solver->checkSat().isUnsat());
+
+  TS_ASSERT_THROWS_NOTHING(unsat_core = d_solver->getUnsatCore());
+
+  d_solver->resetAssertions();
+  for (const auto& t : unsat_core)
+  {
+    d_solver->assertFormula(t);
+  }
+  Result res = d_solver->checkSat();
+  TS_ASSERT(res.isUnsat());
+#endif
+}
+
+void SolverBlack::testGetValue1()
+{
+  d_solver->setOption("produce-models", "false");
+  Term t = d_solver->mkTrue();
+  d_solver->assertFormula(t);
+  d_solver->checkSat();
+  TS_ASSERT_THROWS(d_solver->getValue(t), CVC4ApiException&);
+}
+
+void SolverBlack::testGetValue2()
+{
+  d_solver->setOption("produce-models", "true");
+  Term t = d_solver->mkFalse();
+  d_solver->assertFormula(t);
+  d_solver->checkSat();
+  TS_ASSERT_THROWS(d_solver->getValue(t), CVC4ApiException&);
+}
+
+void SolverBlack::testGetValue3()
+{
+  d_solver->setOption("produce-models", "true");
+  Sort uSort = d_solver->mkUninterpretedSort("u");
+  Sort intSort = d_solver->getIntegerSort();
+  Sort boolSort = d_solver->getBooleanSort();
+  Sort uToIntSort = d_solver->mkFunctionSort(uSort, intSort);
+  Sort intPredSort = d_solver->mkFunctionSort(intSort, boolSort);
+  std::vector<Term> unsat_core;
+
+  Term x = d_solver->mkConst(uSort, "x");
+  Term y = d_solver->mkConst(uSort, "y");
+  Term z = d_solver->mkConst(uSort, "z");
+  Term f = d_solver->mkConst(uToIntSort, "f");
+  Term p = d_solver->mkConst(intPredSort, "p");
+  Term zero = d_solver->mkReal(0);
+  Term one = d_solver->mkReal(1);
+  Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
+  Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
+  Term sum = d_solver->mkTerm(PLUS, f_x, f_y);
+  Term p_0 = d_solver->mkTerm(APPLY_UF, p, zero);
+  Term p_f_y = d_solver->mkTerm(APPLY_UF, p, f_y);
+
+  d_solver->assertFormula(d_solver->mkTerm(LEQ, zero, f_x));
+  d_solver->assertFormula(d_solver->mkTerm(LEQ, zero, f_y));
+  d_solver->assertFormula(d_solver->mkTerm(LEQ, sum, one));
+  d_solver->assertFormula(p_0.notTerm());
+  d_solver->assertFormula(p_f_y);
+  TS_ASSERT(d_solver->checkSat().isSat());
+  TS_ASSERT_THROWS_NOTHING(d_solver->getValue(x));
+  TS_ASSERT_THROWS_NOTHING(d_solver->getValue(y));
+  TS_ASSERT_THROWS_NOTHING(d_solver->getValue(z));
+  TS_ASSERT_THROWS_NOTHING(d_solver->getValue(sum));
+  TS_ASSERT_THROWS_NOTHING(d_solver->getValue(p_f_y));
+
+  Solver slv;
+  TS_ASSERT_THROWS(slv.getValue(x), CVC4ApiException&);
+}
+
 void SolverBlack::testPush1()
 {
   d_solver->setOption("incremental", "true");
@@ -1168,6 +1425,32 @@ void SolverBlack::testPop3()
   TS_ASSERT_THROWS(d_solver->pop(1), CVC4ApiException&);
 }
 
+void SolverBlack::testPrintModel1()
+{
+  d_solver->setOption("produce-models", "false");
+  Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
+  d_solver->assertFormula(x.eqTerm(x));
+  TS_ASSERT_THROWS(d_solver->printModel(std::cout), CVC4ApiException&);
+}
+
+void SolverBlack::testPrintModel2()
+{
+  d_solver->setOption("produce-models", "true");
+  Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
+  d_solver->assertFormula(x.eqTerm(x).notTerm());
+  d_solver->checkSat();
+  TS_ASSERT_THROWS(d_solver->printModel(std::cout), CVC4ApiException&);
+}
+
+void SolverBlack::testPrintModel3()
+{
+  d_solver->setOption("produce-models", "true");
+  Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
+  d_solver->assertFormula(x.eqTerm(x));
+  d_solver->checkSat();
+  TS_ASSERT_THROWS_NOTHING(d_solver->printModel(std::cout));
+}
+
 void SolverBlack::testSetInfo()
 {
   TS_ASSERT_THROWS(d_solver->setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException&);
@@ -1483,20 +1766,30 @@ void SolverBlack::testMkSygusVar()
   TS_ASSERT_THROWS(d_solver->mkSygusVar(Sort()), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkSygusVar(d_solver->getNullSort(), "a"),
                    CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkSygusVar(boolSort), CVC4ApiException&);
 }
 
 void SolverBlack::testMkSygusGrammar()
 {
   Term nullTerm;
   Term boolTerm = d_solver->mkBoolean(true);
-  Term intTerm = d_solver->mkReal(1);
+  Term boolVar = d_solver->mkVar(d_solver->getBooleanSort());
+  Term intVar = d_solver->mkVar(d_solver->getIntegerSort());
 
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusGrammar({}, {intTerm}));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusGrammar({boolTerm}, {intTerm}));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusGrammar({}, {intVar}));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusGrammar({boolVar}, {intVar}));
   TS_ASSERT_THROWS(d_solver->mkSygusGrammar({}, {}), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkSygusGrammar({}, {nullTerm}), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkSygusGrammar({nullTerm}, {intTerm}),
+  TS_ASSERT_THROWS(d_solver->mkSygusGrammar({}, {boolTerm}), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkSygusGrammar({boolTerm}, {intVar}),
                    CVC4ApiException&);
+  Solver slv;
+  Term boolVar2 = slv.mkVar(slv.getBooleanSort());
+  Term intVar2 = slv.mkVar(slv.getIntegerSort());
+  TS_ASSERT_THROWS_NOTHING(slv.mkSygusGrammar({boolVar2}, {intVar2}));
+  TS_ASSERT_THROWS(slv.mkSygusGrammar({boolVar}, {intVar2}), CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkSygusGrammar({boolVar2}, {intVar}), CVC4ApiException&);
 }
 
 void SolverBlack::testSynthFun()
@@ -1528,6 +1821,13 @@ void SolverBlack::testSynthFun()
   TS_ASSERT_THROWS(d_solver->synthFun("f5", {}, boolToBool), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->synthFun("f6", {x}, boolean, g2),
                    CVC4ApiException&);
+  Solver slv;
+  Term x2 = slv.mkVar(slv.getBooleanSort());
+  TS_ASSERT_THROWS_NOTHING(slv.synthFun("f1", {x2}, slv.getBooleanSort()));
+  TS_ASSERT_THROWS(slv.synthFun("", {}, d_solver->getBooleanSort()),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.synthFun("f1", {x}, d_solver->getBooleanSort()),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testSynthInv()
@@ -1564,6 +1864,9 @@ void SolverBlack::testAddSygusConstraint()
   TS_ASSERT_THROWS_NOTHING(d_solver->addSygusConstraint(boolTerm));
   TS_ASSERT_THROWS(d_solver->addSygusConstraint(nullTerm), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->addSygusConstraint(intTerm), CVC4ApiException&);
+
+  Solver slv;
+  TS_ASSERT_THROWS(slv.addSygusConstraint(boolTerm), CVC4ApiException&);
 }
 
 void SolverBlack::testAddSygusInvConstraint()
@@ -1619,6 +1922,23 @@ void SolverBlack::testAddSygusInvConstraint()
 
   TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, trans, trans),
                    CVC4ApiException&);
+  Solver slv;
+  Sort boolean2 = slv.getBooleanSort();
+  Sort real2 = slv.getRealSort();
+  Term inv22 = slv.declareFun("inv", {real2}, boolean2);
+  Term pre22 = slv.declareFun("pre", {real2}, boolean2);
+  Term trans22 = slv.declareFun("trans", {real2, real2}, boolean2);
+  Term post22 = slv.declareFun("post", {real2}, boolean2);
+  TS_ASSERT_THROWS_NOTHING(
+      slv.addSygusInvConstraint(inv22, pre22, trans22, post22));
+  TS_ASSERT_THROWS(slv.addSygusInvConstraint(inv, pre22, trans22, post22),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.addSygusInvConstraint(inv22, pre, trans22, post22),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.addSygusInvConstraint(inv22, pre22, trans, post22),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.addSygusInvConstraint(inv22, pre22, trans22, post),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testGetSynthSolution()
@@ -1639,6 +1959,9 @@ void SolverBlack::testGetSynthSolution()
 
   TS_ASSERT_THROWS(d_solver->getSynthSolution(nullTerm), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->getSynthSolution(x), CVC4ApiException&);
+
+  Solver slv;
+  TS_ASSERT_THROWS(slv.getSynthSolution(f), CVC4ApiException&);
 }
 
 void SolverBlack::testGetSynthSolutions()
@@ -1661,4 +1984,7 @@ void SolverBlack::testGetSynthSolutions()
   TS_ASSERT_THROWS(d_solver->getSynthSolutions({}), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->getSynthSolutions({nullTerm}), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->getSynthSolutions({x}), CVC4ApiException&);
+
+  Solver slv;
+  TS_ASSERT_THROWS(slv.getSynthSolutions({x}), CVC4ApiException&);
 }