Forcing a type check on Node construction in debug mode (Fixes: #188)

NOTE: mkNode/mkExpr/parsing functions can now throw type checking exceptions

7 files changed, 133 insertions, 110 deletions

diff --git a/test/regress/regress0/precedence/not-eq.cvc b/test/regress/regress0/precedence/not-eq.cvc
index 16c812086..6d712d43d 100644
--- a/test/regress/regress0/precedence/not-eq.cvc
+++ b/test/regress/regress0/precedence/not-eq.cvc
@@ -1,7 +1,7 @@
 % EXPECT: VALID
 % Simple test for right precedence of = and NOT.
 
-A, B: BOOLEAN;
+A, B: INT;
 
 QUERY (NOT A = B) <=> (NOT (A = B));
 % EXIT: 20
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 4849e55cb..e000e618e 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -37,8 +37,8 @@ private:
 
   Expr* a_bool;
   Expr* b_bool;
-  Expr* c_bool_mult;
-  Expr* mult_op;
+  Expr* c_bool_and;
+  Expr* and_op;
   Expr* plus_op;
   Type* fun_type;
   Expr* fun_op;
@@ -58,8 +58,8 @@ public:
 
       a_bool = new Expr(d_em->mkVar("a",d_em->booleanType()));
       b_bool = new Expr(d_em->mkVar("b", d_em->booleanType()));
-      c_bool_mult = new Expr(d_em->mkExpr(MULT, *a_bool, *b_bool));
-      mult_op = new Expr(d_em->mkConst(MULT));
+      c_bool_and = new Expr(d_em->mkExpr(AND, *a_bool, *b_bool));
+      and_op = new Expr(d_em->mkConst(AND));
       plus_op = new Expr(d_em->mkConst(PLUS));
       fun_type = new Type(d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType()));
       fun_op = new Expr(d_em->mkVar("f", *fun_type));
@@ -88,8 +88,8 @@ public:
       delete fun_type;
       delete fun_op;
       delete plus_op;
-      delete mult_op;
-      delete c_bool_mult;
+      delete and_op;
+      delete c_bool_and;
       delete b_bool;
       delete a_bool;
 
@@ -122,7 +122,7 @@ public:
     TS_ASSERT(!(e < e2));
     TS_ASSERT(e.isNull());
     TS_ASSERT(e2.isNull());
-    Expr f = d_em->mkExpr(PLUS, *a_bool, *b_bool);
+    Expr f = d_em->mkExpr(OR, *a_bool, *b_bool);
     Expr f2 = f;
     TS_ASSERT(!f.isNull());
     TS_ASSERT(!f2.isNull());
@@ -130,12 +130,12 @@ public:
     TS_ASSERT(f2 == f);
     TS_ASSERT(!(f2 < f));
     TS_ASSERT(!(f < f2));
