New C++ Api: Comprehensive guards for member functions of class Sort. (#6136)

1 files changed, 506 insertions, 116 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 933177783..9d55a7eb6 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1001,102 +1001,336 @@ std::vector<Sort> Sort::typeNodeVectorToSorts(
   return sorts;
 }
 
-/* Helpers                                                                    */
-/* -------------------------------------------------------------------------- */
-
-/* Split out to avoid nested API calls (problematic with API tracing).        */
-/* .......................................................................... */
-
-bool Sort::isNullHelper() const { return d_type->isNull(); }
-
-bool Sort::operator==(const Sort& s) const { return *d_type == *s.d_type; }
+bool Sort::operator==(const Sort& s) const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return *d_type == *s.d_type;
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::operator!=(const Sort& s) const { return *d_type != *s.d_type; }
+bool Sort::operator!=(const Sort& s) const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return *d_type != *s.d_type;
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::operator<(const Sort& s) const { return *d_type < *s.d_type; }
+bool Sort::operator<(const Sort& s) const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return *d_type < *s.d_type;
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::operator>(const Sort& s) const { return *d_type > *s.d_type; }
+bool Sort::operator>(const Sort& s) const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return *d_type > *s.d_type;
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::operator<=(const Sort& s) const { return *d_type <= *s.d_type; }
+bool Sort::operator<=(const Sort& s) const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return *d_type <= *s.d_type;
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::operator>=(const Sort& s) const { return *d_type >= *s.d_type; }
+bool Sort::operator>=(const Sort& s) const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return *d_type >= *s.d_type;
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isNull() const { return isNullHelper(); }
+bool Sort::isNull() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return isNullHelper();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isBoolean() const { return d_type->isBoolean(); }
+bool Sort::isBoolean() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isBoolean();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isInteger() const { return d_type->isInteger(); }
+bool Sort::isInteger() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isInteger();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isReal() const { return d_type->isReal(); }
+bool Sort::isReal() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isReal();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isString() const { return d_type->isString(); }
+bool Sort::isString() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isString();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isRegExp() const { return d_type->isRegExp(); }
+bool Sort::isRegExp() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isRegExp();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isRoundingMode() const { return d_type->isRoundingMode(); }
+bool Sort::isRoundingMode() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isRoundingMode();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isBitVector() const { return d_type->isBitVector(); }
+bool Sort::isBitVector() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isBitVector();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isFloatingPoint() const { return d_type->isFloatingPoint(); }
+bool Sort::isFloatingPoint() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isFloatingPoint();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isDatatype() const { return d_type->isDatatype(); }
+bool Sort::isDatatype() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isDatatype();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
 bool Sort::isParametricDatatype() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
   if (!d_type->isDatatype()) return false;
   return d_type->isParametricDatatype();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
-bool Sort::isConstructor() const { return d_type->isConstructor(); }
-bool Sort::isSelector() const { return d_type->isSelector(); }
-bool Sort::isTester() const { return d_type->isTester(); }
+bool Sort::isConstructor() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isConstructor();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isFunction() const { return d_type->isFunction(); }
+bool Sort::isSelector() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isSelector();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isPredicate() const { return d_type->isPredicate(); }
+bool Sort::isTester() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isTester();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isTuple() const { return d_type->isTuple(); }
+bool Sort::isFunction() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isFunction();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isRecord() const { return d_type->isRecord(); }
+bool Sort::isPredicate() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isPredicate();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isArray() const { return d_type->isArray(); }
+bool Sort::isTuple() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isTuple();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isSet() const { return d_type->isSet(); }
+bool Sort::isRecord() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isRecord();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
+
+bool Sort::isArray() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isArray();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isBag() const { return d_type->isBag(); }
+bool Sort::isSet() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isSet();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isSequence() const { return d_type->isSequence(); }
+bool Sort::isBag() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isBag();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isUninterpretedSort() const { return d_type->isSort(); }
+bool Sort::isSequence() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isSequence();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isSortConstructor() const { return d_type->isSortConstructor(); }
+bool Sort::isUninterpretedSort() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isSort();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isFirstClass() const { return d_type->isFirstClass(); }
+bool Sort::isSortConstructor() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isSortConstructor();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
-bool Sort::isFunctionLike() const { return d_type->isFunctionLike(); }
+bool Sort::isFirstClass() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isFirstClass();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
+
+bool Sort::isFunctionLike() const
+{
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  return d_type->isFunctionLike();
+  ////////
+  CVC4_API_TRY_CATCH_END;
+}
 
 bool Sort::isSubsortOf(const Sort& s) const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_ARG_CHECK_SOLVER("sort", s);
+  //////// all checks before this line
   return d_type->isSubtypeOf(*s.d_type);
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 bool Sort::isComparableTo(const Sort& s) const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_ARG_CHECK_SOLVER("sort", s);
+  //////// all checks before this line
   return d_type->isComparableTo(*s.d_type);
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 Datatype Sort::getDatatype() const
 {
   NodeManagerScope scope(d_solver->getNodeManager());
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isDatatype()) << "Expected datatype sort.";
+  //////// all checks before this line
   return Datatype(d_solver, d_type->getDType());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 Sort Sort::instantiate(const std::vector<Sort>& params) const
 {
   NodeManagerScope scope(d_solver->getNodeManager());
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  CVC4_API_CHECK_SORTS(params);
   CVC4_API_CHECK(isParametricDatatype() || isSortConstructor())
       << "Expected parametric datatype or sort constructor sort.";
+  //////// all checks before this line
   std::vector<CVC4::TypeNode> tparams = sortVectorToTypeNodes(params);
   if (d_type->isDatatype())
   {
@@ -1104,40 +1338,59 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
   }
   Assert(d_type->isSortConstructor());
   return Sort(d_solver, d_solver->getNodeManager()->mkSort(*d_type, tparams));
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 Sort Sort::substitute(const Sort& sort, const Sort& replacement) const
 {
   NodeManagerScope scope(d_solver->getNodeManager());
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  CVC4_API_CHECK_SORT(sort);
+  CVC4_API_CHECK_SORT(replacement);
+  //////// all checks before this line
   return Sort(
       d_solver,
       d_type->substitute(sort.getTypeNode(), replacement.getTypeNode()));
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 Sort Sort::substitute(const std::vector<Sort>& sorts,
                       const std::vector<Sort>& replacements) const
 {
   NodeManagerScope scope(d_solver->getNodeManager());
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
+  CVC4_API_CHECK_SORTS(sorts);
+  CVC4_API_CHECK_SORTS(replacements);
+  //////// all checks before this line
 
   std::vector<CVC4::TypeNode> tSorts = sortVectorToTypeNodes(sorts),
                               tReplacements =
                                   sortVectorToTypeNodes(replacements);
-
   return Sort(d_solver,
               d_type->substitute(tSorts.begin(),
                                  tSorts.end(),
                                  tReplacements.begin(),
                                  tReplacements.end()));
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 std::string Sort::toString() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
   if (d_solver != nullptr)
   {
     NodeManagerScope scope(d_solver->getNodeManager());
     return d_type->toString();
   }
   return d_type->toString();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 const CVC4::TypeNode& Sort::getTypeNode(void) const { return *d_type; }
@@ -1146,201 +1399,336 @@ const CVC4::TypeNode& Sort::getTypeNode(void) const { return *d_type; }
 
 size_t Sort::getConstructorArity() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
+  //////// all checks before this line
   return d_type->getNumChildren() - 1;
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 std::vector<Sort> Sort::getConstructorDomainSorts() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
+  //////// all checks before this line
   return typeNodeVectorToSorts(d_solver, d_type->getArgTypes());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 Sort Sort::getConstructorCodomainSort() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
+  //////// all checks before this line
   return Sort(d_solver, d_type->getConstructorRangeType());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 /* Selector sort ------------------------------------------------------- */
 
 Sort Sort::getSelectorDomainSort() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
+  //////// all checks before this line
   return Sort(d_solver, d_type->getSelectorDomainType());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 Sort Sort::getSelectorCodomainSort() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
+  //////// all checks before this line
   return Sort(d_solver, d_type->getSelectorRangeType());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 /* Tester sort ------------------------------------------------------- */
 
 Sort Sort::getTesterDomainSort() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
+  //////// all checks before this line
   return Sort(d_solver, d_type->getTesterDomainType());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 Sort Sort::getTesterCodomainSort() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
+  //////// all checks before this line
   return d_solver->getBooleanSort();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 /* Function sort ------------------------------------------------------- */
 
 size_t Sort::getFunctionArity() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
+  //////// all checks before this line
   return d_type->getNumChildren() - 1;
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 std::vector<Sort> Sort::getFunctionDomainSorts() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
+  //////// all checks before this line
   return typeNodeVectorToSorts(d_solver, d_type->getArgTypes());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 Sort Sort::getFunctionCodomainSort() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isFunction()) << "Not a function sort" << (*this);
+  //////// all checks before this line
   return Sort(d_solver, d_type->getRangeType());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 /* Array sort ---------------------------------------------------------- */
 
 Sort Sort::getArrayIndexSort() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isArray()) << "Not an array sort.";
+  //////// all checks before this line
   return Sort(d_solver, d_type->getArrayIndexType());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 Sort Sort::getArrayElementSort() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isArray()) << "Not an array sort.";
+  //////// all checks before this line
   return Sort(d_solver, d_type->getArrayConstituentType());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 /* Set sort ------------------------------------------------------------ */
 
 Sort Sort::getSetElementSort() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isSet()) << "Not a set sort.";
