portfolio merge

80 files changed, 4651 insertions, 605 deletions

diff --git a/.gitignore b/.gitignore
index 2bb76f9dc..e2c448004 100644
--- a/.gitignore
+++ b/.gitignore
@@ -25,3 +25,5 @@ generated/
 /lcov/
 .cvc4_config
 config.reconfig
+*.swp
+/debug/
diff --git a/AUTHORS b/AUTHORS
index f5897d574..db0cf4a9c 100644
--- a/AUTHORS
+++ b/AUTHORS
@@ -1,5 +1,6 @@
 The core authors and designers of CVC4 are:
 
+  Kshitij Bansal <kshitij@cs.nyu.edu>, New York University
   Clark Barrett <barrett@cs.nyu.edu>, New York University
   François Bobot <bobot@lri.fr>, Paris-Sud University
   Christopher Conway <cconway@cs.nyu.edu>, New York University
@@ -27,5 +28,7 @@ CVC4 contains the pkg.m4 autoconf module by Scott James Remnant.
 CVC4 contains the ax_tls.m4 autoconf module by Alan Woodland and
 Diego Elio Petteno.
 
+CVC4 contains the boost.m4 autoconf module by Benoit Sigoure.
+
 CVC4 maintainer versions contain the script autogen.sh, by the
 U.S. Army Research Laboratory
diff --git a/COPYING b/COPYING
index bcb21aa3d..9d9e116fd 100644
--- a/COPYING
+++ b/COPYING
@@ -145,6 +145,32 @@ See config/ax_tls.m4.  Its copyright:
   modified version of the Autoconf Macro, you may extend this special
   exception to the GPL to apply to your modified version as well.
 
+CVC4 incorporates the m4 macro file "boost.m4", excluded from the above
+copyright and downloaded from http://github.com/tsuna/boost.m4 .
+See config/boost.m4.  Its copyright:
+
+  Copyright (C) 2007  Benoit Sigoure <tsuna@lrde.epita.fr>
+
+  This program is free software: you can redistribute it and/or modify
+  it under the terms of the GNU General Public License as published by
+  the Free Software Foundation, either version 3 of the License, or
+  (at your option) any later version.
+
+  This program is distributed in the hope that it will be useful,
+  but WITHOUT ANY WARRANTY; without even the implied warranty of
+  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+  GNU General Public License for more details.
+
+  You should have received a copy of the GNU General Public License
+  along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+  Additional permission under section 7 of the GNU General Public
+  License, version 3 ("GPLv3"):
+
+  If you convey this file as part of a work that contains a
+  configuration script generated by Autoconf, you may do so under
+  terms of your choice.
+
 CVC4 incorporates code from ANTLR3, excluded from the above copyright.
 See http://www.antlr.org/, and the files src/parser/bounded_token_buffer.h,
 src/parser/bounded_token_buffer.cpp, and src/parser/antlr_input_imports.cpp.
diff --git a/Makefile.builds.in b/Makefile.builds.in
index 21d172623..054b4eb7b 100644
--- a/Makefile.builds.in
+++ b/Makefile.builds.in
@@ -30,6 +30,9 @@ bindir = @bindir@
 libdir = @libdir@
 abs_builddir = @abs_builddir@
 distdir = @PACKAGE@-@VERSION@
+AM_DEFAULT_VERBOSITY = @AM_DEFAULT_VERBOSITY@
+SHELL = @SHELL@
+LIBTOOL = $(CURRENT_BUILD)/libtool
 
 # Are we building the libcvc4compat library ?
 CVC4_BUILD_LIBCOMPAT = @CVC4_BUILD_LIBCOMPAT@
@@ -40,21 +43,56 @@ BUILDING_STATIC = @BUILDING_STATIC@
 BUILDING_SHARED = @BUILDING_SHARED@
 STATIC_BINARY = @STATIC_BINARY@
 
+# @
+AM_V_at = $(am__v_at_$(V))
+am__v_at_ = $(am__v_at_$(AM_DEFAULT_VERBOSITY))
+am__v_at_0 = @
+am__v_at_1 =
+# mkinstalldirs (never prefix with @; not a top-level instruction)
+AM_V_mkdir_noat = $(am__v_mkdir_noat_$(V))
+am__v_mkdir_noat_ = $(am__v_mkdir_noat_$(AM_DEFAULT_VERBOSITY))
+am__v_mkdir_noat_0 = $(SHELL) -c 'echo "   MKDIR $$@"; $(mkinstalldirs) "$$@"' bash
+am__v_mkdir_noat_1 = $(mkinstalldirs)
+# mkinstalldirs (can prefix with @)
+AM_V_mkdir = $(am__v_mkdir_$(V))
+am__v_mkdir_ = $(am__v_mkdir_$(AM_DEFAULT_VERBOSITY))
+am__v_mkdir_0 = @$(am__v_mkdir_noat_0)
+am__v_mkdir_1 = $(am__v_mkdir_noat_1)
+# libtool --mode=install install
+AM_V_ltinstall = $(am__v_ltinstall_$(V))
+am__v_ltinstall_ = $(am__v_ltinstall_$(AM_DEFAULT_VERBOSITY))
+am__v_ltinstall_0 = @$(SHELL) -c 'echo "   LTINS $$1"; $(LIBTOOL) --silent --mode=install install "$$@"' bash
+am__v_ltinstall_1 = $(LIBTOOL) --mode=install install
+# install_sh (never prefix with @)
+AM_V_install_sh_noat = $(am__v_install_sh_noat_$(V))
+am__v_install_sh_noat_ = $(am__v_install_sh_noat_$(AM_DEFAULT_VERBOSITY))
+am__v_install_sh_noat_0 = $(SHELL) -c 'echo "   INSTL $$1"; $(install_sh) "$$@"' bash
+am__v_install_sh_noat_1 = $(install_sh)
+# relinking
+AM_V_relink = $(am__v_relink_$(V))
+am__v_relink_ = $(am__v_relink_$(AM_DEFAULT_VERBOSITY))
+am__v_relink_0 = echo "   RELNK"
+am__v_relink_1 = :
+
+# all the binaries that might need to be installed
+# (it's not a fatal error for one/some don't exist in a given build
+# configuration)
+CVC4_BINARIES = cvc4 pcvc4
+
 .PHONY: _default_build_ all
 _default_build_: all
 all:
 #	build the current build profile
-	+(cd $(CURRENT_BUILD) && $(MAKE) $@)
+	$(AM_V_at)(cd $(CURRENT_BUILD) && $(MAKE) $@)
 #	set up builds/$(CURRENT_BUILD)/...prefix.../bin
 #	and builds/$(CURRENT_BUILD)/...prefix.../lib
-	$(mkinstalldirs) "$(CURRENT_BUILD)$(bindir)" "$(CURRENT_BUILD)$(libdir)"
+	$(AM_V_mkdir) "$(CURRENT_BUILD)$(bindir)"
+	$(AM_V_mkdir) "$(CURRENT_BUILD)$(libdir)"
 #	install libcvc4
-	$(CURRENT_BUILD)/libtool --mode=install install -v \
-		$(CURRENT_BUILD)/src/libcvc4.la \
+	$(AM_V_ltinstall) $(CURRENT_BUILD)/src/libcvc4.la \
 		"$(abs_builddir)$(libdir)"
 #	install libcvc4parser
-	$(CURRENT_BUILD)/libtool --mode=install install -v \
-		$(CURRENT_BUILD)/src/parser/libcvc4parser.la \
+	$(AM_V_ltinstall) $(CURRENT_BUILD)/src/parser/libcvc4parser.la \
 		"$(abs_builddir)$(libdir)"
 ifeq ($(CVC4_BUILD_LIBCOMPAT),yes)
 #	install libcvc4compat
@@ -65,35 +103,47 @@ endif
 ifeq ($(BUILDING_SHARED)$(STATIC_BINARY),10)
 #	if we're building shared libs and the binary is not static, relink
 #	the handling with empty $relink_command is a hack for Mac OS
-	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:'`; \
-		if test -z "$$relink_command"; then \
-			$(mkinstalldirs) "$(CURRENT_BUILD)$(bindir)/.libs"; \
-			$(install_sh) \
-				$(CURRENT_BUILD)/src/main/.libs/cvc4 \
-				"$(abs_builddir)$(bindir)/.libs"; \
-			$(install_sh) \
-				$(CURRENT_BUILD)/src/main/cvc4 \
-				"$(abs_builddir)$(bindir)"; \
+	$(AM_V_at)thelibdir="$(abs_builddir)$(libdir)"; \
+	progdir="$(abs_builddir)$(bindir)"; for file in $(CVC4_BINARIES); do \
+		if test -r $(CURRENT_BUILD)/src/main/$$file; then \
+			eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/$$file | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \
+			if test -z "$$relink_command"; then \
+				$(AM_V_mkdir_noat) "$(CURRENT_BUILD)$(bindir)/.libs"; \
+				$(AM_V_install_sh_noat) \
+					$(CURRENT_BUILD)/src/main/.libs/$$file \
+					"$(abs_builddir)$(bindir)/.libs"; \
+				$(AM_V_install_sh_noat) \
+					$(CURRENT_BUILD)/src/main/$$file \
+					"$(abs_builddir)$(bindir)"; \
+			else \
+				$(AM_V_relink) "$$file"; eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"; \
+			fi; \
 		else \
-			eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"; \
-		fi
+			rm -f "$(abs_builddir)$(bindir)/$$file"; \
+		fi; \
+	done
 else
 #	if we're building static libs only, just install the driver binary directly
-	$(install_sh) \
-		$(CURRENT_BUILD)/src/main/cvc4 \
-		"$(abs_builddir)$(bindir)"
+	$(AM_V_at)for file in $(CVC4_BINARIES); do \
+		if test -r $(CURRENT_BUILD)/src/main/$$file; then \
+			$(AM_V_install_sh_noat) \
+				$(CURRENT_BUILD)/src/main/$$file \
+				"$(abs_builddir)$(bindir)"; \
+		else \
+			rm -f "$(abs_builddir)$(bindir)/$$file"; \
+		fi; \
+	done
 endif
 #	set up builds/$(CURRENT_BUILD)/bin and builds/$(CURRENT_BUILD)/lib
-	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
+	$(AM_V_at)test -e $(CURRENT_BUILD)/lib || ln -sfv "$(abs_builddir)$(libdir)" $(CURRENT_BUILD)/lib
+	$(AM_V_at)test -e $(CURRENT_BUILD)/bin || ln -sfv "$(abs_builddir)$(bindir)" $(CURRENT_BUILD)/bin
 #	set up builds/...prefix.../bin and builds/...prefix.../lib
-	$(mkinstalldirs) ".$(bindir)" ".$(libdir)"
+	$(AM_V_mkdir) ".$(bindir)"
+	$(AM_V_mkdir) ".$(libdir)"
 #	install libcvc4
