Fixing test failures in production build

3 files changed, 54 insertions, 41 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 8cfd50f08..bf0e2f96e 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -252,61 +252,68 @@ Expr ExprManager::mkVar(const Type& type) {
 
 Expr ExprManager::mkAssociative(Kind kind,
                                 const std::vector<Expr>& children) {
-  Assert( metakind::isAssociative(kind), "Illegal kind in mkAssociative" );
+  CheckArgument( metakind::isAssociative(kind), kind,
+                 "Illegal kind in mkAssociative: %s",
+                 kind::kindToString(kind).c_str());
 
   NodeManagerScope nms(d_nodeManager);
   const unsigned int max = maxArity(kind);
   const unsigned int min = minArity(kind);
   unsigned int numChildren = children.size();
 
+  /* If the number of children is within bounds, then there's nothing to do. */
   if( numChildren <= max ) {
     return mkExpr(kind,children);
-  } else {
-    std::vector<Expr>::const_iterator it = children.begin() ;
-    std::vector<Expr>::const_iterator end = children.end() ;
-
-    /* The new top-level children and the children of each sub node */
-    std::vector<Node> newChildren;
-    std::vector<Node> subChildren;
-
-    while( it != end && numChildren > max ) {
-      /* Grab the next max children and make a node for them. */
-      for( std::vector<Expr>::const_iterator next = it + max;
-           it != next;
-           ++it, --numChildren ) {
-        subChildren.push_back(it->getNode());
-      }
-      Node subNode = d_nodeManager->mkNode(kind,subChildren);
-      newChildren.push_back(subNode);
+  } 
+
+  std::vector<Expr>::const_iterator it = children.begin() ;
+  std::vector<Expr>::const_iterator end = children.end() ;
 
-      subChildren.clear();
+  /* The new top-level children and the children of each sub node */
+  std::vector<Node> newChildren;
+  std::vector<Node> subChildren;
+
+  while( it != end && numChildren > max ) {
+    /* Grab the next max children and make a node for them. */
+    for( std::vector<Expr>::const_iterator next = it + max;
+         it != next;
+         ++it, --numChildren ) {
+      subChildren.push_back(it->getNode());
     }
+    Node subNode = d_nodeManager->mkNode(kind,subChildren);
+    newChildren.push_back(subNode);
+
+    subChildren.clear();
+  }
 
-    /* If there's children left, "top off" the Expr. */
-    if(numChildren > 0) {
-      /* If the leftovers are too few, just copy them into newChildren;
-       * otherwise make a new sub-node  */
-      if(numChildren < min) {
-        for(; it != end; ++it) {
-          newChildren.push_back(it->getNode());
-        }
-      } else {
-        for(; it != end; ++it) {
-          subChildren.push_back(it->getNode());
-        }
-        Node subNode = d_nodeManager->mkNode(kind, subChildren);
-        newChildren.push_back(subNode);
+  /* If there's children left, "top off" the Expr. */
+  if(numChildren > 0) {
+    /* If the leftovers are too few, just copy them into newChildren;
+     * otherwise make a new sub-node  */
+    if(numChildren < min) {
+      for(; it != end; ++it) {
+        newChildren.push_back(it->getNode());
       }
+    } else {
+      for(; it != end; ++it) {
+        subChildren.push_back(it->getNode());
+      }
+      Node subNode = d_nodeManager->mkNode(kind, subChildren);
+      newChildren.push_back(subNode);
     }
+  }
 
-    /* It would be really weird if this happened, but let's make sure. */
-    Assert( newChildren.size() >= min, "Too few new children in mkAssociative" );
-    /* We could call mkAssociative recursively with newChildren in this case, but it
-     * would take an astonishing number of children to make this fail. */
-    Assert( newChildren.size() <= max, "Too many new children in mkAssociative" );
+  /* It's inconceivable we could have enough children for this to fail
+   * (more than 2^32, in most cases?). */
+  AlwaysAssert( newChildren.size() <= max,
+                "Too many new children in mkAssociative" );
 
-    return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) );
-  }
+  /* It would be really weird if this happened (it would require
+   * min > 2, for one thing), but let's make sure. */
+  AlwaysAssert( newChildren.size() >= min, 
+                "Too few new children in mkAssociative" );
+
+  return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) );
 }
 
 unsigned ExprManager::minArity(Kind kind) {
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index c48afc10d..dc203061c 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -1,7 +1,7 @@
 # All unit tests
 UNIT_TESTS = \
 	expr/expr_public \
-    expr/expr_manager_public \
+        expr/expr_manager_public \
 	expr/node_white \
 	expr/node_black \
 	expr/kind_black \
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index e3be1bedd..78c38d782 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -338,13 +338,18 @@ public:
 
   }
 
+  /* This test is only valid if assertions are enabled. */
   void testMkNodeTooFew() {
+#ifdef CVC4_ASSERTIONS
     TS_ASSERT_THROWS( d_nodeManager->mkNode(AND), AssertionException );
     Node x = d_nodeManager->mkVar( d_nodeManager->booleanType() );
     TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, x), AssertionException );
+#endif
   }
 
+  /* This test is only valid if assertions are enabled. */
   void testMkNodeTooMany() {
+#ifdef CVC4_ASSERTIONS
     std::vector<Node> vars;
     const unsigned int max = metakind::getUpperBoundForKind(AND);
     TypeNode boolType = d_nodeManager->booleanType();
@@ -352,6 +357,7 @@ public:
       vars.push_back( d_nodeManager->mkVar(boolType) );
     }
     TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, vars), AssertionException );
+#endif
   }
 
 };