type checking for define-fun in production builds; related to (and might resolve) bug 212

3 files changed, 8 insertions, 10 deletions

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index bb227f92f..29164ffa5 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -60,6 +60,8 @@ namespace expr {
  */
 class CVC4_PUBLIC TypeCheckingException : public Exception {
 
+  friend class SmtEngine;
+
 private:
 
   /** The expression responsible for the error */
diff --git a/src/expr/node.h b/src/expr/node.h
index bd6b53522..871f1e0d7 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -53,7 +53,7 @@ class TypeCheckingExceptionPrivate : public Exception {
 
 private:
 
-  /** The node repsonsible for the failure */
+  /** The node responsible for the failure */
   NodeTemplate<true>* d_node;
 
 protected:
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index c0f489d7a..0860365bc 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -789,15 +789,11 @@ inline TypeNode NodeManager::mkSort(TypeNode constructor,
          constructor.getNumChildren() == 0,
          "expected a sort constructor");
   Assert(children.size() > 0, "expected non-zero # of children");
-  uint64_t arity;
-  std::string name;
-  bool hasArityAttribute =
-    getAttribute(constructor.d_nv, expr::SortArityAttr(), arity);
-  Assert(hasArityAttribute, "expected a sort constructor");
-  bool hasNameAttribute =
-    getAttribute(constructor.d_nv, expr::VarNameAttr(), name);
-  Assert(hasNameAttribute, "expected a sort constructor");
-  Assert(arity == children.size(),
+  Assert( hasAttribute(constructor.d_nv, expr::SortArityAttr()) &&
+          hasAttribute(constructor.d_nv, expr::VarNameAttr()),
+          "expected a sort constructor" );
+  std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr());
+  Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) == children.size(),
          "arity mismatch in application of sort constructor");
   NodeBuilder<> nb(this, kind::SORT_TYPE);
   Node sortTag = Node(constructor.d_nv->d_children[0]);