+  //////// all checks before this line
   return Sort(d_solver, d_type->getSetElementType());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 /* Bag sort ------------------------------------------------------------ */
 
 Sort Sort::getBagElementSort() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isBag()) << "Not a bag sort.";
+  //////// all checks before this line
   return Sort(d_solver, d_type->getBagElementType());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 /* Sequence sort ------------------------------------------------------- */
 
 Sort Sort::getSequenceElementSort() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isSequence()) << "Not a sequence sort.";
+  //////// all checks before this line
   return Sort(d_solver, d_type->getSequenceElementType());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 /* Uninterpreted sort -------------------------------------------------- */
 
 std::string Sort::getUninterpretedSortName() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
+  //////// all checks before this line
   return d_type->getName();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 bool Sort::isUninterpretedSortParameterized() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
-  // This method is not implemented in the NodeManager, since whether a
-  // uninterpreted sort is parametrized is irrelevant for solving.
+  //////// all checks before this line
+
+  /* This method is not implemented in the NodeManager, since whether a
+   * uninterpreted sort is parameterized is irrelevant for solving. */
   return d_type->getNumChildren() > 0;
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 std::vector<Sort> Sort::getUninterpretedSortParamSorts() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
-  // This method is not implemented in the NodeManager, since whether a
-  // uninterpreted sort is parametrized is irrelevant for solving.
+  //////// all checks before this line
+
+  /* This method is not implemented in the NodeManager, since whether a
+   * uninterpreted sort is parameterized is irrelevant for solving. */
   std::vector<TypeNode> params;
   for (size_t i = 0, nchildren = d_type->getNumChildren(); i < nchildren; i++)
   {
     params.push_back((*d_type)[i]);
   }
   return typeNodeVectorToSorts(d_solver, params);
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 /* Sort constructor sort ----------------------------------------------- */
 
 std::string Sort::getSortConstructorName() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