-    TS_ASSERT(f == d_em->mkExpr(PLUS, *a_bool, *b_bool));
+    TS_ASSERT(f == d_em->mkExpr(OR, *a_bool, *b_bool));
   }
 
   void testAssignment() {
     /* Expr& operator=(const Expr& e); */
-    Expr e = d_em->mkExpr(PLUS, *a_bool, *b_bool);
+    Expr e = d_em->mkExpr(OR, *a_bool, *b_bool);
     Expr f;
     TS_ASSERT(f.isNull());
     f = e;
@@ -144,7 +144,7 @@ public:
     TS_ASSERT(f == e);
     TS_ASSERT(!(f < e));
     TS_ASSERT(!(e < f));
-    TS_ASSERT(f == d_em->mkExpr(PLUS, *a_bool, *b_bool));
+    TS_ASSERT(f == d_em->mkExpr(OR, *a_bool, *b_bool));
   }
 
   void testEquality() {
@@ -167,43 +167,43 @@ public:
 
     TS_ASSERT(*null < *a_bool);
     TS_ASSERT(*null < *b_bool);
-    TS_ASSERT(*null < *c_bool_mult);
+    TS_ASSERT(*null < *c_bool_and);
     TS_ASSERT(*null < *d_apply_fun_bool);
     TS_ASSERT(*null < *plus_op);
-    TS_ASSERT(*null < *mult_op);
+    TS_ASSERT(*null < *and_op);
     TS_ASSERT(*null < *i1);
     TS_ASSERT(*null < *i2);
     TS_ASSERT(*null < *r1);
     TS_ASSERT(*null < *r2);
 
     TS_ASSERT(*a_bool < *b_bool);
-    TS_ASSERT(*a_bool < *c_bool_mult);
+    TS_ASSERT(*a_bool < *c_bool_and);
     TS_ASSERT(*a_bool < *d_apply_fun_bool);
     TS_ASSERT(!(*b_bool < *a_bool));
-    TS_ASSERT(!(*c_bool_mult < *a_bool));
+    TS_ASSERT(!(*c_bool_and < *a_bool));
     TS_ASSERT(!(*d_apply_fun_bool < *a_bool));
 
-    TS_ASSERT(*b_bool < *c_bool_mult);
+    TS_ASSERT(*b_bool < *c_bool_and);
     TS_ASSERT(*b_bool < *d_apply_fun_bool);
-    TS_ASSERT(!(*c_bool_mult < *b_bool));
+    TS_ASSERT(!(*c_bool_and < *b_bool));
     TS_ASSERT(!(*d_apply_fun_bool < *b_bool));
 
-    TS_ASSERT(*c_bool_mult < *d_apply_fun_bool);
-    TS_ASSERT(!(*d_apply_fun_bool < *c_bool_mult));
+    TS_ASSERT(*c_bool_and < *d_apply_fun_bool);
+    TS_ASSERT(!(*d_apply_fun_bool < *c_bool_and));
 
-    TS_ASSERT(*mult_op < *c_bool_mult);
-    TS_ASSERT(*mult_op < *d_apply_fun_bool);
+    TS_ASSERT(*and_op < *c_bool_and);
+    TS_ASSERT(*and_op < *d_apply_fun_bool);
     TS_ASSERT(*plus_op < *d_apply_fun_bool);
-    TS_ASSERT(!(*c_bool_mult < *mult_op));
-    TS_ASSERT(!(*d_apply_fun_bool < *mult_op));
+    TS_ASSERT(!(*c_bool_and < *and_op));
+    TS_ASSERT(!(*d_apply_fun_bool < *and_op));
     TS_ASSERT(!(*d_apply_fun_bool < *plus_op));
 
     TS_ASSERT(!(*null < *null));
     TS_ASSERT(!(*a_bool < *a_bool));
     TS_ASSERT(!(*b_bool < *b_bool));
-    TS_ASSERT(!(*c_bool_mult < *c_bool_mult));
+    TS_ASSERT(!(*c_bool_and < *c_bool_and));
     TS_ASSERT(!(*plus_op < *plus_op));
-    TS_ASSERT(!(*mult_op < *mult_op));
+    TS_ASSERT(!(*and_op < *and_op));
     TS_ASSERT(!(*d_apply_fun_bool < *d_apply_fun_bool));
   }
 
@@ -212,8 +212,8 @@ public:
 
     TS_ASSERT(a_bool->getKind() == VARIABLE);
     TS_ASSERT(b_bool->getKind() == VARIABLE);
-    TS_ASSERT(c_bool_mult->getKind() == MULT);
-    TS_ASSERT(mult_op->getKind() == BUILTIN);
+    TS_ASSERT(c_bool_and->getKind() == AND);
+    TS_ASSERT(and_op->getKind() == BUILTIN);
     TS_ASSERT(plus_op->getKind() == BUILTIN);
     TS_ASSERT(d_apply_fun_bool->getKind() == APPLY_UF);
     TS_ASSERT(null->getKind() == NULL_EXPR);
@@ -229,8 +229,8 @@ public:
 
     TS_ASSERT(a_bool->getNumChildren() == 0);
     TS_ASSERT(b_bool->getNumChildren() == 0);
