fixes to build structure, util classes, lots of fixes to Node and NodeBuilder. outstanding SEGVs fixed

36 files changed, 240 insertions, 65 deletions

diff --git a/Makefile.builds.in b/Makefile.builds.in
index 00551ea6f..789fb0bae 100644
--- a/Makefile.builds.in
+++ b/Makefile.builds.in
@@ -11,6 +11,8 @@ prefix = @prefix@
 bindir = @bindir@
 libdir = @libdir@
 abs_builddir = @abs_builddir@
+BUILDING_STATIC = @BUILDING_STATIC@
+BUILDING_SHARED = @BUILDING_SHARED@
 
 .PHONY: _default_build_ all
 _default_build_: all
@@ -19,17 +21,27 @@ all:
 	$(mkinstalldirs) "$(CURRENT_BUILD)$(bindir)" "$(CURRENT_BUILD)$(libdir)"
 	$(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "$(abs_builddir)$(libdir)"
 	$(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la "$(abs_builddir)$(libdir)"
+ifeq ($(BUILDING_SHARED),1)
 	thelibdir="$(abs_builddir)$(libdir)"; progdir="$(abs_builddir)$(bindir)"; file=cvc4; \
 		eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \
 		eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"
+endif
+ifeq ($(BUILDING_STATIC),1)
+	install -v $(CURRENT_BUILD)/src/main/cvc4 "$(abs_builddir)$(bindir)"
+endif
 	test -e $(CURRENT_BUILD)/lib || ln -sfv "$(abs_builddir)$(libdir)" $(CURRENT_BUILD)/lib
 	test -e $(CURRENT_BUILD)/bin || ln -sfv "$(abs_builddir)$(bindir)" $(CURRENT_BUILD)/bin
 	mkdir -pv ".$(bindir)" ".$(libdir)"
 	$(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "`pwd`$(libdir)"
 	$(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la "`pwd`$(libdir)"
+ifeq ($(BUILDING_SHARED),1)
 	thelibdir="`pwd`$(libdir)"; progdir="`pwd`$(bindir)"; file=cvc4; \
 		eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \
 		eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"
+endif
+ifeq ($(BUILDING_STATIC),1)
+	install -v $(CURRENT_BUILD)/src/main/cvc4 "`pwd`$(bindir)"
+endif
 	test -e lib || ln -sfv ".$(libdir)" lib
 	test -e bin || ln -sfv ".$(bindir)" bin
 
diff --git a/Makefile.in b/Makefile.in
index 139f43cc0..c67c877a1 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -120,6 +120,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/configure b/configure
index 16c2aa0b9..8e60591d9 100755
--- a/configure
+++ b/configure
@@ -713,6 +713,8 @@ mk_include
 CVC4_PARSER_LIBRARY_VERSION
 CVC4_LIBRARY_VERSION
 CVC4_LIBRARY_RELEASE_CODE
+BUILDING_STATIC
+BUILDING_SHARED
 ANTLR_LDFLAGS
 ANTLR_INCLUDES
 PERL
@@ -5456,13 +5458,13 @@ if test "${lt_cv_nm_interface+set}" = set; then :
 else
   lt_cv_nm_interface="BSD nm"
   echo "int some_variable = 0;" > conftest.$ac_ext
-  (eval echo "\"\$as_me:5459: $ac_compile\"" >&5)
+  (eval echo "\"\$as_me:5461: $ac_compile\"" >&5)
   (eval "$ac_compile" 2>conftest.err)
   cat conftest.err >&5
-  (eval echo "\"\$as_me:5462: $NM \\\"conftest.$ac_objext\\\"\"" >&5)
+  (eval echo "\"\$as_me:5464: $NM \\\"conftest.$ac_objext\\\"\"" >&5)
   (eval "$NM \"conftest.$ac_objext\"" 2>conftest.err > conftest.out)
   cat conftest.err >&5
-  (eval echo "\"\$as_me:5465: output\"" >&5)
+  (eval echo "\"\$as_me:5467: output\"" >&5)
   cat conftest.out >&5
   if $GREP 'External.*some_variable' conftest.out > /dev/null; then
     lt_cv_nm_interface="MS dumpbin"
@@ -6665,7 +6667,7 @@ ia64-*-hpux*)
   ;;
 *-*-irix6*)
   # Find out which ABI we are using.
-  echo '#line 6668 "configure"' > conftest.$ac_ext
+  echo '#line 6670 "configure"' > conftest.$ac_ext
   if { { eval echo "\"\$as_me\":${as_lineno-$LINENO}: \"$ac_compile\""; } >&5
   (eval $ac_compile) 2>&5
   ac_status=$?
@@ -8133,11 +8135,11 @@ else
    -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
    -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
    -e 's:$: $lt_compiler_flag:'`
-   (eval echo "\"\$as_me:8136: $lt_compile\"" >&5)
+   (eval echo "\"\$as_me:8138: $lt_compile\"" >&5)
    (eval "$lt_compile" 2>conftest.err)
    ac_status=$?
    cat conftest.err >&5
-   echo "$as_me:8140: \$? = $ac_status" >&5
+   echo "$as_me:8142: \$? = $ac_status" >&5
    if (exit $ac_status) && test -s "$ac_outfile"; then
      # The compiler can only warn and ignore the option if not recognized
      # So say no if there are warnings other than the usual output.
@@ -8472,11 +8474,11 @@ else
    -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
    -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
    -e 's:$: $lt_compiler_flag:'`
-   (eval echo "\"\$as_me:8475: $lt_compile\"" >&5)
+   (eval echo "\"\$as_me:8477: $lt_compile\"" >&5)
    (eval "$lt_compile" 2>conftest.err)
    ac_status=$?
    cat conftest.err >&5
-   echo "$as_me:8479: \$? = $ac_status" >&5
+   echo "$as_me:8481: \$? = $ac_status" >&5
    if (exit $ac_status) && test -s "$ac_outfile"; then
      # The compiler can only warn and ignore the option if not recognized
      # So say no if there are warnings other than the usual output.
@@ -8577,11 +8579,11 @@ else
    -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
    -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
    -e 's:$: $lt_compiler_flag:'`
-   (eval echo "\"\$as_me:8580: $lt_compile\"" >&5)
+   (eval echo "\"\$as_me:8582: $lt_compile\"" >&5)
    (eval "$lt_compile" 2>out/conftest.err)
    ac_status=$?
    cat out/conftest.err >&5
-   echo "$as_me:8584: \$? = $ac_status" >&5
+   echo "$as_me:8586: \$? = $ac_status" >&5
    if (exit $ac_status) && test -s out/conftest2.$ac_objext
    then
      # The compiler can only warn and ignore the option if not recognized
@@ -8632,11 +8634,11 @@ else
    -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
    -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
    -e 's:$: $lt_compiler_flag:'`
-   (eval echo "\"\$as_me:8635: $lt_compile\"" >&5)
+   (eval echo "\"\$as_me:8637: $lt_compile\"" >&5)
    (eval "$lt_compile" 2>out/conftest.err)
    ac_status=$?
    cat out/conftest.err >&5
-   echo "$as_me:8639: \$? = $ac_status" >&5
+   echo "$as_me:8641: \$? = $ac_status" >&5
    if (exit $ac_status) && test -s out/conftest2.$ac_objext
    then
      # The compiler can only warn and ignore the option if not recognized
@@ -11015,7 +11017,7 @@ else
   lt_dlunknown=0; lt_dlno_uscore=1; lt_dlneed_uscore=2
   lt_status=$lt_dlunknown
   cat > conftest.$ac_ext <<_LT_EOF
-#line 11018 "configure"
+#line 11020 "configure"
 #include "confdefs.h"
 
 #if HAVE_DLFCN_H
@@ -11111,7 +11113,7 @@ else
   lt_dlunknown=0; lt_dlno_uscore=1; lt_dlneed_uscore=2
   lt_status=$lt_dlunknown
   cat > conftest.$ac_ext <<_LT_EOF
-#line 11114 "configure"
+#line 11116 "configure"
 #include "confdefs.h"
 
 #if HAVE_DLFCN_H
@@ -14666,11 +14668,11 @@ else
    -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
    -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
    -e 's:$: $lt_compiler_flag:'`
-   (eval echo "\"\$as_me:14669: $lt_compile\"" >&5)
+   (eval echo "\"\$as_me:14671: $lt_compile\"" >&5)
    (eval "$lt_compile" 2>conftest.err)
    ac_status=$?
    cat conftest.err >&5
-   echo "$as_me:14673: \$? = $ac_status" >&5
+   echo "$as_me:14675: \$? = $ac_status" >&5
    if (exit $ac_status) && test -s "$ac_outfile"; then
      # The compiler can only warn and ignore the option if not recognized
      # So say no if there are warnings other than the usual output.
@@ -14765,11 +14767,11 @@ else
    -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
    -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
    -e 's:$: $lt_compiler_flag:'`
-   (eval echo "\"\$as_me:14768: $lt_compile\"" >&5)
+   (eval echo "\"\$as_me:14770: $lt_compile\"" >&5)
    (eval "$lt_compile" 2>out/conftest.err)
    ac_status=$?
    cat out/conftest.err >&5
-   echo "$as_me:14772: \$? = $ac_status" >&5
+   echo "$as_me:14774: \$? = $ac_status" >&5
    if (exit $ac_status) && test -s out/conftest2.$ac_objext
    then
      # The compiler can only warn and ignore the option if not recognized
@@ -14817,11 +14819,11 @@ else
    -e 's:.*FLAGS}\{0,1\} :&$lt_compiler_flag :; t' \
    -e 's: [^ ]*conftest\.: $lt_compiler_flag&:; t' \
    -e 's:$: $lt_compiler_flag:'`
-   (eval echo "\"\$as_me:14820: $lt_compile\"" >&5)
+   (eval echo "\"\$as_me:14822: $lt_compile\"" >&5)
    (eval "$lt_compile" 2>out/conftest.err)
    ac_status=$?
    cat out/conftest.err >&5
-   echo "$as_me:14824: \$? = $ac_status" >&5
+   echo "$as_me:14826: \$? = $ac_status" >&5
    if (exit $ac_status) && test -s out/conftest2.$ac_objext
    then
      # The compiler can only warn and ignore the option if not recognized
@@ -16444,6 +16446,11 @@ fi
 
 # Prepare configure output
 
+if test "$enable_shared" = yes; then BUILDING_SHARED=1; fi
+if test "$enable_static" = yes; then BUILDING_STATIC=1; fi
+
+
+
 
 
 
diff --git a/configure.ac b/configure.ac
index 80fc73fdd..2937f62d7 100644
--- a/configure.ac
+++ b/configure.ac
@@ -399,6 +399,11 @@ AC_TYPE_SIZE_T
 
 # Prepare configure output
 
+if test "$enable_shared" = yes; then BUILDING_SHARED=1; fi
+if test "$enable_static" = yes; then BUILDING_STATIC=1; fi
+AC_SUBST(BUILDING_SHARED)
+AC_SUBST(BUILDING_STATIC)
+
 AC_SUBST(CVC4_LIBRARY_RELEASE_CODE)
 AC_SUBST(CVC4_LIBRARY_VERSION)
 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
diff --git a/contrib/Makefile.in b/contrib/Makefile.in
index a86658b70..8df42980b 100644
--- a/contrib/Makefile.in
+++ b/contrib/Makefile.in
@@ -63,6 +63,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/doc/Makefile.in b/doc/Makefile.in
index 99ff59b1c..745314a39 100644
--- a/doc/Makefile.in
+++ b/doc/Makefile.in
@@ -63,6 +63,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/src/Makefile.in b/src/Makefile.in
index 9099b92be..08f7c6421 100644
--- a/src/Makefile.in
+++ b/src/Makefile.in
@@ -159,6 +159,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/src/context/Makefile.in b/src/context/Makefile.in
index c4f82d42a..5428ba8b9 100644
--- a/src/context/Makefile.in
+++ b/src/context/Makefile.in
@@ -92,6 +92,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/src/expr/Makefile.in b/src/expr/Makefile.in
index 4892220d8..848d8d72b 100644
--- a/src/expr/Makefile.in
+++ b/src/expr/Makefile.in
@@ -93,6 +93,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/src/expr/node.h b/src/expr/node.h
index fd2603ffa..b40443923 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -25,6 +25,7 @@
 
 #include "cvc4_config.h"
 #include "expr/kind.h"
+#include "util/Assert.h"
 
 namespace CVC4 {
   class Node;
@@ -105,6 +106,11 @@ public:
   bool operator==(const Node& e) const { return d_ev == e.d_ev; }
   bool operator!=(const Node& e) const { return d_ev != e.d_ev; }
 
+  Node operator[](int i) const {
+    Assert(i >= 0 && i < d_ev->d_nchildren);
+    return Node(d_ev->d_children[i]);
+  }
+
   /**
    * We compare by expression ids so, keeping things deterministic and having
    * that subexpressions have to be smaller than the enclosing expressions.
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 1dee91735..747854d23 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -168,6 +168,7 @@ public:
 
   NodeBuilder& append(const Node& n) {
     Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    Debug("prop") << "append: " << this << " " << n << "[" << n.d_ev << "]" << std::endl;
     allocateEvIfNecessaryForAppend();
     NodeValue* ev = n.d_ev;
     d_hash = NodeValue::computeHash(d_hash, ev);
@@ -364,7 +365,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder() :
   d_used(false),
   d_ev(&d_inlineEv),
   d_inlineEv(0),
-  d_childrenStorage(0) {}
+  d_childrenStorage() {}
 
 template <unsigned nchild_thresh>
 inline NodeBuilder<nchild_thresh>::NodeBuilder(Kind k) :
@@ -373,9 +374,9 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(Kind k) :
   d_used(false),
   d_ev(&d_inlineEv),
   d_inlineEv(0),
-  d_childrenStorage(0) {
+  d_childrenStorage() {
 
-  Message() << "kind " << k << std::endl;
+  //Message() << "kind " << k << std::endl;
   d_inlineEv.d_kind = k;
 }
 
@@ -386,13 +387,13 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<nchild_thresh>&
   d_used(nb.d_used),
   d_ev(&d_inlineEv),
   d_inlineEv(0),
-  d_childrenStorage(0) {
+  d_childrenStorage() {
 
   if(evIsAllocated(nb)) {
     realloc(nb->d_size, false);
-    std::copy(d_ev->begin(), nb.d_ev->begin(), nb.d_ev->end());
+    std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_ev->begin());
   } else {
-    std::copy(d_inlineEv.begin(), nb.d_ev->begin(), nb.d_ev->end());
+    std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_inlineEv.begin());
   }
 }
 
@@ -404,13 +405,13 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<N>& nb) :
   d_used(nb.d_used),
   d_ev(&d_inlineEv),
   d_inlineEv(0),
-  d_childrenStorage(0) {
+  d_childrenStorage() {
 
   if(nb.d_ev->d_nchildren > nchild_thresh) {
     realloc(nb.d_size, false);
-    std::copy(d_ev->begin(), nb.d_ev->begin(), nb.d_ev->end());
+    std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_ev->begin());
   } else {
-    std::copy(d_inlineEv.begin(), nb.d_ev->begin(), nb.d_ev->end());
+    std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_inlineEv.begin());
   }
 }
 
@@ -421,7 +422,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm) :
   d_used(false),
   d_ev(&d_inlineEv),
   d_inlineEv(0),
-  d_childrenStorage(0) {}
+  d_childrenStorage() {}
 
 template <unsigned nchild_thresh>
 inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) :
@@ -432,7 +433,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) :
   d_inlineEv(0),
   d_childrenStorage() {
 
-  Message() << "kind " << k << std::endl;
+  //Message() << "kind " << k << std::endl;
   d_inlineEv.d_kind = k;
 }
 
@@ -466,9 +467,9 @@ void NodeBuilder<nchild_thresh>::realloc() {
     d_ev->d_rc = 0;
     d_ev->d_kind = d_inlineEv.d_kind;
     d_ev->d_nchildren = nchild_thresh;
-    std::copy(d_ev->d_children,
-              d_inlineEv.d_children,
-              d_inlineEv.d_children + nchild_thresh);
+    std::copy(d_inlineEv.d_children,
+              d_inlineEv.d_children + nchild_thresh,
+              d_ev->d_children);
   }
 }
 
@@ -489,9 +490,9 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) {
     d_ev->d_kind = d_inlineEv.d_kind;
     d_ev->d_nchildren = nchild_thresh;
     if(copy) {
-      std::copy(d_ev->d_children,
-                d_inlineEv.d_children,
-                d_inlineEv.d_children + nchild_thresh);
+      std::copy(d_inlineEv.d_children,
+                d_inlineEv.d_children + nchild_thresh,
+                d_ev->d_children);
     }
   }
 }
@@ -502,6 +503,21 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
   Assert(d_ev->d_kind != UNDEFINED_KIND,
          "Can't make an expression of an undefined kind!");
 
+  if(d_ev->d_kind == VARIABLE) {
+    Assert(d_ev->d_nchildren == 0);
+    NodeValue *ev = (NodeValue*)
+      std::malloc(sizeof(NodeValue) +
+                  ( sizeof(NodeValue*) * d_inlineEv.d_nchildren ));
+    ev->d_nchildren = 0;
+    ev->d_kind = VARIABLE;
+    ev->d_id = NodeValue::next_id++;// FIXME multithreading
+    ev->d_rc = 0;
+    d_used = true;
+    d_ev = NULL;
+    Debug("prop") << "result: " << Node(ev) << std::endl;
+    return Node(ev);
+  }
+
   // implementation differs depending on whether the expression value
   // was malloc'ed or not
 
@@ -510,6 +526,7 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
     if(ev != NULL) {
       // expression already exists in node manager
       d_used = true;
+      Debug("prop") << "result: " << Node(ev) << std::endl;
       return Node(ev);
     }
 
@@ -520,30 +537,41 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
     // this inserts into the NodeManager;
     // return the result of lookup() in case another thread beat us to it
     d_used = true;
-    return d_nm->lookup(d_hash, ev);
+    Node n = d_nm->lookup(d_hash, ev);
+    Debug("prop") << "result: " << n << std::endl;
+    return n;
   }
 
   NodeValue *ev = d_nm->lookupNoInsert(d_hash, &d_inlineEv);
   if(ev != NULL) {
     // expression already exists in node manager
     d_used = true;
+    Debug("prop") << "result: " << Node(ev) << std::endl;
     return Node(ev);
   }
 
   // otherwise create the canonical expression value for this node
   ev = (NodeValue*)
     std::malloc(sizeof(NodeValue) +
-                ( sizeof(NodeValue*) * d_inlineEv.d_nchildren) );
-  ev->d_nchildren = d_ev->d_nchildren;
-  ev->d_kind = d_ev->d_kind;
+                ( sizeof(NodeValue*) * d_inlineEv.d_nchildren ));
+  ev->d_nchildren = d_inlineEv.d_nchildren;
+  ev->d_kind = d_inlineEv.d_kind;
   ev->d_id = NodeValue::next_id++;// FIXME multithreading
   ev->d_rc = 0;
+  std::copy(d_inlineEv.d_children,
+            d_inlineEv.d_children + d_inlineEv.d_nchildren,
+            ev->d_children);
   d_used = true;
   d_ev = NULL;
 
   // this inserts into the NodeManager;
   // return the result of lookup() in case another thread beat us to it
-  return d_nm->lookup(d_hash, ev);
+  if(ev->numChildren()) {
+    Debug("prop") << "ev first child: " << *ev->ev_begin() << std::endl;
+  }
+  Node n = d_nm->lookup(d_hash, ev);
+  Debug("prop") << "result: " << n << std::endl;
+  return n;
 }
 
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index eba8c4d18..a307eb11f 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -58,6 +58,7 @@ Node NodeManager::lookup(uint64_t hash, NodeValue* ev) {
 
       return *j;
     }
+
     // didn't find it, insert
     std::vector<Node> v;
     Node e(ev);
@@ -99,6 +100,7 @@ NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) {
 
       return j->d_ev;
     }
+
     // didn't find it, don't insert
     return 0;
   }
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 954fe0aaa..985ad15a7 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -177,7 +177,7 @@ namespace CVC4 {
 namespace expr {
 
 inline Node NodeValue::node_iterator::operator*() {
-  return Node((NodeValue*) d_i);
+  return Node(*d_i);
 }
 
 }/* CVC4::expr namespace */
diff --git a/src/main/Makefile.in b/src/main/Makefile.in
index 8e2c49989..6a2677109 100644
--- a/src/main/Makefile.in
+++ b/src/main/Makefile.in
@@ -94,6 +94,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 81cbc2df8..123bc3204 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -110,7 +110,8 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
       }
 
       if(strcmp(optarg, "help")) {
-        throw OptionException(string("unknown language for --lang: `") + argv[optind] + "'.  Try --lang help.");
+        throw OptionException(string("unknown language for --lang: `") +
+                              optarg + "'.  Try --lang help.");
       }
 
       fputs(lang_help, stdout);
@@ -132,13 +133,13 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
       break;
 
     case '?':
-      throw OptionException(string("can't understand option: `") + argv[optind] + "'");
+      throw OptionException(string("can't understand option"));// + argv[optind - 1] + "'");
 
     case ':':
-      throw OptionException(string("option `") + argv[optind] + "' missing its required argument");
+      throw OptionException(string("option missing its required argument"));// + argv[optind - 1] + "' missing its required argument");
 
     default:
-      throw OptionException(string("can't understand option: `") + argv[optind] + "'");
+      throw OptionException(string("can't understand option"));//: `") + argv[optind - 1] + "'");
     }
 
   }