+  //////// all checks before this line
   return d_type->getName();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 size_t Sort::getSortConstructorArity() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
+  //////// all checks before this line
   return d_type->getSortConstructorArity();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 /* Bit-vector sort ----------------------------------------------------- */
 
 uint32_t Sort::getBVSize() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isBitVector()) << "Not a bit-vector sort.";
+  //////// all checks before this line
   return d_type->getBitVectorSize();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 /* Floating-point sort ------------------------------------------------- */
 
 uint32_t Sort::getFPExponentSize() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
+  //////// all checks before this line
   return d_type->getFloatingPointExponentSize();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 uint32_t Sort::getFPSignificandSize() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
+  //////// all checks before this line
   return d_type->getFloatingPointSignificandSize();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 /* Datatype sort ------------------------------------------------------- */
 
 std::vector<Sort> Sort::getDatatypeParamSorts() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort.";
-  std::vector<CVC4::TypeNode> typeNodes = d_type->getParamTypes();
-  return typeNodeVectorToSorts(d_solver, typeNodes);
+  //////// all checks before this line
+  return typeNodeVectorToSorts(d_solver, d_type->getParamTypes());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 size_t Sort::getDatatypeArity() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isDatatype()) << "Not a datatype sort.";
+  //////// all checks before this line
   return d_type->getNumChildren() - 1;
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 /* Tuple sort ---------------------------------------------------------- */
 
 size_t Sort::getTupleLength() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isTuple()) << "Not a tuple sort.";
+  //////// all checks before this line
   return d_type->getTupleLength();
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 std::vector<Sort> Sort::getTupleSorts() const
 {
+  CVC4_API_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(isTuple()) << "Not a tuple sort.";
-  std::vector<CVC4::TypeNode> typeNodes = d_type->getTupleTypes();
-  return typeNodeVectorToSorts(d_solver, typeNodes);
+  //////// all checks before this line
+  return typeNodeVectorToSorts(d_solver, d_type->getTupleTypes());
+  ////////
+  CVC4_API_TRY_CATCH_END;
 }
 
 /* --------------------------------------------------------------------- */