-    TS_ASSERT(c_bool_mult->getNumChildren() == 2);
-    TS_ASSERT(mult_op->getNumChildren() == 0);
+    TS_ASSERT(c_bool_and->getNumChildren() == 2);
+    TS_ASSERT(and_op->getNumChildren() == 0);
     TS_ASSERT(plus_op->getNumChildren() == 0);
     TS_ASSERT(d_apply_fun_bool->getNumChildren() == 1);
     TS_ASSERT(null->getNumChildren() == 0);
@@ -247,17 +247,17 @@ public:
 
     TS_ASSERT(!a_bool->hasOperator());
     TS_ASSERT(!b_bool->hasOperator());
-    TS_ASSERT(c_bool_mult->hasOperator());
-    TS_ASSERT(!mult_op->hasOperator());
+    TS_ASSERT(c_bool_and->hasOperator());
+    TS_ASSERT(!and_op->hasOperator());
     TS_ASSERT(!plus_op->hasOperator());
     TS_ASSERT(d_apply_fun_bool->hasOperator());
     TS_ASSERT(!null->hasOperator());
 
     TS_ASSERT_THROWS(a_bool->getOperator(), IllegalArgumentException);
     TS_ASSERT_THROWS(b_bool->getOperator(), IllegalArgumentException);
-    TS_ASSERT(c_bool_mult->getOperator() == *mult_op);
+    TS_ASSERT(c_bool_and->getOperator() == *and_op);
     TS_ASSERT_THROWS(plus_op->getOperator(), IllegalArgumentException);
-    TS_ASSERT_THROWS(mult_op->getOperator(), IllegalArgumentException);
+    TS_ASSERT_THROWS(and_op->getOperator(), IllegalArgumentException);
     TS_ASSERT(d_apply_fun_bool->getOperator() == *fun_op);
     TS_ASSERT_THROWS(null->getOperator(), IllegalArgumentException);
   }
@@ -269,9 +269,10 @@ public:
     TS_ASSERT(a_bool->getType(true) == d_em->booleanType());
     TS_ASSERT(b_bool->getType(false) == d_em->booleanType());
     TS_ASSERT(b_bool->getType(true) == d_em->booleanType());
-    TS_ASSERT_THROWS(c_bool_mult->getType(true), TypeCheckingException);
+    TS_ASSERT_THROWS(d_em->mkExpr(MULT,*a_bool,*b_bool).getType(true), 
+                     TypeCheckingException);
 // These need better support for operators
-//    TS_ASSERT(mult_op->getType().isNull());
+//    TS_ASSERT(and_op->getType().isNull());
 //    TS_ASSERT(plus_op->getType().isNull());
     TS_ASSERT(d_apply_fun_bool->getType() == d_em->booleanType());
     TS_ASSERT(i1->getType().isInteger());
@@ -285,8 +286,8 @@ public:
 
     TS_ASSERT(a_bool->toString() == "a");
     TS_ASSERT(b_bool->toString() == "b");
-    TS_ASSERT(c_bool_mult->toString() == "(MULT a b)");
-    TS_ASSERT(mult_op->toString() == "(BUILTIN MULT)");
+    TS_ASSERT(c_bool_and->toString() == "(AND a b)");
+    TS_ASSERT(and_op->toString() == "(BUILTIN AND)");
     TS_ASSERT(plus_op->toString() == "(BUILTIN PLUS)");
     TS_ASSERT(d_apply_fun_bool->toString() == "(APPLY_UF f a)");
     TS_ASSERT(null->toString() == "null");
@@ -304,8 +305,8 @@ public:
     stringstream si1, si2, sr1, sr2;
     a_bool->toStream(sa);
     b_bool->toStream(sb);
-    c_bool_mult->toStream(sc);
-    mult_op->toStream(smult);
+    c_bool_and->toStream(sc);
+    and_op->toStream(smult);
     plus_op->toStream(splus);
     d_apply_fun_bool->toStream(sd);
     null->toStream(snull);