-	$(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "`pwd`$(libdir)"
+	$(AM_V_ltinstall) $(CURRENT_BUILD)/src/libcvc4.la "`pwd`$(libdir)"
 #	install libcvc4parser
-	$(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la "`pwd`$(libdir)"
+	$(AM_V_ltinstall) $(CURRENT_BUILD)/src/parser/libcvc4parser.la "`pwd`$(libdir)"
 ifeq ($(CVC4_BUILD_LIBCOMPAT),yes)
 #	install libcvc4compat
 	$(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/compat/libcvc4compat.la "`pwd`$(libdir)"
@@ -101,26 +151,39 @@ endif
 ifeq ($(BUILDING_SHARED)$(STATIC_BINARY),10)
 #	if we're building shared libs and the binary is not static, relink
 #	the handling with empty $relink_command is a hack for Mac OS
-	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:'`; \
-		if test -z "$$relink_command"; then \
-			$(mkinstalldirs) ".$(bindir)/.libs"; \
-			$(install_sh) \
-				$(CURRENT_BUILD)/src/main/.libs/cvc4 \
-				"`pwd`$(bindir)/.libs"; \
-			$(install_sh) \
-				$(CURRENT_BUILD)/src/main/cvc4 \
-				"`pwd`$(bindir)"; \
+	$(AM_V_at)thelibdir="`pwd`$(libdir)"; progdir="`pwd`$(bindir)"; for file in $(CVC4_BINARIES); do \
+		if test -r $(CURRENT_BUILD)/src/main/$$file; then \
+			eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/$$file | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \
+			if test -z "$$relink_command"; then \
+				$(AM_V_mkdir_noat) ".$(bindir)/.libs"; \
+				$(AM_V_install_sh_noat) \
+					$(CURRENT_BUILD)/src/main/.libs/$$file \
+					"`pwd`$(bindir)/.libs"; \
+				$(AM_V_install_sh_noat) \
+					$(CURRENT_BUILD)/src/main/$$file \
+					"`pwd`$(bindir)"; \
+			else \
+				$(AM_V_relink) "$$file"; eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"; \
+			fi; \
 		else \
-			eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"; \
-		fi
+			rm -f "`pwd`$(bindir)/$$file"; \
+		fi; \
+	done
 else
 #	if we're building static libs only, just install the driver binary directly
-	$(install_sh) $(CURRENT_BUILD)/src/main/cvc4 "`pwd`$(bindir)"
+	$(AM_V_at)for file in $(CVC4_BINARIES); do \
+		if test -r $(CURRENT_BUILD)/src/main/$$file; then \
+			$(AM_V_install_sh_noat) \
+				$(CURRENT_BUILD)/src/main/$$file \
+				"`pwd`$(bindir)"; \
+		else \
+			rm -f "`pwd`$(bindir)/$$file"; \
+		fi; \
+	done
 endif
 #	set up builds/bin and builds/lib
-	test -e lib || ln -sfv ".$(libdir)" lib
-	test -e bin || ln -sfv ".$(bindir)" bin
+	$(AM_V_at)test -e lib || ln -sfv ".$(libdir)" lib
+	$(AM_V_at)test -e bin || ln -sfv ".$(bindir)" bin
 	rm -f examples; ln -sf "$(CURRENT_BUILD)/examples" examples
 
 # The descent into "src" with target "check" is to build check
diff --git a/README b/README
index 23fdf9a51..981eeaa60 100644
--- a/README
+++ b/README
@@ -37,6 +37,7 @@ GNU C and C++ (gcc and g++), reasonably recent versions
 GNU Make
 GNU Bash
 GMP v4.2 (GNU Multi-Precision arithmetic library)
+The Boost C++ threading library (libboost_thread)
 libantlr3c v3.2 (ANTLR parser generator)
 Optional: CLN v1.3 (Class Library for Numbers)
 Optional: CUDD v2.4.2 (Colorado University Decision Diagram package)
diff --git a/config/boost.m4 b/config/boost.m4
new file mode 100644
index 000000000..b9c60d9c3
--- /dev/null
+++ b/config/boost.m4
@@ -0,0 +1,1044 @@
+# boost.m4: Locate Boost headers and libraries for autoconf-based projects.
+# Copyright (C) 2007, 2008, 2009, 2010  Benoit Sigoure <tsuna@lrde.epita.fr>
+#
+# This program is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# Additional permission under section 7 of the GNU General Public
+# License, version 3 ("GPLv3"):
+#
+# If you convey this file as part of a work that contains a
+# configuration script generated by Autoconf, you may do so under
+# terms of your choice.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+m4_define([_BOOST_SERIAL], [m4_translit([
+# serial 13
+], [#
+], [])])
+
+# Original sources can be found at http://github.com/tsuna/boost.m4
+# You can fetch the latest version of the script by doing:
+#   wget http://github.com/tsuna/boost.m4/raw/master/build-aux/boost.m4
+
+# ------ #
+# README #
+# ------ #
+
+# This file provides several macros to use the various Boost libraries.
+# The first macro is BOOST_REQUIRE.  It will simply check if it's possible to
+# find the Boost headers of a given (optional) minimum version and it will
+# define BOOST_CPPFLAGS accordingly.  It will add an option --with-boost to
+# your configure so that users can specify non standard locations.
+# If the user's environment contains BOOST_ROOT and --with-boost was not
+# specified, --with-boost=$BOOST_ROOT is implicitly used.
+# For more README and documentation, go to http://github.com/tsuna/boost.m4
+# Note: THESE MACROS ASSUME THAT YOU USE LIBTOOL.  If you don't, don't worry,
+# simply read the README, it will show you what to do step by step.
+
+m4_pattern_forbid([^_?BOOST_])
+
+
+# _BOOST_SED_CPP(SED-PROGRAM, PROGRAM,
+#                [ACTION-IF-FOUND], [ACTION-IF-NOT-FOUND])
+# --------------------------------------------------------
+# Same as AC_EGREP_CPP, but leave the result in conftest.i.
+# PATTERN is *not* overquoted, as in AC_EGREP_CPP.  It could be useful
+# to turn this into a macro which extracts the value of any macro.
+m4_define([_BOOST_SED_CPP],
+[AC_LANG_PREPROC_REQUIRE()dnl
+AC_REQUIRE([AC_PROG_SED])dnl
+AC_LANG_CONFTEST([AC_LANG_SOURCE([[$2]])])
+AS_IF([dnl eval is necessary to expand ac_cpp.
+dnl Ultrix and Pyramid sh refuse to redirect output of eval, so use subshell.
+dnl Beware of Windows end-of-lines, for instance if we are running
+dnl some Windows programs under Wine.  In that case, boost/version.hpp
+dnl is certainly using "\r\n", but the regular Unix shell will only
+dnl strip `\n' with backquotes, not the `\r'.  This results in
+dnl boost_cv_lib_version='1_37\r' for instance, which breaks
+dnl everything else.
+dnl Cannot use 'dnl' after [$4] because a trailing dnl may break AC_CACHE_CHECK
+(eval "$ac_cpp conftest.$ac_ext") 2>&AS_MESSAGE_LOG_FD |
+  tr -d '\r' |
+  $SED -n -e "$1" >conftest.i 2>&1],
+  [$3],
+  [$4])
+rm -rf conftest*
+])# AC_EGREP_CPP
+
+
+
+# BOOST_REQUIRE([VERSION], [ACTION-IF-NOT-FOUND])
+# -----------------------------------------------
+# Look for Boost.  If version is given, it must either be a literal of the form
+# "X.Y.Z" where X, Y and Z are integers (the ".Z" part being optional) or a
+# variable "$var".
+# Defines the value BOOST_CPPFLAGS.  This macro only checks for headers with
+# the required version, it does not check for any of the Boost libraries.
+# On # success, defines HAVE_BOOST.  On failure, calls the optional
+# ACTION-IF-NOT-FOUND action if one was supplied.
+# Otherwise aborts with an error message.
+AC_DEFUN([BOOST_REQUIRE],
+[AC_REQUIRE([AC_PROG_CXX])dnl
+AC_REQUIRE([AC_PROG_GREP])dnl
+echo "$as_me: this is boost.m4[]_BOOST_SERIAL" >&AS_MESSAGE_LOG_FD
+boost_save_IFS=$IFS
+boost_version_req=$1
+IFS=.
+set x $boost_version_req 0 0 0
+IFS=$boost_save_IFS
+shift
+boost_version_req=`expr "$[1]" '*' 100000 + "$[2]" '*' 100 + "$[3]"`
+boost_version_req_string=$[1].$[2].$[3]
+AC_ARG_WITH([boost],
+   [AS_HELP_STRING([--with-boost=DIR],
+                   [prefix of Boost $1 @<:@guess@:>@])])dnl
+AC_ARG_VAR([BOOST_ROOT],[Location of Boost installation])dnl
+# If BOOST_ROOT is set and the user has not provided a value to
+# --with-boost, then treat BOOST_ROOT as if it the user supplied it.
+if test x"$BOOST_ROOT" != x; then
+  if test x"$with_boost" = x; then
+    AC_MSG_NOTICE([Detected BOOST_ROOT; continuing with --with-boost=$BOOST_ROOT])
+    with_boost=$BOOST_ROOT
+  else
+    AC_MSG_NOTICE([Detected BOOST_ROOT=$BOOST_ROOT, but overridden by --with-boost=$with_boost])
+  fi
+fi
+AC_SUBST([DISTCHECK_CONFIGURE_FLAGS],
+         ["$DISTCHECK_CONFIGURE_FLAGS '--with-boost=$with_boost'"])
+boost_save_CPPFLAGS=$CPPFLAGS
+  AC_CACHE_CHECK([for Boost headers version >= $boost_version_req_string],
+    [boost_cv_inc_path],
+    [boost_cv_inc_path=no
+AC_LANG_PUSH([C++])dnl
+m4_pattern_allow([^BOOST_VERSION$])dnl
+    AC_LANG_CONFTEST([AC_LANG_PROGRAM([[#include <boost/version.hpp>
+#if !defined BOOST_VERSION
+# error BOOST_VERSION is not defined
+#elif BOOST_VERSION < $boost_version_req
+# error Boost headers version < $boost_version_req
+#endif
+]])])
+    # If the user provided a value to --with-boost, use it and only it.
+    case $with_boost in #(
+      ''|yes) set x '' /opt/local/include /usr/local/include /opt/include \
+                 /usr/include C:/Boost/include;; #(
+      *)      set x "$with_boost/include" "$with_boost";;
+    esac
+    shift
+    for boost_dir
+    do
+    # Without --layout=system, Boost (or at least some versions) installs
+    # itself in <prefix>/include/boost-<version>.  This inner loop helps to
+    # find headers in such directories.
+    #
+    # Any ${boost_dir}/boost-x_xx directories are searched in reverse version
+    # order followed by ${boost_dir}.  The final '.' is a sentinel for
+    # searching $boost_dir" itself.  Entries are whitespace separated.
+    #
+    # I didn't indent this loop on purpose (to avoid over-indented code)
+    boost_layout_system_search_list=`cd "$boost_dir" 2>/dev/null \
+        && ls -1 | "${GREP}" '^boost-' | sort -rn -t- -k2 \
+        && echo .`
+    for boost_inc in $boost_layout_system_search_list
+    do
+      if test x"$boost_inc" != x.; then
+        boost_inc="$boost_dir/$boost_inc"
+      else
+        boost_inc="$boost_dir" # Uses sentinel in boost_layout_system_search_list
+      fi
+      if test x"$boost_inc" != x; then
+        # We are going to check whether the version of Boost installed
+        # in $boost_inc is usable by running a compilation that
+        # #includes it.  But if we pass a -I/some/path in which Boost
+        # is not installed, the compiler will just skip this -I and
+        # use other locations (either from CPPFLAGS, or from its list
+        # of system include directories).  As a result we would use
+        # header installed on the machine instead of the /some/path
+        # specified by the user.  So in that precise case (trying
+        # $boost_inc), make sure the version.hpp exists.
+        #
+        # Use test -e as there can be symlinks.
+        test -e "$boost_inc/boost/version.hpp" || continue
+        CPPFLAGS="$CPPFLAGS -I$boost_inc"
+      fi
+      AC_COMPILE_IFELSE([], [boost_cv_inc_path=yes], [boost_cv_version=no])
+      if test x"$boost_cv_inc_path" = xyes; then
+        if test x"$boost_inc" != x; then
+          boost_cv_inc_path=$boost_inc
+        fi
+        break 2
+      fi
+    done
+    done
+AC_LANG_POP([C++])dnl
+    ])
+    case $boost_cv_inc_path in #(
+      no)
+        boost_errmsg="cannot find Boost headers version >= $boost_version_req_string"
+        m4_if([$2], [],  [AC_MSG_ERROR([$boost_errmsg])],
+                        [AC_MSG_NOTICE([$boost_errmsg])])
+        $2
+        ;;#(
+      yes)
+        BOOST_CPPFLAGS=
+        ;;#(
+      *)
+        AC_SUBST([BOOST_CPPFLAGS], ["-I$boost_cv_inc_path"])
+        ;;
+    esac
+  if test x"$boost_cv_inc_path" != xno; then
+  AC_DEFINE([HAVE_BOOST], [1],
+            [Defined if the requested minimum BOOST version is satisfied])
+  AC_CACHE_CHECK([for Boost's header version],
+    [boost_cv_lib_version],
+    [m4_pattern_allow([^BOOST_LIB_VERSION$])dnl
+     _BOOST_SED_CPP([/^boost-lib-version = /{s///;s/\"//g;p;g;}],
+                    [#include <boost/version.hpp>
+boost-lib-version = BOOST_LIB_VERSION],
+    [boost_cv_lib_version=`cat conftest.i`])])
+    # e.g. "134" for 1_34_1 or "135" for 1_35
+    boost_major_version=`echo "$boost_cv_lib_version" | sed 's/_//;s/_.*//'`
+    case $boost_major_version in #(
+      '' | *[[!0-9]]*)
+        AC_MSG_ERROR([invalid value: boost_major_version=$boost_major_version])
+        ;;
+    esac
+fi
+CPPFLAGS=$boost_save_CPPFLAGS
+])# BOOST_REQUIRE
+
+# BOOST_STATIC()
+# --------------
+# Add the "--enable-static-boost" configure argument. If this argument is given
+# on the command line, static versions of the libraries will be looked up.
+AC_DEFUN([BOOST_STATIC],
+  [AC_ARG_ENABLE([static-boost],
+     [AC_HELP_STRING([--enable-static-boost],
+               [Prefer the static boost libraries over the shared ones [no]])],
+     [enable_static_boost=yes],
+     [enable_static_boost=no])])# BOOST_STATIC
+
+# BOOST_FIND_HEADER([HEADER-NAME], [ACTION-IF-NOT-FOUND], [ACTION-IF-FOUND])
+# --------------------------------------------------------------------------
+# Wrapper around AC_CHECK_HEADER for Boost headers.  Useful to check for
+# some parts of the Boost library which are only made of headers and don't
+# require linking (such as Boost.Foreach).
+#
+# Default ACTION-IF-NOT-FOUND: Fail with a fatal error unless Boost couldn't be
+# found in the first place, in which case by default a notice is issued to the
+# user.  Presumably if we haven't died already it's because it's OK to not have
+# Boost, which is why only a notice is issued instead of a hard error.
+#
+# Default ACTION-IF-FOUND: define the preprocessor symbol HAVE_<HEADER-NAME> in
+# case of success # (where HEADER-NAME is written LIKE_THIS, e.g.,
+# HAVE_BOOST_FOREACH_HPP).
+AC_DEFUN([BOOST_FIND_HEADER],
+[AC_REQUIRE([BOOST_REQUIRE])dnl
+if test x"$boost_cv_inc_path" = xno; then
+  m4_default([$2], [AC_MSG_NOTICE([Boost not available, not searching for $1])])
+else
+AC_LANG_PUSH([C++])dnl
+boost_save_CPPFLAGS=$CPPFLAGS
+CPPFLAGS="$CPPFLAGS $BOOST_CPPFLAGS"
+AC_CHECK_HEADER([$1],
+  [m4_default([$3], [AC_DEFINE(AS_TR_CPP([HAVE_$1]), [1],
+                               [Define to 1 if you have <$1>])])],
+  [m4_default([$2], [AC_MSG_ERROR([cannot find $1])])])
+CPPFLAGS=$boost_save_CPPFLAGS
+AC_LANG_POP([C++])dnl
+fi
+])# BOOST_FIND_HEADER
+
+
+# BOOST_FIND_LIB([LIB-NAME], [PREFERRED-RT-OPT], [HEADER-NAME], [CXX-TEST],
+#                [CXX-PROLOGUE])
+# -------------------------------------------------------------------------
+# Look for the Boost library LIB-NAME (e.g., LIB-NAME = `thread', for
+# libboost_thread).  Check that HEADER-NAME works and check that
+# libboost_LIB-NAME can link with the code CXX-TEST.  The optional argument
+# CXX-PROLOGUE can be used to include some C++ code before the `main'
+# function.
+#
+# Invokes BOOST_FIND_HEADER([HEADER-NAME]) (see above).
+#
+# Boost libraries typically come compiled with several flavors (with different
+# runtime options) so PREFERRED-RT-OPT is the preferred suffix.  A suffix is one
+# or more of the following letters: sgdpn (in that order).  s = static
+# runtime, d = debug build, g = debug/diagnostic runtime, p = STLPort build,
+# n = (unsure) STLPort build without iostreams from STLPort (it looks like `n'
+# must always be used along with `p').  Additionally, PREFERRED-RT-OPT can
+# start with `mt-' to indicate that there is a preference for multi-thread
+# builds.  Some sample values for PREFERRED-RT-OPT: (nothing), mt, d, mt-d, gdp
+# ...  If you want to make sure you have a specific version of Boost
+# (eg, >= 1.33) you *must* invoke BOOST_REQUIRE before this macro.
+AC_DEFUN([BOOST_FIND_LIB],
+[AC_REQUIRE([BOOST_REQUIRE])dnl
+AC_REQUIRE([_BOOST_FIND_COMPILER_TAG])dnl
+AC_REQUIRE([BOOST_STATIC])dnl
+AC_REQUIRE([_BOOST_GUESS_WHETHER_TO_USE_MT])dnl
+if test x"$boost_cv_inc_path" = xno; then
+  AC_MSG_NOTICE([Boost not available, not searching for the Boost $1 library])
+else
+dnl The else branch is huge and wasn't intended on purpose.
+AC_LANG_PUSH([C++])dnl
+AS_VAR_PUSHDEF([Boost_lib], [boost_cv_lib_$1])dnl
+AS_VAR_PUSHDEF([Boost_lib_LDFLAGS], [boost_cv_lib_$1_LDFLAGS])dnl
+AS_VAR_PUSHDEF([Boost_lib_LDPATH], [boost_cv_lib_$1_LDPATH])dnl
+AS_VAR_PUSHDEF([Boost_lib_LIBS], [boost_cv_lib_$1_LIBS])dnl
+BOOST_FIND_HEADER([$3])
+boost_save_CPPFLAGS=$CPPFLAGS
+CPPFLAGS="$CPPFLAGS $BOOST_CPPFLAGS"
+# Now let's try to find the library.  The algorithm is as follows: first look
+# for a given library name according to the user's PREFERRED-RT-OPT.  For each
+# library name, we prefer to use the ones that carry the tag (toolset name).
+# Each library is searched through the various standard paths were Boost is
+# usually installed.  If we can't find the standard variants, we try to
+# enforce -mt (for instance on MacOSX, libboost_threads.dylib doesn't exist
+# but there's -obviously- libboost_threads-mt.dylib).
+AC_CACHE_CHECK([for the Boost $1 library], [Boost_lib],
+  [Boost_lib=no
+  case "$2" in #(
+    mt | mt-) boost_mt=-mt; boost_rtopt=;; #(
+    mt* | mt-*) boost_mt=-mt; boost_rtopt=`expr "X$2" : 'Xmt-*\(.*\)'`;; #(
+    *) boost_mt=; boost_rtopt=$2;;
+  esac
+  if test $enable_static_boost = yes; then
+    boost_rtopt="s$boost_rtopt"
+  fi
+  # Find the proper debug variant depending on what we've been asked to find.
+  case $boost_rtopt in #(
+    *d*) boost_rt_d=$boost_rtopt;; #(
+    *[[sgpn]]*) # Insert the `d' at the right place (in between `sg' and `pn')
+      boost_rt_d=`echo "$boost_rtopt" | sed 's/\(s*g*\)\(p*n*\)/\1\2/'`;; #(
+    *) boost_rt_d='-d';;
+  esac
+  # If the PREFERRED-RT-OPT are not empty, prepend a `-'.
+  test -n "$boost_rtopt" && boost_rtopt="-$boost_rtopt"
+  $boost_guess_use_mt && boost_mt=-mt
+  # Look for the abs path the static archive.
+  # $libext is computed by Libtool but let's make sure it's non empty.
+  test -z "$libext" &&
+    AC_MSG_ERROR([the libext variable is empty, did you invoke Libtool?])
+  boost_save_ac_objext=$ac_objext
+  # Generate the test file.
+  AC_LANG_CONFTEST([AC_LANG_PROGRAM([#include <$3>
+$5], [$4])])
+dnl Optimization hacks: compiling C++ is slow, especially with Boost.  What
+dnl we're trying to do here is guess the right combination of link flags
+dnl (LIBS / LDFLAGS) to use a given library.  This can take several
+dnl iterations before it succeeds and is thus *very* slow.  So what we do
+dnl instead is that we compile the code first (and thus get an object file,
+dnl typically conftest.o).  Then we try various combinations of link flags
+dnl until we succeed to link conftest.o in an executable.  The problem is
+dnl that the various TRY_LINK / COMPILE_IFELSE macros of Autoconf always
+dnl remove all the temporary files including conftest.o.  So the trick here
+dnl is to temporarily change the value of ac_objext so that conftest.o is
+dnl preserved accross tests.  This is obviously fragile and I will burn in
+dnl hell for not respecting Autoconf's documented interfaces, but in the
+dnl mean time, it optimizes the macro by a factor of 5 to 30.
+dnl Another small optimization: the first argument of AC_COMPILE_IFELSE left
+dnl empty because the test file is generated only once above (before we
+dnl start the for loops).
+  AC_COMPILE_IFELSE([],
+    [ac_objext=do_not_rm_me_plz],
+    [AC_MSG_ERROR([cannot compile a test that uses Boost $1])])
+  ac_objext=$boost_save_ac_objext
+  boost_failed_libs=
+# Don't bother to ident the 6 nested for loops, only the 2 innermost ones
+# matter.
+for boost_tag_ in -$boost_cv_lib_tag ''; do
+for boost_ver_ in -$boost_cv_lib_version ''; do
+for boost_mt_ in $boost_mt -mt ''; do
+for boost_rtopt_ in $boost_rtopt '' -d; do
+  for boost_lib in \
+    boost_$1$boost_tag_$boost_mt_$boost_rtopt_$boost_ver_ \
+    boost_$1$boost_tag_$boost_rtopt_$boost_ver_ \
+    boost_$1$boost_tag_$boost_mt_$boost_ver_ \
+    boost_$1$boost_tag_$boost_ver_
+  do
+    # Avoid testing twice the same lib
+    case $boost_failed_libs in #(
+      *@$boost_lib@*) continue;;
+    esac
+    # If with_boost is empty, we'll search in /lib first, which is not quite
+    # right so instead we'll try to a location based on where the headers are.
+    boost_tmp_lib=$with_boost
+    test x"$with_boost" = x && boost_tmp_lib=${boost_cv_inc_path%/include}
+    for boost_ldpath in "$boost_tmp_lib/lib" '' \
+             /opt/local/lib /usr/local/lib /opt/lib /usr/lib \
+             "$with_boost" C:/Boost/lib /lib /usr/lib64 /lib64
+    do
+      test -e "$boost_ldpath" || continue
+      boost_save_LDFLAGS=$LDFLAGS
+      # Are we looking for a static library?
+      case $boost_ldpath:$boost_rtopt_ in #(
+        *?*:*s*) # Yes (Non empty boost_ldpath + s in rt opt)
+          Boost_lib_LIBS="$boost_ldpath/lib$boost_lib.$libext"
+          test -e "$Boost_lib_LIBS" || continue;; #(
+        *) # No: use -lboost_foo to find the shared library.
+          Boost_lib_LIBS="-l$boost_lib";;
+      esac
+      boost_save_LIBS=$LIBS
+      LIBS="$Boost_lib_LIBS $LIBS"
+      test x"$boost_ldpath" != x && LDFLAGS="$LDFLAGS -L$boost_ldpath"
+dnl First argument of AC_LINK_IFELSE left empty because the test file is
+dnl generated only once above (before we start the for loops).
+      _BOOST_AC_LINK_IFELSE([],
+                            [Boost_lib=yes], [Boost_lib=no])
+      ac_objext=$boost_save_ac_objext
+      LDFLAGS=$boost_save_LDFLAGS
+      LIBS=$boost_save_LIBS
+      if test x"$Boost_lib" = xyes; then
+        Boost_lib_LDFLAGS="-L$boost_ldpath -R$boost_ldpath"
+        Boost_lib_LDPATH="$boost_ldpath"
+        break 6
+      else
+        boost_failed_libs="$boost_failed_libs@$boost_lib@"
+      fi
+    done
+  done
+done
+done
+done
+done
+rm -f conftest.$ac_objext
+])
+case $Boost_lib in #(
+  no) _AC_MSG_LOG_CONFTEST
+    AC_MSG_ERROR([cannot not find the flags to link with Boost $1])
+    ;;
+esac
+AC_SUBST(AS_TR_CPP([BOOST_$1_LDFLAGS]), [$Boost_lib_LDFLAGS])
+AC_SUBST(AS_TR_CPP([BOOST_$1_LDPATH]), [$Boost_lib_LDPATH])
+AC_SUBST([BOOST_LDPATH], [$Boost_lib_LDPATH])
+AC_SUBST(AS_TR_CPP([BOOST_$1_LIBS]), [$Boost_lib_LIBS])
+CPPFLAGS=$boost_save_CPPFLAGS
+AS_VAR_POPDEF([Boost_lib])dnl
+AS_VAR_POPDEF([Boost_lib_LDFLAGS])dnl
+AS_VAR_POPDEF([Boost_lib_LDPATH])dnl
+AS_VAR_POPDEF([Boost_lib_LIBS])dnl
+AC_LANG_POP([C++])dnl
+fi
+])# BOOST_FIND_LIB
+
+
+# --------------------------------------- #
+# Checks for the various Boost libraries. #
+# --------------------------------------- #
+
+# List of boost libraries: http://www.boost.org/libs/libraries.htm
+# The page http://beta.boost.org/doc/libs is useful: it gives the first release
+# version of each library (among other things).
+
+# BOOST_ARRAY()
+# -------------
+# Look for Boost.Array
+AC_DEFUN([BOOST_ARRAY],
+[BOOST_FIND_HEADER([boost/array.hpp])])
+
+
+# BOOST_ASIO()
+# ------------
+# Look for Boost.Asio (new in Boost 1.35).
+AC_DEFUN([BOOST_ASIO],
+[AC_REQUIRE([BOOST_SYSTEM])dnl
+BOOST_FIND_HEADER([boost/asio.hpp])])
+
+
+# BOOST_BIND()
+# ------------
+# Look for Boost.Bind
+AC_DEFUN([BOOST_BIND],
+[BOOST_FIND_HEADER([boost/bind.hpp])])
+
+
+# BOOST_CONVERSION()
+# ------------------
+# Look for Boost.Conversion (cast / lexical_cast)
+AC_DEFUN([BOOST_CONVERSION],
+[BOOST_FIND_HEADER([boost/cast.hpp])
+BOOST_FIND_HEADER([boost/lexical_cast.hpp])
+])# BOOST_CONVERSION
+
+
+# BOOST_DATE_TIME([PREFERRED-RT-OPT])
+# -----------------------------------
+# Look for Boost.Date_Time.  For the documentation of PREFERRED-RT-OPT, see the
+# documentation of BOOST_FIND_LIB above.
+AC_DEFUN([BOOST_DATE_TIME],
+[BOOST_FIND_LIB([date_time], [$1],
+                [boost/date_time/posix_time/posix_time.hpp],
+                [boost::posix_time::ptime t;])
+])# BOOST_DATE_TIME
+
+
+# BOOST_FILESYSTEM([PREFERRED-RT-OPT])
+# ------------------------------------
+# Look for Boost.Filesystem.  For the documentation of PREFERRED-RT-OPT, see
+# the documentation of BOOST_FIND_LIB above.
+# Do not check for boost/filesystem.hpp because this file was introduced in
+# 1.34.
+AC_DEFUN([BOOST_FILESYSTEM],
+[# Do we have to check for Boost.System?  This link-time dependency was
+# added as of 1.35.0.  If we have a version <1.35, we must not attempt to
+# find Boost.System as it didn't exist by then.
+if test $boost_major_version -ge 135; then
+BOOST_SYSTEM([$1])
+fi # end of the Boost.System check.
+boost_filesystem_save_LIBS=$LIBS
+boost_filesystem_save_LDFLAGS=$LDFLAGS
+m4_pattern_allow([^BOOST_SYSTEM_(LIBS|LDFLAGS)$])dnl
+LIBS="$LIBS $BOOST_SYSTEM_LIBS"
+LDFLAGS="$LDFLAGS $BOOST_SYSTEM_LDFLAGS"
+BOOST_FIND_LIB([filesystem], [$1],
+                [boost/filesystem/path.hpp], [boost::filesystem::path p;])
+LIBS=$boost_filesystem_save_LIBS
+LDFLAGS=$boost_filesystem_save_LDFLAGS
+])# BOOST_FILESYSTEM
+
+
+# BOOST_FOREACH()
+# ---------------
+# Look for Boost.Foreach
+AC_DEFUN([BOOST_FOREACH],
+[BOOST_FIND_HEADER([boost/foreach.hpp])])
+
+
+# BOOST_FORMAT()
+# --------------
+# Look for Boost.Format
+# Note: we can't check for boost/format/format_fwd.hpp because the header isn't
+# standalone.  It can't be compiled because it triggers the following error:
+# boost/format/detail/config_macros.hpp:88: error: 'locale' in namespace 'std'
+#                                                  does not name a type
+AC_DEFUN([BOOST_FORMAT],
+[BOOST_FIND_HEADER([boost/format.hpp])])
+
+
+# BOOST_FUNCTION()
+# ----------------
+# Look for Boost.Function
+AC_DEFUN([BOOST_FUNCTION],
+[BOOST_FIND_HEADER([boost/function.hpp])])
+
+
+# BOOST_GRAPH([PREFERRED-RT-OPT])
+# -------------------------------
+# Look for Boost.Graphs.  For the documentation of PREFERRED-RT-OPT, see the
+# documentation of BOOST_FIND_LIB above.
+AC_DEFUN([BOOST_GRAPH],
+[BOOST_FIND_LIB([graph], [$1],
+                [boost/graph/adjacency_list.hpp], [boost::adjacency_list<> g;])
+])# BOOST_GRAPH
+
+
+# BOOST_IOSTREAMS([PREFERRED-RT-OPT])
+# -------------------------------
+# Look for Boost.IOStreams.  For the documentation of PREFERRED-RT-OPT, see the
+# documentation of BOOST_FIND_LIB above.
+AC_DEFUN([BOOST_IOSTREAMS],
+[BOOST_FIND_LIB([iostreams], [$1],
+                [boost/iostreams/device/file_descriptor.hpp],
+                [boost::iostreams::file_descriptor fd; fd.close();])
+])# BOOST_IOSTREAMS
+
+
+# BOOST_HASH()
+# ------------
+# Look for Boost.Functional/Hash
+AC_DEFUN([BOOST_HASH],
+[BOOST_FIND_HEADER([boost/functional/hash.hpp])])
+
+
+# BOOST_LAMBDA()
+# --------------
+# Look for Boost.Lambda
+AC_DEFUN([BOOST_LAMBDA],
+[BOOST_FIND_HEADER([boost/lambda/lambda.hpp])])
+
+
+# BOOST_MATH()
+# ------------
+# Look for Boost.Math
+# TODO: This library isn't header-only but it comes in multiple different
+# flavors that don't play well with BOOST_FIND_LIB (e.g, libboost_math_c99,
+# libboost_math_c99f, libboost_math_c99l, libboost_math_tr1,
+# libboost_math_tr1f, libboost_math_tr1l).  This macro must be fixed to do the
+# right thing anyway.
+AC_DEFUN([BOOST_MATH],
+[BOOST_FIND_HEADER([boost/math/special_functions.hpp])])
+
+
+# BOOST_MULTIARRAY()
+# ------------------
+# Look for Boost.MultiArray
+AC_DEFUN([BOOST_MULTIARRAY],
+[BOOST_FIND_HEADER([boost/multi_array.hpp])])
+
+
+# BOOST_NUMERIC_CONVERSION()
+# --------------------------
+# Look for Boost.NumericConversion (policy-based numeric conversion)
+AC_DEFUN([BOOST_NUMERIC_CONVERSION],
+[BOOST_FIND_HEADER([boost/numeric/conversion/converter.hpp])
+])# BOOST_NUMERIC_CONVERSION
+
+
+# BOOST_OPTIONAL()
+# ----------------
+# Look for Boost.Optional
+AC_DEFUN([BOOST_OPTIONAL],
+[BOOST_FIND_HEADER([boost/optional.hpp])])
+
+
+# BOOST_PREPROCESSOR()
+# --------------------
+# Look for Boost.Preprocessor
+AC_DEFUN([BOOST_PREPROCESSOR],
+[BOOST_FIND_HEADER([boost/preprocessor/repeat.hpp])])
+
+
+# BOOST_PROGRAM_OPTIONS([PREFERRED-RT-OPT])
+# -----------------------------------------
+# Look for Boost.Program_options.  For the documentation of PREFERRED-RT-OPT, see
+# the documentation of BOOST_FIND_LIB above.
+AC_DEFUN([BOOST_PROGRAM_OPTIONS],
+[BOOST_FIND_LIB([program_options], [$1],
+                [boost/program_options.hpp],
+                [boost::program_options::options_description d("test");])
+])# BOOST_PROGRAM_OPTIONS
+
+
+# BOOST_REF()
+# -----------
+# Look for Boost.Ref
+AC_DEFUN([BOOST_REF],
+[BOOST_FIND_HEADER([boost/ref.hpp])])
+
+
+# BOOST_REGEX([PREFERRED-RT-OPT])
+# -------------------------------
+# Look for Boost.Regex.  For the documentation of PREFERRED-RT-OPT, see the
+# documentation of BOOST_FIND_LIB above.
+AC_DEFUN([BOOST_REGEX],
+[BOOST_FIND_LIB([regex], [$1],
+                [boost/regex.hpp],
+                [boost::regex exp("*"); boost::regex_match("foo", exp);])
+])# BOOST_REGEX
+
+
+# BOOST_SERIALIZATION([PREFERRED-RT-OPT])
+# ---------------------------------------
+# Look for Boost.Serialization.  For the documentation of PREFERRED-RT-OPT, see
+# the documentation of BOOST_FIND_LIB above.
+AC_DEFUN([BOOST_SERIALIZATION],
+[BOOST_FIND_LIB([serialization], [$1],
+                [boost/archive/text_oarchive.hpp],
+                [std::ostream* o = 0; // Cheap way to get an ostream...
+                boost::archive::text_oarchive t(*o);])
+])# BOOST_SIGNALS
+
+
+# BOOST_SIGNALS([PREFERRED-RT-OPT])
+# ---------------------------------
+# Look for Boost.Signals.  For the documentation of PREFERRED-RT-OPT, see the
+# documentation of BOOST_FIND_LIB above.
+AC_DEFUN([BOOST_SIGNALS],
+[BOOST_FIND_LIB([signals], [$1],
+                [boost/signal.hpp],
+                [boost::signal<void ()> s;])
+])# BOOST_SIGNALS
+
+
+# BOOST_SMART_PTR()
+# -----------------
+# Look for Boost.SmartPtr
+AC_DEFUN([BOOST_SMART_PTR],
+[BOOST_FIND_HEADER([boost/scoped_ptr.hpp])
+BOOST_FIND_HEADER([boost/shared_ptr.hpp])
+])
+
+
+# BOOST_STATICASSERT()
+# --------------------
+# Look for Boost.StaticAssert
+AC_DEFUN([BOOST_STATICASSERT],
+[BOOST_FIND_HEADER([boost/static_assert.hpp])])
+
+
+# BOOST_STRING_ALGO()
+# -------------------
+# Look for Boost.StringAlgo
+AC_DEFUN([BOOST_STRING_ALGO],
+[BOOST_FIND_HEADER([boost/algorithm/string.hpp])
+])
+
+
+# BOOST_SYSTEM([PREFERRED-RT-OPT])
+# --------------------------------
+# Look for Boost.System.  For the documentation of PREFERRED-RT-OPT, see the
+# documentation of BOOST_FIND_LIB above.  This library was introduced in Boost
+# 1.35.0.
+AC_DEFUN([BOOST_SYSTEM],
+[BOOST_FIND_LIB([system], [$1],
+                [boost/system/error_code.hpp],
+                [boost::system::error_code e; e.clear();])
+])# BOOST_SYSTEM
+
+
+# BOOST_TEST([PREFERRED-RT-OPT])
+# ------------------------------
+# Look for Boost.Test.  For the documentation of PREFERRED-RT-OPT, see the
+# documentation of BOOST_FIND_LIB above.
+AC_DEFUN([BOOST_TEST],
+[m4_pattern_allow([^BOOST_CHECK$])dnl
+BOOST_FIND_LIB([unit_test_framework], [$1],
+               [boost/test/unit_test.hpp], [BOOST_CHECK(2 == 2);],
+               [using boost::unit_test::test_suite;
+               test_suite* init_unit_test_suite(int argc, char ** argv)
+               { return NULL; }])
+])# BOOST_TEST
+
+
+# BOOST_THREADS([PREFERRED-RT-OPT])
+# ---------------------------------
+# Look for Boost.Thread.  For the documentation of PREFERRED-RT-OPT, see the
+# documentation of BOOST_FIND_LIB above.
+# FIXME: Provide an alias "BOOST_THREAD".
+AC_DEFUN([BOOST_THREADS],
+[dnl Having the pthread flag is required at least on GCC3 where
+dnl boost/thread.hpp would complain if we try to compile without
+dnl -pthread on GNU/Linux.
+AC_REQUIRE([_BOOST_PTHREAD_FLAG])dnl
+boost_threads_save_LIBS=$LIBS
+boost_threads_save_CPPFLAGS=$CPPFLAGS
+LIBS="$LIBS $boost_cv_pthread_flag"
+# Yes, we *need* to put the -pthread thing in CPPFLAGS because with GCC3,
+# boost/thread.hpp will trigger a #error if -pthread isn't used:
+#   boost/config/requires_threads.hpp:47:5: #error "Compiler threading support
+#   is not turned on. Please set the correct command line options for
+#   threading: -pthread (Linux), -pthreads (Solaris) or -mthreads (Mingw32)"
+CPPFLAGS="$CPPFLAGS $boost_cv_pthread_flag"
+BOOST_FIND_LIB([thread], [$1],
+                [boost/thread.hpp], [boost::thread t; boost::mutex m;])
+BOOST_THREAD_LIBS="$BOOST_THREAD_LIBS $boost_cv_pthread_flag"
+BOOST_CPPFLAGS="$BOOST_CPPFLAGS $boost_cv_pthread_flag"
+LIBS=$boost_threads_save_LIBS
+CPPFLAGS=$boost_threads_save_CPPFLAGS
+])# BOOST_THREADS
+
+
+# BOOST_TOKENIZER()
+# -----------------
+# Look for Boost.Tokenizer
+AC_DEFUN([BOOST_TOKENIZER],
+[BOOST_FIND_HEADER([boost/tokenizer.hpp])])
+
+
+# BOOST_TRIBOOL()
+# ---------------
+# Look for Boost.Tribool
+AC_DEFUN([BOOST_TRIBOOL],
+[BOOST_FIND_HEADER([boost/logic/tribool_fwd.hpp])
+BOOST_FIND_HEADER([boost/logic/tribool.hpp])
+])
+
+
+# BOOST_TUPLE()
+# -------------
+# Look for Boost.Tuple
+AC_DEFUN([BOOST_TUPLE],
+[BOOST_FIND_HEADER([boost/tuple/tuple.hpp])])
+
+
+# BOOST_TYPETRAITS()
+# --------------------
+# Look for Boost.TypeTraits
+AC_DEFUN([BOOST_TYPETRAITS],
+[BOOST_FIND_HEADER([boost/type_traits.hpp])])
+
+
+# BOOST_UTILITY()
+# ---------------
+# Look for Boost.Utility (noncopyable, result_of, base-from-member idiom,
+# etc.)
+AC_DEFUN([BOOST_UTILITY],
+[BOOST_FIND_HEADER([boost/utility.hpp])])
+
+
+# BOOST_VARIANT()
+# ---------------
+# Look for Boost.Variant.
+AC_DEFUN([BOOST_VARIANT],
+[BOOST_FIND_HEADER([boost/variant/variant_fwd.hpp])
+BOOST_FIND_HEADER([boost/variant.hpp])])
+
+
+# BOOST_WAVE([PREFERRED-RT-OPT])
+# ------------------------------
+# NOTE: If you intend to use Wave/Spirit with thread support, make sure you
+# call BOOST_THREADS first.
+# Look for Boost.Wave.  For the documentation of PREFERRED-RT-OPT, see the
+# documentation of BOOST_FIND_LIB above.
+AC_DEFUN([BOOST_WAVE],
+[AC_REQUIRE([BOOST_FILESYSTEM])dnl
+AC_REQUIRE([BOOST_DATE_TIME])dnl
+boost_wave_save_LIBS=$LIBS
+boost_wave_save_LDFLAGS=$LDFLAGS
+m4_pattern_allow([^BOOST_((FILE)?SYSTEM|DATE_TIME|THREAD)_(LIBS|LDFLAGS)$])dnl
+LIBS="$LIBS $BOOST_SYSTEM_LIBS $BOOST_FILESYSTEM_LIBS $BOOST_DATE_TIME_LIBS\
+$BOOST_THREAD_LIBS"
+LDFLAGS="$LDFLAGS $BOOST_SYSTEM_LDFLAGS $BOOST_FILESYSTEM_LDFLAGS\
+$BOOST_DATE_TIME_LDFLAGS $BOOST_THREAD_LDFLAGS"
+BOOST_FIND_LIB([wave], [$1],
+                [boost/wave.hpp],
+                [boost::wave::token_id id; get_token_name(id);])
+LIBS=$boost_wave_save_LIBS
+LDFLAGS=$boost_wave_save_LDFLAGS
+])# BOOST_WAVE
+
+
+# BOOST_XPRESSIVE()
+# -----------------
+# Look for Boost.Xpressive (new since 1.36.0).
+AC_DEFUN([BOOST_XPRESSIVE],
+[BOOST_FIND_HEADER([boost/xpressive/xpressive.hpp])])
+
+
+# ----------------- #
+# Internal helpers. #
+# ----------------- #
+
+
+# _BOOST_PTHREAD_FLAG()
+# ---------------------
+# Internal helper for BOOST_THREADS.  Based on ACX_PTHREAD:
+# http://autoconf-archive.cryp.to/acx_pthread.html
+AC_DEFUN([_BOOST_PTHREAD_FLAG],
+[AC_REQUIRE([AC_PROG_CXX])dnl
+AC_REQUIRE([AC_CANONICAL_HOST])dnl
+AC_LANG_PUSH([C++])dnl
+AC_CACHE_CHECK([for the flags needed to use pthreads], [boost_cv_pthread_flag],
+[ boost_cv_pthread_flag=
+  # The ordering *is* (sometimes) important.  Some notes on the
+  # individual items follow:
+  # (none): in case threads are in libc; should be tried before -Kthread and
+  #       other compiler flags to prevent continual compiler warnings
+  # -lpthreads: AIX (must check this before -lpthread)
+  # -Kthread: Sequent (threads in libc, but -Kthread needed for pthread.h)
+  # -kthread: FreeBSD kernel threads (preferred to -pthread since SMP-able)
+  # -llthread: LinuxThreads port on FreeBSD (also preferred to -pthread)
+  # -pthread: GNU Linux/GCC (kernel threads), BSD/GCC (userland threads)
+  # -pthreads: Solaris/GCC
+  # -mthreads: MinGW32/GCC, Lynx/GCC
+  # -mt: Sun Workshop C (may only link SunOS threads [-lthread], but it
+  #      doesn't hurt to check since this sometimes defines pthreads too;
+  #      also defines -D_REENTRANT)
+  #      ... -mt is also the pthreads flag for HP/aCC
+  # -lpthread: GNU Linux, etc.
+  # --thread-safe: KAI C++
+  case $host_os in #(
+    *solaris*)
+      # On Solaris (at least, for some versions), libc contains stubbed
+      # (non-functional) versions of the pthreads routines, so link-based
+      # tests will erroneously succeed.  (We need to link with -pthreads/-mt/
+      # -lpthread.)  (The stubs are missing pthread_cleanup_push, or rather
+      # a function called by this macro, so we could check for that, but
+      # who knows whether they'll stub that too in a future libc.)  So,
+      # we'll just look for -pthreads and -lpthread first:
+      boost_pthread_flags="-pthreads -lpthread -mt -pthread";; #(
+    *)
+      boost_pthread_flags="-lpthreads -Kthread -kthread -llthread -pthread \
+                           -pthreads -mthreads -lpthread --thread-safe -mt";;
+  esac
+  # Generate the test file.
+  AC_LANG_CONFTEST([AC_LANG_PROGRAM([#include <pthread.h>],
+    [pthread_t th; pthread_join(th, 0);
+    pthread_attr_init(0); pthread_cleanup_push(0, 0);
+    pthread_create(0,0,0,0); pthread_cleanup_pop(0);])])
+  for boost_pthread_flag in '' $boost_pthread_flags; do
+    boost_pthread_ok=false
+dnl Re-use the test file already generated.
+    boost_pthreads__save_LIBS=$LIBS
+    LIBS="$LIBS $boost_pthread_flag"
+    AC_LINK_IFELSE([],
+      [if grep ".*$boost_pthread_flag" conftest.err; then
+         echo "This flag seems to have triggered warnings" >&AS_MESSAGE_LOG_FD
+       else
+         boost_pthread_ok=:; boost_cv_pthread_flag=$boost_pthread_flag
+       fi])
+    LIBS=$boost_pthreads__save_LIBS
+    $boost_pthread_ok && break
+  done
+])
+AC_LANG_POP([C++])dnl
+])# _BOOST_PTHREAD_FLAG
+
+
+# _BOOST_gcc_test(MAJOR, MINOR)
+# -----------------------------
+# Internal helper for _BOOST_FIND_COMPILER_TAG.
+m4_define([_BOOST_gcc_test],
+["defined __GNUC__ && __GNUC__ == $1 && __GNUC_MINOR__ == $2 && !defined __ICC @ gcc$1$2"])dnl
+
+
+# _BOOST_FIND_COMPILER_TAG()
+# --------------------------
+# Internal.  When Boost is installed without --layout=system, each library
+# filename will hold a suffix that encodes the compiler used during the
+# build.  The Boost build system seems to call this a `tag'.
+AC_DEFUN([_BOOST_FIND_COMPILER_TAG],
+[AC_REQUIRE([AC_PROG_CXX])dnl
+AC_REQUIRE([AC_CANONICAL_HOST])dnl
+AC_CACHE_CHECK([for the toolset name used by Boost for $CXX], [boost_cv_lib_tag],
+[boost_cv_lib_tag=unknown
+if test x$boost_cv_inc_path != xno; then
+  AC_LANG_PUSH([C++])dnl
+  # The following tests are mostly inspired by boost/config/auto_link.hpp
+  # The list is sorted to most recent/common to oldest compiler (in order
+  # to increase the likelihood of finding the right compiler with the
+  # least number of compilation attempt).
+  # Beware that some tests are sensible to the order (for instance, we must
+  # look for MinGW before looking for GCC3).
+  # I used one compilation test per compiler with a #error to recognize
+  # each compiler so that it works even when cross-compiling (let me know
+  # if you know a better approach).
+  # Known missing tags (known from Boost's tools/build/v2/tools/common.jam):
+  #   como, edg, kcc, bck, mp, sw, tru, xlc
+  # I'm not sure about my test for `il' (be careful: Intel's ICC pre-defines
+  # the same defines as GCC's).
+  for i in \
+    _BOOST_gcc_test(4, 5) \
+    _BOOST_gcc_test(4, 4) \
+    _BOOST_gcc_test(4, 3) \
+    _BOOST_gcc_test(4, 2) \
+    _BOOST_gcc_test(4, 1) \
+    _BOOST_gcc_test(4, 0) \
+    "defined __GNUC__ && __GNUC__ == 3 && !defined __ICC \
+     && (defined WIN32 || defined WINNT || defined _WIN32 || defined __WIN32 \
+         || defined __WIN32__ || defined __WINNT || defined __WINNT__) @ mgw" \
+    _BOOST_gcc_test(3, 4) \
+    _BOOST_gcc_test(3, 3) \
+    "defined _MSC_VER && _MSC_VER >= 1500 @ vc90" \
+    "defined _MSC_VER && _MSC_VER == 1400 @ vc80" \
+    _BOOST_gcc_test(3, 2) \
+    "defined _MSC_VER && _MSC_VER == 1310 @ vc71" \
+    _BOOST_gcc_test(3, 1) \
+    _BOOST_gcc_test(3, 0) \
+    "defined __BORLANDC__ @ bcb" \
+    "defined __ICC && (defined __unix || defined __unix__) @ il" \
+    "defined __ICL @ iw" \
+    "defined _MSC_VER && _MSC_VER == 1300 @ vc7" \
+    _BOOST_gcc_test(2, 95) \
+    "defined __MWERKS__ && __MWERKS__ <= 0x32FF @ cw9" \
+    "defined _MSC_VER && _MSC_VER < 1300 && !defined UNDER_CE @ vc6" \
+    "defined _MSC_VER && _MSC_VER < 1300 && defined UNDER_CE @ evc4" \
+    "defined __MWERKS__ && __MWERKS__ <= 0x31FF @ cw8"
+  do
+    boost_tag_test=`expr "X$i" : 'X\([[^@]]*\) @ '`
+    boost_tag=`expr "X$i" : 'X[[^@]]* @ \(.*\)'`
+    AC_COMPILE_IFELSE([AC_LANG_PROGRAM([[
+#if $boost_tag_test
+/* OK */
+#else
+# error $boost_tag_test
+#endif
+]])], [boost_cv_lib_tag=$boost_tag; break], [])
+  done
+AC_LANG_POP([C++])dnl
+  case $boost_cv_lib_tag in #(
+    # Some newer (>= 1.35?) versions of Boost seem to only use "gcc" as opposed
+    # to "gcc41" for instance.
+    *-gcc | *'-gcc ') :;; #(  Don't re-add -gcc: it's already in there.
+    gcc*)
+      boost_tag_x=
+      case $host_os in #(
+        darwin*)
+          if test $boost_major_version -ge 136; then
+            # The `x' added in r46793 of Boost.
+            boost_tag_x=x
+          fi;;
+      esac
+      # We can specify multiple tags in this variable because it's used by
+      # BOOST_FIND_LIB that does a `for tag in -$boost_cv_lib_tag' ...
+      boost_cv_lib_tag="$boost_tag_x$boost_cv_lib_tag -${boost_tag_x}gcc"
+      ;; #(
+    unknown)
+      AC_MSG_WARN([[could not figure out which toolset name to use for $CXX]])
+      boost_cv_lib_tag=
+      ;;
+  esac
+fi])dnl end of AC_CACHE_CHECK
+])# _BOOST_FIND_COMPILER_TAG
+
+
+# _BOOST_GUESS_WHETHER_TO_USE_MT()
+# --------------------------------
+# Compile a small test to try to guess whether we should favor MT (Multi
+# Thread) flavors of Boost.  Sets boost_guess_use_mt accordingly.
+AC_DEFUN([_BOOST_GUESS_WHETHER_TO_USE_MT],
+[# Check whether we do better use `mt' even though we weren't ask to.
+AC_COMPILE_IFELSE([AC_LANG_PROGRAM([[
+#if defined _REENTRANT || defined _MT || defined __MT__
+/* use -mt */
+#else
+# error MT not needed
+#endif
+]])], [boost_guess_use_mt=:], [boost_guess_use_mt=false])
+])
+
+# _BOOST_AC_LINK_IFELSE(PROGRAM, [ACTION-IF-TRUE], [ACTION-IF-FALSE])
+# -------------------------------------------------------------------
+# Fork of _AC_LINK_IFELSE that preserves conftest.o across calls.  Fragile,
+# will break when Autoconf changes its internals.  Requires that you manually
+# rm -f conftest.$ac_objext in between to really different tests, otherwise
+# you will try to link a conftest.o left behind by a previous test.
+# Used to aggressively optimize BOOST_FIND_LIB (see the big comment in this
+# macro).
+#
+# Don't use "break" in the actions, as it would short-circuit some code
+# this macro runs after the actions.
+m4_define([_BOOST_AC_LINK_IFELSE],
+[m4_ifvaln([$1], [AC_LANG_CONFTEST([$1])])dnl
+rm -f conftest$ac_exeext
+boost_save_ac_ext=$ac_ext
+boost_use_source=:
+# If we already have a .o, re-use it.  We change $ac_ext so that $ac_link
+# tries to link the existing object file instead of compiling from source.
+test -f conftest.$ac_objext && ac_ext=$ac_objext && boost_use_source=false &&
+  _AS_ECHO_LOG([re-using the existing conftest.$ac_objext])
+AS_IF([_AC_DO_STDERR($ac_link) && {
+	 test -z "$ac_[]_AC_LANG_ABBREV[]_werror_flag" ||
+	 test ! -s conftest.err
+       } && test -s conftest$ac_exeext && {
+	 test "$cross_compiling" = yes ||
+	 $as_executable_p conftest$ac_exeext
+dnl FIXME: use AS_TEST_X instead when 2.61 is widespread enough.
+       }],
+      [$2],
+      [if $boost_use_source; then
+         _AC_MSG_LOG_CONFTEST
+       fi
+       $3])
+ac_objext=$boost_save_ac_objext
+ac_ext=$boost_save_ac_ext
+dnl Delete also the IPA/IPO (Inter Procedural Analysis/Optimization)
+dnl information created by the PGI compiler (conftest_ipa8_conftest.oo),
+dnl as it would interfere with the next link command.
+rm -f core conftest.err conftest_ipa8_conftest.oo \
+      conftest$ac_exeext m4_ifval([$1], [conftest.$ac_ext])[]dnl
+])# _BOOST_AC_LINK_IFELSE
+
+# Local Variables:
+# mode: autoconf
+# End:
diff --git a/configure.ac b/configure.ac
index a36a38636..3ea9d3457 100644
--- a/configure.ac
+++ b/configure.ac
@@ -842,6 +842,23 @@ AC_CHECK_HEADERS([getopt.h unistd.h])
 #AC_TYPE_UINT64_T
 #AC_TYPE_SIZE_T
 
+AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
+
+# look for boost library, but don't make it a fatal error if not found
+cvc4_has_threads=maybe
+BOOST_REQUIRE([], [cvc4_has_threads=no])
+if test $cvc4_has_threads = no; then
+  AC_MSG_WARN([disabling multithreaded support])
+else
+  BOOST_THREADS
+  if test -n "$BOOST_THREAD_LIBS"; then
+    cvc4_has_threads=yes
+  else
+    AC_MSG_WARN([disabling multithreaded support])
+    cvc4_has_threads=no
+  fi
+fi
+
 # Whether to build compatibility library
 CVC4_BUILD_LIBCOMPAT=yes
 AC_ARG_WITH([compat],
@@ -859,18 +876,28 @@ AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes])
 # Check for availability of TLS support (e.g. __thread storage class)
 AC_MSG_CHECKING([whether to use compiler-supported TLS if available])
 AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS]))
-if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then
-  AC_MSG_RESULT([yes])
-  AX_TLS([CVC4_TLS=$ac_cv_tls], [CVC4_TLS=])
-else
-  AC_MSG_RESULT([no])
-  CVC4_TLS=
-fi
-if test -n "$CVC4_TLS"; then
+if test $cvc4_has_threads = no; then
+  # We disable TLS entirely by simply telling the build system that
+  # the empty string is the __thread keyword.
+  AC_MSG_RESULT([multithreading disabled])
   CVC4_TLS_SUPPORTED=1
+  CVC4_TLS=
+  CVC4_TLS_explanation='disabled (no multithreading support)'
 else
-  CVC4_TLS='pthread_getspecific()'
-  CVC4_TLS_SUPPORTED=0
+  if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then
+    AC_MSG_RESULT([yes])
+    AX_TLS([CVC4_TLS=$ac_cv_tls], [CVC4_TLS=])
+  else
+    AC_MSG_RESULT([no])
+    CVC4_TLS=
+  fi
+  if test -n "$CVC4_TLS"; then
+    CVC4_TLS_SUPPORTED=1
+    CVC4_TLS_explanation="$CVC4_TLS"
+  else
+    CVC4_TLS_explanation='pthread_getspecific()'
+    CVC4_TLS_SUPPORTED=0
+  fi
 fi
 AC_SUBST([CVC4_TLS])
 AC_SUBST([CVC4_TLS_SUPPORTED])
@@ -1001,6 +1028,16 @@ AC_CONFIG_FILES([
   m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | sort | sed 's,\.am$,,'])
 )
 
+if test $cvc4_has_threads = yes; then
+  support_multithreaded='with boost threading library'
+  AM_CONDITIONAL([CVC4_HAS_THREADS], [true])
+  AC_SUBST([CVC4_HAS_THREADS], 1)
+else
+  support_multithreaded='no'
+  AM_CONDITIONAL([CVC4_HAS_THREADS], [false])
+  AC_SUBST([CVC4_HAS_THREADS], 0)
+fi
+
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h])
@@ -1047,6 +1084,17 @@ normally suggest.  For full details of CLN and its license, please visit
 To build CVC4 with GMP instead (which is covered under the more permissive
 LGPL), configure --without-cln.
 
+WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
+WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
+
+Note that CLN is UNSAFE FOR USE in parallel contexts!
+This build of CVC4 cannot be used safely as a portfolio solver.
+since the result of building with CLN will include numerous race
+conditions on the refcounts internal to CLN.
+
+WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
+WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
+
 "
 else
   mplibrary='gmp (LGPL)'
@@ -1091,6 +1139,9 @@ Static binary: $enable_static_binary
 Compat lib   : $CVC4_BUILD_LIBCOMPAT
 Bindings     : ${CVC4_LANGUAGE_BINDINGS:-none}
 
+Multithreaded: $support_multithreaded
+TLS support  : $CVC4_TLS_explanation
+
 MP library   : $mplibrary
 
 CPPFLAGS     : $CPPFLAGS
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 6a070a88a..6baa4613f 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -28,6 +28,12 @@ libexpr_la_SOURCES = \
 	declaration_scope.cpp \
 	expr_manager_scope.h \
 	node_self_iterator.h \
+	variable_type_map.h \
+	pickle_data.h \
+	pickle_data.cpp \
+	pickler.h \
+	pickler.cpp \
+	node_self_iterator.h \
 	expr_stream.h \
 	kind_map.h
 
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 7d060186a..ba29b6c34 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -126,6 +126,10 @@ void EmptyCommand::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
+Command* EmptyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  return new EmptyCommand(d_name);
+}
+
 /* class AssertCommand */
 
 AssertCommand::AssertCommand(const BoolExpr& e) throw() :
@@ -145,6 +149,10 @@ void AssertCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
+Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  return new AssertCommand(d_expr.exportTo(exprManager, variableMap));
+}
+
 /* class PushCommand */
 
 void PushCommand::invoke(SmtEngine* smtEngine) throw() {
@@ -156,6 +164,10 @@ void PushCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
+Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  return new PushCommand;
+}
+
 /* class PopCommand */
 
 void PopCommand::invoke(SmtEngine* smtEngine) throw() {
@@ -173,6 +185,12 @@ CheckSatCommand::CheckSatCommand() throw() :
   d_expr() {
 }
 
+Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  return new PopCommand();
+}
+
+/* class CheckSatCommand */
+
 CheckSatCommand::CheckSatCommand(const BoolExpr& expr) throw() :
   d_expr(expr) {
 }
@@ -202,6 +220,12 @@ void CheckSatCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap));
+  c->d_result = d_result;
+  return c;
+}
+
 /* class QueryCommand */
 
 QueryCommand::QueryCommand(const BoolExpr& e) throw() :
@@ -233,6 +257,12 @@ void QueryCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap));
+  c->d_result = d_result;
+  return c;
+}
+
 /* class QuitCommand */
 
 QuitCommand::QuitCommand() throw() {
@@ -243,6 +273,10 @@ void QuitCommand::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
+Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  return new QuitCommand();
+}
+
 /* class CommentCommand */
 
 CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) {
@@ -257,6 +291,10 @@ void CommentCommand::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
+Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  return new CommentCommand(d_comment);
+}
+
 /* class CommandSequence */
 
 CommandSequence::CommandSequence() throw() :
@@ -299,6 +337,15 @@ CommandSequence::const_iterator CommandSequence::begin() const throw() {
   return d_commandSequence.begin();
 }
 
+Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  CommandSequence* seq = new CommandSequence();
+  for(iterator i = begin(); i != end(); ++i) {
+    seq->addCommand((*i)->exportTo(exprManager, variableMap));
+  }
+  seq->d_index = d_index;
+  return seq;
+}
+
 CommandSequence::const_iterator CommandSequence::end() const throw() {
   return d_commandSequence.end();
 }
@@ -338,6 +385,12 @@ void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("declarations") << *this << endl;
 }
 
+Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager,
+                                          ExprManagerMapCollection& variableMap) {
+  return new DeclareFunctionCommand(d_symbol,
+                                    d_type.exportTo(exprManager, variableMap));
+}
+
 /* class DeclareTypeCommand */
 
 DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() :
@@ -358,6 +411,12 @@ void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("declarations") << *this << endl;
 }
 
+Command* DeclareTypeCommand::exportTo(ExprManager* exprManager,
+                                      ExprManagerMapCollection& variableMap) {
+  return new DeclareTypeCommand(d_symbol, d_arity,
+                                d_type.exportTo(exprManager, variableMap));
+}
+
 /* class DefineTypeCommand */
 
 DefineTypeCommand::DefineTypeCommand(const std::string& id,
@@ -388,6 +447,14 @@ void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
+Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  vector<Type> params;
+  transform(d_params.begin(), d_params.end(), back_inserter(params),
+            ExportTransformer(exprManager, variableMap));
+  Type type = d_type.exportTo(exprManager, variableMap);
+  return new DefineTypeCommand(d_symbol, params, type);
+}
+
 /* class DefineFunctionCommand */
 
 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
@@ -429,6 +496,15 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
+Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  Expr func = d_func.exportTo(exprManager, variableMap);
+  vector<Expr> formals;
+  transform(d_formals.begin(), d_formals.end(), back_inserter(formals),
+            ExportTransformer(exprManager, variableMap));
+  Expr formula = d_formula.exportTo(exprManager, variableMap);
+  return new DefineFunctionCommand(d_symbol, func, formals, formula);
+}
+
 /* class DefineNamedFunctionCommand */
 
 DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id,
@@ -446,6 +522,15 @@ void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
+Command* DefineNamedFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  Expr func = d_func.exportTo(exprManager, variableMap);
+  vector<Expr> formals;
+  transform(d_formals.begin(), d_formals.end(), back_inserter(formals),
+            ExportTransformer(exprManager, variableMap));
+  Expr formula = d_formula.exportTo(exprManager, variableMap);
+  return new DefineNamedFunctionCommand(d_symbol, func, formals, formula);
+}
+
 /* class Simplify */
 
 SimplifyCommand::SimplifyCommand(Expr term) throw() :
@@ -473,6 +558,12 @@ void SimplifyCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* SimplifyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  SimplifyCommand* c = new SimplifyCommand(d_term.exportTo(exprManager, variableMap));
+  c->d_result = d_result.exportTo(exprManager, variableMap);
+  return c;
+}
+
 /* class GetValueCommand */
 
 GetValueCommand::GetValueCommand(Expr term) throw() :
@@ -505,6 +596,12 @@ void GetValueCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetValueCommand* c = new GetValueCommand(d_term.exportTo(exprManager, variableMap));
+  c->d_result = d_result.exportTo(exprManager, variableMap);
+  return c;
+}
+
 /* class GetAssignmentCommand */
 
 GetAssignmentCommand::GetAssignmentCommand() throw() {
@@ -531,6 +628,12 @@ void GetAssignmentCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetAssignmentCommand* c = new GetAssignmentCommand;
+  c->d_result = d_result;
+  return c;
+}
+
 /* class GetProofCommand */
 
 GetProofCommand::GetProofCommand() throw() {
@@ -557,6 +660,12 @@ void GetProofCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetProofCommand* c = new GetProofCommand;
+  c->d_result = d_result;
+  return c;
+}
+
 /* class GetAssertionsCommand */
 
 GetAssertionsCommand::GetAssertionsCommand() throw() {
@@ -586,6 +695,12 @@ void GetAssertionsCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetAssertionsCommand* c = new GetAssertionsCommand;
+  c->d_result = d_result;
+  return c;
+}
+
 /* class SetBenchmarkStatusCommand */
 
 SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() :
@@ -608,6 +723,11 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
+Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  SetBenchmarkStatusCommand* c = new SetBenchmarkStatusCommand(d_status);
+  return c;
+}
+
 /* class SetBenchmarkLogicCommand */
 
 SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() :
@@ -627,6 +747,11 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
+Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  SetBenchmarkLogicCommand* c = new SetBenchmarkLogicCommand(d_logic);
+  return c;
+}
+
 /* class SetInfoCommand */
 
 SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() :
@@ -653,6 +778,11 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
+Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  SetInfoCommand* c = new SetInfoCommand(d_flag, d_sexpr);
+  return c;
+}
+
 /* class GetInfoCommand */
 
 GetInfoCommand::GetInfoCommand(std::string flag) throw() :
@@ -688,6 +818,12 @@ void GetInfoCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetInfoCommand* c = new GetInfoCommand(d_flag);
+  c->d_result = d_result;
+  return c;
+}
+
 /* class SetOptionCommand */
 
 SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() :
@@ -714,6 +850,11 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
+Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  SetOptionCommand* c = new SetOptionCommand(d_flag, d_sexpr);
+  return c;
+}
+
 /* class GetOptionCommand */
 
 GetOptionCommand::GetOptionCommand(std::string flag) throw() :
@@ -747,6 +888,12 @@ void GetOptionCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetOptionCommand* c = new GetOptionCommand(d_flag);
+  c->d_result = d_result;
+  return c;
+}
+
 /* class DatatypeDeclarationCommand */
 
 DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() :