@@ -1356,6 +1744,14 @@ size_t SortHashFunction::operator()(const Sort& s) const
   return TypeNodeHashFunction()(*s.d_type);
 }
 
+/* Helpers                                                                    */
+/* -------------------------------------------------------------------------- */
+
+/* Split out to avoid nested API calls (problematic with API tracing).        */
+/* .......................................................................... */
+
+bool Sort::isNullHelper() const { return d_type->isNull(); }
+
 /* -------------------------------------------------------------------------- */
 /* Op                                                                     */
 /* -------------------------------------------------------------------------- */
@@ -3689,10 +4085,10 @@ 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(), "child term", children[i], i)
+        !children[i].isNull(), "child term", children, i)
         << "non-null term";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        this == children[i].d_solver, "child term", children[i], i)
+        this == children[i].d_solver, "child term", children, i)
         << "a child term associated to this solver object";
   }
 
@@ -3791,10 +4187,10 @@ Term Solver::mkTermHelper(const Op& op, 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(), "child term", children[i], i)
+        !children[i].isNull(), "child term", children, i)
         << "non-null term";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        this == children[i].d_solver, "child term", children[i], i)
+        this == children[i].d_solver, "child term", children, i)
         << "child term associated to this solver object";
   }
   checkMkTerm(op.d_kind, children.size());
@@ -3818,14 +4214,12 @@ std::vector<Sort> Solver::mkDatatypeSortsInternal(
   std::vector<CVC4::DType> datatypes;
   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)
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == dtypedecls[i].d_solver, "datatype declaration", dtypedecls, i)
         << "a datatype declaration associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(dtypedecls[i].getNumConstructors() > 0,
                                          "datatype declaration",
-                                         dtypedecls[i],
+                                         dtypedecls,
                                          i)
         << "a datatype declaration with at least one constructor";
     datatypes.push_back(dtypedecls[i].getDatatype());
@@ -3834,10 +4228,10 @@ std::vector<Sort> Solver::mkDatatypeSortsInternal(
   for (auto& sort : unresolvedSorts)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !sort.isNull(), "unresolved sort", sort, i)
+        !sort.isNull(), "unresolved sort", unresolvedSorts, i)
         << "non-null sort";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        this == sort.d_solver, "unresolved sort", sort, i)
+        this == sort.d_solver, "unresolved sort", unresolvedSorts, i)
         << "an unresolved sort associated to this solver object";
     i += 1;
   }
@@ -3861,15 +4255,15 @@ Term Solver::synthFunHelper(const std::string& symbol,
   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)
+        this == boundVars[i].d_solver, "bound variable", boundVars, i)
         << "bound variable associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !boundVars[i].isNull(), "bound variable", boundVars[i], i)
+        !boundVars[i].isNull(), "bound variable", boundVars, i)
         << "a non-null term";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
         "bound variable",
-        boundVars[i],
+        boundVars,
         i)
         << "a bound variable";
     varTypes.push_back(boundVars[i].d_node->getType());
@@ -4188,13 +4582,13 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts,
   for (size_t i = 0, size = sorts.size(); i < size; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !sorts[i].isNull(), "parameter sort", sorts[i], i)
+        !sorts[i].isNull(), "parameter sort", sorts, i)
         << "non-null sort";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        this == sorts[i].d_solver, "parameter sort", sorts[i], i)
+        this == sorts[i].d_solver, "parameter sort", sorts, i)
         << "sort associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
+        sorts[i].isFirstClass(), "parameter sort", sorts, i)
         << "first-class sort as parameter sort for function sort";
   }
   CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain)
@@ -4231,13 +4625,13 @@ Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const
   for (size_t i = 0, size = sorts.size(); i < size; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !sorts[i].isNull(), "parameter sort", sorts[i], i)
+        !sorts[i].isNull(), "parameter sort", sorts, i)
         << "non-null sort";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        this == sorts[i].d_solver, "parameter sort", sorts[i], i)
+        this == sorts[i].d_solver, "parameter sort", sorts, i)
         << "sort associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
+        sorts[i].isFirstClass(), "parameter sort", sorts, i)
         << "first-class sort as parameter sort for predicate sort";
   }
   std::vector<TypeNode> types = Sort::sortVectorToTypeNodes(sorts);