@@ -317,8 +318,8 @@ public:
 
     TS_ASSERT(sa.str() == "a");
     TS_ASSERT(sb.str() == "b");
-    TS_ASSERT(sc.str() == "(MULT a b)");
-    TS_ASSERT(smult.str() == "(BUILTIN MULT)");
+    TS_ASSERT(sc.str() == "(AND a b)");
+    TS_ASSERT(smult.str() == "(BUILTIN AND)");
     TS_ASSERT(splus.str() == "(BUILTIN PLUS)");
     TS_ASSERT(sd.str() == "(APPLY_UF f a)");
     TS_ASSERT(snull.str() == "null");
@@ -334,8 +335,8 @@ public:
 
     TS_ASSERT(!a_bool->isNull());
     TS_ASSERT(!b_bool->isNull());
-    TS_ASSERT(!c_bool_mult->isNull());
-    TS_ASSERT(!mult_op->isNull());
+    TS_ASSERT(!c_bool_and->isNull());
+    TS_ASSERT(!and_op->isNull());
     TS_ASSERT(!plus_op->isNull());
     TS_ASSERT(!d_apply_fun_bool->isNull());
     TS_ASSERT(null->isNull());
@@ -346,8 +347,8 @@ public:
 
     TS_ASSERT(!a_bool->isConst());
     TS_ASSERT(!b_bool->isConst());
-    TS_ASSERT(!c_bool_mult->isConst());
-    TS_ASSERT(mult_op->isConst());
+    TS_ASSERT(!c_bool_and->isConst());
+    TS_ASSERT(and_op->isConst());
     TS_ASSERT(plus_op->isConst());
     TS_ASSERT(!d_apply_fun_bool->isConst());
     TS_ASSERT(!null->isConst());
@@ -359,9 +360,9 @@ public:
 
     TS_ASSERT_THROWS(a_bool->getConst<Kind>(), IllegalArgumentException);
     TS_ASSERT_THROWS(b_bool->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(c_bool_mult->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT(mult_op->getConst<Kind>() == MULT);
-    TS_ASSERT_THROWS(mult_op->getConst<Integer>(), IllegalArgumentException);
+    TS_ASSERT_THROWS(c_bool_and->getConst<Kind>(), IllegalArgumentException);
+    TS_ASSERT(and_op->getConst<Kind>() == AND);
+    TS_ASSERT_THROWS(and_op->getConst<Integer>(), IllegalArgumentException);
     TS_ASSERT(plus_op->getConst<Kind>() == PLUS);
     TS_ASSERT_THROWS(plus_op->getConst<Rational>(), IllegalArgumentException);
     TS_ASSERT_THROWS(d_apply_fun_bool->getConst<Kind>(), IllegalArgumentException);
@@ -383,8 +384,8 @@ public:
 
     TS_ASSERT(a_bool->getExprManager() == d_em);
     TS_ASSERT(b_bool->getExprManager() == d_em);
-    TS_ASSERT(c_bool_mult->getExprManager() == d_em);
-    TS_ASSERT(mult_op->getExprManager() == d_em);
+    TS_ASSERT(c_bool_and->getExprManager() == d_em);
+    TS_ASSERT(and_op->getExprManager() == d_em);
     TS_ASSERT(plus_op->getExprManager() == d_em);
     TS_ASSERT(d_apply_fun_bool->getExprManager() == d_em);
     TS_ASSERT(null->getExprManager() == NULL);
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index c79832583..f1bb7c251 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -40,6 +40,7 @@ private:
   NodeManager* d_nodeManager;
   NodeManagerScope* d_scope;
   TypeNode *d_booleanType;
+  TypeNode *d_realType;
 
 public:
 
@@ -48,6 +49,7 @@ public:
     d_nodeManager = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nodeManager);
     d_booleanType = new TypeNode(d_nodeManager->booleanType());
+    d_realType = new TypeNode(d_nodeManager->realType());
   }
 
   void tearDown() {
@@ -265,8 +267,9 @@ public:
   void testEqNode() {
     /* Node eqNode(const Node& right) const; */
 
-    Node left = d_nodeManager->mkConst(true);
-    Node right = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false));
+    TypeNode t = d_nodeManager->mkSort();
+    Node left = d_nodeManager->mkVar(t);
+    Node right = d_nodeManager->mkVar(t);
     Node eq = left.eqNode(right);
 
     TS_ASSERT(EQUAL == eq.getKind());
