New C++ API: Fix checks for mkTerm. (#2820)

This required fixing the OpTerm handling for mkTerm functions in the API.

1 files changed, 18 insertions, 9 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index e6b89b498..d0d36508f 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -301,21 +301,30 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3,
   }
 }
 
-Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
+Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children)
+{
+  const size_t nchildren = children.size();
   const kind::MetaKind mk = kind::metaKindOf(kind);
-  const unsigned n = children.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
   PrettyCheckArgument(
-      mk == kind::metakind::PARAMETERIZED ||
-      mk == kind::metakind::OPERATOR, kind,
+      mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR,
+      kind,
       "Only operator-style expressions are made with mkExpr(); "
       "to make variables and constants, see mkVar(), mkBoundVar(), "
       "and mkConst().");
   PrettyCheckArgument(
-      n >= minArity(kind) && n <= maxArity(kind), kind,
-      "Exprs with kind %s must have at least %u children and "
-      "at most %u children (the one under construction has %u)",
-      kind::kindToString(kind).c_str(),
-      minArity(kind), maxArity(kind), n);
+      mk != kind::metakind::PARAMETERIZED || nchildren > 0,
+      kind,
+      "Terms with kind %s must have an operator expression as first argument",
+      kind::kindToString(kind).c_str());
+  const size_t n = nchildren - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
+  PrettyCheckArgument(n >= minArity(kind) && n <= maxArity(kind),
+                      kind,
+                      "Exprs with kind %s must have at least %u children and "
+                      "at most %u children (the one under construction has %u)",
+                      kind::kindToString(kind).c_str(),
+                      minArity(kind),
+                      maxArity(kind),
+                      n);
 
   NodeManagerScope nms(d_nodeManager);