@@ -4257,10 +4651,10 @@ Sort Solver::mkRecordSort(
   for (const auto& p : fields)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !p.second.isNull(), "parameter sort", p.second, i)
+        !p.second.isNull(), "parameter sort", fields, i)
         << "non-null sort";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        this == p.second.d_solver, "parameter sort", p.second, i)
+        this == p.second.d_solver, "parameter sort", fields, i)
         << "sort associated to this solver object";
     i += 1;
     f.emplace_back(p.first, *p.second.d_type);
@@ -4338,13 +4732,13 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
   for (size_t i = 0, size = sorts.size(); i < size; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !sorts[i].isNull(), "parameter sort", sorts[i], i)
+        !sorts[i].isNull(), "parameter sort", sorts, i)
         << "non-null sort";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        this == sorts[i].d_solver, "parameter sort", sorts[i], i)
+        this == sorts[i].d_solver, "parameter sort", sorts, i)
         << "sort associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !sorts[i].isFunctionLike(), "parameter sort", sorts[i], i)
+        !sorts[i].isFunctionLike(), "parameter sort", sorts, i)
         << "non-function-like sort as parameter sort for tuple sort";
   }
   return mkTupleSortHelper(sorts);
@@ -4849,10 +5243,10 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name,
   for (size_t i = 0, size = params.size(); i < size; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !params[i].isNull(), "parameter sort", params[i], i)
+        !params[i].isNull(), "parameter sort", params, i)
         << "non-null sort";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        this == params[i].d_solver, "parameter sort", params[i], i)
+        this == params[i].d_solver, "parameter sort", params, i)
         << "sort associated to this solver object";
   }
   return DatatypeDecl(this, name, params, isCoDatatype);
@@ -4982,17 +5376,15 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts,
   std::vector<CVC4::Node> args;
   for (size_t i = 0, size = sorts.size(); i < size; i++)
   {
-    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !sorts[i].isNull(), "sort", sorts[i], i)
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(!sorts[i].isNull(), "sort", sorts, i)
         << "non-null sort";
-    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !terms[i].isNull(), "term", terms[i], i)
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(!terms[i].isNull(), "term", terms, i)
         << "non-null term";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        this == terms[i].d_solver, "child term", terms[i], i)
+        this == terms[i].d_solver, "child term", terms, 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)
+        this == sorts[i].d_solver, "child sort", sorts, i)
         << "child sort associated to this solver object";
     args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_node);
   }
@@ -5385,10 +5777,8 @@ Sort Solver::declareDatatype(
   DatatypeDecl dtdecl(this, symbol);
   for (size_t i = 0, size = ctors.size(); i < size; i++)
   {
-    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == ctors[i].d_solver,
-                                         "datatype constructor declaration",
-                                         ctors[i],
-                                         i)
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == ctors[i].d_solver, "datatype constructor declaration", ctors, i)
         << "datatype constructor declaration associated to this solver object";
     dtdecl.addConstructor(ctors[i]);
   }
@@ -5408,10 +5798,10 @@ Term Solver::declareFun(const std::string& symbol,
   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)
+        this == sorts[i].d_solver, "parameter sort", sorts, i)
         << "parameter sort associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
+        sorts[i].isFirstClass(), "parameter sort", sorts, i)
         << "first-class sort as parameter sort for function sort";
   }
   CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
@@ -5460,17 +5850,17 @@ Term Solver::defineFun(const std::string& symbol,
   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)
+        this == bound_vars[i].d_solver, "bound variable", bound_vars, i)
         << "bound variable associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
         "bound variable",
-        bound_vars[i],
+        bound_vars,
         i)
         << "a bound variable";
     CVC4::TypeNode t = bound_vars[i].d_node->getType();
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        t.isFirstClass(), "sort of parameter", bound_vars[i], i)
+        t.isFirstClass(), "sort of parameter", bound_vars, i)
         << "first-class sort of parameter of defined function";
     domain_types.push_back(t);
   }
@@ -5509,18 +5899,18 @@ Term Solver::defineFun(const Term& fun,
     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)
+          this == bound_vars[i].d_solver, "bound variable", bound_vars, i)
           << "bound variable associated to this solver object";
       CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
           bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
           "bound variable",
-          bound_vars[i],
+          bound_vars,
           i)
           << "a bound variable";
       CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
           domain_sorts[i] == bound_vars[i].getSort(),
           "sort of parameter",
-          bound_vars[i],
+          bound_vars,
           i)
           << "'" << domain_sorts[i] << "'";
     }