diff --git a/src/parser/Makefile.in b/src/parser/Makefile.in
index 31ae05da5..b6c6ae102 100644
--- a/src/parser/Makefile.in
+++ b/src/parser/Makefile.in
@@ -163,6 +163,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/src/parser/cvc/Makefile.in b/src/parser/cvc/Makefile.in
index 28b80800e..e63b15e26 100644
--- a/src/parser/cvc/Makefile.in
+++ b/src/parser/cvc/Makefile.in
@@ -96,6 +96,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/src/parser/smt/Makefile.in b/src/parser/smt/Makefile.in
index 6145b4c4e..a65d62c88 100644
--- a/src/parser/smt/Makefile.in
+++ b/src/parser/smt/Makefile.in
@@ -96,6 +96,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/src/prop/Makefile.in b/src/prop/Makefile.in
index c6538df38..e5ac92c61 100644
--- a/src/prop/Makefile.in
+++ b/src/prop/Makefile.in
@@ -130,6 +130,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/src/prop/minisat/Makefile.in b/src/prop/minisat/Makefile.in
index 1dbc8da9f..278d68790 100644
--- a/src/prop/minisat/Makefile.in
+++ b/src/prop/minisat/Makefile.in
@@ -92,6 +92,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index ffd335453..afc84a5b4 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -64,7 +64,13 @@ static void doAtom(SimpSolver* minisat, map<Node, Var>* vars, Node e, vec<Lit>*
     c->push(Lit(v->second, true));
     return;
   }