@@ -326,7 +329,7 @@ public:
     Node a = d_nodeManager->mkVar(*d_booleanType);
     Node b = d_nodeManager->mkVar(*d_booleanType);
 
-    Node cnd = d_nodeManager->mkNode(PLUS, a, b);
+    Node cnd = d_nodeManager->mkNode(OR, a, b);
     Node thenBranch = d_nodeManager->mkConst(true);
     Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false));
     Node ite = cnd.iteNode(thenBranch, elseBranch);
@@ -395,10 +398,13 @@ public:
     n = d_nodeManager->mkNode(IFF, a, b);
     TS_ASSERT(IFF == n.getKind());
 
-    n = d_nodeManager->mkNode(PLUS, a, b);
+    Node x = d_nodeManager->mkVar(*d_realType);
+    Node y = d_nodeManager->mkVar(*d_realType);
+
+    n = d_nodeManager->mkNode(PLUS, x, y);
     TS_ASSERT(PLUS == n.getKind());
 
-    n = d_nodeManager->mkNode(UMINUS, a);
+    n = d_nodeManager->mkNode(UMINUS, x);
     TS_ASSERT(UMINUS == n.getKind());
   }
 
@@ -408,7 +414,7 @@ public:
     TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
 
     Node f = d_nodeManager->mkVar(predType);
-    Node a = d_nodeManager->mkVar(booleanType);
+    Node a = d_nodeManager->mkVar(sort);
     Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a);
 
     TS_ASSERT( fa.hasOperator() );
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 7f315f092..e3883b824 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -29,6 +29,7 @@
 #include "expr/kind.h"
 #include "context/context.h"
 #include "util/Assert.h"
+#include "util/rational.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -42,6 +43,7 @@ private:
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
   TypeNode* d_booleanType;
+  TypeNode* d_realType;
 
 public:
 
@@ -52,6 +54,7 @@ public:
 
     specKind = PLUS;
     d_booleanType = new TypeNode(d_nm->booleanType());
+    d_realType = new TypeNode(d_nm->realType());
   }
 
   void tearDown() {
@@ -484,7 +487,13 @@ public:
     Node m = d_nm->mkNode(AND, y, z, x);
     Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z);
     Node o = d_nm->mkNode(XOR, y, x);
-    Node p = d_nm->mkNode(PLUS, z, d_nm->mkNode(UMINUS, x), z);
+
+    Node r = d_nm->mkVar(*d_realType);
+    Node s = d_nm->mkVar(*d_realType);
+    Node t = d_nm->mkVar(*d_realType);
+
+    Node p = d_nm->mkNode(EQUAL, d_nm->mkConst<Rational>(0),
+                          d_nm->mkNode(PLUS, r, d_nm->mkNode(UMINUS, s), t));
     Node q = d_nm->mkNode(AND, x, z, d_nm->mkNode(NOT, y));
 
 #ifdef CVC4_ASSERTIONS
@@ -606,43 +615,45 @@ public:
 
   void testConvenienceBuilders() {
     Node a = d_nm->mkVar(*d_booleanType);
+
     Node b = d_nm->mkVar(*d_booleanType);
     Node c = d_nm->mkVar(*d_booleanType);
-    Node d = d_nm->mkVar(*d_booleanType);
-    Node e = d_nm->mkVar(*d_booleanType);
-    Node f = d_nm->mkVar(*d_booleanType);
+
+    Node d = d_nm->mkVar(*d_realType);
+    Node e = d_nm->mkVar(*d_realType);
+    Node f = d_nm->mkVar(*d_realType);
 
     Node m = a && b;
-    Node n = (a && b) || c;
-    Node o = d + e - b;
-    Node p = (a && o) || c;
+    TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b));
 