@@ -768,6 +915,11 @@ void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
+Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  std::cout << "We currently do not support exportTo with Datatypes" << std::endl;
+  exit(1);
+  return NULL;
+}
 /* output stream insertion operator for benchmark statuses */
 std::ostream& operator<<(std::ostream& out,
                          BenchmarkStatus status) throw() {
diff --git a/src/expr/command.h b/src/expr/command.h
index cf8c1b615..2d87fefc2 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -32,6 +32,7 @@
 
 #include "expr/expr.h"
 #include "expr/type.h"
+#include "expr/variable_type_map.h"
 #include "util/result.h"
 #include "util/sexpr.h"
 #include "util/datatype.h"
@@ -177,6 +178,10 @@ public:
 };/* class CommandFailure */
 
 class CVC4_PUBLIC Command {
+  // intentionally not permitted
+  Command(const Command&) CVC4_UNDEFINED;
+  Command& operator=(const Command&) CVC4_UNDEFINED;
+
 protected:
   /**
    * This field contains a command status if the command has been
@@ -210,6 +215,29 @@ public:
 
   virtual void printResult(std::ostream& out) const throw();
 
+  /**
+   * Maps this Command into one for a different ExprManager, using
+   * variableMap for the translation and extending it with any new
+   * mappings.
+   */
+  virtual Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) = 0;
+
+protected:
+  class ExportTransformer {
+    ExprManager* d_exprManager;
+    ExprManagerMapCollection& d_variableMap;
+  public:
+    ExportTransformer(ExprManager* exprManager, ExprManagerMapCollection& variableMap) :
+      d_exprManager(exprManager),
+      d_variableMap(variableMap) {
+    }
+    Expr operator()(Expr e) {
+      return e.exportTo(d_exprManager, d_variableMap);
+    }
+    Type operator()(Type t) {
+      return t.exportTo(d_exprManager, d_variableMap);
+    }
+  };/* class Command::ExportTransformer */
 };/* class Command */
 
 /**
@@ -224,6 +252,7 @@ public:
   ~EmptyCommand() throw() {}
   std::string getName() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class EmptyCommand */
 
 class CVC4_PUBLIC AssertCommand : public Command {
@@ -234,18 +263,21 @@ public:
   ~AssertCommand() throw() {}
   BoolExpr getExpr() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class AssertCommand */
 
 class CVC4_PUBLIC PushCommand : public Command {
 public:
   ~PushCommand() throw() {}
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class PushCommand */
 
 class CVC4_PUBLIC PopCommand : public Command {
 public:
   ~PopCommand() throw() {}
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class PopCommand */
 
 class CVC4_PUBLIC DeclarationDefinitionCommand : public Command {
@@ -265,6 +297,7 @@ public:
   ~DeclareFunctionCommand() throw() {}
   Type getType() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class DeclareFunctionCommand */
 
 class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand {
@@ -277,6 +310,7 @@ public:
   size_t getArity() const throw();
   Type getType() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class DeclareTypeCommand */
 
 class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand {
@@ -290,6 +324,7 @@ public:
   const std::vector<Type>& getParameters() const throw();
   Type getType() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class DefineTypeCommand */
 
 class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand {
@@ -306,6 +341,7 @@ public:
   const std::vector<Expr>& getFormals() const throw();
   Expr getFormula() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class DefineFunctionCommand */
 
 /**
@@ -318,6 +354,7 @@ public:
   DefineNamedFunctionCommand(const std::string& id, Expr func,
                              const std::vector<Expr>& formals, Expr formula) throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class DefineNamedFunctionCommand */
 
 class CVC4_PUBLIC CheckSatCommand : public Command {
@@ -332,6 +369,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   Result getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class CheckSatCommand */
 
 class CVC4_PUBLIC QueryCommand : public Command {
@@ -345,6 +383,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   Result getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class QueryCommand */
 
 // this is TRANSFORM in the CVC presentation language
@@ -359,6 +398,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   Expr getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class SimplifyCommand */
 
 class CVC4_PUBLIC GetValueCommand : public Command {
@@ -372,6 +412,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   Expr getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class GetValueCommand */
 
 class CVC4_PUBLIC GetAssignmentCommand : public Command {
@@ -383,6 +424,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   SExpr getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class GetAssignmentCommand */
 
 class CVC4_PUBLIC GetProofCommand : public Command {
@@ -394,6 +436,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   Proof* getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class GetProofCommand */
 
 class CVC4_PUBLIC GetAssertionsCommand : public Command {
@@ -405,6 +448,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   std::string getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class GetAssertionsCommand */
 
 class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
@@ -415,6 +459,7 @@ public:
   ~SetBenchmarkStatusCommand() throw() {}
   BenchmarkStatus getStatus() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class SetBenchmarkStatusCommand */
 
 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
@@ -425,6 +470,7 @@ public:
   ~SetBenchmarkLogicCommand() throw() {}
   std::string getLogic() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class SetBenchmarkLogicCommand */
 
 class CVC4_PUBLIC SetInfoCommand : public Command {
@@ -437,6 +483,7 @@ public:
   std::string getFlag() const throw();
   SExpr getSExpr() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class SetInfoCommand */
 
 class CVC4_PUBLIC GetInfoCommand : public Command {
@@ -450,6 +497,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   std::string getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class GetInfoCommand */
 
 class CVC4_PUBLIC SetOptionCommand : public Command {
@@ -462,6 +510,7 @@ public:
   std::string getFlag() const throw();
   SExpr getSExpr() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class SetOptionCommand */
 
 class CVC4_PUBLIC GetOptionCommand : public Command {
@@ -475,6 +524,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   std::string getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class GetOptionCommand */
 
 class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
@@ -486,6 +536,7 @@ public:
   DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw();
   const std::vector<DatatypeType>& getDatatypes() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class DatatypeDeclarationCommand */
 
 class CVC4_PUBLIC QuitCommand : public Command {
@@ -493,6 +544,7 @@ public:
   QuitCommand() throw();
   ~QuitCommand() throw() {}
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class QuitCommand */
 
 class CVC4_PUBLIC CommentCommand : public Command {
@@ -502,6 +554,7 @@ public:
   ~CommentCommand() throw() {}
   std::string getComment() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class CommentCommand */
 
 class CVC4_PUBLIC CommandSequence : public Command {
@@ -528,6 +581,7 @@ public:
   iterator begin() throw();
   iterator end() throw();
 
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class CommandSequence */
 
 class CVC4_PUBLIC DeclarationSequence : public CommandSequence {
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 576d0324d..83a80ed13 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -18,6 +18,7 @@
 
 #include "expr/node_manager.h"
 #include "expr/expr_manager.h"
+#include "expr/variable_type_map.h"
 #include "context/context.h"
 #include "util/options.h"
 #include "util/stats.h"
@@ -30,7 +31,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 34 "${template}"
+#line 35 "${template}"
 
 #ifdef CVC4_STATISTICS_ON
   #define INC_STAT(kind) \
@@ -829,6 +830,52 @@ Context* ExprManager::getContext() const {
   return d_ctxt;
 }
 
+namespace expr {
+
+Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
+
+TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, ExprManagerMapCollection& vmap) {
+  Debug("export") << "type: " << n << std::endl;
+  Assert(n.getKind() == kind::SORT_TYPE ||
+         n.getMetaKind() != kind::metakind::PARAMETERIZED,
+         "PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
+  if(n.getKind() == kind::TYPE_CONSTANT) {
+    return to->mkTypeConst(n.getConst<TypeConstant>());
+  } else if(n.getKind() == kind::BITVECTOR_TYPE) {
+    return to->mkBitVectorType(n.getConst<BitVectorSize>());
+  }
+  Type from_t = from->toType(n);
+  Type& to_t = vmap.d_typeMap[from_t];
+  if(! to_t.isNull()) {
+    Debug("export") << "+ mapped `" << from_t << "' to `" << to_t << "'" << std::endl;
+    return *Type::getTypeNode(to_t);
+  }
+  NodeBuilder<> children(to, n.getKind());
+  if(n.getKind() == kind::SORT_TYPE) {
+    Debug("export") << "type: operator: " << n.getOperator() << std::endl;
+    // make a new sort tag in target node manager
+    Node sortTag = NodeBuilder<0>(to, kind::SORT_TAG);
+    children << sortTag;
+  }
+  for(TypeNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
+    Debug("export") << "type: child: " << *i << std::endl;
+    children << exportTypeInternal(*i, from, to, vmap);
+  }
+  TypeNode out = children.constructTypeNode();// FIXME thread safety
+  to_t = to->toType(out);
+  return out;
+}/* exportTypeInternal() */
+
+}/* CVC4::expr namespace */
+
+Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap) {
+  Assert(t.d_nodeManager != em->d_nodeManager,
+         "Can't export a Type to the same ExprManager");
+  NodeManagerScope ems(t.d_nodeManager);
+  return Type(em->d_nodeManager,
+              new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap)));
+}
+
 ${mkConst_implementations}
 
 }/* CVC4 namespace */
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 81d30fd1e..eecb40f3e 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -42,6 +42,13 @@ class SmtEngine;
 class NodeManager;
 struct Options;
 class IntStat;
+class ExprManagerMapCollection;
+
+namespace expr {
+  namespace pickle {
+    class Pickler;
+  }/* CVC4::expr::pickle namespace */
+}/* CVC4::expr namespace */
 
 namespace context {
   class Context;
@@ -404,6 +411,11 @@ public:
   Expr mkVar(const std::string& name, Type type);
   Expr mkVar(Type type);
 
+  /** Export an expr to a different ExprManager */
+  //static Expr exportExpr(const Expr& e, ExprManager* em);
+  /** Export a type to a different ExprManager */
+  static Type exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap);
+
   /** Returns the minimum arity of the given kind. */
   static unsigned minArity(Kind kind);
 
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 3c376f632..c510ce381 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -19,8 +19,10 @@
 #include "expr/expr.h"
 #include "expr/node.h"
 #include "expr/expr_manager_scope.h"
+#include "expr/variable_type_map.h"
 #include "util/Assert.h"
 
+#include <vector>
 #include <iterator>
 #include <utility>
 
@@ -30,7 +32,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 34 "${template}"
+#line 36 "${template}"
 
 using namespace CVC4::kind;
 using namespace std;
@@ -105,6 +107,72 @@ ExprManager* Expr::getExprManager() const {
   return d_exprManager;
 }
 
+namespace expr {
+
+static Node exportConstant(TNode n, NodeManager* to);
+
+Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap) {
+  if(n.getMetaKind() == kind::metakind::CONSTANT) {
+    return exportConstant(n, NodeManager::fromExprManager(to));
+  } else if(n.getMetaKind() == kind::metakind::VARIABLE) {
+    Expr from_e(from, new Node(n));
+    Expr& to_e = vmap.d_typeMap[from_e];
+    if(! to_e.isNull()) {
+Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::endl;
+      return to_e.getNode();
+    } else {
+      // construct new variable in other manager:
+      // to_e is a ref, so this inserts from_e -> to_e
+      std::string name;
+      Type type = from->exportType(from_e.getType(), to, vmap);
+      if(Node::fromExpr(from_e).getAttribute(VarNameAttr(), name)) {
+        to_e = to->mkVar(name, type);// FIXME thread safety
+Debug("export") << "+ exported var `" << from_e << "'[" << from_e.getId() << "] with name `" << name << "' and type `" << from_e.getType() << "' to `" << to_e << "'[" << to_e.getId() << "] with type `" << type << "'" << std::endl;
+      } else {
+        to_e = to->mkVar(type);// FIXME thread safety
+Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << from_e.getType() << "' to `" << to_e << "' with type `" << type << "'" << std::endl;
+      }
+      uint64_t to_int = (uint64_t)(to_e.getNode().d_nv);
+      uint64_t from_int = (uint64_t)(from_e.getNode().d_nv);
+      vmap.d_from[to_int] = from_int;
+      vmap.d_to[from_int] = to_int;
+      vmap.d_typeMap[to_e] = from_e;// insert other direction too
+      return Node::fromExpr(to_e);
+    }
+  } else {
+    std::vector<Node> children;
+Debug("export") << "n: " << n << std::endl;
+    if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+Debug("export") << "+ parameterized, op is " << n.getOperator() << std::endl;
+      children.reserve(n.getNumChildren() + 1);
+      children.push_back(exportInternal(n.getOperator(), from, to, vmap));
+    } else {
+      children.reserve(n.getNumChildren());
+    }
+    for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
+Debug("export") << "+ child: " << *i << std::endl;
+      children.push_back(exportInternal(*i, from, to, vmap));
+    }
+    if(Debug.isOn("export")) {
+      ExprManagerScope ems(*to);
+      Debug("export") << "children for export from " << n << std::endl;
+      for(std::vector<Node>::iterator i = children.begin(), i_end = children.end(); i != i_end; ++i) {
+        Debug("export") << "  child: " << *i << std::endl;
+      }
+    }
+    return NodeManager::fromExprManager(to)->mkNode(n.getKind(), children);// FIXME thread safety
+  }
+}/* exportInternal() */
+
+}/* CVC4::expr namespace */
+
+Expr Expr::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  Assert(d_exprManager != exprManager,
+         "No sense in cloning an Expr in the same ExprManager");
+  ExprManagerScope ems(*this);
+  return Expr(exprManager, new Node(expr::exportInternal(*d_node, d_exprManager, exprManager, variableMap)));
+}
+
 Expr& Expr::operator=(const Expr& e) {
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
@@ -449,4 +517,16 @@ void Expr::debugPrint() {
 
 ${getConst_implementations}
 
+namespace expr {
+
+static Node exportConstant(TNode n, NodeManager* to) {
+  Assert(n.getMetaKind() == kind::metakind::CONSTANT);
+  switch(n.getKind()) {
+${exportConstant_cases}
+
+  default: Unhandled(n.getKind());
+  }
+}/* exportConstant() */
+
+}/* CVC4::expr namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index b54ec20d4..56396da01 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -49,6 +49,8 @@ namespace CVC4 {
 template <bool ref_count>
 class NodeTemplate;
 
+class NodeManager;
+
 class Expr;
 class ExprManager;
 class SmtEngine;
@@ -56,6 +58,20 @@ class Type;
 class TypeCheckingException;
 class TypeCheckingExceptionPrivate;
 
+namespace expr {
+  namespace pickle {
+    class Pickler;
+  }/* CVC4::expr::pickle namespace */
+}/* CVC4::expr namespace */
+
+namespace prop {
+  class SatSolver;
+}/* CVC4::prop namespace */
+
+class ExprManagerMapCollection;
+
+struct ExprHashFunction;
+
 namespace smt {
   class SmtEnginePrivate;
 }/* CVC4::smt namespace */
@@ -64,6 +80,8 @@ namespace expr {
   class CVC4_PUBLIC ExprSetDepth;
   class CVC4_PUBLIC ExprPrintTypes;
   class CVC4_PUBLIC ExprSetLanguage;
+
+  NodeTemplate<true> exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
 }/* CVC4::expr namespace */
 
 /**
@@ -437,6 +455,13 @@ public:
   ExprManager* getExprManager() const;
 
   /**
+   * Maps this Expr into one for a different ExprManager, using
+   * variableMap for the translation and extending it with any new
+   * mappings.
+   */
+  Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+
+  /**
    * IOStream manipulator to set the maximum depth of Exprs when
    * pretty-printing.  -1 means print to any depth.  E.g.:
    *
@@ -510,6 +535,10 @@ protected:
   friend class ExprManager;
   friend class NodeManager;
   friend class TypeCheckingException;
+  friend class expr::pickle::Pickler;
+  friend class prop::SatSolver;
+  friend NodeTemplate<true> expr::exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
+
   friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e);
   template <bool ref_count> friend class NodeTemplate;
 
@@ -828,7 +857,7 @@ public:
 
 ${getConst_instantiations}
 
-#line 832 "${template}"
+#line 861 "${template}"
 
 namespace expr {
 
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 69f7019ab..0cae68ed0 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -60,6 +60,7 @@ getConst_instantiations=
 getConst_implementations=
 mkConst_instantiations=
 mkConst_implementations=
+exportConstant_cases=
 
 seen_theory=false
 seen_theory_builtin=false
@@ -193,6 +194,8 @@ template <> $2 const & Expr::getConst() const {
   return d_node->getConst< $2 >();
 }
 "
+  exportConstant_cases="${exportConstant_cases}
+  case $1: return to->mkConst(n.getConst< $2 >());"
 }
 
 function check_theory_seen {
@@ -244,6 +247,7 @@ for var in \
     getConst_implementations \
     mkConst_instantiations \
     mkConst_implementations \
+    exportConstant_cases \
     typechecker_includes \
     typerules \
     ; do
diff --git a/src/expr/node.h b/src/expr/node.h
index 57b02b05b..37499c3bf 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -49,6 +49,12 @@ namespace CVC4 {
 class TypeNode;
 class NodeManager;
 
+namespace expr {
+  namespace pickle {
+    class PicklerPrivate;
+  }/* CVC4::expr::pickle namespace */
+}/* CVC4::expr namespace */
+
 template <bool ref_count>
 class NodeTemplate;
 
@@ -177,6 +183,9 @@ class NodeTemplate {
    */
   friend class expr::NodeValue;
 
+  friend class expr::pickle::PicklerPrivate;
+  friend Node expr::exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
+
   /** A convenient null-valued encapsulated pointer */
   static NodeTemplate s_null;
 
@@ -200,6 +209,7 @@ class NodeTemplate {
 
   friend class NodeTemplate<true>;
   friend class NodeTemplate<false>;
+  friend class TypeNode;
   friend class NodeManager;
 
   template <unsigned nchild_thresh>
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index ded7ad8fe..c5d41816e 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -928,7 +928,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
     // reference counts in this case.
     nv->d_nchildren = 0;
     nv->d_kind = d_nv->d_kind;
-    nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+    nv->d_id = d_nm->next_id++;// FIXME multithreading
     nv->d_rc = 0;
     setUsed();
     if(Debug.isOn("gc")) {
@@ -1015,7 +1015,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
       }
       nv->d_nchildren = d_inlineNv.d_nchildren;
       nv->d_kind = d_inlineNv.d_kind;
-      nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+      nv->d_id = d_nm->next_id++;// FIXME multithreading
       nv->d_rc = 0;
 
       std::copy(d_inlineNv.d_children,
@@ -1069,7 +1069,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
 
       crop();
       expr::NodeValue* nv = d_nv;
-      nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+      nv->d_id = d_nm->next_id++;// FIXME multithreading
       d_nv = &d_inlineNv;
       d_nvMaxChildren = nchild_thresh;
       setUsed();
@@ -1118,7 +1118,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
     // reference counts in this case.
     nv->d_nchildren = 0;
     nv->d_kind = d_nv->d_kind;
-    nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+    nv->d_id = d_nm->next_id++;// FIXME multithreading
     nv->d_rc = 0;
     Debug("gc") << "creating node value " << nv
                 << " [" << nv->d_id << "]: " << *nv << "\n";
@@ -1194,7 +1194,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
       }
       nv->d_nchildren = d_inlineNv.d_nchildren;
       nv->d_kind = d_inlineNv.d_kind;
-      nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+      nv->d_id = d_nm->next_id++;// FIXME multithreading
       nv->d_rc = 0;
 
       std::copy(d_inlineNv.d_children,
@@ -1248,7 +1248,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
       }
       nv->d_nchildren = d_nv->d_nchildren;
       nv->d_kind = d_nv->d_kind;
-      nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+      nv->d_id = d_nm->next_id++;// FIXME multithreading
       nv->d_rc = 0;
 
       std::copy(d_nv->d_children,
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 2bf0a864a..1d4b7d3d1 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -84,6 +84,7 @@ NodeManager::NodeManager(context::Context* ctxt,
   d_optionsAllocated(new Options()),
   d_options(d_optionsAllocated),
   d_statisticsRegistry(new StatisticsRegistry()),
+  next_id(0),
   d_attrManager(ctxt),
   d_exprManager(exprManager),
   d_nodeUnderDeletion(NULL),
@@ -98,6 +99,7 @@ NodeManager::NodeManager(context::Context* ctxt,
   d_optionsAllocated(NULL),
   d_options(&options),
   d_statisticsRegistry(new StatisticsRegistry()),
+  next_id(0),
   d_attrManager(ctxt),
   d_exprManager(exprManager),
   d_nodeUnderDeletion(NULL),
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 3646e91c5..e446b7d71 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -88,6 +88,8 @@ class NodeManager {
 
   NodeValuePool d_nodeValuePool;
 
+  size_t next_id;
+
   expr::attr::AttributeManager d_attrManager;
 
   /** The associated ExprManager */
@@ -503,6 +505,60 @@ public:
                            const AttrKind& attr,
                            const typename AttrKind::value_type& value);
 
+  /**
+   * Retrieve an attribute for a TypeNode.
+   *
+   * @param n the type node
+   * @param attr an instance of the attribute kind to retrieve.
+   * @returns the attribute, if set, or a default-constructed
+   * <code>AttrKind::value_type</code> if not.
+   */
+  template <class AttrKind>
+  inline typename AttrKind::value_type
+  getAttribute(TypeNode n, const AttrKind& attr) const;
+
+  /**
+   * Check whether an attribute is set for a TypeNode.
+   *
+   * @param n the type node
+   * @param attr an instance of the attribute kind to check
+   * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+   */
+  template <class AttrKind>
+  inline bool hasAttribute(TypeNode n,
+                           const AttrKind& attr) const;
+
+  /**
+   * Check whether an attribute is set for a TypeNode and, if so, retieve
+   * it.
+   *
+   * @param n the type node
+   * @param attr an instance of the attribute kind to check
+   * @param value a reference to an object of the attribute's value type.
+   * <code>value</code> will be set to the value of the attribute, if it is
+   * set for <code>nv</code>; otherwise, it will be set to the default value of
+   * the attribute.
+   * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+   */
+  template <class AttrKind>
+  inline bool getAttribute(TypeNode n,
+                           const AttrKind& attr,
+                           typename AttrKind::value_type& value) const;
+
+  /**
+   * Set an attribute for a type node.  If the node doesn't have the
+   * attribute, this function assigns one.  If the type node has one,
+   * this overwrites it.
+   *
+   * @param n the type node
+   * @param attr an instance of the attribute kind to set
+   * @param value the value of <code>attr</code> for <code>n</code>
+   */
+  template <class AttrKind>
+  inline void setAttribute(TypeNode n,
+                           const AttrKind& attr,
+                           const typename AttrKind::value_type& value);
+
   /** Get the (singleton) type for Booleans. */
   inline TypeNode booleanType();
 
@@ -762,6 +818,32 @@ NodeManager::setAttribute(TNode n, const AttrKind&,
   d_attrManager.setAttribute(n.d_nv, AttrKind(), value);
 }
 
+template <class AttrKind>
+inline typename AttrKind::value_type
+NodeManager::getAttribute(TypeNode n, const AttrKind&) const {
+  return d_attrManager.getAttribute(n.d_nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool
+NodeManager::hasAttribute(TypeNode n, const AttrKind&) const {
+  return d_attrManager.hasAttribute(n.d_nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool
+NodeManager::getAttribute(TypeNode n, const AttrKind&,
+                          typename AttrKind::value_type& ret) const {
+  return d_attrManager.getAttribute(n.d_nv, AttrKind(), ret);
+}
+
+template <class AttrKind>
+inline void
+NodeManager::setAttribute(TypeNode n, const AttrKind&,
+                          const typename AttrKind::value_type& value) {
+  d_attrManager.setAttribute(n.d_nv, AttrKind(), value);
+}
+
 
 /** Get the (singleton) type for booleans. */
 inline TypeNode NodeManager::booleanType() {
@@ -965,7 +1047,7 @@ inline TypeNode NodeManager::mkSort() {
 
 inline TypeNode NodeManager::mkSort(const std::string& name) {
   TypeNode type = mkSort();
-  type.setAttribute(expr::VarNameAttr(), name);
+  setAttribute(type, expr::VarNameAttr(), name);
   return type;
 }
 
@@ -986,7 +1068,7 @@ inline TypeNode NodeManager::mkSort(TypeNode constructor,
   nb << sortTag;
   nb.append(children);
   TypeNode type = nb.constructTypeNode();
-  type.setAttribute(expr::VarNameAttr(), name);
+  setAttribute(type, expr::VarNameAttr(), name);
   return type;
 }
 
@@ -997,8 +1079,8 @@ inline TypeNode NodeManager::mkSortConstructor(const std::string& name,
   Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
   nb << sortTag;
   TypeNode type = nb.constructTypeNode();
-  type.setAttribute(expr::VarNameAttr(), name);
-  type.setAttribute(expr::SortArityAttr(), arity);
+  setAttribute(type, expr::VarNameAttr(), name);
+  setAttribute(type, expr::SortArityAttr(), arity);
   return type;
 }
 
@@ -1211,37 +1293,37 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind,
 
 inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) {
   Node n = mkVar(type);
-  n.setAttribute(TypeAttr(), type);
-  n.setAttribute(expr::VarNameAttr(), name);
+  setAttribute(n, TypeAttr(), type);
+  setAttribute(n, expr::VarNameAttr(), name);
   return n;
 }
 
 inline Node* NodeManager::mkVarPtr(const std::string& name,
                                    const TypeNode& type) {
   Node* n = mkVarPtr(type);
-  n->setAttribute(TypeAttr(), type);
-  n->setAttribute(expr::VarNameAttr(), name);
+  setAttribute(*n, TypeAttr(), type);
+  setAttribute(*n, expr::VarNameAttr(), name);
   return n;
 }
 
 inline Node NodeManager::mkVar(const TypeNode& type) {
   Node n = NodeBuilder<0>(this, kind::VARIABLE);
-  n.setAttribute(TypeAttr(), type);
-  n.setAttribute(TypeCheckedAttr(), true);
+  setAttribute(n, TypeAttr(), type);
+  setAttribute(n, TypeCheckedAttr(), true);
   return n;
 }
 
 inline Node* NodeManager::mkVarPtr(const TypeNode& type) {
   Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
-  n->setAttribute(TypeAttr(), type);
-  n->setAttribute(TypeCheckedAttr(), true);
+  setAttribute(*n, TypeAttr(), type);
+  setAttribute(*n, TypeCheckedAttr(), true);
   return n;
 }
 
 inline Node NodeManager::mkSkolem(const TypeNode& type) {
   Node n = NodeBuilder<0>(this, kind::SKOLEM);
-  n.setAttribute(TypeAttr(), type);
-  n.setAttribute(TypeCheckedAttr(), true);
+  setAttribute(n, TypeAttr(), type);
+  setAttribute(n, TypeCheckedAttr(), true);
   return n;
 }
 
@@ -1282,7 +1364,7 @@ NodeClass NodeManager::mkConstInternal(const T& val) {
 
   nv->d_nchildren = 0;
   nv->d_kind = kind::metakind::ConstantMap<T>::kind;
-  nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+  nv->d_id = next_id++;// FIXME multithreading
   nv->d_rc = 0;
 
   //OwningTheory::mkConst(val);
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 89ac7ffca..970d2e0fc 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -33,8 +33,6 @@ using namespace std;
 namespace CVC4 {
 namespace expr {
 
-size_t NodeValue::next_id = 1;
-
 NodeValue NodeValue::s_null(0);
 
 string NodeValue::toString() const {
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 95af57719..e5ecfbc48 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -126,8 +126,6 @@ class NodeValue {
   void inc();
   void dec();
 
-  static size_t next_id;
-
   /**
    * Uninitializing constructor for NodeBuilder's use.
    */
diff --git a/src/expr/pickle_data.cpp b/src/expr/pickle_data.cpp
new file mode 100644
index 000000000..1de8f2cf7
--- /dev/null
+++ b/src/expr/pickle_data.cpp
@@ -0,0 +1,60 @@
+/*********************                                                        */
+/*! \file pickle_data.cpp
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: taking, mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a "pickle" for expressions, CVC4-internal view
+ **
+ ** This is the CVC4-internal view (private data structure) for a
+ ** "pickle" for expressions.  The public-facing view is a "Pickle",
+ ** which just points to a PickleData.  A pickle is a binary
+ ** serialization of an expression that can be converted back into an
+ ** expression in the same or another ExprManager.
+ **/
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#include "expr/pickle_data.h"
+#include "expr/expr.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "expr/node_value.h"
+#include "expr/expr_manager_scope.h"
+#include "expr/variable_type_map.h"
+#include "util/Assert.h"
+#include "expr/kind.h"
+#include "expr/metakind.h"
+
+namespace CVC4 {
+namespace expr {
+namespace pickle {
+
+void PickleData::writeToStringStream(std::ostringstream& oss) const {
+  BlockDeque::const_iterator i = d_blocks.begin(), end = d_blocks.end();
+  for(; i != end; ++i) {
+    Block b = *i;
+    Assert(sizeof(b) * 8 == NBITS_BLOCK);
+    oss << b.d_body.d_data << " ";
+  }
+}
+
+std::string PickleData::toString() const {
+  std::ostringstream oss;
+  oss.flags(std::ios::oct | std::ios::showbase);
+  writeToStringStream(oss);
+  return oss.str();
+}
+
+}/* CVC4::expr::pickle namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
diff --git a/src/expr/pickle_data.h b/src/expr/pickle_data.h
new file mode 100644
index 000000000..dab6e56c3
--- /dev/null
+++ b/src/expr/pickle_data.h
@@ -0,0 +1,122 @@
+/*********************                                                        */
+/*! \file pickle_data.h
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: taking, mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a "pickle" for expressions, CVC4-internal view
+ **
+ ** This is the CVC4-internal view (private data structure) for a
+ ** "pickle" for expressions.  The public-facing view is a "Pickle",
+ ** which just points to a PickleData.  A pickle is a binary
+ ** serialization of an expression that can be converted back into an
+ ** expression in the same or another ExprManager.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PICKLE_DATA_H
+#define __CVC4__PICKLE_DATA_H
+
+#include <sstream>
+#include <deque>
+#include <stack>
+#include <exception>
+
+#include "expr/expr.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "expr/expr_manager.h"
+#include "expr/variable_type_map.h"
+#include "expr/kind.h"
+#include "expr/metakind.h"
+
+namespace CVC4 {
+
+class NodeManager;
+
+namespace expr {
+namespace pickle {
+
+const unsigned NBITS_BLOCK = 32;
+const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND;
+const unsigned NBITS_NCHILDREN = __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN;
+const unsigned NBITS_CONSTBLOCKS = 32;
+
+struct BlockHeader {
+  unsigned d_kind          : NBITS_KIND;
+};/* struct BlockHeader */
+
+struct BlockHeaderOperator {
+  unsigned d_kind          : NBITS_KIND;
+  unsigned d_nchildren     : NBITS_NCHILDREN;
+  unsigned                 : NBITS_BLOCK - (NBITS_KIND + NBITS_NCHILDREN);
+};/* struct BlockHeaderOperator */
+
+struct BlockHeaderConstant {
+  unsigned d_kind          : NBITS_KIND;
+  unsigned d_constblocks   : NBITS_BLOCK - NBITS_KIND;
+};/* struct BlockHeaderConstant */
+
+struct BlockHeaderVariable {
+  unsigned d_kind          : NBITS_KIND;
+  unsigned                 : NBITS_BLOCK - NBITS_KIND;
+};/* struct BlockHeaderVariable */
+
+struct BlockBody  {
+  unsigned d_data          : NBITS_BLOCK;
+};/* struct BlockBody */
+
+union Block {
+  BlockHeader d_header;
+  BlockHeaderConstant d_headerConstant;
+  BlockHeaderOperator d_headerOperator;
+  BlockHeaderVariable d_headerVariable;
+
+  BlockBody d_body;
+};/* union Block */
+
+class PickleData {
+  typedef std::deque<Block> BlockDeque;
+  BlockDeque d_blocks;
+
+public:
+  PickleData& operator<<(Block b) {
+    enqueue(b);
+    return (*this);
+  }
+
+  std::string toString() const;
+
+  void enqueue(Block b) {
+    d_blocks.push_back(b);
+  }
+
+  Block dequeue() {
+    Block b = d_blocks.front();
+    d_blocks.pop_front();
+    return b;
+  }
+
+  bool empty() const { return d_blocks.empty(); }
+  uint32_t size() const { return d_blocks.size(); }
+
+  void swap(PickleData& other){
+    d_blocks.swap(other.d_blocks);
+  }
+
+  void writeToStringStream(std::ostringstream& oss) const;
+};/* class PickleData */
+
+}/* CVC4::expr::pickle namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PICKLE_DATA_H */
diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp
new file mode 100644
index 000000000..f09c552d1
--- /dev/null
+++ b/src/expr/pickler.cpp
@@ -0,0 +1,477 @@
+/*********************                                                        */
+/*! \file pickler.cpp
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: taking, mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a "pickler" for expressions
+ **
+ ** This is a "pickler" for expressions.  It produces a binary
+ ** serialization of an expression that can be converted back
+ ** into an expression in the same or another ExprManager.
+ **/
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#include "expr/pickler.h"
+#include "expr/pickle_data.h"
+#include "expr/expr.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "expr/node_value.h"
+#include "expr/expr_manager_scope.h"
+#include "expr/variable_type_map.h"
+#include "util/Assert.h"
+#include "expr/kind.h"
+#include "expr/metakind.h"
+#include "util/output.h"
+
+namespace CVC4 {
+namespace expr {
+namespace pickle {
+
+class PicklerPrivate {
+public:
+  typedef std::stack<Node> NodeStack;
+  NodeStack d_stack;
+
+  PickleData d_current;
+
+  Pickler& d_pickler;
+
+  NodeManager* const d_nm;
+
+  PicklerPrivate(Pickler& pickler, ExprManager* em) :
+    d_pickler(pickler),
+    d_nm(NodeManager::fromExprManager(em)) {
+  }
+
+  bool atDefaultState(){
+    return d_stack.empty() && d_current.empty();
+  }
+
+  /* Helper functions for toPickle */
+  void toCaseNode(TNode n) throw(AssertionException, PicklingException);
+  void toCaseVariable(TNode n) throw(AssertionException, PicklingException);
+  void toCaseConstant(TNode n);
+  void toCaseOperator(TNode n) throw(AssertionException, PicklingException);
+  void toCaseString(Kind k, const std::string& s);
+
+  /* Helper functions for toPickle */
+  Node fromCaseOperator(Kind k, uint32_t nchildren);
+  Node fromCaseConstant(Kind k, uint32_t nblocks);
+  std::string fromCaseString(uint32_t nblocks);
+  Node fromCaseVariable(Kind k);
+
+};/* class PicklerPrivate */
+
+static Block mkBlockBody4Chars(char a, char b, char c, char d) {
+  Block newBody;
+  newBody.d_body.d_data = (a << 24) | (b << 16) | (c << 8) | d;
+  return newBody;
+}
+
+static char getCharBlockBody(BlockBody body, int i) {
+  Assert(0 <= i && i <= 3);
+
+  switch(i) {
+  case 0: return (body.d_data & 0xff000000) >> 24;
+  case 1: return (body.d_data & 0x00ff0000) >> 16;
+  case 2: return (body.d_data & 0x0000ff00) >> 8;
+  case 3: return (body.d_data & 0x000000ff);
+  default:
+    Unreachable();
+  }
+  return '\0';
+}
+
+static Block mkBlockBody(unsigned data) {
+  Block newBody;
+  newBody.d_body.d_data = data;
+  return newBody;
+}
+
+static Block mkOperatorHeader(Kind k, unsigned numChildren) {
+  Block newHeader;
+  newHeader.d_headerOperator.d_kind = k;
+  newHeader.d_headerOperator.d_nchildren = numChildren;
+  return newHeader;
+}
+
+static Block mkVariableHeader(Kind k) {
+  Block newHeader;
+  newHeader.d_header.d_kind = k;
+  return newHeader;
+}
+
+static Block mkConstantHeader(Kind k, unsigned numBlocks) {
+  Block newHeader;
+  newHeader.d_headerConstant.d_kind = k;
+  newHeader.d_headerConstant.d_constblocks = numBlocks;
+  return newHeader;
+}
+
+Pickler::Pickler(ExprManager* em) :
+  d_private(new PicklerPrivate(*this, em)) {
+}
+
+Pickler::~Pickler() {
+  delete d_private;
+}
+
+void Pickler::toPickle(Expr e, Pickle& p)
+  throw(AssertionException, PicklingException) {
+  Assert(NodeManager::fromExprManager(e.getExprManager()) == d_private->d_nm);
+  Assert(d_private->atDefaultState());
+
+  try{
+    d_private->d_current.swap(*p.d_data);
+    d_private->toCaseNode(e.getTNode());
+    d_private->d_current.swap(*p.d_data);
+  }catch(PicklingException& pe){
+    d_private->d_current = PickleData();
+    Assert(d_private->atDefaultState());
+    throw pe;
+  }
+
+  Assert(d_private->atDefaultState());
+}
+
+void PicklerPrivate::toCaseNode(TNode n)
+  throw(AssertionException, PicklingException) {
+  Debug("pickler") << "toCaseNode: " << n << std::endl;
+  Kind k = n.getKind();
+  kind::MetaKind m = metaKindOf(k);
+  switch(m) {
+  case kind::metakind::CONSTANT:
+    toCaseConstant(n);
+    break;
+  case kind::metakind::VARIABLE:
+    toCaseVariable(n);
+    break;
+  case kind::metakind::OPERATOR:
+  case kind::metakind::PARAMETERIZED:
+    toCaseOperator(n);
+    break;
+  default:
+    Unhandled(m);
+  }
+}
+
+void PicklerPrivate::toCaseOperator(TNode n)
+  throw(AssertionException, PicklingException) {
+  Kind k = n.getKind();
+  kind::MetaKind m = metaKindOf(k);
+  Assert(m == kind::metakind::PARAMETERIZED || m == kind::metakind::OPERATOR);
+  if(m == kind::metakind::PARAMETERIZED) {
+    toCaseNode(n.getOperator());
+  }
+  for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
+    toCaseNode(*i);
+  }
+  d_current << mkOperatorHeader(k, n.getNumChildren());
+}
+
+void PicklerPrivate::toCaseVariable(TNode n)
+  throw(AssertionException, PicklingException) {
+  Kind k = n.getKind();
+  Assert(metaKindOf(k) == kind::metakind::VARIABLE);
+
+  const NodeValue* nv = n.d_nv;
+  uint64_t asInt = reinterpret_cast<uint64_t>(nv);
+  uint64_t mapped = d_pickler.variableToMap(asInt);
+
+  uint32_t firstHalf = mapped >> 32;
+  uint32_t secondHalf = mapped & 0xffffffff;
+
+  d_current << mkVariableHeader(k);
+  d_current << mkBlockBody(firstHalf);
+  d_current << mkBlockBody(secondHalf);
+}
+
+
+void PicklerPrivate::toCaseConstant(TNode n) {
+  Kind k = n.getKind();
+  Assert(metaKindOf(k) == kind::metakind::CONSTANT);
+  switch(k) {
+  case kind::CONST_BOOLEAN:
+    d_current << mkConstantHeader(k, 1);
+    d_current << mkBlockBody(n.getConst<bool>());
+    break;
+  case kind::CONST_INTEGER:
+  case kind::CONST_RATIONAL: {
+    std::string asString;
+    if(k == kind::CONST_INTEGER) {
+      const Integer& i = n.getConst<Integer>();
+      asString = i.toString(16);
+    } else {
+      Assert(k == kind::CONST_RATIONAL);
+      const Rational& q = n.getConst<Rational>();
+      asString = q.toString(16);
+    }
+    toCaseString(k, asString);
+    break;
+  }
+  case kind::BITVECTOR_EXTRACT_OP: {
+    BitVectorExtract bve = n.getConst<BitVectorExtract>();
+    d_current << mkConstantHeader(k, 2);
+    d_current << mkBlockBody(bve.high);
+    d_current << mkBlockBody(bve.low);
+    break;
+  }
+  case kind::CONST_BITVECTOR: {
+    // irritating: we incorporate the size of the string in with the
+    // size of this constant, so it appears as one big constant and
+    // doesn't confuse anybody
+    BitVector bv = n.getConst<BitVector>();
+    std::string asString = bv.getValue().toString(16);
+    d_current << mkConstantHeader(k, 2 + asString.size());
+    d_current << mkBlockBody(bv.getSize());
+    toCaseString(k, asString);
+    break;
+  }
+  default:
+    Unhandled(k);
+  }
+}
+
+void PicklerPrivate::toCaseString(Kind k, const std::string& s) {
+  d_current << mkConstantHeader(k, s.size());
+
+  unsigned size = s.size();
+  unsigned i;
+  for(i = 0; i + 4 <= size; i += 4) {
+    d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], s[i + 3]);
+  }
+  switch(size % 4) {
+  case 0: break;
+  case 1: d_current << mkBlockBody4Chars(s[i + 0], '\0','\0', '\0'); break;
+  case 2: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1], '\0', '\0'); break;
+  case 3: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], '\0'); break;
+  default:
+    Unreachable();
+  }
+
+}
+
+void Pickler::debugPickleTest(Expr e) {
+
+  //ExprManager *em = e.getExprManager();
+  //Expr e1 = mkVar("x", makeType());
+  //return ;
+
+  Pickler pickler(e.getExprManager());
+
+  Pickle p;
+  pickler.toPickle(e, p);
+
+  uint32_t size = p.d_data->size();
+  std::string str = p.d_data->toString();
+
+  Expr from = pickler.fromPickle(p);
+  ExprManagerScope ems(e);
+
+  Debug("pickle") << "before: " << e << std::endl;
+  Debug("pickle") << "after: " << from.getNode() << std::endl;
+  Debug("pickle") << "pickle: (oct) "<< size << " " << str.length() << " " << str << std::endl;
+
+  Assert(p.d_data->empty());
+  Assert(e == from);
+}
+
+Expr Pickler::fromPickle(Pickle& p) {
+  Assert(d_private->atDefaultState());
+
+  d_private->d_current.swap(*p.d_data);
+
+  while(!d_private->d_current.empty()) {
+    Block front = d_private->d_current.dequeue();
+
+    Kind k = (Kind)front.d_header.d_kind;
+    kind::MetaKind m = metaKindOf(k);
+
+    Node result = Node::null();
+    switch(m) {
+    case kind::metakind::VARIABLE:
+      result = d_private->fromCaseVariable(k);
+      break;
+    case kind::metakind::CONSTANT:
+      result = d_private->fromCaseConstant(k, front.d_headerConstant.d_constblocks);
+      break;
+    case kind::metakind::OPERATOR:
+    case kind::metakind::PARAMETERIZED:
+      result = d_private->fromCaseOperator(k, front.d_headerOperator.d_nchildren);
+      break;
+    default:
+      Unhandled(m);
+    }
+    Assert(result != Node::null());
+    d_private->d_stack.push(result);
+  }
+
+  Assert(d_private->d_current.empty());
+  Assert(d_private->d_stack.size() == 1);
+  Node res = d_private->d_stack.top();
+  d_private->d_stack.pop();
+
+  Assert(d_private->atDefaultState());
+
+  return d_private->d_nm->toExpr(res);
+}
+
+Node PicklerPrivate::fromCaseVariable(Kind k) {
+  Assert(metaKindOf(k) == kind::metakind::VARIABLE);
+
+  Block firstHalf = d_current.dequeue();
+  Block secondHalf = d_current.dequeue();
+
+  uint64_t asInt = firstHalf.d_body.d_data;
+  asInt = asInt << 32;
+  asInt = asInt | (secondHalf.d_body.d_data);
+
+  uint64_t mapped = d_pickler.variableFromMap(asInt);
+
+  NodeValue* nv = reinterpret_cast<NodeValue*>(mapped);
+  Node fromNodeValue(nv);
+
+  Assert(fromNodeValue.getKind() == k);
+
+  return fromNodeValue;
+}
+
+Node PicklerPrivate::fromCaseConstant(Kind k, uint32_t constblocks) {
+  switch(k) {
+  case kind::CONST_BOOLEAN: {
+    Assert(constblocks == 1);
+    Block val = d_current.dequeue();
+
+    bool b= val.d_body.d_data;
+    return d_nm->mkConst<bool>(b);
+  }
+  case kind::CONST_INTEGER:
+  case kind::CONST_RATIONAL: {
+    std::string s = fromCaseString(constblocks);
+    if(k == kind::CONST_INTEGER) {
+      Integer i(s, 16);
+      return d_nm->mkConst<Integer>(i);
+    } else {
+      Rational q(s, 16);
+      return d_nm->mkConst<Rational>(q);
+    }
+  }
+  case kind::BITVECTOR_EXTRACT_OP: {
+    Block high = d_current.dequeue();
+    Block low = d_current.dequeue();
+    BitVectorExtract bve(high.d_body.d_data, low.d_body.d_data);
+    return d_nm->mkConst<BitVectorExtract>(bve);
+  }
+  case kind::CONST_BITVECTOR: {
+    unsigned size = d_current.dequeue().d_body.d_data;
+    Block header CVC4_UNUSED = d_current.dequeue();
+    Assert(header.d_headerConstant.d_kind == kind::CONST_BITVECTOR);
+    Assert(header.d_headerConstant.d_constblocks == constblocks - 2);
+    Integer value(fromCaseString(constblocks - 2));
+    BitVector bv(size, value);
+    return d_nm->mkConst(bv);
+  }
+  default:
+    Unhandled(k);
+  }
+}
+
+std::string PicklerPrivate::fromCaseString(uint32_t size) {
+  std::stringstream ss;
+  unsigned i;
+  for(i = 0; i + 4 <= size; i += 4) {
+    Block front = d_current.dequeue();
+    BlockBody body = front.d_body;
+
+    ss << getCharBlockBody(body,0)
+       << getCharBlockBody(body,1)
+       << getCharBlockBody(body,2)
+       << getCharBlockBody(body,3);
+  }
+  Assert(i == size - (size%4) );
+  if(size % 4 != 0) {
+    Block front = d_current.dequeue();
+    BlockBody body = front.d_body;
+    switch(size % 4) {
+    case 1:
+      ss << getCharBlockBody(body,0);
+      break;
+    case 2:
+      ss << getCharBlockBody(body,0)
+         << getCharBlockBody(body,1);
+      break;
+    case 3:
+      ss << getCharBlockBody(body,0)
+         << getCharBlockBody(body,1)
+         << getCharBlockBody(body,2);
+      break;
+    default:
+      Unreachable();
+    }
+  }
+  return ss.str();
+}
+
+Node PicklerPrivate::fromCaseOperator(Kind k, uint32_t nchildren) {
+  kind::MetaKind m = metaKindOf(k);
+  bool parameterized = (m == kind::metakind::PARAMETERIZED);
+  uint32_t npops = nchildren + (parameterized? 1 : 0);
+
+  NodeStack aux;
+  while(npops > 0) {
+    Assert(!d_stack.empty());
+    Node top = d_stack.top();
+    aux.push(top);
+    d_stack.pop();
+    --npops;
+  }
+
+  NodeBuilder<> nb(d_nm, k);
+  while(!aux.empty()) {
+    Node top = aux.top();
+    nb << top;
+    aux.pop();
+  }
+
+  return nb;
+}
+
+Pickle::Pickle() {
+  d_data = new PickleData();
+}
+
+// Just copying the pointer isn't right, we have to copy the
+// underlying data.  Otherwise user-level Pickles will delete the data
+// twice! (once in each thread)
+Pickle::Pickle(const Pickle& p) {
+  d_data = new PickleData(*p.d_data);
+}
+
+Pickle& Pickle::operator = (const Pickle& other) {
+  if (this != &other) {
+    delete d_data;
+    d_data = new PickleData(*other.d_data);
+  }
+  return *this;
+}
+
+
+Pickle::~Pickle() {
+  delete d_data;
+}
+
+}/* CVC4::expr::pickle namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
diff --git a/src/expr/pickler.h b/src/expr/pickler.h
new file mode 100644
index 000000000..264ae0e4b
--- /dev/null
+++ b/src/expr/pickler.h
@@ -0,0 +1,139 @@
+/*********************                                                        */
+/*! \file pickle.h
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: taking, mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a "pickler" for expressions
+ **
+ ** This is a "pickler" for expressions.  It produces a binary
+ ** serialization of an expression that can be converted back
+ ** into an expression in the same or another ExprManager.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__PICKLER_H
+#define __CVC4__PICKLER_H
+
+#include "expr/variable_type_map.h"
+#include "expr/expr.h"
+#include "util/exception.h"
+
+#include <exception>
+#include <stack>
+
+namespace CVC4 {
+
+class ExprManager;
+
+namespace expr {
+namespace pickle {
+
+class Pickler;
+class PicklerPrivate;
+
+class PickleData;// CVC4-internal representation
+
+class CVC4_PUBLIC Pickle {
+  PickleData* d_data;
+  friend class Pickler;
+  friend class PicklerPrivate;
+public:
+  Pickle();
+  Pickle(const Pickle& p);
+  ~Pickle();
+  Pickle& operator = (const Pickle& other);
+};/* class Pickle */
+
+class CVC4_PUBLIC PicklingException : public Exception {
+public:
+  PicklingException() :
+    Exception("Pickling failed") {
+  }
+};/* class PicklingException */
+
+class CVC4_PUBLIC Pickler {
+  PicklerPrivate* d_private;
+
+  friend class PicklerPrivate;
+
+protected:
+  virtual uint64_t variableToMap(uint64_t x) const
+    throw(AssertionException, PicklingException) {
+    return x;
+  }
+  virtual uint64_t variableFromMap(uint64_t x) const {
+    return x;
+  }
+
+public:
+  Pickler(ExprManager* em);
+  ~Pickler();
+
+  /**
+   * Constructs a new Pickle of the node n.
+   * n must be a node allocated in the node manager specified at initialization
+   * time. The new pickle has variables mapped using the VariableIDMap provided
+   * at initialization.
+   * TODO: Fix comment
+   *
+   * @return the pickle, which should be dispose()'d when you're done with it
+   */
+  void toPickle(Expr e, Pickle& p) throw(AssertionException, PicklingException);
+
+  /**
+   * Constructs a node from a Pickle.
+   * This destroys the contents of the Pickle.
+   * The node is created in the NodeManager getNM();
+   * TODO: Fix comment
+   */
+  Expr fromPickle(Pickle& p);
+
+  static void debugPickleTest(Expr e);
+
+};/* class Pickler */
+
+class MapPickler : public Pickler {
+private:
+  const VarMap& d_toMap;
+  const VarMap& d_fromMap;
+
+public:
+  MapPickler(ExprManager* em, const VarMap& to, const VarMap& from):
+    Pickler(em),
+    d_toMap(to),
+    d_fromMap(from) {
+  }
+
+protected:
+
+  virtual uint64_t variableToMap(uint64_t x) const
+    throw(AssertionException, PicklingException){
+    VarMap::const_iterator i = d_toMap.find(x);
+    if(i != d_toMap.end()){
+      return i->second;
+    }else{
+      throw PicklingException();
+    }
+  }
+
+  virtual uint64_t variableFromMap(uint64_t x) const {
+    VarMap::const_iterator i = d_fromMap.find(x);
+    Assert(i != d_fromMap.end());
+    return i->second;
+  }
+};/* class MapPickler */
+
+}/* CVC4::expr::pickle namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PICKLER_H */
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 7e06a05ae..a901af73a 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -162,6 +162,10 @@ ExprManager* Type::getExprManager() const {
   return d_nodeManager->toExprManager();
 }
 
+Type Type::exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) {
+  return ExprManager::exportType(*this, exprManager, vmap);
+}
+
 void Type::toStream(std::ostream& out) const {
   NodeManagerScope nms(d_nodeManager);
   out << *d_typeNode;
diff --git a/src/expr/type.h b/src/expr/type.h
index 0b50fbd3c..34cc925f6 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -35,6 +35,7 @@ class NodeManager;
 class ExprManager;
 class Expr;
 class TypeNode;
+class ExprManagerMapCollection;
 
 class SmtEngine;
 
@@ -75,6 +76,10 @@ struct CVC4_PUBLIC TypeHashFunction {
  */
 std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
 
+namespace expr {
+  TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap);
+}/* CVC4::expr namespace */
+
 /**
  * Class encapsulating CVC4 expression types.
  */
@@ -86,6 +91,7 @@ class CVC4_PUBLIC Type {
   friend class TypeNode;
   friend struct TypeHashStrategy;
   friend std::ostream& CVC4::operator<<(std::ostream& out, const Type& t);
+  friend TypeNode expr::exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap);
 
 protected:
 
@@ -166,6 +172,11 @@ public:
   ExprManager* getExprManager() const;
 
   /**
+   * Exports this type into a different ExprManager.
+   */
+  Type exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap);
+
+  /**
    * Assignment operator.
    * @param t the type to assign to this type
    * @return this type after assignment.
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 553f83276..c7da5ceb7 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -229,6 +229,16 @@ public:
   }
 
   /**
+   * PARAMETERIZED-metakinded types (the SORT_TYPE is one of these)
+   * have an operator.  "Little-p parameterized" types (like Array),
+   * are OPERATORs, not PARAMETERIZEDs.
+   */
+  inline Node getOperator() const {
+    Assert(getMetaKind() == kind::metakind::PARAMETERIZED);
+    return Node(d_nv->getChild(-1));
+  }
+
+  /**
    * Returns the unique id of this node
    *
    * @return the id
diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h
new file mode 100644
index 000000000..a34bec846
--- /dev/null
+++ b/src/expr/variable_type_map.h
@@ -0,0 +1,64 @@
+/*********************                                                        */
+/*! \file variable_type_map.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__VARIABLE_TYPE_MAP_H
+#define __CVC4__VARIABLE_TYPE_MAP_H
+
+#include "expr/expr.h"
+#include "util/hash.h"
+
+namespace CVC4 {
+
+class Expr;
+struct ExprHashFunction;
+class Type;
+struct TypeHashFunction;
+
+class CVC4_PUBLIC VariableTypeMap {
+  /**
+   * A map Expr -> Expr, intended to be used for a mapping of variables
+   * between two ExprManagers.
+   */
+  std::hash_map<Expr, Expr, ExprHashFunction> d_variables;
+
+  /**
+   * A map Type -> Type, intended to be used for a mapping of types
+   * between two ExprManagers.
+   */
+  std::hash_map<Type, Type, TypeHashFunction> d_types;
+
+public:
+  Expr& operator[](Expr e) { return d_variables[e]; }
+  Type& operator[](Type t) { return d_types[t]; }
+
+};/* class VariableTypeMap */
+
+typedef __gnu_cxx::hash_map<uint64_t, uint64_t> VarMap;
+
+struct CVC4_PUBLIC ExprManagerMapCollection {
+  VariableTypeMap d_typeMap;
+  VarMap d_to;
+  VarMap d_from;
+};
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__VARIABLE_MAP_H */
diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 78d468000..ae7764e32 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -4,16 +4,42 @@ AM_CPPFLAGS = \
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas
 
 bin_PROGRAMS = cvc4
+
 noinst_LIBRARIES = libmain.a
 
 libmain_a_SOURCES = \
 	interactive_shell.h \
 	interactive_shell.cpp \
 	main.h \
-	main.cpp \
 	util.cpp
 
-cvc4_SOURCES =
+if CVC4_HAS_THREADS
+bin_PROGRAMS += pcvc4
+pcvc4_SOURCES = \
+	main.cpp \
+	portfolio.cpp \
+	portfolio.h \
+	driver_portfolio.cpp
+pcvc4_LDADD = \
+	libmain.a \
+	@builddir@/../parser/libcvc4parser.la \
+	@builddir@/../libcvc4.la \
+	@builddir@/../lib/libreplacements.la \
+	$(READLINE_LIBS)
+pcvc4_CPPFLAGS = $(AM_CPPFLAGS) $(BOOST_CPPFLAGS)
+pcvc4_LDADD += $(BOOST_THREAD_LIBS) -lpthread
+pcvc4_LDADD += $(BOOST_THREAD_LDFLAGS)
+
+if STATIC_BINARY
+pcvc4_LINK = $(CXXLINK) -all-static
+else
+pcvc4_LINK = $(CXXLINK)
+endif
+endif
+
+cvc4_SOURCES = \
+	main.cpp \
+	driver.cpp
 cvc4_LDADD = \
 	libmain.a \
 	@builddir@/../parser/libcvc4parser.la \
@@ -44,3 +70,4 @@ cvc4_LINK = $(CXXLINK) -all-static
 else
 cvc4_LINK = $(CXXLINK)
 endif
+
diff --git a/src/main/driver.cpp b/src/main/driver.cpp
new file mode 100644
index 000000000..e9bfde024
--- /dev/null
+++ b/src/main/driver.cpp
@@ -0,0 +1,355 @@
+/*********************                                                        */
+/*! \file driver.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): barrett, dejan, taking
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011, 2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Driver for (sequential) CVC4 executable
+ **
+ ** Driver for (sequential) CVC4 executable.
+ **/
+
+#include <cstdlib>
+#include <cstring>
+#include <fstream>
+#include <iostream>
+#include <new>
+
+#include <stdio.h>
+#include <unistd.h>
+
+#include "cvc4autoconfig.h"
+#include "main/main.h"
+#include "main/interactive_shell.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+#include "parser/parser_exception.h"
+#include "expr/expr_manager.h"
+#include "smt/smt_engine.h"
+#include "expr/command.h"
+#include "util/Assert.h"
+#include "util/configuration.h"
+#include "util/options.h"
+#include "util/output.h"
+#include "util/result.h"
+#include "util/stats.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::parser;
+using namespace CVC4::main;
+
+static bool doCommand(SmtEngine&, Command*, Options&);
+
+namespace CVC4 {
+  namespace main {
+    /** Global options variable */
+    CVC4_THREADLOCAL(Options*) pOptions;
+
+    /** Full argv[0] */
+    const char *progPath;
+
+    /** Just the basename component of argv[0] */
+    const char *progName;
+
+    /** A pointer to the StatisticsRegistry (the signal handlers need it) */
+    CVC4::StatisticsRegistry* pStatistics;
+  }
+}
+
+
+void printUsage(Options& options, bool full) {
+  stringstream ss;
+  ss << "usage: " << options.binary_name << " [options] [input-file]" << endl
+      << endl
+      << "Without an input file, or with `-', CVC4 reads from standard input." << endl
+      << endl
+      << "CVC4 options:" << endl;
+  if(full) {
+    Options::printUsage( ss.str(), *options.out );
+  } else {
+    Options::printShortUsage( ss.str(), *options.out );
+  }
+}
+
+int runCvc4(int argc, char* argv[], Options& options) {
+
+  // For the signal handlers' benefit
+  pOptions = &options;
+
+  // Initialize the signal handlers
+  cvc4_init();
+
+  progPath = argv[0];
+
+  // Parse the options
+  int firstArgIndex = options.parseOptions(argc, argv);
+
+  progName = options.binary_name.c_str();
+
+  if( options.help ) {
+    printUsage(options, true);
+    exit(1);
+  } else if( options.languageHelp ) {
+    Options::printLanguageHelp(*options.out);
+    exit(1);
+  } else if( options.version ) {
+    *options.out << Configuration::about().c_str() << flush;
+    exit(0);
+  }
+
+  segvNoSpin = options.segvNoSpin;
+
+  // If in competition mode, set output stream option to flush immediately
+#ifdef CVC4_COMPETITION_MODE
+  *options.out << unitbuf;
+#endif
+
+  // We only accept one input file
+  if(argc > firstArgIndex + 1) {
+    throw Exception("Too many input files specified.");
+  }
+
+  // If no file supplied we will read from standard input
+  const bool inputFromStdin =
+    firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
+
+  // if we're reading from stdin on a TTY, default to interactive mode
+  if(!options.interactiveSetByUser) {
+    options.interactive = inputFromStdin && isatty(fileno(stdin));
+  }
+
+  // Determine which messages to show based on smtcomp_mode and verbosity
+  if(Configuration::isMuzzledBuild()) {
+    Debug.setStream(CVC4::null_os);
+    Trace.setStream(CVC4::null_os);
+    Notice.setStream(CVC4::null_os);
+    Chat.setStream(CVC4::null_os);
+    Message.setStream(CVC4::null_os);
+    Warning.setStream(CVC4::null_os);
+    Dump.setStream(CVC4::null_os);
+  } else {
+    if(options.verbosity < 2) {
+      Chat.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 1) {
+      Notice.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 0) {
+      Message.setStream(CVC4::null_os);
+      Warning.setStream(CVC4::null_os);
+    }
+  }
+
+  // Create the expression manager
+  ExprManager exprMgr(options);
+
+  // Create the SmtEngine
+  SmtEngine smt(&exprMgr);
+
+  // signal handlers need access
+  pStatistics = smt.getStatisticsRegistry();
+
+  // Auto-detect input language by filename extension
+  const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
+
+  ReferenceStat< const char* > s_statFilename("filename", filename);
+  RegisterStatistic statFilenameReg(exprMgr, &s_statFilename);
+
+  if(options.inputLanguage == language::input::LANG_AUTO) {
+    if( inputFromStdin ) {
+      // We can't do any fancy detection on stdin
+      options.inputLanguage = language::input::LANG_CVC4;
+    } else {
+      unsigned len = strlen(filename);
+      if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
+        options.inputLanguage = language::input::LANG_SMTLIB_V2;
+      } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
+        options.inputLanguage = language::input::LANG_SMTLIB;
+      } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
+                || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
+        options.inputLanguage = language::input::LANG_CVC4;
+      }
+    }
+  }
+
+  if(options.outputLanguage == language::output::LANG_AUTO) {
+    options.outputLanguage = language::toOutputLanguage(options.inputLanguage);
+  }
+
+  // Determine which messages to show based on smtcomp_mode and verbosity
+  if(Configuration::isMuzzledBuild()) {
+    Debug.setStream(CVC4::null_os);
+    Trace.setStream(CVC4::null_os);
+    Notice.setStream(CVC4::null_os);
+    Chat.setStream(CVC4::null_os);
+    Message.setStream(CVC4::null_os);
+    Warning.setStream(CVC4::null_os);
+    Dump.setStream(CVC4::null_os);
+  } else {
+    if(options.verbosity < 2) {
+      Chat.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 1) {
+      Notice.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 0) {
+      Message.setStream(CVC4::null_os);
+      Warning.setStream(CVC4::null_os);
+    }
+
+    Debug.getStream() << Expr::setlanguage(options.outputLanguage);
+    Trace.getStream() << Expr::setlanguage(options.outputLanguage);
+    Notice.getStream() << Expr::setlanguage(options.outputLanguage);
+    Chat.getStream() << Expr::setlanguage(options.outputLanguage);
+    Message.getStream() << Expr::setlanguage(options.outputLanguage);
+    Warning.getStream() << Expr::setlanguage(options.outputLanguage);
+    Dump.getStream() << Expr::setlanguage(options.outputLanguage)
+                     << Expr::setdepth(-1)
+                     << Expr::printtypes(false);
+  }
+
+  Parser* replayParser = NULL;
+  if( options.replayFilename != "" ) {
+    ParserBuilder replayParserBuilder(&exprMgr, options.replayFilename, options);
+
+    if( options.replayFilename == "-") {
+      if( inputFromStdin ) {
+        throw OptionException("Replay file and input file can't both be stdin.");
+      }
+      replayParserBuilder.withStreamInput(cin);
+    }
+    replayParser = replayParserBuilder.build();
+    options.replayStream = new Parser::ExprStream(replayParser);
+  }
+  if( options.replayLog != NULL ) {
+    *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1);
+  }
+
+  // Parse and execute commands until we are done
+  Command* cmd;
+  bool status = true;
+  if( options.interactive ) {
+    InteractiveShell shell(exprMgr, options);
+    Message() << Configuration::getPackageName()
+              << " " << Configuration::getVersionString();
+    if(Configuration::isSubversionBuild()) {
+      Message() << " [" << Configuration::getSubversionId() << "]";
+    }
+    Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
+              << " assertions:"
+              << (Configuration::isAssertionBuild() ? "on" : "off")
+              << endl;
+    if(replayParser != NULL) {
+      // have the replay parser use the declarations input interactively
+      replayParser->useDeclarationsFrom(shell.getParser());
+    }
+    while((cmd = shell.readCommand())) {
+      status = doCommand(smt,cmd, options) && status;
+      delete cmd;
+    }
+  } else {
+    ParserBuilder parserBuilder(&exprMgr, filename, options);
+
+    if( inputFromStdin ) {
+      parserBuilder.withStreamInput(cin);
+    }
+
+    Parser *parser = parserBuilder.build();
+    if(replayParser != NULL) {
+      // have the replay parser use the file's declarations
+      replayParser->useDeclarationsFrom(parser);
+    }
+    while((cmd = parser->nextCommand())) {
+      status = doCommand(smt, cmd, options) && status;
+      delete cmd;
+    }
+    // Remove the parser
+    delete parser;
+  }
+
+  if( options.replayStream != NULL ) {
+    // this deletes the expression parser too
+    delete options.replayStream;
+    options.replayStream = NULL;
+  }
+
+  int returnValue;
+  string result = "unknown";
+  if(status) {
+    result = smt.getInfo(":status").getValue();
+
+    if(result == "sat") {
+      returnValue = 10;
+    } else if(result == "unsat") {
+      returnValue = 20;
+    } else {
+      returnValue = 0;
+    }
+  } else {
+    // there was some kind of error
+    returnValue = 1;
+  }
+
+#ifdef CVC4_COMPETITION_MODE
+  // exit, don't return
+  // (don't want destructors to run)
+  exit(returnValue);
+#endif
+
+  ReferenceStat< Result > s_statSatResult("sat/unsat", result);
+  RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult);
+
+  if(options.statistics) {
+    pStatistics->flushInformation(*options.err);
+  }
+
+  return returnValue;
+}
+
+/** Executes a command. Deletes the command after execution. */
+static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
+  if( options.parseOnly ) {
+    return true;
+  }
+
+  // assume no error
+  bool status = true;
+
+  CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
+  if(seq != NULL) {
+    for(CommandSequence::iterator subcmd = seq->begin();
+        subcmd != seq->end();
+        ++subcmd) {
+      status = doCommand(smt, *subcmd, options) && status;
+    }
+  } else {
+    // by default, symmetry breaker is on only for QF_UF
+    if(! options.ufSymmetryBreakerSetByUser) {
+      SetBenchmarkLogicCommand *logic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd);
+      if(logic != NULL) {
+        options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF");
+      }
+    }
+
+    if(options.verbosity > 0) {
+      *options.out << "Invoking: " << *cmd << endl;
+    }
+
+    if(options.verbosity >= 0) {
+      cmd->invoke(&smt, *options.out);
+    } else {
+      cmd->invoke(&smt);
+    }
+    status = status && cmd->ok();
+  }
+
+  return status;
+}
diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
new file mode 100644
index 000000000..5c8f908f8
--- /dev/null
+++ b/src/main/driver_portfolio.cpp
@@ -0,0 +1,808 @@
+#include <cstdio>
+#include <cstdlib>
+#include <iostream>
+#include <sys/time.h>           // for gettimeofday()
+
+#include <queue>
+
+#include <boost/thread.hpp>
+#include <boost/thread/condition.hpp>
+#include <boost/exception_ptr.hpp>
+#include <boost/lexical_cast.hpp>
+
+#include "cvc4autoconfig.h"
+#include "main/main.h"
+#include "main/interactive_shell.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+#include "parser/parser_exception.h"
+#include "expr/expr_manager.h"
+#include "expr/variable_type_map.h"
+#include "smt/smt_engine.h"
+#include "expr/command.h"
+#include "util/Assert.h"
+#include "util/configuration.h"
+#include "util/options.h"
+#include "util/output.h"
+#include "util/result.h"
+#include "util/stats.h"
+
+#include "expr/pickler.h"
+#include "util/channel.h"
+
+#include "main/portfolio.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::parser;
+using namespace CVC4::main;
+
+/* Global variables */
+
+namespace CVC4 {
+  namespace main {
+
+    StatisticsRegistry theStatisticsRegistry;
+
+    /** A pointer to the StatisticsRegistry (the signal handlers need it) */
+    CVC4::StatisticsRegistry* pStatistics;
+
+  }/* CVC4::main namespace */
+}/* CVC4 namespace */
+
+/* Function declarations */
+
+static bool doCommand(SmtEngine&, Command*, Options&);
+
+Result doSmt(SmtEngine &smt, Command *cmd, Options &options);
+
+template<typename T>
+void sharingManager(int numThreads,
+                    SharedChannel<T>* channelsOut[],
+                    SharedChannel<T>* channelsIn[],
+                    SmtEngine* smts[]);
+
+
+/* To monitor for activity on shared channels */
+bool global_activity;
+bool global_activity_true() { return global_activity; }
+bool global_activity_false() { return not global_activity; }
+boost::condition global_activity_cond;
+
+typedef expr::pickle::Pickle channelFormat; /* Remove once we are using Pickle */
+
+template <typename T>
+class EmptySharedChannel: public SharedChannel<T> {
+public:
+  EmptySharedChannel(int) {}
+  bool push(const T&) { return true; }
+  T pop() { return T(); }
+  bool empty() { return true; }
+  bool full() { return false; }
+};
+
+class PortfolioLemmaOutputChannel : public LemmaOutputChannel {
+private:
+  string d_tag;
+  SharedChannel<channelFormat>* d_sharedChannel;
+  expr::pickle::MapPickler d_pickler;
+
+public:
+  int cnt;
+  PortfolioLemmaOutputChannel(string tag,
+                              SharedChannel<channelFormat> *c,
+                              ExprManager* em,
+                              VarMap& to,
+                              VarMap& from) :
+    d_tag(tag),
+    d_sharedChannel(c),
+    d_pickler(em, to, from)
+    ,cnt(0)
+  {}
+
+  void notifyNewLemma(Expr lemma) {
+    if(Debug.isOn("disable-lemma-sharing")) return;
+    const Options *options = Options::current();
+    if(options->sharingFilterByLength >= 0) { // 0 would mean no-sharing effectively
+      if( int(lemma.getNumChildren()) > options->sharingFilterByLength)
+        return;
+    }
+    ++cnt;
+    Trace("sharing") << d_tag << ": " << lemma << std::endl;
+    expr::pickle::Pickle pkl;
+    try{
+      d_pickler.toPickle(lemma, pkl);
+      d_sharedChannel->push(pkl);
+      if(Trace.isOn("showSharing") and options->thread_id == 0) {
+        *(Options::current()->out) << "thread #0: notifyNewLemma: " << lemma << endl;
+      }
+    }catch(expr::pickle::PicklingException& p){
+      Trace("sharing::blocked") << lemma << std::endl;
+    }
+  }
+
+};
+
+/* class PortfolioLemmaInputChannel */
+class PortfolioLemmaInputChannel : public LemmaInputChannel {
+private:
+  string d_tag;
+  SharedChannel<channelFormat>* d_sharedChannel;
+  expr::pickle::MapPickler d_pickler;
+
+public:
+  PortfolioLemmaInputChannel(string tag,
+                             SharedChannel<channelFormat>* c,
+                             ExprManager* em,
+                             VarMap& to,
+                             VarMap& from) :
+    d_tag(tag),
+    d_sharedChannel(c),
+    d_pickler(em, to, from){
+  }
+
+  bool hasNewLemma(){
+    Debug("lemmaInputChannel") << d_tag << ": " << "hasNewLemma" << endl;
+    return !d_sharedChannel->empty();
+  }
+
+  Expr getNewLemma() {
+    Debug("lemmaInputChannel") << d_tag << ": " << "getNewLemma" << endl;
+    expr::pickle::Pickle pkl = d_sharedChannel->pop();
+
+    Expr e = d_pickler.fromPickle(pkl);
+    if(Trace.isOn("showSharing") and Options::current()->thread_id == 0) {
+      *(Options::current()->out) << "thread #0: getNewLemma: " << e << endl;
+    }
+    return e;
+  }
+
+};/* class PortfolioLemmaInputChannel */
+
+
+
+int runCvc4(int argc, char *argv[], Options& options) {
+
+#ifdef CVC4_CLN_IMP
+  Warning() << "WARNING:" << endl
+            << "WARNING: This build of portfolio-CVC4 uses the CLN library" << endl
+            << "WARNING: which is not thread-safe!  Expect crashes and" << endl
+            << "WARNING: incorrect answers." << endl
+            << "WARNING:" << endl;
+#endif /* CVC4_CLN_IMP */
+
+  /**************************************************************************
+   * runCvc4 outline:
+   * -> Start a couple of timers
+   * -> Processing of options, including thread specific ones
+   * -> Statistics related stuff
+   * -> Create ExprManager, parse commands, duplicate exprMgrs using export
+   * -> Create smtEngines
+   * -> Lemma sharing init
+   * -> Run portfolio, exit/print stats etc.
+   * (This list might become outdated, a timestamp might be good: 7 Dec '11.)
+   **************************************************************************/
+
+  // Timer statistic
+  TimerStat s_totalTime("totalTime");
+  TimerStat s_beforePortfolioTime("beforePortfolioTime");
+  s_totalTime.start();
+  s_beforePortfolioTime.start();
+
+  // For the signal handlers' benefit
+  pOptions = &options;
+
+  // Initialize the signal handlers
+  cvc4_init();
+
+  progPath = argv[0];
+
+
+  /****************************** Options Processing ************************/
+
+  // Parse the options
+  int firstArgIndex = options.parseOptions(argc, argv);
+
+  progName = options.binary_name.c_str();
+
+  if( options.help ) {
+    printUsage(options, true);
+    exit(1);
+  } else if( options.languageHelp ) {
+    Options::printLanguageHelp(*options.out);
+    exit(1);
+  } else if( options.version ) {
+    *options.out << Configuration::about().c_str() << flush;
+    exit(0);
+  }
+
+  int numThreads = options.threads;
+
+  if(options.threadArgv.size() > size_t(numThreads)) {
+    stringstream ss;
+    ss << "--thread" << (options.threadArgv.size() - 1)
+       << " configuration string seen but this portfolio will only contain "
+       << numThreads << " thread(s)!";
+    throw OptionException(ss.str());
+  }
+
+  segvNoSpin = options.segvNoSpin;
+
+  // If in competition mode, set output stream option to flush immediately
+#ifdef CVC4_COMPETITION_MODE
+  *options.out << unitbuf;
+#endif
+
+  // We only accept one input file
+  if(argc > firstArgIndex + 1) {
+    throw Exception("Too many input files specified.");
+  }
+
+  // If no file supplied we will read from standard input
+  const bool inputFromStdin =
+    firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
+
+  // if we're reading from stdin on a TTY, default to interactive mode
+  if(!options.interactiveSetByUser) {
+    options.interactive = inputFromStdin && isatty(fileno(stdin));
+  }
+
+  // Auto-detect input language by filename extension
+  const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
+
+  if(options.inputLanguage == language::input::LANG_AUTO) {
+    if( inputFromStdin ) {
+      // We can't do any fancy detection on stdin
+      options.inputLanguage = language::input::LANG_CVC4;
+    } else {
+      unsigned len = strlen(filename);
+      if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
+        options.inputLanguage = language::input::LANG_SMTLIB_V2;
+      } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
+        options.inputLanguage = language::input::LANG_SMTLIB;
+      } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
+                || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
+        options.inputLanguage = language::input::LANG_CVC4;
+      }
+    }
+  }
+
+  // Determine which messages to show based on smtcomp_mode and verbosity
+  if(Configuration::isMuzzledBuild()) {
+    Debug.setStream(CVC4::null_os);
+    Trace.setStream(CVC4::null_os);
+    Notice.setStream(CVC4::null_os);
+    Chat.setStream(CVC4::null_os);
+    Message.setStream(CVC4::null_os);
+    Warning.setStream(CVC4::null_os);
+  } else {
+    if(options.verbosity < 2) {
+      Chat.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 1) {
+      Notice.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 0) {
+      Message.setStream(CVC4::null_os);
+      Warning.setStream(CVC4::null_os);
+    }
+
+    OutputLanguage language = language::toOutputLanguage(options.inputLanguage);
+    Debug.getStream() << Expr::setlanguage(language);
+    Trace.getStream() << Expr::setlanguage(language);
+    Notice.getStream() << Expr::setlanguage(language);
+    Chat.getStream() << Expr::setlanguage(language);
+    Message.getStream() << Expr::setlanguage(language);
+    Warning.getStream() << Expr::setlanguage(language);
+  }
+
+  vector<Options> threadOptions;
+  for(int i = 0; i < numThreads; ++i) {
+    threadOptions.push_back(options);
+    Options& opts = threadOptions.back();
+
+    // Set thread identifier
+    opts.thread_id = i;
+
+    // If the random-seed is negative, pick a random seed randomly
+    if(options.satRandomSeed < 0)
+      opts.satRandomSeed = (double)rand();
+
+    if(i < (int)options.threadArgv.size() && !options.threadArgv[i].empty()) {
+      // separate out the thread's individual configuration string
+      stringstream optidss;
+      optidss << "--thread" << i;
+      string optid = optidss.str();
+      int targc = 1;
+      char* tbuf = strdup(options.threadArgv[i].c_str());
+      char* p = tbuf;
+      // string length is certainly an upper bound on size needed
+      char** targv = new char*[options.threadArgv[i].size()];
+      char** vp = targv;
+      *vp++ = strdup(optid.c_str());
+      p = strtok(p, " ");
+      while(p != NULL) {
+        *vp++ = p;
+        ++targc;
+        p = strtok(NULL, " ");
+      }
+      *vp++ = NULL;
+      if(targc > 1) { // this is necessary in case you do e.g. --thread0="  "
+        try {
+          opts.parseOptions(targc, targv);
+        } catch(OptionException& e) {
+          stringstream ss;
+          ss << optid << ": " << e.getMessage();
+          throw OptionException(ss.str());
+        }
+        if(optind != targc) {
+          stringstream ss;
+          ss << "unused argument `" << targv[optind]
+             << "' in thread configuration " << optid << " !";
+          throw OptionException(ss.str());
+        }
+        if(opts.threads != numThreads || opts.threadArgv != options.threadArgv) {
+          stringstream ss;
+          ss << "not allowed to set thread options in " << optid << " !";
+          throw OptionException(ss.str());
+        }
+      }
+      free(targv[0]);
+      delete targv;
+      free(tbuf);
+    }
+  }
+
+  // Some more options related stuff
+
+  /* Use satRandomSeed for generating random numbers, in particular satRandomSeed-s */
+  srand((unsigned int)(-options.satRandomSeed));
+
+  assert(numThreads >= 1);      //do we need this?
+
+  /* Output to string stream  */
+  vector<stringstream*> ss_out(numThreads);
+  if(options.verbosity == 0 or options.separateOutput) {
+    for(int i = 0;i <numThreads; ++i) {
+      ss_out[i] = new stringstream;
+      threadOptions[i].out = ss_out[i];
+    }
+  }
+
+  /****************************** Driver Statistics *************************/
+
+  // Statistics init
+  pStatistics = &theStatisticsRegistry;
+
+  StatisticsRegistry driverStatisticsRegistry("driver");
+  theStatisticsRegistry.registerStat_((&driverStatisticsRegistry));
+
+  // Timer statistic
+  RegisterStatistic* statTotatTime =
+    new RegisterStatistic(&driverStatisticsRegistry, &s_totalTime);
+  RegisterStatistic* statBeforePortfolioTime =
+    new RegisterStatistic(&driverStatisticsRegistry, &s_beforePortfolioTime);
+
+  // Filename statistics
+  ReferenceStat< const char* > s_statFilename("filename", filename);
+  RegisterStatistic* statFilenameReg =
+    new RegisterStatistic(&driverStatisticsRegistry, &s_statFilename);
+
+
+  /****************** ExprManager + CommandParsing + Export *****************/
+
+  // Create the expression manager
+  ExprManager* exprMgrs[numThreads];
+  exprMgrs[0] = new ExprManager(threadOptions[0]);
+  ExprManager* exprMgr = exprMgrs[0]; // to avoid having to change code which uses that
+
+  // Parse commands until we are done
+  Command* cmd;
+  // bool status = true;           // Doesn't seem to be use right now: commenting it out
+  CommandSequence* seq = new CommandSequence();
+  if( options.interactive ) {
+    InteractiveShell shell(*exprMgr, options);
+    Message() << Configuration::getPackageName()
+              << " " << Configuration::getVersionString();
+    if(Configuration::isSubversionBuild()) {
+      Message() << " [subversion " << Configuration::getSubversionBranchName()
+                << " r" << Configuration::getSubversionRevision()
+                << (Configuration::hasSubversionModifications() ?
+                    " (with modifications)" : "")
+                << "]";
+    }
+    Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
+              << " assertions:"
+              << (Configuration::isAssertionBuild() ? "on" : "off")
+              << endl;
+    while((cmd = shell.readCommand())) {
+      seq->addCommand(cmd);
+    }
+  } else {
+    ParserBuilder parserBuilder =
+      ParserBuilder(exprMgr, filename).
+        withOptions(options);
+
+    if( inputFromStdin ) {
+      parserBuilder.withStreamInput(cin);
+    }
+
+    Parser *parser = parserBuilder.build();
+    while((cmd = parser->nextCommand())) {
+      seq->addCommand(cmd);
+      // doCommand(smt, cmd, options);
+      // delete cmd;
+    }
+    // Remove the parser
+    delete parser;
+  }
+
+  exprMgr = NULL;               // don't want to use that variable
+                                // after this point
+
+  /* Duplication, Individualisation */
+  ExprManagerMapCollection* vmaps[numThreads]; // vmaps[0] is generally empty
+  Command *seqs[numThreads];
+  seqs[0] = seq;   seq = NULL;
+  for(int i = 1; i < numThreads; ++i) {
+    vmaps[i] = new ExprManagerMapCollection();
+    exprMgrs[i] = new ExprManager(threadOptions[i]);
+    seqs[i] = seqs[0]->exportTo(exprMgrs[i], *(vmaps[i]) );
+  }
+  /**
+   * vmaps[i].d_from [x] = y means
+   *    that in thread #0's expr manager id is y
+   *    and  in thread #i's expr manager id is x
+   * opposite for d_to
+   *
+   * d_from[x] : in a sense gives the id if converting *from* it to
+   *             first thread
+   */
+
+  /**
+   * Create identity variable map for the first thread, with only
+   * those variables which have a corresponding variable in another
+   * thread. (TODO:Also assert, all threads have the same set of
+   * variables mapped.)
+   */
+  if(numThreads >= 2) {
+    // Get keys from the first thread
+    //Set<uint64_t> s = vmaps[1]->d_to.keys();
+    vmaps[0] = new ExprManagerMapCollection(); // identity be default?
+    for(typeof(vmaps[1]->d_to.begin()) i=vmaps[1]->d_to.begin(); i!=vmaps[1]->d_to.end(); ++i) {
+      (vmaps[0]->d_from)[i->first] = i->first;
+    }
+    vmaps[0]->d_to = vmaps[0]->d_from;
+  }
+
+  // Create the SmtEngine(s)
+  SmtEngine *smts[numThreads];
+  for(int i = 0; i < numThreads; ++i) {
+    smts[i] = new SmtEngine(exprMgrs[i]);
+
+    // Register the statistics registry of the thread
+    string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i].thread_id);
+    smts[i]->getStatisticsRegistry()->setName(tag);
+    theStatisticsRegistry.registerStat_( (Stat*)smts[i]->getStatisticsRegistry() );
+  }
+
+  /************************* Lemma sharing init ************************/
+
+  /* Sharing channels */
+  SharedChannel<channelFormat> *channelsOut[numThreads], *channelsIn[numThreads];
+
+  if(numThreads == 1) {
+    // Disable sharing
+    threadOptions[0].sharingFilterByLength = 0;
+  } else {
+    // Setup sharing channels
+    const unsigned int sharingChannelSize = 1000000;
+
+    for(int i = 0; i<numThreads; ++i){
+      if(Debug.isOn("channel-empty")) {
+        channelsOut[i] = new EmptySharedChannel<channelFormat>(sharingChannelSize);
+        channelsIn[i] = new EmptySharedChannel<channelFormat>(sharingChannelSize);
+        continue;
+      }
+      channelsOut[i] = new SynchronizedSharedChannel<channelFormat>(sharingChannelSize);
+      channelsIn[i] = new SynchronizedSharedChannel<channelFormat>(sharingChannelSize);
+    }
+
+    /* Lemma output channel */
+    for(int i = 0; i<numThreads; ++i) {
+      string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i].thread_id);
+      threadOptions[i].lemmaOutputChannel =
+        new PortfolioLemmaOutputChannel(tag, channelsOut[i], exprMgrs[i],
+                                        vmaps[i]->d_from, vmaps[i]->d_to);
+      threadOptions[i].lemmaInputChannel =
+        new PortfolioLemmaInputChannel(tag, channelsIn[i], exprMgrs[i],
+                                       vmaps[i]->d_from, vmaps[i]->d_to);
+    }
+  }
+
+  /************************** End of initialization ***********************/
+
+  /* Portfolio */
+  boost::function<Result()> fns[numThreads];
+
+  for(int i = 0; i < numThreads; ++i) {
+    fns[i] = boost::bind(doSmt, boost::ref(*smts[i]), seqs[i], boost::ref(threadOptions[i]));
+  }
+
+  boost::function<void()>
+    smFn = boost::bind(sharingManager<channelFormat>, numThreads, channelsOut, channelsIn, smts);
+
+  s_beforePortfolioTime.stop();
+  pair<int, Result> portfolioReturn = runPortfolio(numThreads, smFn, fns, true);
+  int winner = portfolioReturn.first;
+  Result result = portfolioReturn.second;
+
+  cout << result << endl;
+
+  /************************* Post printing answer ***********************/
+
+  if(options.printWinner){
+    cout << "The winner is #" << winner << endl;
+  }
+
+  Result satRes = result.asSatisfiabilityResult();
+  int returnValue;
+  if(satRes.isSat() == Result::SAT) {
+    returnValue = 10;
+  } else if(satRes.isSat() == Result::UNSAT) {
+    returnValue = 20;
+  } else {
+    returnValue = 0;
+  }
+
+#ifdef CVC4_COMPETITION_MODE
+  // exit, don't return
+  // (don't want destructors to run)
+  exit(returnValue);
+#endif
+
+  // ReferenceStat< Result > s_statSatResult("sat/unsat", result);
+  // RegisterStatistic statSatResultReg(*exprMgr, &s_statSatResult);
+
+  // Stop timers, enough work done
+  s_totalTime.stop();
+
+  if(options.statistics) {
+    pStatistics->flushInformation(*options.err);
+  }
+
+  if(options.separateOutput) {
+    for(int i = 0; i < numThreads; ++i) {
+      *options.out << "--- Output from thread #" << i << " ---" << endl;
+      *options.out << ss_out[i]->str();
+    }
+  }
+
+  /*if(options.statistics) {
+    double totalTime = double(s_totalTime.getData().tv_sec) +
+        double(s_totalTime.getData().tv_nsec)/1000000000.0;
+    cout.precision(6);
+    *options.err << "real time: " << totalTime << "s\n";
+    int th0_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(options.lemmaOutputChannel)).cnt;
+    int th1_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(threadOptions[1].lemmaOutputChannel)).cnt;
+    *options.err << "lemmas shared by thread #0: " << th0_lemcnt << endl;
+    *options.err << "lemmas shared by thread #1: " << th1_lemcnt << endl;
+    *options.err << "sharing rate: " << double(th0_lemcnt+th1_lemcnt)/(totalTime)
+                 << " lem/sec" << endl;
+    *options.err << "winner: #" << (winner == 0 ? 0 : 1) << endl;
+  }*/
+
+  // destruction is causing segfaults, let us just exit
+  exit(returnValue);
+
+  //delete vmaps;
+
+  delete statTotatTime;
+  delete statBeforePortfolioTime;
+  delete statFilenameReg;
+
+  // delete seq;
+  // delete exprMgr;
+
+  // delete seq2;
+  // delete exprMgr2;
+
+  return returnValue;
+}
+
+/**** Code shared with driver.cpp ****/
+
+namespace CVC4 {
+  namespace main {/* Global options variable */
+    CVC4_THREADLOCAL(Options*) pOptions;
+
+    /** Full argv[0] */
+    const char *progPath;
+
+    /** Just the basename component of argv[0] */
+    const char *progName;
+  }
+}
+
+void printUsage(Options& options, bool full) {
+  stringstream ss;
+  ss << "usage: " << options.binary_name << " [options] [input-file]" << endl
+      << endl
+      << "Without an input file, or with `-', CVC4 reads from standard input." << endl
+      << endl
+      << "CVC4 options:" << endl;
+  if(full) {
+    Options::printUsage( ss.str(), *options.out );
+  } else {
+    Options::printShortUsage( ss.str(), *options.out );
+  }
+}
+
+/** Executes a command. Deletes the command after execution. */
+static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
+  if( options.parseOnly ) {
+    return true;
+  }
+
+  // assume no error
+  bool status = true;
+
+  CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
+  if(seq != NULL) {
+    for(CommandSequence::iterator subcmd = seq->begin();
+        subcmd != seq->end();
+        ++subcmd) {
+      status = doCommand(smt, *subcmd, options) && status;
+    }
+  } else {
+    // by default, symmetry breaker is on only for QF_UF
+    if(! options.ufSymmetryBreakerSetByUser) {
+      SetBenchmarkLogicCommand *logic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd);
+      if(logic != NULL) {
+        options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF");
+      }
+    }
+
+    if(options.verbosity > 0) {
+      *options.out << "Invoking: " << *cmd << endl;
+    }
+
+    if(options.verbosity >= 0) {
+      cmd->invoke(&smt, *options.out);
+    } else {
+      cmd->invoke(&smt);
+    }
+    status = status && cmd->ok();
+  }
+
+  return status;
+}
+
+/**** End of code shared with driver.cpp ****/
+
+/** Create the SMT engine and execute the commands */
+Result doSmt(SmtEngine &smt, Command *cmd, Options &options) {
+
+  try {
+    // For the signal handlers' benefit
+    pOptions = &options;
+
+    // Execute the commands
+    bool status = doCommand(smt, cmd, options);
+
+    // if(options.statistics) {
+    //   smt.getStatisticsRegistry()->flushInformation(*options.err);
+    //   *options.err << "Statistics printing of my thread complete " << endl;
+    // }
+
+    return status ? smt.getStatusOfLastCommand() : Result::SAT_UNKNOWN;
+  } catch(OptionException& e) {
+    *pOptions->out << "unknown" << endl;
+    cerr << "CVC4 Error:" << endl << e << endl;
+    printUsage(*pOptions);
+    return Result::SAT_UNKNOWN;
+  } catch(Exception& e) {
+#ifdef CVC4_COMPETITION_MODE
+    *pOptions->out << "unknown" << endl;
+#endif
+    *pOptions->err << "CVC4 Error:" << endl << e << endl;
+    if(pOptions->statistics) {
+      pStatistics->flushInformation(*pOptions->err);
+    }
+    return Result::SAT_UNKNOWN;
+  } catch(bad_alloc) {
+#ifdef CVC4_COMPETITION_MODE
+    *pOptions->out << "unknown" << endl;
+#endif
+    *pOptions->err << "CVC4 ran out of memory." << endl;
+    if(pOptions->statistics) {
+      pStatistics->flushInformation(*pOptions->err);
+    }
+    return Result::SAT_UNKNOWN;
+  } catch(...) {
+#ifdef CVC4_COMPETITION_MODE
+    *pOptions->out << "unknown" << endl;
+#endif
+    *pOptions->err << "CVC4 threw an exception of unknown type." << endl;
+    return Result::SAT_UNKNOWN;
+  }
+}
+
+template<typename T>
+void sharingManager(int numThreads,
+                    SharedChannel<T> *channelsOut[], // out and in with respect
+                    SharedChannel<T> *channelsIn[],
+                    SmtEngine *smts[])  // to smt engines
+{
+  Trace("sharing") << "sharing: thread started " << std::endl;
+  vector <int> cnt(numThreads); // Debug("sharing")
+
+  vector< queue<T> > queues;
+  for(int i = 0; i < numThreads; ++i){
+    queues.push_back(queue<T>());
+  }
+
+  const unsigned int sharingBroadcastInterval = 1;
+
+  boost::mutex mutex_activity;
+
+  /* Disable interruption, so that we can check manually */
+  boost::this_thread::disable_interruption di;
+
+  while(not boost::this_thread::interruption_requested()) {
+
+    boost::this_thread::sleep(boost::posix_time::milliseconds(sharingBroadcastInterval));
+
+    for(int t = 0; t < numThreads; ++t) {
+
+      if(channelsOut[t]->empty()) continue;      /* No activity on this channel */
+
+      /* Alert if channel full, so that we increase sharingChannelSize
+         or decrease sharingBroadcastInterval */
+      Assert(not channelsOut[t]->full());
+
+      T data = channelsOut[t]->pop();
+
+      if(Trace.isOn("sharing")) {
+        ++cnt[t];
+        Trace("sharing") << "sharing: Got data. Thread #" << t
+                         << ". Chunk " << cnt[t] << std :: endl;
+      }
+
+      for(int u = 0; u < numThreads; ++u) {
+        if(u != t){
+          Trace("sharing") << "sharing: adding to queue " << u << std::endl;
+          queues[u].push(data);
+        }
+      }/* end of inner for: broadcast activity */
+
+    } /* end of outer for: look for activity */
+
+    for(int t = 0; t < numThreads; ++t){
+      /* Alert if channel full, so that we increase sharingChannelSize
+         or decrease sharingBroadcastInterval */
+      Assert(not channelsIn[t]->full());
+
+      while(!queues[t].empty() && !channelsIn[t]->full()){
+        Trace("sharing") << "sharing: pushing on channel " << t << std::endl;
+        T data = queues[t].front();
+        channelsIn[t]->push(data);
+        queues[t].pop();
+      }
+    }
+  } /* end of infinite while */
+
+  Trace("interrupt") << "sharing thread interuppted, interrupting all smtEngines" << std::endl;
+
+  for(int t = 0; t < numThreads; ++t) {
+    Trace("interrupt") << "Interuppting thread #" << t << std::endl;
+    try{
+      smts[t]->interrupt();
+    }catch(ModalException &e){
+      // It's fine, the thread is probably not there.
+      Trace("interrupt") << "Could not interrupt thread #" << t << std::endl;
+    }
+  }
+
+  Trace("sharing") << "sharing: Interuppted, exiting." << std::endl;
+}
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index dca554330..a63d6c67b 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -85,7 +85,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
   d_out(*options.out),
   d_language(options.inputLanguage),
   d_quit(false) {
-  ParserBuilder parserBuilder(&exprManager,INPUT_FILENAME,options);
+  ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, options);
   /* Create parser with bogus input. */
   d_parser = parserBuilder.withStringInput("").build();
 
diff --git a/src/main/main.cpp b/src/main/main.cpp
index ecef7e79f..5d051cdad 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -20,12 +20,10 @@
 #include <cstring>
 #include <fstream>
 #include <iostream>
-#include <new>
 
 #include <stdio.h>
 #include <unistd.h>
 
-#include "cvc4autoconfig.h"
 #include "main/main.h"
 #include "main/interactive_shell.h"
 #include "parser/parser.h"
@@ -43,42 +41,8 @@
 
 using namespace std;
 using namespace CVC4;
-using namespace CVC4::parser;
 using namespace CVC4::main;
 
-static int runCvc4(int argc, char* argv[]);
-static bool doCommand(SmtEngine&, Command*);
-static void printUsage(bool full = false);
-
-namespace CVC4 {
-  namespace main {
-    /** Global options variable */
-    Options options;
-
-    /** Full argv[0] */
-    const char *progPath;
-
-    /** Just the basename component of argv[0] */
-    const char *progName;
-
-    /** A pointer to the StatisticsRegistry (the signal handlers need it) */
-    CVC4::StatisticsRegistry* pStatistics;
-  }
-}
-
-static void printUsage(bool full) {
-  stringstream ss;
-  ss << "usage: " << options.binary_name << " [options] [input-file]" << endl
-      << endl
-      << "Without an input file, or with `-', CVC4 reads from standard input." << endl
-      << endl;
-  if(full) {
-    Options::printUsage( ss.str(), *options.out );
-  } else {
-    Options::printShortUsage( ss.str(), *options.out );
-  }
-}
-
 /**
  * CVC4's main() routine is just an exception-safe wrapper around CVC4.
  * Please don't construct anything here.  Even if the constructor is
@@ -87,14 +51,15 @@ static void printUsage(bool full) {
  * Put everything in runCvc4().
  */
 int main(int argc, char* argv[]) {
+  Options options;
   try {
-    return runCvc4(argc, argv);
+    return runCvc4(argc, argv, options);
   } catch(OptionException& e) {
 #ifdef CVC4_COMPETITION_MODE
     *options.out << "unknown" << endl;
 #endif
     cerr << "CVC4 Error:" << endl << e << endl;
-    printUsage();
+    printUsage(options);
     exit(1);
   } catch(Exception& e) {
 #ifdef CVC4_COMPETITION_MODE
@@ -102,7 +67,7 @@ int main(int argc, char* argv[]) {
 #endif
     *options.err << "CVC4 Error:" << endl << e << endl;
     if(options.statistics && pStatistics != NULL) {
-      pStatistics->flushStatistics(*options.err);
+      pStatistics->flushInformation(*options.err);
     }
     exit(1);
   } catch(bad_alloc&) {
@@ -111,7 +76,7 @@ int main(int argc, char* argv[]) {
 #endif
     *options.err << "CVC4 ran out of memory." << endl;
     if(options.statistics && pStatistics != NULL) {
-      pStatistics->flushStatistics(*options.err);
+      pStatistics->flushInformation(*options.err);
     }
     exit(1);
   } catch(...) {
@@ -122,276 +87,3 @@ int main(int argc, char* argv[]) {
     exit(1);
   }
 }
-
-
-static int runCvc4(int argc, char* argv[]) {
-
-  // Initialize the signal handlers
-  cvc4_init();
-
-  progPath = argv[0];
-
-  // Parse the options
-  int firstArgIndex = options.parseOptions(argc, argv);
-
-  progName = options.binary_name.c_str();
-
-  if( options.help ) {
-    printUsage(true);
-    exit(1);
-  } else if( options.languageHelp ) {
-    Options::printLanguageHelp(*options.out);
-    exit(1);
-  } else if( options.version ) {
-    *options.out << Configuration::about().c_str() << flush;
-    exit(0);
-  }
-
-  segvNoSpin = options.segvNoSpin;
-
-  // If in competition mode, set output stream option to flush immediately
-#ifdef CVC4_COMPETITION_MODE
-  *options.out << unitbuf;
-#endif
-
-  // We only accept one input file
-  if(argc > firstArgIndex + 1) {
-    throw Exception("Too many input files specified.");
-  }
-
-  // If no file supplied we will read from standard input
-  const bool inputFromStdin =
-    firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
-
-  // if we're reading from stdin on a TTY, default to interactive mode
-  if(!options.interactiveSetByUser) {
-    options.interactive = inputFromStdin && isatty(fileno(stdin));
-  }
-
-  // Determine which messages to show based on smtcomp_mode and verbosity
-  if(Configuration::isMuzzledBuild()) {
-    Debug.setStream(CVC4::null_os);
-    Trace.setStream(CVC4::null_os);
-    Notice.setStream(CVC4::null_os);
-    Chat.setStream(CVC4::null_os);
-    Message.setStream(CVC4::null_os);
-    Warning.setStream(CVC4::null_os);
-    Dump.setStream(CVC4::null_os);
-  } else {
-    if(options.verbosity < 2) {
-      Chat.setStream(CVC4::null_os);
-    }
-    if(options.verbosity < 1) {
-      Notice.setStream(CVC4::null_os);
-    }
-    if(options.verbosity < 0) {
-      Message.setStream(CVC4::null_os);
-      Warning.setStream(CVC4::null_os);
-    }
-  }
-
-  // Create the expression manager
-  ExprManager exprMgr(options);
-
-  // Create the SmtEngine
-  SmtEngine smt(&exprMgr);
-
-  // signal handlers need access
-  pStatistics = smt.getStatisticsRegistry();
-
-  // Auto-detect input language by filename extension
-  const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
-
-  ReferenceStat< const char* > s_statFilename("filename", filename);
-  RegisterStatistic statFilenameReg(exprMgr, &s_statFilename);
-
-  if(options.inputLanguage == language::input::LANG_AUTO) {
-    if( inputFromStdin ) {
-      // We can't do any fancy detection on stdin
-      options.inputLanguage = language::input::LANG_CVC4;
-    } else {
-      unsigned len = strlen(filename);
-      if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
-        options.inputLanguage = language::input::LANG_SMTLIB_V2;
-      } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
-        options.inputLanguage = language::input::LANG_SMTLIB;
-      } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
-                || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
-        options.inputLanguage = language::input::LANG_CVC4;
-      }
-    }
-  }
-
-  if(options.outputLanguage == language::output::LANG_AUTO) {
-    options.outputLanguage = language::toOutputLanguage(options.inputLanguage);
-  }
-
-  // Determine which messages to show based on smtcomp_mode and verbosity
-  if(Configuration::isMuzzledBuild()) {
-    Debug.setStream(CVC4::null_os);
-    Trace.setStream(CVC4::null_os);
-    Notice.setStream(CVC4::null_os);
-    Chat.setStream(CVC4::null_os);
-    Message.setStream(CVC4::null_os);
-    Warning.setStream(CVC4::null_os);
-    Dump.setStream(CVC4::null_os);
-  } else {
-    if(options.verbosity < 2) {
-      Chat.setStream(CVC4::null_os);
-    }
-    if(options.verbosity < 1) {
-      Notice.setStream(CVC4::null_os);
-    }
-    if(options.verbosity < 0) {
-      Message.setStream(CVC4::null_os);
-      Warning.setStream(CVC4::null_os);
-    }
-
-    Debug.getStream() << Expr::setlanguage(options.outputLanguage);
-    Trace.getStream() << Expr::setlanguage(options.outputLanguage);
-    Notice.getStream() << Expr::setlanguage(options.outputLanguage);
-    Chat.getStream() << Expr::setlanguage(options.outputLanguage);
-    Message.getStream() << Expr::setlanguage(options.outputLanguage);
-    Warning.getStream() << Expr::setlanguage(options.outputLanguage);
-    Dump.getStream() << Expr::setlanguage(options.outputLanguage)
-                     << Expr::setdepth(-1)
-                     << Expr::printtypes(false);
-  }
-
-  Parser* replayParser = NULL;
-  if( options.replayFilename != "" ) {
-    ParserBuilder replayParserBuilder(&exprMgr, options.replayFilename, options);
-
-    if( options.replayFilename == "-") {
-      if( inputFromStdin ) {
-        throw OptionException("Replay file and input file can't both be stdin.");
-      }
-      replayParserBuilder.withStreamInput(cin);
-    }
-    replayParser = replayParserBuilder.build();
-    options.replayStream = new Parser::ExprStream(replayParser);
-  }
-  if( options.replayLog != NULL ) {
-    *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1);
-  }
-
-  // Parse and execute commands until we are done
-  Command* cmd;
-  bool status = true;
-  if( options.interactive ) {
-    InteractiveShell shell(exprMgr, options);
-    Message() << Configuration::getPackageName()
-              << " " << Configuration::getVersionString();
-    if(Configuration::isSubversionBuild()) {
-      Message() << " [" << Configuration::getSubversionId() << "]";
-    }
-    Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
-              << " assertions:"
-              << (Configuration::isAssertionBuild() ? "on" : "off")
-              << endl;
-    if(replayParser != NULL) {
-      // have the replay parser use the declarations input interactively
-      replayParser->useDeclarationsFrom(shell.getParser());
-    }
-    while((cmd = shell.readCommand())) {
-      status = doCommand(smt, cmd) && status;
-      delete cmd;
-    }
-  } else {
-    ParserBuilder parserBuilder(&exprMgr, filename, options);
-
-    if( inputFromStdin ) {
-      parserBuilder.withStreamInput(cin);
-    }
-
-    Parser *parser = parserBuilder.build();
-    if(replayParser != NULL) {
-      // have the replay parser use the file's declarations
-      replayParser->useDeclarationsFrom(parser);
-    }
-    while((cmd = parser->nextCommand())) {
-      status = doCommand(smt, cmd) && status;
-      delete cmd;
-    }
-    // Remove the parser
-    delete parser;
-  }
-
-  if( options.replayStream != NULL ) {
-    // this deletes the expression parser too
-    delete options.replayStream;
-    options.replayStream = NULL;
-  }
-
-  int returnValue;
-  string result = "unknown";
-  if(status) {
-    result = smt.getInfo(":status").getValue();
-
-    if(result == "sat") {
-      returnValue = 10;
-    } else if(result == "unsat") {
-      returnValue = 20;
-    } else {
-      returnValue = 0;
-    }
-  } else {
-    // there was some kind of error
-    returnValue = 1;
-  }
-
-#ifdef CVC4_COMPETITION_MODE
-  // exit, don't return
-  // (don't want destructors to run)
-  exit(returnValue);
-#endif
-
-  ReferenceStat< Result > s_statSatResult("sat/unsat", result);
-  RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult);
-
-  if(options.statistics) {
-    smt.getStatisticsRegistry()->flushStatistics(*options.err);
-  }
-
-  return returnValue;
-}
-
-/** Executes a command. Deletes the command after execution. */
-static bool doCommand(SmtEngine& smt, Command* cmd) {
-  if( options.parseOnly ) {
-    return true;
-  }
-
-  // assume no error
-  bool status = true;
-
-  CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
-  if(seq != NULL) {
-    for(CommandSequence::iterator subcmd = seq->begin();
-        subcmd != seq->end();
-        ++subcmd) {
-      status = doCommand(smt, *subcmd) && status;
-    }
-  } else {
-    // by default, symmetry breaker is on only for QF_UF
-    if(! options.ufSymmetryBreakerSetByUser) {
-      SetBenchmarkLogicCommand *logic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd);
-      if(logic != NULL) {
-        options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF");
-      }
-    }
-
-    if(options.verbosity > 0) {
-      *options.out << "Invoking: " << *cmd << endl;
-    }
-
-    if(options.verbosity >= 0) {
-      cmd->invoke(&smt, *options.out);
-    } else {
-      cmd->invoke(&smt);
-    }
-    status = status && cmd->ok();
-  }
-
-  return status;
-}
diff --git a/src/main/main.h b/src/main/main.h
index 1771198f4..4df5ccc49 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -22,6 +22,7 @@
 #include "util/options.h"
 #include "util/exception.h"
 #include "util/stats.h"
+#include "util/tls.h"
 #include "cvc4autoconfig.h"
 
 #ifndef __CVC4__MAIN__MAIN_H
@@ -46,8 +47,8 @@ extern CVC4::StatisticsRegistry* pStatistics;
  */
 extern bool segvNoSpin;
 
-/** The options currently in play */
-extern Options options;
+/** A pointer to the options in play */
+extern CVC4_THREADLOCAL(Options*) pOptions;
 
 /** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
 void cvc4_init() throw(Exception);
@@ -55,4 +56,8 @@ void cvc4_init() throw(Exception);
 }/* CVC4::main namespace */
 }/* CVC4 namespace */
 
+/** Actual Cvc4 driver functions **/
+int runCvc4(int argc, char* argv[], CVC4::Options&);
+void printUsage(CVC4::Options&, bool full = false);
+
 #endif /* __CVC4__MAIN__MAIN_H */
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp
new file mode 100644
index 000000000..fc22374cf
--- /dev/null
+++ b/src/main/portfolio.cpp
@@ -0,0 +1,93 @@
+/*********************                                                        */
+/*! \file portfolio.cpp
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include <boost/function.hpp>
+#include <boost/thread.hpp>
+#include <boost/bind.hpp>
+#include <boost/thread/condition.hpp>
+#include <boost/exception_ptr.hpp>
+
+#include "smt/smt_engine.h"
+#include "util/result.h"
+#include "util/options.h"
+
+using namespace boost;
+
+namespace CVC4 {
+
+mutex mutex_done;
+mutex mutex_main_wait;
+condition condition_var_main_wait;
+
+bool global_flag_done = false;
+int global_winner = -1;
+
+template<typename S>
+void runThread(int thread_id, function<S()> threadFn, S& returnValue) {
+  returnValue = threadFn();
+
+  if( mutex_done.try_lock() ) {
+    if(global_flag_done == false) {
+      global_flag_done = true;
+      global_winner = thread_id;
+    }
+    mutex_done.unlock();
+    condition_var_main_wait.notify_all(); // we want main thread to quit
+  }
+}
+
+template<typename T, typename S>
+std::pair<int, S> runPortfolio(int numThreads,
+                               function<T()> driverFn,
+                               function<S()> threadFns[],
+                               bool optionWaitToJoin) {
+  thread thread_driver;
+  thread threads[numThreads];
+  S threads_returnValue[numThreads];
+
+  for(int t = 0; t < numThreads; ++t) {
+    threads[t] = thread(bind(runThread<S>, t, threadFns[t], ref(threads_returnValue[t]) ));
+  }
+
+  if(not driverFn.empty())
+    thread_driver = boost::thread(driverFn);
+
+  while(global_flag_done == false)
+    condition_var_main_wait.wait(mutex_main_wait);
+
+  if(not driverFn.empty()) {
+    thread_driver.interrupt();
+    thread_driver.join();
+  }
+
+  for(int t = 0; t < numThreads; ++t) {
+    if(optionWaitToJoin) {
+      threads[t].join();
+    }
+  }
+
+  return std::pair<int, S>(global_winner,threads_returnValue[global_winner]);
+}
+
+// instantiation
+template
+std::pair<int, Result>
+runPortfolio<void, Result>(int, boost::function<void()>, boost::function<Result()>*, bool);
+
+}/* CVC4 namespace */
diff --git a/src/main/portfolio.h b/src/main/portfolio.h
new file mode 100644
index 000000000..9bc911be3
--- /dev/null
+++ b/src/main/portfolio.h
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file portfolio.h
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#ifndef __CVC4__PORTFOLIO_H
+#define __CVC4__PORTFOLIO_H
+
+#include <boost/function.hpp>
+#include <utility>
+
+#include "smt/smt_engine.h"
+#include "expr/command.h"
+#include "util/options.h"
+
+namespace CVC4 {
+
+template<typename T, typename S>
+std::pair<int, S> runPortfolio(int numThreads, 
+                              boost::function<T()> driverFn,
+                              boost::function<S()> threadFns[],
+                              bool optionWaitToJoin);
+// as we have defined things, S=void would give compile errors
+// do we want to fix this? yes, no, maybe?
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PORTFOLIO_H */
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 89aa5c6aa..35cff4abd 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -51,8 +51,8 @@ bool segvNoSpin = false;
 /** Handler for SIGXCPU, i.e., timeout. */
 void timeout_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by timeout.\n");
-  if(options.statistics && pStatistics != NULL) {
-    pStatistics->flushStatistics(cerr);
+  if(pOptions->statistics && pStatistics != NULL) {
+    pStatistics->flushInformation(cerr);
   }
   abort();
 }
@@ -60,8 +60,8 @@ void timeout_handler(int sig, siginfo_t* info, void*) {
 /** Handler for SIGINT, i.e., when the user hits control C. */
 void sigint_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by user.\n");
-  if(options.statistics && pStatistics != NULL) {
-    pStatistics->flushStatistics(cerr);
+  if(pOptions->statistics && pStatistics != NULL) {
+    pStatistics->flushInformation(cerr);
   }
   abort();
 }
@@ -85,8 +85,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
 
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested, aborting...\n");
-    if(options.statistics && pStatistics != NULL) {
-      pStatistics->flushStatistics(cerr);
+    if(pOptions->statistics && pStatistics != NULL) {
+      pStatistics->flushInformation(cerr);
     }
     abort();
   } else {
@@ -105,8 +105,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
   } else if(addr < 10*1024) {
     cerr << "Looks like a NULL pointer was dereferenced." << endl;
   }
-  if(options.statistics && pStatistics != NULL) {
-    pStatistics->flushStatistics(cerr);
+  if(pOptions->statistics && pStatistics != NULL) {
+    pStatistics->flushInformation(cerr);
   }
   abort();
 #endif /* CVC4_DEBUG */
@@ -118,8 +118,8 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n");
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested, aborting...\n");
-    if(options.statistics && pStatistics != NULL) {
-      pStatistics->flushStatistics(cerr);
+    if(pOptions->statistics && pStatistics != NULL) {
+      pStatistics->flushInformation(cerr);
     }
     abort();
   } else {
@@ -131,8 +131,8 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 executed an illegal instruction.\n");
-  if(options.statistics && pStatistics != NULL) {
-    pStatistics->flushStatistics(cerr);
+  if(pOptions->statistics && pStatistics != NULL) {
+    pStatistics->flushInformation(cerr);
   }
   abort();
 #endif /* CVC4_DEBUG */
@@ -155,8 +155,8 @@ void cvc4unexpected() {
   }
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested.\n");
-    if(options.statistics && pStatistics != NULL) {
-      pStatistics->flushStatistics(cerr);
+    if(pOptions->statistics && pStatistics != NULL) {
+      pStatistics->flushInformation(cerr);
     }
     set_terminate(default_terminator);
   } else {
@@ -168,8 +168,8 @@ void cvc4unexpected() {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n");
-  if(options.statistics && pStatistics != NULL) {
-    pStatistics->flushStatistics(cerr);
+  if(pOptions->statistics && pStatistics != NULL) {
+    pStatistics->flushInformation(cerr);
   }
   set_terminate(default_terminator);
 #endif /* CVC4_DEBUG */
@@ -181,16 +181,16 @@ void cvc4terminate() {
           "CVC4 was terminated by the C++ runtime.\n"
           "Perhaps an exception was thrown during stack unwinding.  "
           "(Don't do that.)\n");
-  if(options.statistics && pStatistics != NULL) {
-    pStatistics->flushStatistics(cerr);
+  if(pOptions->statistics && pStatistics != NULL) {
+    pStatistics->flushInformation(cerr);
   }
   default_terminator();
 #else /* CVC4_DEBUG */
   fprintf(stderr,
           "CVC4 was terminated by the C++ runtime.\n"
           "Perhaps an exception was thrown during stack unwinding.\n");
-  if(options.statistics && pStatistics != NULL) {
-    pStatistics->flushStatistics(cerr);
+  if(pOptions->statistics && pStatistics != NULL) {
+    pStatistics->flushInformation(cerr);
   }
   default_terminator();
 #endif /* CVC4_DEBUG */
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 5c755b5f6..c17956e62 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -28,26 +28,25 @@
 #include "util/options.h"
 
 namespace CVC4 {
-
 namespace parser {
 
-ParserBuilder::ParserBuilder(ExprManager* exprManager, 
-                             const std::string& filename) : 
+ParserBuilder::ParserBuilder(ExprManager* exprManager,
+                             const std::string& filename) :
   d_filename(filename),
   d_exprManager(exprManager) {
-  init(exprManager,filename);
+  init(exprManager, filename);
 }
 
-ParserBuilder::ParserBuilder(ExprManager* exprManager, 
-                             const std::string& filename, 
+ParserBuilder::ParserBuilder(ExprManager* exprManager,
+                             const std::string& filename,
                              const Options& options) :
   d_filename(filename),
   d_exprManager(exprManager) {
-  init(exprManager,filename);
+  init(exprManager, filename);
   withOptions(options);
 }
 
-void ParserBuilder::init(ExprManager* exprManager, 
+void ParserBuilder::init(ExprManager* exprManager,
                          const std::string& filename) {
   d_inputType = FILE_INPUT;
   d_lang = language::input::LANG_AUTO;
@@ -60,26 +59,26 @@ void ParserBuilder::init(ExprManager* exprManager,
   d_parseOnly = false;
 }
 
-Parser *ParserBuilder::build() 
-  throw (InputStreamException,AssertionException) {
-  Input *input = NULL;
+Parser* ParserBuilder::build()
+  throw (InputStreamException, AssertionException) {
+  Input* input = NULL;
   switch( d_inputType ) {
   case FILE_INPUT:
-    input = Input::newFileInput(d_lang,d_filename,d_mmap);
+    input = Input::newFileInput(d_lang, d_filename, d_mmap);
     break;
   case STREAM_INPUT:
     AlwaysAssert( d_streamInput != NULL,
                   "Uninitialized stream input in ParserBuilder::build()" );
-    input = Input::newStreamInput(d_lang,*d_streamInput,d_filename);
+    input = Input::newStreamInput(d_lang, *d_streamInput, d_filename);
     break;
   case STRING_INPUT:
-    input = Input::newStringInput(d_lang,d_stringInput,d_filename);
+    input = Input::newStringInput(d_lang, d_stringInput, d_filename);
     break;
   default:
     Unreachable();
   }
 
-  Parser *parser = NULL;
+  Parser* parser = NULL;
   switch(d_lang) {
   case language::input::LANG_SMTLIB:
     parser = new Smt(d_exprManager, input, d_strictMode, d_parseOnly);
@@ -162,6 +161,5 @@ ParserBuilder& ParserBuilder::withStringInput(const std::string& input) {
   return *this;
 }
 
-} /* namespace parser */
-
-} /* namespace CVC4 */
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 0463a079f..ce01d3c53 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -61,7 +61,7 @@ class CVC4_PUBLIC ParserBuilder {
   std::string d_stringInput;
 
   /** The stream input, if any. */
-  std::istream *d_streamInput;
+  std::istream* d_streamInput;
 
   /** The expression manager */
   ExprManager* d_exprManager;
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 09e072370..7f1456639 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -43,8 +43,9 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace prop {
 
-CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar) :
+CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar, bool fullLitToNodeMap) :
   d_satSolver(satSolver),
+  d_fullLitToNodeMap(fullLitToNodeMap),
   d_registrar(registrar) {
 }
 
@@ -129,7 +130,7 @@ void TseitinCnfStream::ensureLiteral(TNode n) {
                 n.toString().c_str(),
                 n.getType().toString().c_str());
 
-  bool negated = false;
+  bool negated CVC4_UNUSED = false;
   SatLiteral lit;
 
   if(n.getKind() == kind::NOT) {
@@ -178,7 +179,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
   d_translationCache[node.notNode()].level = level;
 
   // If it's a theory literal, need to store it for back queries
-  if ( theoryLiteral ||
+  if ( theoryLiteral || d_fullLitToNodeMap ||
        ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) ||
        Dump.isOn("clauses") ) {
     d_nodeCache[lit] = node;
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 5eaeeef94..c9fd4a08b 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -69,6 +69,13 @@ protected:
   TranslationCache d_translationCache;
   NodeCache d_nodeCache;
 
+  /**
+   * True if the lit-to-Node map should be kept for all lits, not just
+   * theory lits.  This is true if e.g. replay logging is on, which
+   * dumps the Nodes corresponding to decision literals.
+   */
+  const bool d_fullLitToNodeMap;
+
   /** The "registrar" for pre-registration of terms */
   theory::Registrar d_registrar;
 
@@ -179,8 +186,10 @@ public:
    * set of clauses and sends them to the given sat solver.
    * @param satSolver the sat solver to use
    * @param registrar the entity that takes care of preregistration of Nodes
+   * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
+   * even for non-theory literals.
    */
-  CnfStream(SatInputInterface* satSolver, theory::Registrar registrar);
+  CnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap = false);
 
   /**
    * Destructs a CnfStream.  This implementation does nothing, but we
@@ -283,7 +292,7 @@ public:
 private:
 
   /**
-   * Same as above, except that removable is rememebered.
+   * Same as above, except that removable is remembered.
    */
   void convertAndAssert(TNode node, bool negated);
 
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 36f411df4..7df7535dd 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -22,6 +22,7 @@
 #include "prop/sat.h"
 #include "context/context.h"
 #include "theory/theory_engine.h"
+#include "theory/rewriter.h"
 #include "expr/expr_stream.h"
 
 namespace CVC4 {
@@ -89,6 +90,55 @@ TNode SatSolver::getNode(SatLiteral lit) {
 void SatSolver::notifyRestart() {
   d_propEngine->checkTime();
   d_theoryEngine->notifyRestart();
+
+  static uint32_t lemmaCount = 0;
+
+  if(Options::current()->lemmaInputChannel != NULL) {
+    while(Options::current()->lemmaInputChannel->hasNewLemma()) {
+      Debug("shared") << "shared" << std::endl;
+      Expr lemma = Options::current()->lemmaInputChannel->getNewLemma();
+      Node asNode = lemma.getNode();
+      asNode = theory::Rewriter::rewrite(asNode);
+
+      if(d_shared.find(asNode) == d_shared.end()) {
+        d_shared.insert(asNode);
+        if(asNode.getKind() == kind::OR) {
+          ++lemmaCount;
+          if(lemmaCount % 1 == 0) {
+            Debug("shared") << "=) " << asNode << std::endl;
+          }
+          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true);
+        } else {
+          Debug("shared") << "=(" << asNode << std::endl;
+        }
+      } else {
+        Debug("shared") <<"drop shared " << asNode << std::endl;
+      }
+    }
+  }
+}
+
+void SatSolver::notifyNewLemma(SatClause& lemma) {
+  Assert(lemma.size() > 0);
+  if(Options::current()->lemmaOutputChannel != NULL) {
+    if(lemma.size() == 1) {
+      // cannot share units yet
+      //Options::current()->lemmaOutputChannel->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr());
+    } else {
+      NodeBuilder<> b(kind::OR);
+      for(unsigned i = 0, i_end = lemma.size(); i < i_end; ++i) {
+        b << d_cnfStream->getNode(lemma[i]);
+      }
+      Node n = b;
+
+      if(d_shared.find(n) == d_shared.end()) {
+        d_shared.insert(n);
+        Options::current()->lemmaOutputChannel->notifyNewLemma(n.toExpr());
+      } else {
+        Debug("shared") <<"drop new " << n << std::endl;
+      }
+    }
+  }
 }
 
 SatLiteral SatSolver::getNextReplayDecision() {
diff --git a/src/prop/sat.h b/src/prop/sat.h
index be3ed244b..e86443827 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -137,6 +137,12 @@ class SatSolver : public SatInputInterface {
   /** Context we will be using to synchronzie the sat solver */
   context::Context* d_context;
 
+  /**
+   * Set of all lemmas that have been "shared" in the portfolio---i.e.,
+   * all imported and exported lemmas.
+   */
+  std::hash_set<Node, NodeHashFunction> d_shared;
+
   /* Pointer to the concrete SAT solver. Including this via the
      preprocessor saves us a level of indirection vs, e.g., defining a
      sub-class for each solver. */
@@ -263,6 +269,8 @@ public:
 
   void notifyRestart();
 
+  void notifyNewLemma(SatClause& lemma);
+
   SatLiteral getNextReplayDecision();
 
   void logDecision(SatLiteral lit);
@@ -294,6 +302,12 @@ inline SatSolver::SatSolver(PropEngine* propEngine,
   d_minisat->random_var_freq = Options::current()->satRandomFreq;
   d_minisat->random_seed = Options::current()->satRandomSeed;
 
+  // Give access to all possible options in the sat solver
+  d_minisat->var_decay = Options::current()->satVarDecay;
+  d_minisat->clause_decay = Options::current()->satClauseDecay;
+  d_minisat->restart_first = Options::current()->satRestartFirst;
+  d_minisat->restart_inc = Options::current()->satRestartInc;
+
   d_statistics.init(d_minisat);
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a8f2d5700..52a98f414 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -455,6 +455,10 @@ public:
    */
   StatisticsRegistry* getStatisticsRegistry() const;
 
+  Result getStatusOfLastCommand() const {
+    return d_status;
+  }
+
 };/* class SmtEngine */
 
 }/* CVC4 namespace */
diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp
index 3b1f5f395..e74a250a3 100644
--- a/src/theory/arith/arith_priority_queue.cpp
+++ b/src/theory/arith/arith_priority_queue.cpp
@@ -191,12 +191,15 @@ void ArithPriorityQueue::transitionToDifferenceMode() {
 
   switch(d_pivotRule){
   case MINIMUM:
+    Debug("arith::pivotRule") << "Making the minimum heap." << endl;
     make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::minimumRule);
     break;
   case BREAK_TIES:
+    Debug("arith::pivotRule") << "Making the break ties heap." << endl;
     make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::breakTiesRules);
     break;
   case MAXIMUM:
+    Debug("arith::pivotRule") << "Making the maximum heap." << endl;
     make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::maximumRule);
     break;
   }
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 27fb0bb02..26cdb2cdb 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -619,9 +619,9 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
   if(d_queue.empty()){
     return Node::null();
   }
-  static unsigned int instance = 0;
-  ++instance;
 
+  static CVC4_THREADLOCAL(unsigned int) instance = 0;
+  ++instance;
   Debug("arith::updateInconsistentVars") << "begin updateInconsistentVars() "
                                          << instance << endl;
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 64e713b0a..268829105 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1223,7 +1223,7 @@ void TheoryArith::presolve(){
 
   if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); }
 
-  static int callCount = 0;
+  static CVC4_THREADLOCAL(unsigned) callCount = 0;
   Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl;
 
   d_learner.clear();
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 9c69ec684..511982d48 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -29,7 +29,7 @@ namespace arith {
 class ArithConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType();
     return nodeManager->integerType();
   }
@@ -38,7 +38,7 @@ public:
 class ArithOperatorTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TypeNode integerType = nodeManager->integerType();
     TypeNode realType = nodeManager->realType();
     TNode::iterator child_it = n.begin();
@@ -65,7 +65,7 @@ public:
 class ArithPredicateTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
       TypeNode integerType = nodeManager->integerType();
       TypeNode realType = nodeManager->realType();
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index bd3c8ad67..fd9e7cb2f 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -27,7 +27,7 @@ namespace arrays {
 
 struct ArraySelectTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate) {
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
     Assert(n.getKind() == kind::SELECT);
     TypeNode arrayType = n[0].getType(check);
     if( check ) {
@@ -45,7 +45,7 @@ struct ArraySelectTypeRule {
 
 struct ArrayStoreTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate) {
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
     Assert(n.getKind() == kind::STORE);
     TypeNode arrayType = n[0].getType(check);
     if( check ) {
diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index e6c3e0f54..3b30b9f59 100644
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -28,7 +28,7 @@ namespace boolean {
 class BooleanTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TypeNode booleanType = nodeManager->booleanType();
     if( check ) {
       TNode::iterator child_it = n.begin();
@@ -49,7 +49,7 @@ public:
 class IteTypeRule {
   public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TypeNode iteType = n[1].getType(check);
     if( check ) {
       TypeNode booleanType = nodeManager->booleanType();
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 86603f004..cd3e1437f 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -34,7 +34,7 @@ namespace builtin {
 class ApplyTypeRule {
   public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate) {
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
     TNode f = n.getOperator();
     TypeNode fType = f.getType(check);
     if( !fType.isFunction() && n.getNumChildren() > 0 ) {
@@ -72,7 +72,7 @@ class ApplyTypeRule {
 
 class EqualityTypeRule {
   public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) {
     TypeNode booleanType = nodeManager->booleanType();
 
     if( check ) {
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index a232ad33b..566bf3a68 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -84,7 +84,7 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
   return RewriteResponse(REWRITE_DONE, result);
 }
 
-AllRewriteRules* TheoryBVRewriter::s_allRules = NULL;
+CVC4_THREADLOCAL(AllRewriteRules*) TheoryBVRewriter::s_allRules = NULL;
 
 void TheoryBVRewriter::init() {
   s_allRules = new AllRewriteRules;
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 11a55ca61..f0eb621ca 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -32,7 +32,7 @@ struct AllRewriteRules;
 
 class TheoryBVRewriter {
 
-  static AllRewriteRules* s_allRules;
+  static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules;
 
 public:
 
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 926ceb767..192295bc0 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -30,7 +30,7 @@ namespace bv {
 class BitVectorConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
   }
 };
@@ -38,7 +38,7 @@ public:
 class BitVectorCompRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
       TypeNode lhs = n[0].getType(check);
       TypeNode rhs = n[1].getType(check);
@@ -53,7 +53,7 @@ public:
 class BitVectorArithRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     unsigned maxWidth = 0;
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
@@ -72,7 +72,7 @@ public:
 class BitVectorFixedWidthTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TNode::iterator it = n.begin();
     TypeNode t = (*it).getType(check);
     if( check ) {
@@ -93,7 +93,7 @@ public:
 class BitVectorPredicateTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
       TypeNode lhsType = n[0].getType(check);
       if (!lhsType.isBitVector()) {
@@ -111,7 +111,7 @@ public:
 class BitVectorExtractTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>();
 
     // NOTE: We're throwing a type-checking exception here even
@@ -137,7 +137,7 @@ public:
 class BitVectorConcatRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     unsigned size = 0;
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
@@ -158,7 +158,7 @@ public:
 class BitVectorRepeatTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TypeNode t = n[0].getType(check);
     // NOTE: We're throwing a type-checking exception here even
     // when check is false, bc if the argument isn't a bit-vector
@@ -174,7 +174,7 @@ public:
 class BitVectorExtendTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TypeNode t = n[0].getType(check);
     // NOTE: We're throwing a type-checking exception here even
     // when check is false, bc if the argument isn't a bit-vector
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 147fb868e..6385d1467 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -364,6 +364,12 @@ class TheoryEngine {
                        << std::endl
                        << QueryCommand(node.toExpr()) << std::endl;
     }
+
+    // Share with other portfolio threads
+    if(Options::current()->lemmaOutputChannel != NULL) {
+      Options::current()->lemmaOutputChannel->notifyNewLemma(node.toExpr());
+    }
+
     // Remove the ITEs and assert to prop engine
     std::vector<Node> additionalLemmas;
     additionalLemmas.push_back(node);
@@ -514,13 +520,13 @@ public:
   void staticLearning(TNode in, NodeBuilder<>& learned);
 
   /**
-   * Calls presolve() on all active theories and returns true
+   * Calls presolve() on all theories and returns true
    * if one of the theories discovers a conflict.
    */
   bool presolve();
 
    /**
-   * Calls postsolve() on all active theories.
+   * Calls postsolve() on all theories.
    */
   void postsolve();
 
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 927a31e01..9b622bc15 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -28,7 +28,7 @@ namespace uf {
 class UfTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TNode f = n.getOperator();
     TypeNode fType = f.getType(check);
     if( !fType.isFunction() ) {
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index c5a20cd5d..3cb6ea16f 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -50,6 +50,9 @@ libutil_la_SOURCES = \
 	stats.cpp \
 	dynamic_array.h \
 	language.h \
+	lemma_output_channel.h \
+	channel.h \
+	channel.cpp \
 	language.cpp \
 	ntuple.h \
 	recursion_breaker.h \
diff --git a/src/util/channel.cpp b/src/util/channel.cpp
new file mode 100644
index 000000000..998550f8e
--- /dev/null
+++ b/src/util/channel.cpp
@@ -0,0 +1,2 @@
+#include "channel.h"
+
diff --git a/src/util/channel.h b/src/util/channel.h
new file mode 100644
index 000000000..1701feba9
--- /dev/null
+++ b/src/util/channel.h
@@ -0,0 +1,96 @@
+
+#ifndef __CVC4__CHANNEL_H
+#define __CVC4__CHANNEL_H
+
+#include <boost/circular_buffer.hpp>
+#include <boost/thread/mutex.hpp>
+#include <boost/thread/condition.hpp>
+#include <boost/thread/thread.hpp>
+#include <boost/call_traits.hpp>
+#include <boost/progress.hpp>
+#include <boost/bind.hpp>
+
+
+namespace CVC4 {
+
+template <typename T>
+class SharedChannel {
+private:
+  int d_maxsize;                // just call it size?
+public:
+  SharedChannel() {}
+  SharedChannel(int maxsize) : d_maxsize(maxsize) {}
+
+  /* Tries to add element and returns true if successful */
+  virtual bool push(const T&) = 0;
+
+  /* Removes an element from the channel */
+  virtual T pop() = 0;
+  
+  /* */
+  virtual bool empty() = 0; 
+  
+  /* */
+  virtual bool full() = 0;
+};
+
+/* 
+This code is from
+
+http://live.boost.org/doc/libs/1_46_1/libs/circular_buffer/doc/circular_buffer.html#boundedbuffer 
+*/
+template <typename T>
+class SynchronizedSharedChannel: public SharedChannel<T> {
+public:
+  typedef boost::circular_buffer<T> container_type;
+  typedef typename container_type::size_type size_type;
+  typedef typename container_type::value_type value_type;
+  typedef typename boost::call_traits<value_type>::param_type param_type;
+
+  explicit SynchronizedSharedChannel(size_type capacity) : m_unread(0), m_container(capacity) {}
+
+  bool push(param_type item){
+  // param_type represents the "best" way to pass a parameter of type value_type to a method
+  
+    boost::mutex::scoped_lock lock(m_mutex);
+    m_not_full.wait(lock, boost::bind(&SynchronizedSharedChannel<value_type>::is_not_full, this));
+    m_container.push_front(item);
+    ++m_unread;
+    lock.unlock();
+    m_not_empty.notify_one();
+    return true;
+  }//function definitions need to be moved to cpp
+
+  value_type pop(){
+    value_type ret;
+    boost::mutex::scoped_lock lock(m_mutex);
+    m_not_empty.wait(lock, boost::bind(&SynchronizedSharedChannel<value_type>::is_not_empty, this));
+    ret = m_container[--m_unread];
+    lock.unlock();
+    m_not_full.notify_one();
+    return ret;
+  }
+
+
+  bool empty() { return not is_not_empty(); }
+  bool full() { return not is_not_full(); }
+
+private:
+  SynchronizedSharedChannel(const SynchronizedSharedChannel&);              // Disabled copy constructor
+  SynchronizedSharedChannel& operator = (const SynchronizedSharedChannel&); // Disabled assign operator
+
+  bool is_not_empty() const { return m_unread > 0; }
+  bool is_not_full() const { return m_unread < m_container.capacity(); }
+
+  size_type m_unread;
+  container_type m_container;
+  boost::mutex m_mutex;
+  boost::condition m_not_empty;
+  boost::condition m_not_full;
+};
+
+}
+
+#endif /* __CVC4__CHANNEL_H */
+
+
diff --git a/src/util/hash.h b/src/util/hash.h
index 6183c5208..5f0189d44 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -26,6 +26,22 @@
 namespace __gnu_cxx {}
 
 #include <ext/hash_map>
+
+namespace __gnu_cxx {
+
+#if __WORDSIZE == 32
+// on 32-bit, we need a specialization of hash for 64-bit values
+template <>
+struct hash<uint64_t> {
+  size_t operator()(uint64_t v) const {
+    return v;
+  }
+};/* struct hash<uint64_t> */
+#endif /* 32-bit */
+
+}/* __gnu_cxx namespace */
+
+// hackish: treat hash stuff as if it were in std namespace
 namespace std { using namespace __gnu_cxx; }
 
 namespace CVC4 {
diff --git a/src/util/lemma_input_channel.h b/src/util/lemma_input_channel.h
new file mode 100644
index 000000000..1627711ee
--- /dev/null
+++ b/src/util/lemma_input_channel.h
@@ -0,0 +1,19 @@
+#include "cvc4_public.h"
+
+#ifndef __CVC4__LEMMA_INPUT_CHANNEL_H
+#define __CVC4__LEMMA_INPUT_CHANNEL_H
+
+#include "expr/expr.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC LemmaInputChannel {
+public:
+  virtual bool hasNewLemma() = 0;
+  virtual Expr getNewLemma() = 0;
+
+};/* class LemmaOutputChannel */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__LEMMA_INPUT_CHANNEL_H */
diff --git a/src/util/lemma_output_channel.h b/src/util/lemma_output_channel.h
new file mode 100644
index 000000000..720dd6512
--- /dev/null
+++ b/src/util/lemma_output_channel.h
@@ -0,0 +1,46 @@
+/*********************                                                        */
+/*! \file lemma_output_channel.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Mechanism for communication about new lemmas
+ **
+ ** This file defines an interface for use by the theory and propositional
+ ** engines to communicate new lemmas to the "outside world," for example
+ ** for lemma sharing between threads.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__LEMMA_OUTPUT_CHANNEL_H
+#define __CVC4__LEMMA_OUTPUT_CHANNEL_H
+
+#include "expr/expr.h"
+
+namespace CVC4 {
+
+/**
+ * This interface describes a mechanism for the propositional and theory
+ * engines to communicate with the "outside world" about new lemmas being
+ * discovered.
+ */
+class CVC4_PUBLIC LemmaOutputChannel {
+public:
+  /**
+   * Notifies this output channel that there's a new lemma.
+   * The lemma may or may not be in CNF.
+   */
+  virtual void notifyNewLemma(Expr lemma) = 0;
+};/* class LemmaOutputChannel */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__LEMMA_OUTPUT_CHANNEL_H */
diff --git a/src/util/options.cpp b/src/util/options.cpp
index d33064c73..e33fbc263 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -64,6 +64,9 @@ Options::Options() :
   verbosity(0),
   inputLanguage(language::input::LANG_AUTO),
   outputLanguage(language::output::LANG_AUTO),
+  help(false),
+  version(false),
+  languageHelp(false),
   parseOnly(false),
   preprocessOnly(false),
   semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT),
@@ -71,6 +74,7 @@ Options::Options() :
   memoryMap(false),
   strictParsing(false),
   lazyDefinitionExpansion(false),
+  printWinner(false),
   simplificationMode(SIMPLIFICATION_MODE_BATCH),
   doStaticLearning(true),
   interactive(false),
@@ -93,12 +97,23 @@ Options::Options() :
   arithPropagation(true),
   satRandomFreq(0.0),
   satRandomSeed(91648253),// Minisat's default value
+  satVarDecay(0.95),
+  satClauseDecay(0.999),
+  satRestartFirst(25),
+  satRestartInc(3.0),
   pivotRule(MINIMUM),
   arithPivotThreshold(16),
   arithPropagateMaxLength(16),
   ufSymmetryBreaker(false),
   ufSymmetryBreakerSetByUser(false),
-  dioSolver(true)
+  dioSolver(true),
+  lemmaOutputChannel(NULL),
+  lemmaInputChannel(NULL),
+  threads(2),// default should be 1 probably, but say 2 for now
+  threadArgv(),
+  thread_id(-1),
+  separateOutput(false),
+  sharingFilterByLength(-1)
 {
 }
 
@@ -141,6 +156,7 @@ Additional CVC4 options:\n\
    --no-type-checking     never type check expressions\n\
    --no-checking          disable ALL semantic checks, including type checks\n\
    --no-theory-registration disable theory reg (not safe for some theories)\n\
+   --print-winner         enable printing the winning thread (pcvc4 only)\n\
    --trace | -t           trace something (e.g. -t pushpop), can repeat\n\
    --debug | -d           debug something (e.g. -d arith), can repeat\n\
    --show-debug-tags      show all avalable tags for debugging\n\
@@ -157,13 +173,19 @@ Additional CVC4 options:\n\
    --prop-row-length=N    sets the maximum row length to be used in propagation\n\
    --random-freq=P        sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\
    --random-seed=S        sets the random seed for the sat solver\n\
+   --restart-int-base=I   sets the base restart interval for the sat solver (I=25 by default)\n\
+   --restart-int-inc=F    sets the restart interval increase factor for the sat solver (F=3.0 by default)\n\
    --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\
    --disable-arithmetic-propagation turns on arithmetic propagation\n\
    --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al., CADE 2011) [on by default only for QF_UF]\n\
    --disable-symmetry-breaker turns off UF symmetry breaker\n\
    --disable-dio-solver   turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\
+   --threads=N            sets the number of solver threads\n\
+   --threadN=string       configures thread N (0..#threads-1)\n\
+   --filter-lemma-length=N don't share lemmas strictly longer than N\n\
 ";
 
+
 #warning "Change CL options as --disable-variable-removal cannot do anything currently."
 
 static const string languageDescription = "\
@@ -322,8 +344,11 @@ enum OptionValue {
   REPLAY,
   REPLAY_LOG,
   PIVOT_RULE,
+  PRINT_WINNER,
   RANDOM_FREQUENCY,
   RANDOM_SEED,
+  SAT_RESTART_FIRST,
+  SAT_RESTART_INC,
   ARITHMETIC_VARIABLE_REMOVAL,
   ARITHMETIC_PROPAGATION,
   ARITHMETIC_PIVOT_THRESHOLD,
@@ -331,6 +356,9 @@ enum OptionValue {
   ARITHMETIC_DIO_SOLVER,
   ENABLE_SYMMETRY_BREAKER,
   DISABLE_SYMMETRY_BREAKER,
+  PARALLEL_THREADS,
+  PARALLEL_SEPARATE_OUTPUT,
+  PORTFOLIO_FILTER_LENGTH,
   TIME_LIMIT,
   TIME_LIMIT_PER,
   RESOURCE_LIMIT,
@@ -409,11 +437,17 @@ static struct option cmdlineOptions[] = {
   { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH  },
   { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY  },
   { "random-seed" , required_argument, NULL, RANDOM_SEED  },
+  { "restart-int-base", required_argument, NULL, SAT_RESTART_FIRST },
+  { "restart-int-inc", required_argument, NULL, SAT_RESTART_INC },
+  { "print-winner", no_argument     , NULL, PRINT_WINNER  },
   { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL },
   { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION },
   { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER },
   { "enable-symmetry-breaker", no_argument, NULL, ENABLE_SYMMETRY_BREAKER },
   { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER },
+  { "threads", required_argument, NULL, PARALLEL_THREADS },
+  { "separate-output", no_argument, NULL, PARALLEL_SEPARATE_OUTPUT },
+  { "filter-lemma-length", required_argument, NULL, PORTFOLIO_FILTER_LENGTH },
   { "tlimit"     , required_argument, NULL, TIME_LIMIT  },
   { "tlimit-per" , required_argument, NULL, TIME_LIMIT_PER },
   { "rlimit"     , required_argument, NULL, RESOURCE_LIMIT       },
@@ -428,6 +462,13 @@ throw(OptionException) {
   const char *progName = argv[0];
   int c;
 
+  // Reset getopt(), in the case of multiple calls.
+  // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
+  optind = 0;
+#if HAVE_DECL_OPTRESET
+  optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this
+#endif /* HAVE_DECL_OPTRESET */
+
   // find the base name of the program
   const char *x = strrchr(progName, '/');
   if(x != NULL) {
@@ -595,6 +636,10 @@ throw(OptionException) {
       memoryMap = true;
       break;
 
+    case PRINT_WINNER:
+      printWinner = true;
+      break;
+
     case STRICT_PARSING:
       strictParsing = true;
       break;
@@ -807,6 +852,26 @@ throw(OptionException) {
                               optarg + "' is not between 0.0 and 1.0.");
       }
       break;
+      
+    case SAT_RESTART_FIRST:
+      {
+        int i = atoi(optarg);
+        if(i < 1) {
+          throw OptionException("--restart-int-base requires a number bigger than 1");
+        }
+        satRestartFirst = i;
+        break;
+      }
+      
+    case SAT_RESTART_INC:
+      {
+        int i = atoi(optarg);
+        if(i < 1) {
+          throw OptionException("--restart-int-inc requires a number bigger than 1.0");
+        }
+        satRestartInc = i;
+      }
+      break;
 
     case PIVOT_RULE:
       if(!strcmp(optarg, "min")) {
@@ -905,11 +970,40 @@ throw(OptionException) {
       printf("tls        : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no");
       exit(0);
 
+    case PARALLEL_THREADS:
+      threads = atoi(optarg);
+      break;
+
+    case PARALLEL_SEPARATE_OUTPUT:
+      separateOutput = true;
+      break;
+
+    case PORTFOLIO_FILTER_LENGTH:
+      sharingFilterByLength = atoi(optarg);
+      break; 
+
     case ':':
       throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument");
 
     case '?':
     default:
+      if(optopt == 0 &&
+         !strncmp(argv[optind - 1], "--thread", 8) &&
+         strlen(argv[optind - 1]) > 8 &&
+         isdigit(argv[optind - 1][8])) {
+        int tnum = atoi(argv[optind - 1] + 8);
+        threadArgv.resize(tnum + 1);
+        if(threadArgv[tnum] != "") {
+          threadArgv[tnum] += " ";
+        }
+        const char* p = strchr(argv[optind - 1] + 9, '=');
+        if(p == NULL) { // e.g., we have --thread0 "foo"
+          threadArgv[tnum] += argv[optind++];
+        } else { // e.g., we have --thread0="foo"
+          threadArgv[tnum] += p + 1;
+        }
+        break;
+      }
       throw OptionException(string("can't understand option `") + argv[optind - 1] + "'");
     }
   }
diff --git a/src/util/options.h b/src/util/options.h
index d04947b02..6b8054a13 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -27,8 +27,12 @@
 
 #include "util/exception.h"
 #include "util/language.h"
+#include "util/lemma_output_channel.h"
+#include "util/lemma_input_channel.h"
 #include "util/tls.h"
 
+#include <vector>
+
 namespace CVC4 {
 
 class ExprStream;
@@ -104,6 +108,9 @@ struct CVC4_PUBLIC Options {
   /** Should we expand function definitions lazily? */
   bool lazyDefinitionExpansion;
 
+  /** Parallel Only: Whether the winner is printed at the end or not. */
+  bool printWinner;
+
   /** Enumeration of simplification modes (when to simplify). */
   typedef enum {
     /** Simplify the assertions as they come in */
@@ -187,6 +194,18 @@ struct CVC4_PUBLIC Options {
    **/
   double satRandomSeed;
 
+  /** Variable activity decay factor for Minisat */
+  double satVarDecay;
+  
+  /** Clause activity decay factor for Minisat */
+  double satClauseDecay;
+
+  /** Base restart interval for Minisat */
+  int satRestartFirst;
+
+  /** Restart interval increase factor for Minisat */
+  double satRestartInc;
+
   /** The pivot rule for arithmetic */
   typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule;
   ArithPivotRule pivotRule;
@@ -220,6 +239,28 @@ struct CVC4_PUBLIC Options {
    */
   bool dioSolver;
 
+  /** The output channel to receive notfication events for new lemmas */
+  LemmaOutputChannel* lemmaOutputChannel;
+  LemmaInputChannel* lemmaInputChannel;
+
+  /** Total number of threads */
+  int threads;
+
+  /** Thread configuration (a string to be passed to parseOptions) */
+  std::vector<std::string> threadArgv;
+
+  /** Thread ID, for internal use in case of multi-threaded run */
+  int thread_id;
+
+  /** 
+   * In multi-threaded setting print output of each thread at the
+   * end of run, separated by a divider ("----").
+   **/
+  bool separateOutput;
+
+  /** Filter depending on length of lemma */
+  int sharingFilterByLength;
+
   Options();
 
   /**
diff --git a/src/util/stats.cpp b/src/util/stats.cpp
index 474d8fa7a..709f80b04 100644
--- a/src/util/stats.cpp
+++ b/src/util/stats.cpp
@@ -31,6 +31,7 @@
 using namespace CVC4;
 
 std::string Stat::s_delim(",");
+std::string StatisticsRegistry::s_regDelim("::");
 
 StatisticsRegistry* StatisticsRegistry::current() {
   return NodeManager::currentNM()->getStatisticsRegistry();
@@ -45,6 +46,14 @@ void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) {
 #endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::registerStat() */
 
+void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException)
+{
+#ifdef CVC4_STATISTICS_ON
+  AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end());
+  d_registeredStats.insert(s);
+#endif /* CVC4_STATISTICS_ON */
+}/* StatisticsRegistry::registerStat_() */
+
 void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) {
 #ifdef CVC4_STATISTICS_ON
   StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats;
@@ -54,17 +63,33 @@ void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) {
 #endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::unregisterStat() */
 
-void StatisticsRegistry::flushStatistics(std::ostream& out) {
+void StatisticsRegistry::unregisterStat_(Stat* s) throw(AssertionException) {
+#ifdef CVC4_STATISTICS_ON
+  AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end());
+  d_registeredStats.erase(s);
+#endif /* CVC4_STATISTICS_ON */
+}/* StatisticsRegistry::unregisterStat_() */
+
+void StatisticsRegistry::flushInformation(std::ostream& out) const {
 #ifdef CVC4_STATISTICS_ON
   for(StatSet::iterator i = d_registeredStats.begin();
       i != d_registeredStats.end();
       ++i) {
     Stat* s = *i;
+    if(d_name != "") {
+      out << d_name << s_regDelim;
+    }
     s->flushStat(out);
     out << std::endl;
   }
 #endif /* CVC4_STATISTICS_ON */
-}/* StatisticsRegistry::flushStatistics() */
+}/* StatisticsRegistry::flushInformation() */
+
+void StatisticsRegistry::flushStat(std::ostream &out) const {;
+#ifdef CVC4_STATISTICS_ON
+  flushInformation(out);
+#endif /* CVC4_STATISTICS_ON */
+}
 
 StatisticsRegistry::const_iterator StatisticsRegistry::begin() {
   return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.begin();
@@ -93,16 +118,9 @@ void TimerStat::stop() {
 }/* TimerStat::stop() */
 
 RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) :
-    d_em(&em), d_stat(stat) {
-  ExprManagerScope ems(*d_em);
-  StatisticsRegistry::registerStat(d_stat);
-}/* RegisterStatistic::RegisterStatistic(ExprManager&, Stat*) */
-
-RegisterStatistic::~RegisterStatistic() {
-  if(d_em != NULL) {
-    ExprManagerScope ems(*d_em);
-    StatisticsRegistry::unregisterStat(d_stat);
-  } else {
-    StatisticsRegistry::unregisterStat(d_stat);
-  }
-}/* RegisterStatistic::~RegisterStatistic() */
+  d_reg(NULL),
+  d_stat(stat) {
+  ExprManagerScope ems(em);
+  d_reg = StatisticsRegistry::current();
+  d_reg->registerStat_(d_stat);
+}
diff --git a/src/util/stats.h b/src/util/stats.h
index 719bbaab6..63e732305 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -2,7 +2,7 @@
 /*! \file stats.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: mdeters
+ ** Major contributors: mdeters, kshitij
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
@@ -47,84 +47,32 @@ class ExprManager;
 class CVC4_PUBLIC Stat;
 
 /**
- * The main statistics registry.  This registry maintains the list of
- * currently active statistics and is able to "flush" them all.
- */
-class CVC4_PUBLIC StatisticsRegistry {
-private:
-  /** A helper class for comparing two statistics */
-  struct StatCmp {
-    inline bool operator()(const Stat* s1, const Stat* s2) const;
-  };/* class StatisticsRegistry::StatCmp */
-
-  /** A type for a set of statistics */
-  typedef std::set< Stat*, StatCmp > StatSet;
-
-  /** The set of currently active statistics */
-  StatSet d_registeredStats;
-
-  /** Private copy constructor undefined (no copy permitted). */
-  StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED;
-
-public:
-
-  /** Construct a statistics registry */
-  StatisticsRegistry() { }
-
-  /** An iterator type over a set of statistics */
-  typedef StatSet::const_iterator const_iterator;
-
-  /** Get a pointer to the current statistics registry */
-  static StatisticsRegistry* current();
-
-  /** Flush all statistics to the given output stream. */
-  void flushStatistics(std::ostream& out);
-
-  /** Register a new statistic, making it active. */
-  static void registerStat(Stat* s) throw(AssertionException);
-
-  /** Unregister an active statistic, making it inactive. */
-  static void unregisterStat(Stat* s) throw(AssertionException);
-
-  /**
-   * Get an iterator to the beginning of the range of the set of active
-   * (registered) statistics.
-   */
-  static const_iterator begin();
-
-  /**
-   * Get an iterator to the end of the range of the set of active
-   * (registered) statistics.
-   */
-  static const_iterator end();
-
-};/* class StatisticsRegistry */
-
-
-/**
  * The base class for all statistics.
  *
- * This base class keeps the name of the statistic and declares two (pure)
- * virtual functionss flushInformation() and getValue().  Derived classes
- * must implement these functions and pass their name to the base class
- * constructor.
+ * This base class keeps the name of the statistic and declares the (pure)
+ * virtual function flushInformation().  Derived classes must implement
+ * this function and pass their name to the base class constructor.
  *
  * This class also (statically) maintains the delimiter used to separate
  * the name and the value when statistics are output.
  */
 class CVC4_PUBLIC Stat {
 private:
-  /** The name of this statistic */
-  std::string d_name;
-
   /**
    * The delimiter between name and value to use when outputting a
    * statistic.
    */
   static std::string s_delim;
 
+protected:
+  /** The name of this statistic */
+  std::string d_name;
+
 public:
 
+  /** Nullary constructor, does nothing */
+  Stat() { }
+
   /**
    * Construct a statistic with the given name.  Debug builds of CVC4
    * will throw an assertion exception if the given name contains the
@@ -149,8 +97,10 @@ public:
   /**
    * Flush the name,value pair of this statistic to an output stream.
    * Uses the statistic delimiter string between name and value.
+   *
+   * May be redefined by a child class
    */
-  void flushStat(std::ostream& out) const {
+  virtual void flushStat(std::ostream& out) const {
     if(__CVC4_USE_STATISTICS) {
       out << d_name << s_delim;
       flushInformation(out);
@@ -163,21 +113,18 @@ public:
   }
 
   /** Get the value of this statistic as a string. */
-  virtual std::string getValue() const = 0;
+  std::string getValue() const {
+    std::stringstream ss;
+    flushInformation(ss);
+    return ss.str();
+  }
 
 };/* class Stat */
 
-inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1,
-                                                    const Stat* s2) const {
-  return s1->getName() < s2->getName();
-}
-
 /**
  * A class to represent a "read-only" data statistic of type T.  Adds to
  * the Stat base class the pure virtual function getData(), which returns
- * type T, along with an implementation of getValue(), which converts the
- * type T to a string using an existing stream insertion operator defined
- * on T, and flushInformation(), which outputs the statistic value to an
+ * type T, and flushInformation(), which outputs the statistic value to an
  * output stream (using the same existing stream insertion operator).
  *
  * Template class T must have stream insertion operation defined:
@@ -204,13 +151,6 @@ public:
     }
   }
 
-  /** Get the value of the statistic as a string. */
-  std::string getValue() const {
-    std::stringstream ss;
-    ss << getData();
-    return ss.str();
-  }
-
 };/* class ReadOnlyDataStat<T> */
 
 
@@ -480,20 +420,20 @@ private:
    * have seen so far.
    */
   uint32_t d_count;
+  double d_sum;
 
 public:
   /** Construct an average statistic with the given name. */
   AverageStat(const std::string& name) :
-    BackedStat<double>(name, 0.0), d_count(0) {
+    BackedStat<double>(name, 0.0), d_count(0), d_sum(0.0) {
   }
 
   /** Add an entry to the running-average calculation. */
   void addEntry(double e) {
     if(__CVC4_USE_STATISTICS) {
-      double oldSum = d_count * getData();
       ++d_count;
-      double newSum = oldSum + e;
-      setData(newSum / d_count);
+      d_sum += e;
+      setData(d_sum / d_count);
     }
   }
 
@@ -535,13 +475,102 @@ public:
     return (*this);
   }
 
-  std::string getValue() const {
-    std::stringstream ss;
-    flushInformation(ss);
-    return ss.str();
+};/* class ListStat */
+
+/****************************************************************************/
+/* Statistics Registry                                                      */
+/****************************************************************************/
+
+/**
+ * The main statistics registry.  This registry maintains the list of
+ * currently active statistics and is able to "flush" them all.
+ */
+class CVC4_PUBLIC StatisticsRegistry : public Stat {
+private:
+  /** A helper class for comparing two statistics */
+  struct StatCmp {
+    inline bool operator()(const Stat* s1, const Stat* s2) const;
+  };/* class StatisticsRegistry::StatCmp */
+
+  /** A type for a set of statistics */
+  typedef std::set< Stat*, StatCmp > StatSet;
+
+  /** The set of currently active statistics */
+  StatSet d_registeredStats;
+
+  /** Private copy constructor undefined (no copy permitted). */
+  StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED;
+
+  static std::string s_regDelim;
+public:
+
+  /** Construct an nameless statistics registry */
+  StatisticsRegistry() {}
+
+  /** Construct a statistics registry */
+  StatisticsRegistry(const std::string& name) throw(CVC4::AssertionException) :
+    Stat(name) {
+    if(__CVC4_USE_STATISTICS) {
+      AlwaysAssert(d_name.find(s_regDelim) == std::string::npos);
+    }
   }
 
-};/* class ListStat */
+  /** 
+   * Set the name of this statistic registry, used as prefix during
+   * output.
+   *
+   * TODO: Get rid of this function once we have ability to set the
+   * name of StatisticsRegistry at creation time.
+   */
+  void setName(const std::string& name) {
+    d_name = name;
+  }
+
+  /** An iterator type over a set of statistics */
+  typedef StatSet::const_iterator const_iterator;
+
+  /** Get a pointer to the current statistics registry */
+  static StatisticsRegistry* current();
+
+  /** Flush all statistics to the given output stream. */
+  void flushInformation(std::ostream& out) const;
+
+  /** Obsolete flushStatistics -- use flushInformation */
+  //void flushStatistics(std::ostream& out) const;
+
+  /** Overridden to avoid the name being printed */
+  void flushStat(std::ostream &out) const;
+
+  /** Register a new statistic, making it active. */
+  static void registerStat(Stat* s) throw(AssertionException);
+
+  /** Register a new statistic */
+  void registerStat_(Stat* s) throw(AssertionException);
+
+  /** Unregister an active statistic, making it inactive. */
+  static void unregisterStat(Stat* s) throw(AssertionException);
+
+  /** Unregister a new statistic */
+  void unregisterStat_(Stat* s) throw(AssertionException);
+
+  /**
+   * Get an iterator to the beginning of the range of the set of active
+   * (registered) statistics.
+   */
+  static const_iterator begin();
+
+  /**
+   * Get an iterator to the end of the range of the set of active
+   * (registered) statistics.
+   */
+  static const_iterator end();
+
+};/* class StatisticsRegistry */
+
+inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1,
+                                                    const Stat* s2) const {
+  return s1->getName() < s2->getName();
+}
 
 /****************************************************************************/
 /* Some utility functions for timespec                                    */
@@ -753,19 +782,30 @@ public:
  * registration and unregistration.
  */
 class CVC4_PUBLIC RegisterStatistic {
-  ExprManager* d_em;
+  StatisticsRegistry* d_reg;
   Stat* d_stat;
 public:
-  RegisterStatistic(Stat* stat) : d_stat(stat) {
-    Assert(StatisticsRegistry::current() != NULL,
-           "You need to specify an expression manager "
-           "on which to set the statistic");
+  RegisterStatistic(Stat* stat) :
+      d_reg(StatisticsRegistry::current()),
+      d_stat(stat) {
+    Assert(d_reg != NULL, "There is no current statistics registry!");
     StatisticsRegistry::registerStat(d_stat);
   }
 
+  RegisterStatistic(StatisticsRegistry* reg, Stat* stat) :
+    d_reg(reg),
+    d_stat(stat) {
+    Assert(d_reg != NULL,
+           "You need to specify a statistics registry"
+           "on which to set the statistic");
+    d_reg->registerStat_(d_stat);
+  }
+
   RegisterStatistic(ExprManager& em, Stat* stat);
 
-  ~RegisterStatistic();
+  ~RegisterStatistic() {
+    d_reg->unregisterStat_(d_stat);
+  }
 
 };/* class RegisterStatistic */
 
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 27ebac603..0bc78e6c4 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,9 +1,10 @@
 SUBDIRS = . arith precedence uf uflra bv arrays datatypes lemmas push-pop preprocess
 
+BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k
diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index fdd0ad4ed..d6b2b143a 100644
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -1,9 +1,10 @@
 SUBDIRS = . integers
 
+BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 8d65ee3a9..1cdfec8fc 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -1,9 +1,10 @@
 SUBDIRS = . core
 
+BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k
diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am
index fa0144da0..6a36f5188 100644
--- a/test/regress/regress0/bv/core/Makefile.am
+++ b/test/regress/regress0/bv/core/Makefile.am
@@ -1,7 +1,8 @@
+BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../../run_regression --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../../run_regression @top_builddir@/src/main/$(BINARY)
 endif
 
 # These are run for all build profiles.
diff --git a/test/regress/regress0/lemmas/Makefile.am b/test/regress/regress0/lemmas/Makefile.am
index 70375e1d7..94104ed49 100644
--- a/test/regress/regress0/lemmas/Makefile.am
+++ b/test/regress/regress0/lemmas/Makefile.am
@@ -1,9 +1,10 @@
 SUBDIRS = . 
 
+BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k
diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am
index 6d60bcb4f..719b196ca 100644
--- a/test/regress/regress0/precedence/Makefile.am
+++ b/test/regress/regress0/precedence/Makefile.am
@@ -1,7 +1,8 @@
+BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
 endif
 
 # These are run for all build profiles.
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 827dc04aa..aedf03470 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -1,9 +1,10 @@
 SUBDIRS = . 
 
+BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index 3a9749598..e7dae1080 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -1,7 +1,8 @@
+BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
 endif
 
 # These are run for all build profiles.
diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am
index bee9e8d76..f32e980ad 100644
--- a/test/regress/regress0/uflra/Makefile.am
+++ b/test/regress/regress0/uflra/Makefile.am
@@ -1,7 +1,8 @@
+BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k
diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am
index c7087219a..2135cf55b 100644
--- a/test/regress/regress1/Makefile.am
+++ b/test/regress/regress1/Makefile.am
@@ -1,9 +1,10 @@
 SUBDIRS = . arith
 
+BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k
diff --git a/test/regress/regress1/arith/Makefile.am b/test/regress/regress1/arith/Makefile.am
index 046efe65f..3eb33d311 100644
--- a/test/regress/regress1/arith/Makefile.am
+++ b/test/regress/regress1/arith/Makefile.am
@@ -1,7 +1,8 @@
+BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
 endif
 
 # These are run for all build profiles.
diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am
index 8a17bf6b2..d084ad47a 100644
--- a/test/regress/regress2/Makefile.am
+++ b/test/regress/regress2/Makefile.am
@@ -1,9 +1,10 @@
 SUBDIRS = .
 
+BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k
diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am
index 08a675273..201e332d1 100644
--- a/test/regress/regress3/Makefile.am
+++ b/test/regress/regress3/Makefile.am
@@ -1,9 +1,10 @@
 SUBDIRS = .
 
+BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k