* Addressed issues brought up in Chris's review of Morgan's

  NodeManager (bug #65).  Better documentation, etc.

* As part of this, removed NodeManager::mkVar() (which created a
  variable of unknown type).  This requires changes to lots of unit
  tests, which were using this function.

* Performed some review of parser code (my code review #73).

  + I changed the way exceptions were caught and rethrown in
    src/parser/input.cpp.

  + ParserExceptions weren't being properly constructed (d_line and
    d_column weren't intiialized and could contain junk, leading to
    weird error messages).  Fixed.

* Fix to the current working directory used by run_regression script.
  Makes exceptional output easier to match against (in expected error
  output).

* (configure.ac) Ensure that CFLAGS has -fexceptions in it, in case we
  compile any C code and don't use the C++ compiler.

1 files changed, 15 insertions, 12 deletions

diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 2a7b3623e..eec6949f0 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -37,6 +37,7 @@ private:
   Context* d_ctxt;
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
+  Type* d_booleanType;
 
 public:
 
@@ -44,7 +45,9 @@ public:
     d_ctxt = new Context;
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
+
     specKind = PLUS;
+    d_booleanType = d_nm->booleanType();
   }
 
   void tearDown() {
@@ -209,9 +212,9 @@ public:
 
   void testIterator() {
     NodeBuilder<> b;
-    Node x = d_nm->mkVar();
-    Node y = d_nm->mkVar();
-    Node z = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
+    Node y = d_nm->mkVar(d_booleanType);
+    Node z = d_nm->mkVar(d_booleanType);
     b << x << y << z << AND;
 
     {
@@ -460,9 +463,9 @@ public:
   }
 
   void testAppend() {
-    Node x = d_nm->mkVar();
-    Node y = d_nm->mkVar();
-    Node z = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
+    Node y = d_nm->mkVar(d_booleanType);
+    Node z = d_nm->mkVar(d_booleanType);
     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);
@@ -587,12 +590,12 @@ public:
   }
 
   void testConvenienceBuilders() {
-    Node a = d_nm->mkVar();
-    Node b = d_nm->mkVar();
-    Node c = d_nm->mkVar();
-    Node d = d_nm->mkVar();
-    Node e = d_nm->mkVar();
-    Node f = d_nm->mkVar();
+    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 m = a && b;
     Node n = a && b || c;