-    Node x = d + e + o - m;
-    Node y = f - a - c + e;
+    Node n = (a && b) || c;
+    TS_ASSERT_EQUALS(n, d_nm->mkNode(OR, m, c));
 
-    Node q = a && b && c;
+    Node p = (a && m) || n;
+    TS_ASSERT_EQUALS(p, d_nm->mkNode(OR, d_nm->mkNode(AND, a, m), n));
 
-    Node r = (e && d && b && a) || (x && y) || f || (q && a);
+    Node w = d + e - f;
+    TS_ASSERT_EQUALS(w, d_nm->mkNode(PLUS, d, e, d_nm->mkNode(UMINUS, f)));
 
-    TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b));
-    TS_ASSERT_EQUALS(n, d_nm->mkNode(OR, m, c));
-    TS_ASSERT_EQUALS(o, d_nm->mkNode(PLUS, d, e, d_nm->mkNode(UMINUS, b)));
-    TS_ASSERT_EQUALS(p, d_nm->mkNode(OR, d_nm->mkNode(AND, a, o), c));
+    Node x = d + e + w - f;
+    TS_ASSERT_EQUALS(x, d_nm->mkNode(PLUS, d, e, w, d_nm->mkNode(UMINUS, f)));
 
-    TS_ASSERT_EQUALS(x, d_nm->mkNode(PLUS, d, e, o, d_nm->mkNode(UMINUS, m)));
+    Node y = f - x - e + w;
     TS_ASSERT_EQUALS(y, d_nm->mkNode(PLUS,
                                      f,
-                                     d_nm->mkNode(UMINUS, a),
-                                     d_nm->mkNode(UMINUS, c),
-                                     e));
+                                     d_nm->mkNode(UMINUS, x),
+                                     d_nm->mkNode(UMINUS, e),
+                                     w));
 
+    Node q = a && b && c;
     TS_ASSERT_EQUALS(q, d_nm->mkNode(AND, a, b, c));
 
+    Node r = (c && b && a) || (m && n) || p || (a && p);
     TS_ASSERT_EQUALS(r, d_nm->mkNode(OR,
-                                     d_nm->mkNode(AND, e, d, b, a),
-                                     d_nm->mkNode(AND, x, y),
-                                     f,
-                                     d_nm->mkNode(AND, q, a)));
+                                     d_nm->mkNode(AND, c, b, a),
+                                     d_nm->mkNode(AND, m, n),
+                                     p,
+                                     d_nm->mkNode(AND, a, p)));
 
     TS_ASSERT_EQUALS(Node((a && b) && c), d_nm->mkNode(AND, a, b, c));
     TS_ASSERT_EQUALS(Node(a && (b && c)), d_nm->mkNode(AND, a, d_nm->mkNode(AND, b, c)));
@@ -653,28 +664,28 @@ public:
     TS_ASSERT_EQUALS(Node((a || b) && c), d_nm->mkNode(AND, d_nm->mkNode(OR, a, b), c));
     TS_ASSERT_EQUALS(Node(a || (b && c)), d_nm->mkNode(OR, a, d_nm->mkNode(AND, b, c)));
 