-  Unhandled();
+  if(e.getKind() == OR) {
+    for(Node::iterator i = e.begin(); i != e.end(); ++i) {
+      doAtom(minisat, vars, *i, c);
+    }
+    return;
+  }
+  Unhandled(e.getKind());
 }
 
 static void doClause(SimpSolver* minisat, map<Node, Var>* vars, map<Var, Node>* varsReverse, Node e) {
@@ -72,6 +78,20 @@ static void doClause(SimpSolver* minisat, map<Node, Var>* vars, map<Var, Node>*
   Debug("prop") << "  " << e << endl;
   if(e.getKind() == VARIABLE || e.getKind() == NOT) {
     doAtom(minisat, vars, e, &c);
+  } else if(e.getKind() == FALSE) {
+    // inconsistency
+    Notice() << "adding FALSE clause" << endl;
+    Var v = minisat->newVar();
+    c.push(Lit(v, true));
+    minisat->addClause(c);
+    Notice() << "added unit clause " << v << " [[ " << (*varsReverse)[v] << " ]]" << endl;
+    c.clear();
+    c.push(Lit(v, false));
+    minisat->addClause(c);
+    Notice() << "added unit clause -" << v << " [[ -" << (*varsReverse)[v] << " ]]" << endl;
+  } else if(e.getKind() == TRUE) {
+    Notice() << "adding TRUE clause (do nothing)" << endl;
+    // do nothing
   } else {
     Assert(e.getKind() == OR);
     for(Node::iterator i = e.begin(); i != e.end(); ++i) {
@@ -101,7 +121,7 @@ void PropEngine::solve(Node e) {
   d_sat.verbosity = 1;
   bool result = d_sat.solve();
 
-  Notice() << "result is " << (result ? "sat" : "unsat") << endl;
+  Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
   if(result) {
     Notice() << "model:" << endl;
     for(int i = 0; i < d_sat.model.size(); ++i)
diff --git a/src/smt/Makefile.in b/src/smt/Makefile.in
index 35126e382..aa00d5e25 100644
--- a/src/smt/Makefile.in
+++ b/src/smt/Makefile.in
@@ -92,6 +92,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4c7f6a156..018936f7c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -15,37 +15,55 @@
 #include "smt/smt_engine.h"
 #include "util/exception.h"
 #include "util/command.h"
+#include "util/output.h"
+#include "expr/node_builder.h"
 
 namespace CVC4 {
 
 SmtEngine::SmtEngine(ExprManager* em, Options* opts) throw() :
-    d_public_em(em),
-    d_em(em->getNodeManager()),
-    d_opts(opts),
-    d_de(),
-    d_te(),
-    d_prop(d_de, d_te) {
-  }
+  d_assertions(),
+  d_public_em(em),
+  d_nm(em->getNodeManager()),
+  d_opts(opts),
+  d_de(),
+  d_te(),
+  d_prop(d_de, d_te) {
+}
 
 SmtEngine::~SmtEngine() {
 
 }
 
 void SmtEngine::doCommand(Command* c) {
+  NodeManagerScope nms(d_nm);
   c->invoke(this);
 }
 
 Node SmtEngine::preprocess(const Node& e) {
+  if(e.getKind() == NOT) {
+    if(e[0].getKind() == TRUE) {
+      return d_nm->mkNode(FALSE);
+    } else if(e[0].getKind() == FALSE) {
+      return d_nm->mkNode(TRUE);
+    } else if(e[0].getKind() == NOT) {
+      return preprocess(e[0][0]);
+    }
+  }
   return e;
 }
 
 Node SmtEngine::processAssertionList() {
-  Node asserts;
+  if(d_assertions.size() == 1) {
+    return d_assertions[0];
+  }
+
+  NodeBuilder<> asserts(AND);
   for(std::vector<Node>::iterator i = d_assertions.begin();
       i != d_assertions.end();
       ++i) {
-    asserts = asserts.isNull() ? *i : d_em->mkNode(AND, asserts, *i);
+    asserts << *i;
   }
+
   return asserts;
 }
 
@@ -61,25 +79,34 @@ Result SmtEngine::quickCheck() {
 }
 
 void SmtEngine::addFormula(const Node& e) {
+  Debug("smt") << "push_back assertion " << e << std::endl;
   d_assertions.push_back(e);
 }
 
 Result SmtEngine::checkSat(const BoolExpr& e) {
+  NodeManagerScope nms(d_nm);
   Node node_e = preprocess(e.getNode());
   addFormula(node_e);
   return check();
 }
 
 Result SmtEngine::query(const BoolExpr& e) {
-  Node node_e = preprocess(e.getNode());
+  NodeManagerScope nms(d_nm);
+  Node node_e = preprocess(d_nm->mkNode(NOT, e.getNode()));
   addFormula(node_e);
   return check();
 }
 
 Result SmtEngine::assertFormula(const BoolExpr& e) {
+  NodeManagerScope nms(d_nm);
   Node node_e = preprocess(e.getNode());
   addFormula(node_e);
   return quickCheck();
 }
 
+Expr SmtEngine::simplify(const Expr& e) {
+  Expr simplify(const Expr& e);
+  Unimplemented();
+}
+
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 98cffb6de..027d3d603 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -118,7 +118,7 @@ private:
   ExprManager *d_public_em;
 
   /** Out internal expression/node manager */
-  NodeManager *d_em;
+  NodeManager *d_nm;
 
   /** User-level options */
   Options *d_opts;
diff --git a/src/theory/Makefile.in b/src/theory/Makefile.in
index dafd68b6c..379d1171b 100644
--- a/src/theory/Makefile.in
+++ b/src/theory/Makefile.in
@@ -130,6 +130,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/src/theory/uf/Makefile.in b/src/theory/uf/Makefile.in
index 3b3cd6bbb..b1a6081d2 100644
--- a/src/theory/uf/Makefile.in
+++ b/src/theory/uf/Makefile.in
@@ -78,6 +78,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/src/util/Assert.h b/src/util/Assert.h
index 49c97e9b6..d8e881613 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -113,6 +113,28 @@ public:
   }
 };/* class UnhandledCaseException */
 
+class CVC4_PUBLIC UnimplementedOperationException : public AssertionException {
+protected:
+  UnimplementedOperationException() : AssertionException() {}
+
+public:
+  UnimplementedOperationException(const char* function, const char* file,
+                                  unsigned line, const char* fmt, ...) :
+    AssertionException() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Unimplemented code encountered",
+              NULL, function, file, line, fmt, args);
+    va_end(args);
+  }
+
+  UnimplementedOperationException(const char* function, const char* file,
+                                  unsigned line) :
+    AssertionException() {
+    construct("Unimplemented code encountered", NULL, function, file, line);
+  }
+};/* class UnimplementedOperationException */
+
 class CVC4_PUBLIC IllegalArgumentException : public AssertionException {
 protected:
   IllegalArgumentException() : AssertionException() {}
@@ -172,6 +194,8 @@ public:
   throw UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define Unhandled(msg...) \
   throw UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+#define Unimplemented(msg...) \
+  throw UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define IllegalArgument(arg, msg...) \
   throw IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define CheckArgument(cond, arg, msg...)         \
diff --git a/src/util/Makefile.in b/src/util/Makefile.in
index 3ac892aba..686f4cc33 100644
--- a/src/util/Makefile.in
+++ b/src/util/Makefile.in
@@ -93,6 +93,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/src/util/output.h b/src/util/output.h
index 57ce5f3ca..c1e513703 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -55,7 +55,7 @@ public:
   // Yeting option not possible here
 
   std::ostream& operator()(const char* tag) {
-    if(d_tags.find(tag) != d_tags.end())
+    if(d_tags.find(std::string(tag)) != d_tags.end())
       return *d_os;
     else return null_os;
   }
diff --git a/test/Makefile.in b/test/Makefile.in
index c2eabd8a4..6e8fff2a7 100644
--- a/test/Makefile.in
+++ b/test/Makefile.in
@@ -103,6 +103,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am
index bee3e3a85..c5e6ec676 100644
--- a/test/regress/Makefile.am
+++ b/test/regress/Makefile.am
@@ -1,4 +1,4 @@
-TESTS_ENVIRONMENT = @top_builddir@/bin/cvc4
+TESTS_ENVIRONMENT = @top_builddir@/../../bin/cvc4
 TESTS = \
 	simple.cvc \
 	simple.smt \
diff --git a/test/regress/Makefile.in b/test/regress/Makefile.in
index 4ba824928..2670ecd65 100644
--- a/test/regress/Makefile.in
+++ b/test/regress/Makefile.in
@@ -65,6 +65,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
@@ -190,7 +192,7 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-TESTS_ENVIRONMENT = @top_builddir@/bin/cvc4
+TESTS_ENVIRONMENT = @top_builddir@/../../bin/cvc4
 TESTS = \
 	simple.cvc \
 	simple.smt \
diff --git a/test/regress/simple2.smt b/test/regress/simple2.smt
index c8db8c13f..e917d1b64 100644
--- a/test/regress/simple2.smt
+++ b/test/regress/simple2.smt
@@ -5,9 +5,9 @@
 :extrapreds ((x1))
 :extrapreds ((x2))
 :extrapreds ((x3))
-:assumption (or x1 (not x0))
 :formula
-(and (or x0 (not x3))
+(and (or x1 (not x0))
+     (or x0 (not x3))
      (or x3 x2)
      (not x1))
 )
diff --git a/test/system/Makefile.in b/test/system/Makefile.in
index 14e1ac9c7..4b457a954 100644
--- a/test/system/Makefile.in
+++ b/test/system/Makefile.in
@@ -65,6 +65,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index df85ba805..fcaa2cc5d 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -4,6 +4,8 @@ UNIT_TESTS = \
 	expr/node_black \
 	parser/parser_black
 
+TESTS_DEPENDENCIES = $(abs_top_builddir)/src/libcvc4.la $(abs_top_builddir)/src/parser/libcvc4parser.la
+
 # things that aren't tests but that tests rely on and need to
 # go into the distribution
 TEST_DEPS =
diff --git a/test/unit/Makefile.in b/test/unit/Makefile.in
index 4d20d59de..49912b26c 100644
--- a/test/unit/Makefile.in
+++ b/test/unit/Makefile.in
@@ -88,6 +88,8 @@ AUTOCONF = @AUTOCONF@
 AUTOHEADER = @AUTOHEADER@
 AUTOMAKE = @AUTOMAKE@
 AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
 CC = @CC@
 CCDEPMODE = @CCDEPMODE@
 CFLAGS = @CFLAGS@
@@ -220,6 +222,7 @@ UNIT_TESTS = \
 	expr/node_black \
 	parser/parser_black
 
+TESTS_DEPENDENCIES = $(abs_top_builddir)/src/libcvc4.la $(abs_top_builddir)/src/parser/libcvc4parser.la
 
 # things that aren't tests but that tests rely on and need to
 # go into the distribution