@@ -5570,17 +5960,17 @@ Term Solver::defineFunRec(const std::string& symbol,
   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)
+        this == bound_vars[i].d_solver, "bound variable", bound_vars, i)
         << "bound variable associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
         "bound variable",
-        bound_vars[i],
+        bound_vars,
         i)
         << "a bound variable";
     CVC4::TypeNode t = bound_vars[i].d_node->getType();
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        t.isFirstClass(), "sort of parameter", bound_vars[i], i)
+        t.isFirstClass(), "sort of parameter", bound_vars, i)
         << "first-class sort of parameter of defined function";
     domain_types.push_back(t);
   }
@@ -5628,18 +6018,18 @@ Term Solver::defineFunRec(const Term& fun,
     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)
+          this == bound_vars[i].d_solver, "bound variable", bound_vars, i)
           << "bound variable associated to this solver object";
       CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
           bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
           "bound variable",
-          bound_vars[i],
+          bound_vars,
           i)
           << "a bound variable";
       CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
           domain_sorts[i] == bound_vars[i].getSort(),
           "sort of parameter",
-          bound_vars[i],
+          bound_vars,
           i)
           << "'" << domain_sorts[i] << "'";
     }
@@ -5691,9 +6081,10 @@ void Solver::defineFunsRec(const std::vector<Term>& funs,
     const Term& term = terms[j];
 
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        this == fun.d_solver, "function", fun, j)
+        this == fun.d_solver, "function", funs, j)
         << "function associated to this solver object";
-    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == term.d_solver, "term", term, j)
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == term.d_solver, "term", terms, j)
         << "term associated to this solver object";
 
     if (fun.getSort().isFunction())
@@ -5707,19 +6098,19 @@ void Solver::defineFunsRec(const std::vector<Term>& funs,
         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)
+              this == bvars[k].d_solver, "bound variable", bvars, k)
               << "bound variable associated to this solver object";
           CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
               bvars[k].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
               "bound variable",
-              bvars[k],
+              bvars,
               k)
               << "a bound variable";
         }
         CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
             domain_sorts[i] == bvars[i].getSort(),
             "sort of parameter",
-            bvars[i],
+            bvars,
             i)
             << "'" << domain_sorts[i] << "' in parameter bound_vars[" << j
             << "]";
@@ -5885,7 +6276,7 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
   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)
+        this == terms[i].d_solver, "term", terms, i)
         << "term associated to this solver object";
     /* Can not use emplace_back here since constructor is private. */
     res.push_back(getValueHelper(terms[i]));
@@ -6082,11 +6473,10 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const
       << "a non-empty set of terms";
   for (size_t i = 0, tsize = terms.size(); i < tsize; ++i)
   {
-    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !terms[i].isNull(), "term", terms[i], i)
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(!terms[i].isNull(), "term", terms, i)
         << "a non-null term";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        this == terms[i].d_solver, "term", terms[i], i)
+        this == terms[i].d_solver, "term", terms, i)
         << "a term associated to this solver object";
   }
   NodeManagerScope scope(getNodeManager());
@@ -6216,15 +6606,15 @@ Grammar Solver::mkSygusGrammar(const std::vector<Term>& boundVars,
   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)
+        this == boundVars[i].d_solver, "bound variable", boundVars, i)
         << "bound variable associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !boundVars[i].isNull(), "bound variable", boundVars[i], i)
+        !boundVars[i].isNull(), "bound variable", boundVars, i)
         << "a non-null term";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
         "bound variable",
-        boundVars[i],
+        boundVars,
         i)
         << "a bound variable";
   }
@@ -6232,15 +6622,15 @@ 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, "non-terminal", ntSymbols[i], i)
+        this == ntSymbols[i].d_solver, "non-terminal", ntSymbols, i)
         << "term associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !ntSymbols[i].isNull(), "non-terminal", ntSymbols[i], i)
+        !ntSymbols[i].isNull(), "non-terminal", ntSymbols, i)
         << "a non-null term";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         ntSymbols[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
         "non-terminal",
-        ntSymbols[i],
+        ntSymbols,
         i)
         << "a bound variable";
   }
@@ -6396,10 +6786,10 @@ std::vector<Term> Solver::getSynthSolutions(
   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)
+        this == terms[i].d_solver, "parameter term", terms, i)
         << "parameter term associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !terms[i].isNull(), "parameter term", terms[i], i)
+        !terms[i].isNull(), "parameter term", terms, i)
         << "non-null term";
   }