-    TS_ASSERT_EQUALS(Node((a + b) + c), d_nm->mkNode(PLUS, a, b, c));
-    TS_ASSERT_EQUALS(Node(a + (b + c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(PLUS, b, c)));
-    TS_ASSERT_EQUALS(Node((a - b) - c), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, b), d_nm->mkNode(UMINUS, c)));
-    TS_ASSERT_EQUALS(Node(a - (b - c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, b, d_nm->mkNode(UMINUS, c)))));
-    TS_ASSERT_EQUALS(Node((a * b) * c), d_nm->mkNode(MULT, a, b, c));
-    TS_ASSERT_EQUALS(Node(a * (b * c)), d_nm->mkNode(MULT, a, d_nm->mkNode(MULT, b, c)));
-    TS_ASSERT_EQUALS(Node((a + b) - c), d_nm->mkNode(PLUS, a, b, d_nm->mkNode(UMINUS, c)));
-    TS_ASSERT_EQUALS(Node(a + (b - c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(PLUS, b, d_nm->mkNode(UMINUS, c))));
-    TS_ASSERT_EQUALS(Node((a - b) + c), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, b), c));
-    TS_ASSERT_EQUALS(Node(a - (b + c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, b, c))));
-    TS_ASSERT_EQUALS(Node((a + b) * c), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, a, b), c));
-    TS_ASSERT_EQUALS(Node(a + (b * c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(MULT, b, c)));
-    TS_ASSERT_EQUALS(Node((a - b) * c), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, b)), c));
-    TS_ASSERT_EQUALS(Node(a - (b * c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, d_nm->mkNode(MULT, b, c))));
-    TS_ASSERT_EQUALS(Node((a * b) + c), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, a, b), c));
-    TS_ASSERT_EQUALS(Node(a * (b + c)), d_nm->mkNode(MULT, a, d_nm->mkNode(PLUS, b, c)));
-    TS_ASSERT_EQUALS(Node((a * b) - c), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, a, b), d_nm->mkNode(UMINUS, c)));
-    TS_ASSERT_EQUALS(Node(a * (b - c)), d_nm->mkNode(MULT, a, d_nm->mkNode(PLUS, b, d_nm->mkNode(UMINUS, c))));
-
-    TS_ASSERT_EQUALS(Node(-a), d_nm->mkNode(UMINUS, a));
-    TS_ASSERT_EQUALS(Node(- a - b), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, a), d_nm->mkNode(UMINUS, b)));
-    TS_ASSERT_EQUALS(Node(- a + b), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, a), b));
-    TS_ASSERT_EQUALS(Node(- a * b), d_nm->mkNode(MULT, d_nm->mkNode(UMINUS, a), b));
+    TS_ASSERT_EQUALS(Node((d + e) + f), d_nm->mkNode(PLUS, d, e, f));
+    TS_ASSERT_EQUALS(Node(d + (e + f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(PLUS, e, f)));
+    TS_ASSERT_EQUALS(Node((d - e) - f), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, e), d_nm->mkNode(UMINUS, f)));
+    TS_ASSERT_EQUALS(Node(d - (e - f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, e, d_nm->mkNode(UMINUS, f)))));
+    TS_ASSERT_EQUALS(Node((d * e) * f), d_nm->mkNode(MULT, d, e, f));
+    TS_ASSERT_EQUALS(Node(d * (e * f)), d_nm->mkNode(MULT, d, d_nm->mkNode(MULT, e, f)));
+    TS_ASSERT_EQUALS(Node((d + e) - f), d_nm->mkNode(PLUS, d, e, d_nm->mkNode(UMINUS, f)));
+    TS_ASSERT_EQUALS(Node(d + (e - f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(PLUS, e, d_nm->mkNode(UMINUS, f))));
+    TS_ASSERT_EQUALS(Node((d - e) + f), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, e), f));
+    TS_ASSERT_EQUALS(Node(d - (e + f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, e, f))));
+    TS_ASSERT_EQUALS(Node((d + e) * f), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, d, e), f));
+    TS_ASSERT_EQUALS(Node(d + (e * f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(MULT, e, f)));
+    TS_ASSERT_EQUALS(Node((d - e) * f), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, e)), f));
+    TS_ASSERT_EQUALS(Node(d - (e * f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, d_nm->mkNode(MULT, e, f))));
+    TS_ASSERT_EQUALS(Node((d * e) + f), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, d, e), f));
+    TS_ASSERT_EQUALS(Node(d * (e + f)), d_nm->mkNode(MULT, d, d_nm->mkNode(PLUS, e, f)));
+    TS_ASSERT_EQUALS(Node((d * e) - f), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, d, e), d_nm->mkNode(UMINUS, f)));
+    TS_ASSERT_EQUALS(Node(d * (e - f)), d_nm->mkNode(MULT, d, d_nm->mkNode(PLUS, e, d_nm->mkNode(UMINUS, f))));
+
+    TS_ASSERT_EQUALS(Node(-d), d_nm->mkNode(UMINUS, d));
+    TS_ASSERT_EQUALS(Node(- d - e), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, d), d_nm->mkNode(UMINUS, e)));
+    TS_ASSERT_EQUALS(Node(- d + e), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, d), e));
+    TS_ASSERT_EQUALS(Node(- d * e), d_nm->mkNode(MULT, d_nm->mkNode(UMINUS, d), e));
   }
 };
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 1f986732c..0e0835327 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -191,7 +191,7 @@ public:
     tryGoodInput("CHECKSAT FALSE;");
     tryGoodInput("a, b : BOOLEAN;");
     tryGoodInput("a, b : BOOLEAN; QUERY (a => b) AND a => b;");
-    tryGoodInput("T, U : TYPE; f : T -> U; x : T; CHECKSAT f(x) = x;");
+    tryGoodInput("T, U : TYPE; f : T -> U; x : T; y : U; CHECKSAT f(x) = y;");
     tryGoodInput("T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;");
     tryGoodInput("%% nothing but a comment");
     tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment");
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 570fa74a4..8132cc262 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -261,10 +261,12 @@ public:
   }
 
   void testRewriterComplicated() {
+    try {
     Node x = d_nm->mkVar("x", d_nm->integerType());
     Node y = d_nm->mkVar("y", d_nm->realType());
-    Node z1 = d_nm->mkVar("z1", d_nm->mkSort("U"));
-    Node z2 = d_nm->mkVar("z2", d_nm->mkSort("U"));
+    TypeNode u = d_nm->mkSort("U");
+    Node z1 = d_nm->mkVar("z1", u);
+    Node z2 = d_nm->mkVar("z2", u);
     Node f = d_nm->mkVar("f", d_nm->mkFunctionType(d_nm->integerType(),
                                                    d_nm->integerType()));
     Node g = d_nm->mkVar("g", d_nm->mkFunctionType(d_nm->realType(),
@@ -279,10 +281,8 @@ public:
     Node gy = d_nm->mkNode(APPLY_UF, g, y);
     Node z1eqz2 = d_nm->mkNode(EQUAL, z1, z2);
     Node f1eqf2 = d_nm->mkNode(EQUAL, f1, f2);
-    Node ffxeqgy = d_nm->mkNode(EQUAL,
-                                ffx,
-                                gy);
-    Node and1 = d_nm->mkNode(AND, ffxeqgy, z1eqz2, ffx);
+    Node ffxeqgy = d_nm->mkNode(EQUAL, ffx, gy);
+    Node and1 = d_nm->mkNode(AND, ffxeqgy, z1eqz2);
     Node ffxeqf1 = d_nm->mkNode(EQUAL, ffx, f1);
     Node or1 = d_nm->mkNode(OR, and1, ffxeqf1);
     // make the expression:
@@ -350,5 +350,9 @@ public:
     TS_ASSERT(FakeTheory::nothingMoreExpected());
 
     TS_ASSERT_EQUALS(nOut, nExpected);
+    } catch( TypeCheckingExceptionPrivate& e ) {
+      cerr << "Type error: " << e.getMessage() << ": " << e.getNode();
+      throw;
+    }
   }
 };
diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h
index 8e72c428f..f273de30f 100644
--- a/test/unit/theory/theory_uf_white.h
+++ b/test/unit/theory/theory_uf_white.h
@@ -74,7 +74,8 @@ public:
   }
 
   void testPushPopSimple() {
-    Node x = d_nm->mkVar(*d_booleanType);
+    TypeNode t = d_nm->mkSort();
+    Node x = d_nm->mkVar(t);
     Node x_eq_x = x.eqNode(x);
 
     d_ctxt->push();