added model generation for bv subtheories and bv-inequality solver option

68 files changed, 1393 insertions, 308 deletions

diff --git a/NEWS b/NEWS
index 3c38aab56..9d4b5452d 100644
--- a/NEWS
+++ b/NEWS
@@ -15,5 +15,6 @@ Changes since 1.0
   use -q.  Previously, this would silence all output (including "sat" or
   "unsat") as well.  Now, single -q silences messages and warnings, and
   double -qq silences all output (except on exception or signal).
+* Boolean term support in datatypes
 
--- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 20 Feb 2013 18:31:50 -0500
+-- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 20 Mar 2013 20:03:50 -0400
diff --git a/src/Makefile.am b/src/Makefile.am
index b505750d4..1dbf77451 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -137,7 +137,7 @@ gitinfo: gitinfo.tmp
 # .PHONY ensures the .tmp version is always rebuilt (to check for any changes)
 .PHONY: gitinfo.tmp
 gitinfo.tmp:
-	$(AM_V_GEN)(cd "$(top_srcdir)"; if ! grep -q '^ref: refs/heads/' .git/HEAD; then echo; fi; sed 's,^ref: refs/heads/,,' .git/HEAD; git show-ref refs/heads/`sed 's,^ref: refs/heads/,,' .git/HEAD`; echo "Modifications: `test -z \"\`git status -s -uno\`\" && echo false || echo true`") >"$@" 2>/dev/null || true
+	$(AM_V_GEN)(cd "$(top_srcdir)"; if test -e .git/HEAD; then if ! grep -q '^ref: refs/heads/' .git/HEAD; then echo; fi; sed 's,^ref: refs/heads/,,' .git/HEAD; git show-ref refs/heads/`sed 's,^ref: refs/heads/,,' .git/HEAD`; echo "Modifications: `test -z \"\`git status -s -uno\`\" && echo false || echo true`"; fi) >"$@" 2>/dev/null || true
 
 install-data-local:
 	(echo include/cvc4.h; \
diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index 301150b12..dcc4bc858 100644
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -163,7 +163,7 @@ CLEANFILES = \
 EXTRA_DIST = \
 	swig.h \
 	java_iterator_adapter.h \
-	java_output_stream_adapter.h
+	java_stream_adapters.h
 
 MOSTLYCLEANFILES = \
         .swig_deps \
diff --git a/src/bindings/java_output_stream_adapter.h b/src/bindings/java_output_stream_adapter.h
deleted file mode 100644
index 6830e508d..000000000
--- a/src/bindings/java_output_stream_adapter.h
+++ /dev/null
@@ -1,50 +0,0 @@
-/*********************                                                        */
-/*! \file java_output_stream_adapter.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-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief An OutputStream adapter for the Java bindings
- **
- ** An OutputStream adapter for the Java bindings.  This works with a lot
- ** of help from SWIG, and custom typemaps in the ".i" SWIG interface files
- ** for CVC4.  The basic idea is that, when a CVC4 function with a
- ** std::ostream& parameter is called, a Java-side binding is generated
- ** taking a java.io.OutputStream.  Now, the problem is that std::ostream
- ** has no Java equivalent, and java.io.OutputStream has no C++ equivalent,
- ** so we use this class (which exists on both sides) as the go-between.
- ** The wrapper connecting the Java function (taking an OutputStream) and
- ** the C++ function (taking an ostream) creates a JavaOutputStreamAdapter,
- ** and call the C++ function with the stringstream inside.  After the call,
- ** the generated stream material is collected and output to the Java-side
- ** OutputStream.
- **/
-
-// private to the bindings layer
-#ifndef SWIGJAVA
-#  error This should only be included from the Java bindings layer.
-#endif /* SWIGJAVA */
-
-#ifndef __CVC4__BINDINGS__JAVA_OUTPUT_STREAM_ADAPTER_H
-#define __CVC4__BINDINGS__JAVA_OUTPUT_STREAM_ADAPTER_H
-
-namespace CVC4 {
-
-class JavaOutputStreamAdapter {
-  std::stringstream d_ss;
-
-public:
-  JavaOutputStreamAdapter() { }
-
-  std::string toString() { return d_ss.str(); }
-
-};/* class JavaOutputStreamAdapter */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__BINDINGS__JAVA_OUTPUT_STREAM_ADAPTER_H */
diff --git a/src/bindings/java_stream_adapters.h b/src/bindings/java_stream_adapters.h
new file mode 100644
index 000000000..daeb06e18
--- /dev/null
+++ b/src/bindings/java_stream_adapters.h
@@ -0,0 +1,113 @@
+/*********************                                                        */
+/*! \file java_stream_adapters.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-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An OutputStream adapter for the Java bindings
+ **
+ ** An OutputStream adapter for the Java bindings.  This works with a lot
+ ** of help from SWIG, and custom typemaps in the ".i" SWIG interface files
+ ** for CVC4.  The basic idea is that, when a CVC4 function with a
+ ** std::ostream& parameter is called, a Java-side binding is generated
+ ** taking a java.io.OutputStream.  Now, the problem is that std::ostream
+ ** has no Java equivalent, and java.io.OutputStream has no C++ equivalent,
+ ** so we use this class (which exists on both sides) as the go-between.
+ ** The wrapper connecting the Java function (taking an OutputStream) and
+ ** the C++ function (taking an ostream) creates a JavaOutputStreamAdapter,
+ ** and call the C++ function with the stringstream inside.  After the call,
+ ** the generated stream material is collected and output to the Java-side
+ ** OutputStream.
+ **/
+
+// private to the bindings layer
+#ifndef SWIGJAVA
+#  error This should only be included from the Java bindings layer.
+#endif /* SWIGJAVA */
+
+#include <sstream>
+#include <set>
+#include <cassert>
+#include <iostream>
+#include <string>
+#include <jni.h>
+
+#ifndef __CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H
+#define __CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H
+
+namespace CVC4 {
+
+class JavaOutputStreamAdapter {
+  std::stringstream d_ss;
+
+public:
+  JavaOutputStreamAdapter() { }
+
+  std::string toString() { return d_ss.str(); }
+
+};/* class JavaOutputStreamAdapter */
+
+class JavaInputStreamAdapter : public std::stringstream {
+  static std::set<JavaInputStreamAdapter*> s_adapters;
+  jobject inputStream;
+
+  JavaInputStreamAdapter& operator=(const JavaInputStreamAdapter&);
+  JavaInputStreamAdapter(const JavaInputStreamAdapter&);
+
+public:
+  JavaInputStreamAdapter(jobject inputStream) : inputStream(inputStream) {
+    s_adapters.insert(this);
+  }
+
+  ~JavaInputStreamAdapter() {
+    s_adapters.erase(this);
+  }
+
+  static void pullAdapters(JNIEnv* jenv) {
+    for(std::set<JavaInputStreamAdapter*>::iterator i = s_adapters.begin();
+        i != s_adapters.end();
+        ++i) {
+      (*i)->pull(jenv);
+    }
+  }
+
+  jobject getInputStream() const {
+    return inputStream;
+  }
+
+  void pull(JNIEnv* jenv) {
+    if(fail() || eof()) {
+      clear();
+    }
+    jclass clazz = jenv->FindClass("java/io/InputStream");
+    assert(clazz != NULL && jenv->ExceptionOccurred() == NULL);
+    jmethodID method = jenv->GetMethodID(clazz, "available", "()I");
+    assert(method != NULL && jenv->ExceptionOccurred() == NULL);
+    jint available = jenv->CallIntMethod(inputStream, method);
+    assert(jenv->ExceptionOccurred() == NULL);
+    jbyteArray bytes = jenv->NewByteArray(available);
+    assert(bytes != NULL && jenv->ExceptionOccurred() == NULL);
+    method = jenv->GetMethodID(clazz, "read", "([B)I");
+    assert(method != NULL && jenv->ExceptionOccurred() == NULL);
+    jint nread = jenv->CallIntMethod(inputStream, method, bytes);
+    assert(jenv->ExceptionOccurred() == NULL);
+    jbyte* bptr = jenv->GetByteArrayElements(bytes, NULL);
+    assert(jenv->ExceptionOccurred() == NULL);
+    std::copy(bptr, bptr + nread, std::ostream_iterator<char>(*this));
+    *this << std::flush;
+    jenv->ReleaseByteArrayElements(bytes, bptr, 0);
+    assert(jenv->ExceptionOccurred() == NULL);
+    assert(good());
+    assert(!eof());
+  }
+
+};/* class JavaInputStreamAdapter */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H */
diff --git a/src/cvc4.i b/src/cvc4.i
index 3f11fafc2..925152248 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -54,6 +54,9 @@ using namespace CVC4;
 #include "expr/expr.h"
 #include "util/datatype.h"
 #include "expr/command.h"
+#include "bindings/java_stream_adapters.h"
+
+std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %}
 
 %template(vectorCommandPtr) std::vector< CVC4::Command* >;
@@ -72,7 +75,10 @@ using namespace CVC4;
 
 #ifdef SWIGJAVA
 
-%exception {
+#include "bindings/java_iterator_adapter.h"
+#include "bindings/java_stream_adapters.h"
+
+%exception %{
   try {
     $action
   } catch(CVC4::Exception& e) {
@@ -81,12 +87,19 @@ using namespace CVC4;
     std::string explanation = ss.str();
     SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
   }
-}
+%}
 
 // Create a mapping from C++ Exceptions to Java Exceptions.
 // This is in a couple of throws typemaps, simply because it's sensitive to SWIG's concept of which namespace we're in.
 %typemap(throws) Exception %{
-  jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/$1_type");
+  std::string name = "edu/nyu/acsys/$1_type";
+  size_t i = name.find("::");
+  if(i != std::string::npos) {
+    size_t j = name.rfind("::");
+    assert(i <= j);
+    name.replace(i, j - i + 2, "/");
+  }
+  jclass clazz = jenv->FindClass(name.c_str());
   assert(clazz != NULL && jenv->ExceptionOccurred() == NULL);
   jmethodID method = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
   assert(method != NULL && jenv->ExceptionOccurred() == NULL);
@@ -97,8 +110,11 @@ using namespace CVC4;
 %}
 %typemap(throws) CVC4::Exception %{
   std::string name = "edu/nyu/acsys/$1_type";
-  for(size_t i = name.find("::"); i != std::string::npos; i = name.find("::")) {
-    name.replace(i, 2, "/");
+  size_t i = name.find("::");
+  if(i != std::string::npos) {
+    size_t j = name.rfind("::");
+    assert(i <= j);
+    name.replace(i, j - i + 2, "/");
   }
   jclass clazz = jenv->FindClass(name.c_str());
   assert(clazz != NULL && jenv->ExceptionOccurred() == NULL);
@@ -146,6 +162,76 @@ using namespace CVC4;
          post="    new java.io.PrintStream($javainput).print(temp$javainput.toString());")
          std::ostream& "edu.nyu.acsys.CVC4.JavaOutputStreamAdapter.getCPtr(temp$javainput)"
 
+%typemap(jni) std::istream& "jlong"
+%typemap(jtype) std::istream& "long"
+%typemap(jstype) std::istream& "java.io.InputStream"
+%typemap(javain,
+         pre="    edu.nyu.acsys.CVC4.JavaInputStreamAdapter temp$javainput = edu.nyu.acsys.CVC4.JavaInputStreamAdapter.get($javainput);", pgcppname="temp$javainput",
+         post="")
+         std::istream& "edu.nyu.acsys.CVC4.JavaInputStreamAdapter.getCPtr(temp$javainput)"
+%typemap(in) jobject inputStream %{
+  $1 = jenv->NewGlobalRef($input);
+%}
+%typemap(out) CVC4::JavaInputStreamAdapter* %{
+  $1->pull(jenv);
+  *(CVC4::JavaInputStreamAdapter **)&$result = $1;
+%}
+%typemap(javacode) CVC4::JavaInputStreamAdapter %{
+  private static java.util.HashMap streams = new java.util.HashMap();
+  public static JavaInputStreamAdapter get(java.io.InputStream is) {
+    if(streams.containsKey(is)) {
+      return (JavaInputStreamAdapter) streams.get(is);
+    }
+    JavaInputStreamAdapter adapter = new JavaInputStreamAdapter(is);
+    streams.put(is, adapter);
+    return adapter;
+  }
+%}
+%typemap(javafinalize) CVC4::JavaInputStreamAdapter %{
+  protected void finalize() {
+    streams.remove(getInputStream());
+    delete();
+  }
+%}
+%ignore CVC4::JavaInputStreamAdapter::init(JNIEnv*);
+%ignore CVC4::JavaInputStreamAdapter::pullAdapters(JNIEnv*);
+%javamethodmodifiers CVC4::JavaInputStreamAdapter::getInputStream() const "private";
+%javamethodmodifiers CVC4::JavaInputStreamAdapter::JavaInputStreamAdapter(jobject) "private";
+
+%exception CVC4::parser::Parser::nextCommand() %{
+  try {
+    CVC4::JavaInputStreamAdapter::pullAdapters(jenv);
+    $action
+  } catch(CVC4::Exception& e) {
+    std::stringstream ss;
+    ss << e.what() << ": " << e.getMessage();
+    std::string explanation = ss.str();
+    SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
+  }
+%}
+%exception CVC4::parser::Parser::nextExpression() %{
+  try {
+    CVC4::JavaInputStreamAdapter::pullAdapters(jenv);
+    $action
+  } catch(CVC4::Exception& e) {
+    std::stringstream ss;
+    ss << e.what() << ": " << e.getMessage();
+    std::string explanation = ss.str();
+    SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
+  }
+%}
+%exception CVC4::JavaInputStreamAdapter::~JavaInputStreamAdapter() %{
+  try {
+    jenv->DeleteGlobalRef(arg1->getInputStream());
+    $action
+  } catch(CVC4::Exception& e) {
+    std::stringstream ss;
+    ss << e.what() << ": " << e.getMessage();
+    std::string explanation = ss.str();
+    SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
+  }
+%}
+
 #endif /* SWIGJAVA */
 
 %include "util/integer.i"
diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp
index 31963eee0..ecd31a4cc 100644
--- a/src/decision/relevancy.cpp
+++ b/src/decision/relevancy.cpp
@@ -28,6 +28,11 @@
 
 // Relevancy stuff
 
+const double Relevancy::secondsPerDecision = 0.001;
+const double Relevancy::secondsPerExpense = 1e-7;
+const double Relevancy::EPS = 1e-9;
+
+
 void Relevancy::setJustified(TNode n)
 {
   Debug("decision") << " marking [" << n.getId() << "]"<< n << "as justified" << std::endl;
diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h
index bfd30ddde..23d980a1b 100644
--- a/src/decision/relevancy.h
+++ b/src/decision/relevancy.h
@@ -109,9 +109,10 @@ class Relevancy : public RelevancyStrategy {
   bool d_multipleBacktrace;
   //bool d_computeRelevancy;     // are we in a mode where we compute relevancy?
 
-  static const double secondsPerDecision = 0.001;
-  static const double secondsPerExpense = 1e-7;
-  static const double EPS = 1e-9;
+  static const double secondsPerDecision;
+  static const double secondsPerExpense;
+  static const double EPS;
+
   /** Maximum time this algorithm should spent as part of whole algorithm */
   double d_maxTimeAsPercentageOfTotalTime;
 
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 5159f6b5a..eab41ee38 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -936,7 +936,7 @@ TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, Expr
       ("export of types belonging to theory of DATATYPES kinds unsupported");
   }
   if(n.getMetaKind() == kind::metakind::PARAMETERIZED &&
-     n.getKind() != kind::SORT_TYPE) { 
+     n.getKind() != kind::SORT_TYPE) {
     throw ExportUnsupportedException
       ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
   }
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 5f813dbe8..bd3827f47 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -713,6 +713,10 @@ public:
   operator Node();
   operator Node() const;
 
+  // similarly for TypeNode
+  operator TypeNode();
+  operator TypeNode() const;
+
   NodeBuilder<nchild_thresh>& operator&=(TNode);
   NodeBuilder<nchild_thresh>& operator|=(TNode);
   NodeBuilder<nchild_thresh>& operator+=(TNode);
@@ -902,6 +906,16 @@ NodeBuilder<nchild_thresh>::operator Node() const {
 }
 
 template <unsigned nchild_thresh>
+NodeBuilder<nchild_thresh>::operator TypeNode() {
+  return constructTypeNode();
+}
+
+template <unsigned nchild_thresh>
+NodeBuilder<nchild_thresh>::operator TypeNode() const {
+  return constructTypeNode();
+}
+
+template <unsigned nchild_thresh>
 expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
   Assert(!isUsed(), "NodeBuilder is one-shot only; "
          "attempt to access it after conversion");
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 236f48017..7522b8110 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -94,15 +94,32 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
     if(t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) {
       return true;
     }
-    if(isTuple() != t.isTuple() || isRecord() != t.isRecord() ||
-       getNumChildren() != t.getNumChildren()) {
+    if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
       return false;
     }
-    // children must be subtypes of t's, in order
-    for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
-      if(!(*i).isSubtypeOf(*j)) {
+    if(isTuple()) {
+      if(getNumChildren() != t.getNumChildren()) {
         return false;
       }
+      // children must be subtypes of t's, in order
+      for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
+        if(!(*i).isSubtypeOf(*j)) {
+          return false;
+        }
+      }
+    } else {
+      const Record& r1 = getConst<Record>();
+      const Record& r2 = t.getConst<Record>();
+      if(r1.getNumFields() != r2.getNumFields()) {
+        return false;
+      }
+      // r1's fields must be subtypes of r2's, in order
+      // names must match also
+      for(Record::const_iterator i = r1.begin(), j = r2.begin(); i != r1.end(); ++i, ++j) {
+        if((*i).first != (*j).first || !(*i).second.isSubtypeOf((*j).second)) {
+          return false;
+        }
+      }
     }
     return true;
   }
@@ -125,15 +142,32 @@ bool TypeNode::isComparableTo(TypeNode t) const {
          NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) {
         return true;
       }
-      if(isTuple() != t.isTuple() || isRecord() != t.isRecord() ||
-         getNumChildren() != t.getNumChildren()) {
+      if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
         return false;
       }
-      // children must be comparable to t's, in order
-      for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
-        if(!(*i).isComparableTo(*j)) {
+      if(isTuple()) {
+        if(getNumChildren() != t.getNumChildren()) {
+          return false;
+        }
+        // children must be comparable to t's, in order
+        for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
+          if(!(*i).isComparableTo(*j)) {
+            return false;
+          }
+        }
+      } else {
+        const Record& r1 = getConst<Record>();
+        const Record& r2 = t.getConst<Record>();
+        if(r1.getNumFields() != r2.getNumFields()) {
           return false;
         }
+        // r1's fields must be comparable to r2's, in order
+        // names must match also
+        for(Record::const_iterator i = r1.begin(), j = r2.begin(); i != r1.end(); ++i, ++j) {
+          if((*i).first != (*j).first || !(*i).second.isComparableTo((*j).second)) {
+            return false;
+          }
+        }
       }
       return true;
     } else {
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 0e71e1539..45ee52121 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -123,17 +123,14 @@ void CommandExecutorPortfolio::lemmaSharingInit()
     }
 
     /* Output to string stream  */
-    if(d_options[options::verbosity] == 0
-       || d_options[options::separateOutput]) {
-      assert(d_ostringstreams.size() == 0);
-      for(unsigned i = 0; i < d_numThreads; ++i) {
-        d_ostringstreams.push_back(new ostringstream);
-        d_threadOptions[i].set(options::out, d_ostringstreams[i]);
-
-        // important even for muzzled builds (to get result output right)
-        *d_threadOptions[i][options::out]
-          << Expr::setlanguage(d_threadOptions[i][options::outputLanguage]);
-      }
+    assert(d_ostringstreams.size() == 0);
+    for(unsigned i = 0; i < d_numThreads; ++i) {
+      d_ostringstreams.push_back(new ostringstream);
+      d_threadOptions[i].set(options::out, d_ostringstreams[i]);
+
+      // important even for muzzled builds (to get result output right)
+      *d_threadOptions[i][options::out]
+        << Expr::setlanguage(d_threadOptions[i][options::outputLanguage]);
     }
   }
 }/* CommandExecutorPortfolio::lemmaSharingInit() */
@@ -208,7 +205,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
       cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) );
     bool ret = smtEngineInvoke(d_smts[d_lastWinner],
                                cmdExported,
-                               d_threadOptions[d_lastWinner][options::out]);
+                               d_options[options::verbosity] >= -1 ? d_threadOptions[d_lastWinner][options::out] : NULL);
     if(d_lastWinner != 0) delete cmdExported;
     return ret;
   } else if(mode == 1) {               // portfolio
@@ -274,7 +271,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
       fns[i] = boost::bind(smtEngineInvoke,
                            d_smts[i],
                            seqs[i],
-                           d_threadOptions[i][options::out]
+                           d_options[options::verbosity] >= -1 ? d_threadOptions[i][options::out] : NULL
                            );
     }
 
@@ -332,7 +329,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
       cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) );
     bool ret = smtEngineInvoke(d_smts[d_lastWinner],
                                cmdExported,
-                               d_threadOptions[d_lastWinner][options::out]);
+                               d_options[options::verbosity] >= -1 ? d_threadOptions[d_lastWinner][options::out] : NULL);
     if(d_lastWinner != 0) delete cmdExported;
     return ret;
   } else {
diff --git a/src/main/options b/src/main/options
index caea63f5a..14a7a9f3f 100644
--- a/src/main/options
+++ b/src/main/options
@@ -31,8 +31,6 @@ option threadArgv std::vector<std::string> :include <vector> <string>
  Thread configuration (a string to be passed to parseOptions)
 option thread_id int :default -1
  Thread ID, for internal use in case of multi-threaded run
-option separateOutput bool :default false
- In multi-threaded setting print output of each thread at the end of run, separated by a divider ("----").
 option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write
  don't share (among portfolio threads) lemmas strictly longer than N
 option fallbackSequential  --fallback-sequential bool :default false
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 020db0d50..89f6c8db5 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -185,8 +185,9 @@ public:
   std::string getUnparsedText();
 
   /** Get the ANTLR3 lexer for this input. */
-  pANTLR3_LEXER getAntlr3Lexer(){ return d_lexer; };
+  pANTLR3_LEXER getAntlr3Lexer() { return d_lexer; }
 
+  pANTLR3_INPUT_STREAM getAntlr3InputStream() { return d_antlr3InputStream; }
 protected:
   /** Create an input. This input takes ownership of the given input stream,
    * and will delete it at destruction time.
diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp
index 8c4f1b0be..46853056b 100644
--- a/src/parser/antlr_line_buffered_input.cpp
+++ b/src/parser/antlr_line_buffered_input.cpp
@@ -21,15 +21,11 @@
 #include <cassert>
 
 #include "util/output.h"
+#include "parser/antlr_line_buffered_input.h"
 
 namespace CVC4 {
 namespace parser {
 
-typedef struct ANTLR3_LINE_BUFFERED_INPUT_STREAM {
-  ANTLR3_INPUT_STREAM antlr;
-  std::istream* in;
-} *pANTLR3_LINE_BUFFERED_INPUT_STREAM;
-
 static pANTLR3_INPUT_STREAM    antlr3CreateLineBufferedStream(std::istream& in);
 
 static void
@@ -213,7 +209,9 @@ myLA(pANTLR3_INT_STREAM is, ANTLR3_INT32 la) {
     Debug("pipe") << "LA" << std::endl;
     if	(( ((pANTLR3_UINT8)input->nextChar) + la - 1) >= (((pANTLR3_UINT8)input->data) + input->sizeBuf))
     {
-      std::istream& in = *((pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)->in;
+      std::istream& in = *((CVC4::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)->in;
+      //MGD
+      // in.clear();
       if(!in) {
         Debug("pipe") << "EOF" << std::endl;
         return	ANTLR3_CHARSTREAM_EOF;
@@ -246,7 +244,7 @@ myLA(pANTLR3_INT_STREAM is, ANTLR3_INT32 la) {
       ++input->sizeBuf;
     }
 
-    Debug("pipe") << "READ POINTER[" << la << "] AT: >>" << std::string(((char*)input->nextChar), input->sizeBuf - (((char*)input->nextChar) - (char*)input->data) + 1) << "<< returning '" << (char)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << "' (" << (unsigned)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << ")" << std::endl;
+    Debug("pipe") << "READ POINTER[" << la << "] AT: >>" << std::string(((char*)input->nextChar), input->sizeBuf - (((char*)input->nextChar) - (char*)input->data)) << "<< returning '" << (char)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << "' (" << (unsigned)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << ")" << std::endl;
     return	(ANTLR3_UCHAR)(*((pANTLR3_UINT8)input->nextChar + la - 1));
 }
 
@@ -356,7 +354,6 @@ antlr3CreateLineBufferedStream(std::istream& in)
         input->isAllocated	= ANTLR3_FALSE;
 
         ((pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)->in = &in;
-
 	// Call the common 8 bit input stream handler
 	// initialization.
 	//
diff --git a/src/parser/antlr_line_buffered_input.h b/src/parser/antlr_line_buffered_input.h
index 83df19a2d..fb0c16dbe 100644
--- a/src/parser/antlr_line_buffered_input.h
+++ b/src/parser/antlr_line_buffered_input.h
@@ -25,6 +25,11 @@
 namespace CVC4 {
 namespace parser {
 
+typedef struct ANTLR3_LINE_BUFFERED_INPUT_STREAM {
+  ANTLR3_INPUT_STREAM antlr;
+  std::istream* in;
+} *pANTLR3_LINE_BUFFERED_INPUT_STREAM;
+
 pANTLR3_INPUT_STREAM
 antlr3LineBufferedStreamNew(std::istream& in, ANTLR3_UINT32 encoding, pANTLR3_UINT8 name);
 
diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp
index 6a6ae8609..108b67307 100644
--- a/src/parser/bounded_token_buffer.cpp
+++ b/src/parser/bounded_token_buffer.cpp
@@ -473,9 +473,11 @@ static pANTLR3_COMMON_TOKEN nextToken(pBOUNDED_TOKEN_BUFFER buffer) {
 
   tokenStream = buffer->commonTstream;
 
+  /*
   if( buffer->done == ANTLR3_TRUE ) {
     return &(tokenStream->tstream->tokenSource->eofToken);
   }
+  */
 
   /* Pick out the next token from the token source
    * Remember we just get a pointer (reference if you like) here
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 8b77362b2..90f17426b 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -446,26 +446,20 @@ Command* Parser::nextCommand() throw(ParserException) {
   if(!d_commandQueue.empty()) {
     cmd = d_commandQueue.front();
     d_commandQueue.pop_front();
-    if(cmd == NULL) {
-      setDone();
-    }
+    setDone(cmd == NULL);
   } else {
-    if(!done()) {
-      try {
-        cmd = d_input->parseCommand();
-        d_commandQueue.push_back(cmd);
-        cmd = d_commandQueue.front();
-        d_commandQueue.pop_front();
-        if(cmd == NULL) {
-          setDone();
-        }
-      } catch(ParserException& e) {
-        setDone();
-        throw;
-      } catch(exception& e) {
-        setDone();
-        parseError(e.what());
-      }
+    try {
+      cmd = d_input->parseCommand();
+      d_commandQueue.push_back(cmd);
+      cmd = d_commandQueue.front();
+      d_commandQueue.pop_front();
+      setDone(cmd == NULL);
+    } catch(ParserException& e) {
+      setDone();
+      throw;
+    } catch(exception& e) {
+      setDone();
+      parseError(e.what());
     }
   }
   Debug("parser") << "nextCommand() => " << cmd << std::endl;
@@ -478,9 +472,7 @@ Expr Parser::nextExpression() throw(ParserException) {
   if(!done()) {
     try {
       result = d_input->parseExpr();
-      if(result.isNull()) {
-        setDone();
-      }
+      setDone(result.isNull());
     } catch(ParserException& e) {
       setDone();
       throw;
diff --git a/src/parser/parser.i b/src/parser/parser.i
index 5e10973d4..5b23555ea 100644
--- a/src/parser/parser.i
+++ b/src/parser/parser.i
@@ -9,14 +9,13 @@ namespace CVC4 {
     %ignore operator<<(std::ostream&, DeclarationCheck);
     %ignore operator<<(std::ostream&, SymbolType);
 
-  class ParserExprStream : public CVC4::ExprStream {
-    Parser* d_parser;
-  public:
-    ParserExprStream(Parser* parser) : d_parser(parser) {}
-    ~ParserExprStream() { delete d_parser; }
-    Expr nextExpr() { return d_parser->nextExpression(); }
-  };/* class Parser::ExprStream */
-
+    class ParserExprStream : public CVC4::ExprStream {
+      Parser* d_parser;
+    public:
+      ParserExprStream(Parser* parser) : d_parser(parser) {}
+      ~ParserExprStream() { delete d_parser; }
+      Expr nextExpr() { return d_parser->nextExpression(); }
+    };/* class Parser::ExprStream */
   }/* namespace CVC4::parser */
 }/* namespace CVC4 */
 
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 2cfeaafc1..524344612 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -817,7 +817,7 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t
     TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
     if( options::modelUninterpDtEnum() && tn.isSort() &&
         tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
-      out << "DATATYPE " << std::endl;
+      out << "DATATYPE" << std::endl;
       out << "  " << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " = ";
       for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
         if (i>0) {
@@ -1068,7 +1068,18 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr
       out << ',' << endl;
     }
     const Datatype& dt = (*i).getDatatype();
-    out << "  " << dt.getName() << " = ";
+    out << "  " << dt.getName();
+    if(dt.isParametric()) {
+      out << '[';
+      for(size_t j = 0; j < dt.getNumParameters(); ++j) {
+        if(j > 0) {
+          out << ',';
+        }
+        out << dt.getParameter(j);
+      }
+      out << ']';
+    }
+    out << " = ";
     bool firstConstructor = true;
     for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
       if(! firstConstructor) {
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 35184e42e..09d8fcbd4 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -21,6 +21,8 @@
 #include "smt/smt_engine.h"
 #include "theory/theory_engine.h"
 #include "theory/model.h"
+#include "theory/booleans/boolean_term_conversion_mode.h"
+#include "theory/booleans/options.h"
 #include "expr/kind.h"
 #include "util/hash.h"
 #include "util/bool.h"
@@ -31,10 +33,56 @@
 
 using namespace std;
 using namespace CVC4::theory;
+using namespace CVC4::theory::booleans;
 
 namespace CVC4 {
 namespace smt {
 
+BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) :
+  d_smt(smt),
+  d_ff(),
+  d_tt(),
+  d_ffDt(),
+  d_ttDt(),
+  d_termCache(),
+  d_typeCache() {
+
+  // set up our "false" and "true" conversions based on command-line option
+  if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS ||
+     options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_NATIVE) {
+    d_ff = NodeManager::currentNM()->mkConst(BitVector(1u, 0u));
+    d_tt = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+  }
+  if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS) {
+    d_ffDt = d_ff;
+    d_ttDt = d_tt;
+  } else {
+    Datatype spec("BooleanTerm");
+    // don't change the order; false is assumed to come first by the model postprocessor
+    spec.addConstructor(DatatypeConstructor("BT_False"));
+    spec.addConstructor(DatatypeConstructor("BT_True"));
+    const Datatype& dt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(spec).getDatatype();
+    d_ffDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_False"].getConstructor()));
+    d_ttDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_True"].getConstructor()));
+    // mark this datatype type as being special for Boolean term conversion
+    TypeNode::fromType(dt.getDatatypeType()).setAttribute(BooleanTermAttr(), Node::null());
+    if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_DATATYPES) {
+      Assert(d_ff.isNull() && d_tt.isNull());
+      d_ff = d_ffDt;
+      d_tt = d_ttDt;
+    }
+  }
+
+  // assert that we set it up correctly
+  Assert(!d_ff.isNull() && !d_tt.isNull());
+  Assert(!d_ffDt.isNull() && !d_ttDt.isNull());
+  Assert(d_ff != d_tt);
+  Assert(d_ff.getType() == d_tt.getType());
+  Assert(d_ffDt != d_ttDt);
+  Assert(d_ffDt.getType() == d_ttDt.getType());
+
+}/* BooleanTermConverter::BooleanTermConverter() */
+
 static inline bool isBoolean(TNode top, unsigned i) {
   switch(top.getKind()) {
   case kind::NOT:
@@ -63,27 +111,51 @@ static inline bool isBoolean(TNode top, unsigned i) {
   }
 }
 
-const Datatype& BooleanTermConverter::booleanTermsConvertDatatype(const Datatype& dt) throw() {
-  return dt;
-  // boolean terms not supported in datatypes, yet
+const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw() {
+  const Datatype*& out = d_datatypeCache[&dt];
+  if(out != NULL) {
+    return *out;
+  }
 
-  Debug("boolean-terms") << "booleanTermsConvertDatatype: considering " << dt.getName() << endl;
+  Debug("boolean-terms") << "convertDatatype: considering " << dt.getName() << endl;
   for(Datatype::const_iterator c = dt.begin(); c != dt.end(); ++c) {
     TypeNode t = TypeNode::fromType((*c).getConstructor().getType());
     for(TypeNode::const_iterator a = t.begin(); a != t.end(); ++a) {
-      if((*a).isBoolean()) {
-        Datatype newDt(dt.getName() + "'");
+      TypeNode converted = convertType(*a, true);
+      Debug("boolean-terms") << "GOT: " << converted << ":" << converted.getId() << endl;
+      if(*a != converted) {
+        SortConstructorType mySelfType;
+        set<Type> unresolvedTypes;
+        if(dt.isParametric()) {
+          mySelfType = NodeManager::currentNM()->toExprManager()->mkSortConstructor(dt.getName() + "'", dt.getNumParameters());
+          unresolvedTypes.insert(mySelfType);
+        }
+        vector<Datatype> newDtVector;
+        if(dt.isParametric()) {
+          newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters()));
+        } else {
+          newDtVector.push_back(Datatype(dt.getName() + "'"));
+        }
+        Datatype& newDt = newDtVector.front();
         Debug("boolean-terms") << "found a Boolean arg in constructor " << (*c).getName() << endl;
         for(c = dt.begin(); c != dt.end(); ++c) {
           DatatypeConstructor ctor((*c).getName() + "'", (*c).getTesterName() + "'");
           t = TypeNode::fromType((*c).getConstructor().getType());
           for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
-            if((*a).getType().getRangeType().isBoolean()) {
-              ctor.addArg((*a).getName() + "'", NodeManager::currentNM()->mkBitVectorType(1).toType());
-            } else {
-              Type argType = (*a).getType().getRangeType();
-              if(argType.isDatatype() && DatatypeType(argType).getDatatype() == dt) {
+            Type argType = (*a).getType().getRangeType();
+            if(argType.isDatatype() && DatatypeType(argType).getDatatype() == dt) {
+              Debug("boolean-terms") << "argtype " << argType << " is self" << endl;
+              if(dt.isParametric()) {
+                Debug("boolean-terms") << "is-parametric self is " << mySelfType << endl;
+                ctor.addArg((*a).getName() + "'", mySelfType.instantiate(DatatypeType(argType).getDatatype().getParameters()));
+              } else {
                 ctor.addArg((*a).getName() + "'", DatatypeSelfType());
+              }
+            } else {
+              Debug("boolean-terms") << "argtype " << argType << " is NOT self" << endl;
+              converted = convertType(TypeNode::fromType(argType), true);
+              if(TypeNode::fromType(argType) != converted) {
+                ctor.addArg((*a).getName() + "'", converted.toType());
               } else {
                 ctor.addArg((*a).getName() + "'", argType);
               }
@@ -91,22 +163,107 @@ const Datatype& BooleanTermConverter::booleanTermsConvertDatatype(const Datatype
           }
           newDt.addConstructor(ctor);
         }
-        DatatypeType newDtt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(newDt);
+        vector<DatatypeType> newDttVector =
+          NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(newDtVector, unresolvedTypes);
+        DatatypeType& newDtt = newDttVector.front();
         const Datatype& newD = newDtt.getDatatype();
         for(c = dt.begin(); c != dt.end(); ++c) {
           Debug("boolean-terms") << "constructor " << (*c).getConstructor() << ":" << (*c).getConstructor().getType() << " made into " << newD[(*c).getName() + "'"].getConstructor() << ":" << newD[(*c).getName() + "'"].getConstructor().getType() << endl;
-          d_booleanTermCache[make_pair(Node::fromExpr((*c).getConstructor()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
-          d_booleanTermCache[make_pair(Node::fromExpr((*c).getTester()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
+          Node::fromExpr(newD[(*c).getName() + "'"].getConstructor()).setAttribute(BooleanTermAttr(), Node::fromExpr((*c).getConstructor()));// other attr?
+          Debug("boolean-terms") << "mapped " << newD[(*c).getName() + "'"].getConstructor() << " to " << (*c).getConstructor() << endl;
+          d_termCache[make_pair(Node::fromExpr((*c).getConstructor()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
+          d_termCache[make_pair(Node::fromExpr((*c).getTester()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
           for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
-            d_booleanTermCache[make_pair(Node::fromExpr((*a).getSelector()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
+            d_termCache[make_pair(Node::fromExpr((*a).getSelector()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
           }
         }
+        out = &newD;
         return newD;
       }
     }
   }
+
+  out = &dt;
   return dt;
-}/* BooleanTermConverter::booleanTermsConvertDatatype() */
+
+}/* BooleanTermConverter::convertDatatype() */
+
+TypeNode BooleanTermConverter::convertType(TypeNode type, bool datatypesContext) {
+  Debug("boolean-terms") << "CONVERT-TYPE[" << type << ":" << type.getId() << ", " << datatypesContext << "]" << endl;
+  // This function recursively converts the type.
+  if(type.isBoolean()) {
+    return datatypesContext ? d_ttDt.getType() : d_tt.getType();
+  }
+  const pair<TypeNode, bool> cacheKey(type, datatypesContext);
+  if(d_typeCache.find(cacheKey) != d_typeCache.end()) {
+    TypeNode out = d_typeCache[cacheKey];
+    return out.isNull() ? type : out;
+  }
+  TypeNode& outNode = d_typeCache[cacheKey];
+  if(type.getKind() == kind::DATATYPE_TYPE ||
+     type.getKind() == kind::PARAMETRIC_DATATYPE) {
+    bool parametric = (type.getKind() == kind::PARAMETRIC_DATATYPE);
+    const Datatype& dt = parametric ? type[0].getConst<Datatype>() : type.getConst<Datatype>();
+    TypeNode out = TypeNode::fromType(convertDatatype(dt).getDatatypeType());
+    Debug("boolean-terms") << "AFTER, got "<< out << " param:" << parametric << endl;
+    if(parametric) {
+      // re-parameterize the translation
+      vector<TypeNode> params = type.getParamTypes();
+      for(size_t i = 0; i < params.size(); ++i) {
+        Debug("boolean-terms") << "in loop, got "<< params[i] << endl;
+        params[i] = convertType(params[i], true);
+        Debug("boolean-terms") << "in loop, convert to "<< params[i] << endl;
+      }
+      params.insert(params.begin(), out[0]);
+      out = NodeManager::currentNM()->mkTypeNode(kind::PARAMETRIC_DATATYPE, params);
+      Debug("boolean-terms") << "got OUT: " << out << endl;
+    }
+    if(out != type) {
+      outNode = out;// cache it
+      Debug("boolean-terms") << "OUT is same as TYPE" << endl;
+    } else Debug("boolean-terms") << "OUT is DIFFERENT FROM TYPE" << endl;
+    return out;
+  }
+  if(type.isRecord()) {
+    const Record& rec = type.getConst<Record>();
+    vector< pair<string, Type> > flds;
+    for(Record::const_iterator i = rec.begin(); i != rec.end(); ++i) {
+      TypeNode converted = convertType(TypeNode::fromType((*i).second), true);
+      if(TypeNode::fromType((*i).second) != converted) {
+        flds.push_back(make_pair((*i).first, converted.toType()));
+      } else {
+        flds.push_back(*i);
+      }
+    }
+    TypeNode newRec = NodeManager::currentNM()->mkRecordType(Record(flds));
+    Debug("tuprec") << "converted " << type << " to " << newRec << endl;
+    if(newRec != type) {
+      outNode = newRec;// cache it
+    }
+    return newRec;
+  }
+  if(type.getNumChildren() > 0) {
+    Debug("boolean-terms") << "here at A for " << type << ":" << type.getId() << endl;
+    // This should handle tuples and arrays ok.
+    // Might handle function types too, but they can't go
+    // in other types, so it doesn't matter.
+    NodeBuilder<> b(type.getKind());
+    if(type.getMetaKind() == kind::metakind::PARAMETERIZED) {
+      b << type.getOperator();
+    }
+    for(TypeNode::iterator i = type.begin(); i != type.end(); ++i) {
+      b << convertType(*i, false);
+    }
+    TypeNode out = b;
+    if(out != type) {
+      outNode = out;// cache it
+    }
+    Debug("boolean-terms") << "here at B, returning " << out << ":" << out.getId() << endl;
+    return out;
+  }
+  // leave the cache at Null
+  return type;
+}/* BooleanTermConverter::convertType() */
 
 // look for vars from "vars" that occur in a term-context in n; transfer them to output.
 static void collectVarsInTermContext(TNode n, std::set<TNode>& vars, std::set<TNode>& output, bool boolParent, std::hash_set< std::pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> >& alreadySeen) {
@@ -134,11 +291,21 @@ static void collectVarsInTermContext(TNode n, std::set<TNode>& vars, std::set<TN
   }
 }
 
-Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, std::map<TNode, Node>& quantBoolVars) throw() {
-  Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - boolParent=" << boolParent << endl;
+Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw() {
+  Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - parentTheory=" << parentTheory << endl;
+
+  // we only distinguish between datatypes, booleans, and "other", and we
+  // don't even distinguish datatypes except when in "native" conversion
+  // mode
+  if(parentTheory != theory::THEORY_BOOL) {
+    if(options::booleanTermConversionMode() != BOOLEAN_TERM_CONVERT_NATIVE ||
+       parentTheory != theory::THEORY_DATATYPES) {
+      parentTheory = theory::THEORY_BUILTIN;
+    }
+  }
 
-  BooleanTermCache::iterator i = d_booleanTermCache.find(make_pair<Node, bool>(top, boolParent));
-  if(i != d_booleanTermCache.end()) {
+  BooleanTermCache::iterator i = d_termCache.find(make_pair<Node, theory::TheoryId>(top, parentTheory));
+  if(i != d_termCache.end()) {
     return (*i).second.isNull() ? Node(top) : (*i).second;
   }
 
@@ -147,22 +314,24 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st
 
   NodeManager* nm = NodeManager::currentNM();
 
-  Node one = nm->mkConst(BitVector(1u, 1u));
-  Node zero = nm->mkConst(BitVector(1u, 0u));
-
   if(quantBoolVars.find(top) != quantBoolVars.end()) {
     // this Bool variable is quantified over and we're changing it to a BitVector var
-    if(boolParent) {
-      return quantBoolVars[top].eqNode(one);
+    if(parentTheory == theory::THEORY_BOOL) {
+      return quantBoolVars[top].eqNode(d_tt);
     } else {
       return quantBoolVars[top];
     }
   }
 
-  if(!boolParent && top.getType().isBoolean()) {
+  if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean()) {
     // still need to rewrite e.g. function applications over boolean
-    Node topRewritten = rewriteBooleanTermsRec(top, true, quantBoolVars);
-    Node n = nm->mkNode(kind::ITE, topRewritten, one, zero);
+    Node topRewritten = rewriteBooleanTermsRec(top, theory::THEORY_BOOL, quantBoolVars);
+    Node n;
+    if(parentTheory == theory::THEORY_DATATYPES) {
+      n = nm->mkNode(kind::ITE, topRewritten, d_ttDt, d_ffDt);
+    } else {
+      n = nm->mkNode(kind::ITE, topRewritten, d_tt, d_ff);
+    }
     Debug("boolean-terms") << "constructed ITE: " << n << endl;
     return n;
   }
@@ -176,19 +345,19 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st
       if(constituentType.isBoolean()) {
         // we have store_all(true) or store_all(false)
         // just turn it into store_all(1) or store_all(0)
-        Node newConst = nm->mkConst(BitVector(1u, asa.getExpr().getConst<bool>() ? 1u : 0u));
         if(indexType.isBoolean()) {
           // change index type to BV(1) also
-          indexType = nm->mkBitVectorType(1);
+          indexType = d_tt.getType();
         }
-        ArrayStoreAll asaRepl(nm->mkArrayType(indexType, nm->mkBitVectorType(1)).toType(), newConst.toExpr());
+        ArrayStoreAll asaRepl(nm->mkArrayType(indexType, d_tt.getType()).toType(),
+                              (asa.getExpr().getConst<bool>() ? d_tt : d_ff).toExpr());
         Node n = nm->mkConst(asaRepl);
         Debug("boolean-terms") << " returning new store_all: " << n << endl;
         return n;
       }
       if(indexType.isBoolean()) {
         // must change index type to BV(1)
-        indexType = nm->mkBitVectorType(1);
+        indexType = d_tt.getType();
         ArrayStoreAll asaRepl(nm->mkArrayType(indexType, TypeNode::fromType(constituentType)).toType(), asa.getExpr());
         Node n = nm->mkConst(asaRepl);
         Debug("boolean-terms") << " returning new store_all: " << n << endl;
@@ -200,9 +369,10 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st
     TypeNode t = top.getType();
     if(t.isFunction()) {
       for(unsigned i = 0; i < t.getNumChildren() - 1; ++i) {
-        if(t[i].isBoolean()) {
+        TypeNode newType = convertType(t[i], false);
+        if(newType != t[i]) {
           vector<TypeNode> argTypes = t.getArgTypes();
-          replace(argTypes.begin(), argTypes.end(), t[i], nm->mkBitVectorType(1));
+          replace(argTypes.begin(), argTypes.end(), t[i], d_tt.getType());
           TypeNode newType = nm->mkFunctionType(argTypes, t.getRangeType());
           Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "__boolterm__",
                                 newType, "a function introduced by Boolean-term conversion",
@@ -216,7 +386,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st
             Node var = nm->mkBoundVar(t[j]);
             boundVarsBuilder << var;
             if(t[j].isBoolean()) {
-              bodyBuilder << nm->mkNode(kind::ITE, var, one, zero);
+              bodyBuilder << nm->mkNode(kind::ITE, var, d_tt, d_ff);
             } else {
               bodyBuilder << var;
             }
@@ -226,105 +396,112 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st
           Node lam = nm->mkNode(kind::LAMBDA, boundVars, body);
           Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl;
           d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam);
-          d_booleanTermCache[make_pair(top, boolParent)] = n;
+          d_termCache[make_pair(top, parentTheory)] = n;
           return n;
         }
       }
     } else if(t.isArray()) {
-      TypeNode indexType = t.getArrayIndexType();
-      TypeNode constituentType = t.getArrayConstituentType();
-      bool rewrite = false;
-      if(indexType.isBoolean()) {
-        indexType = nm->mkBitVectorType(1);
-        rewrite = true;
-      }
-      if(constituentType.isBoolean()) {
-        constituentType = nm->mkBitVectorType(1);
-        rewrite = true;
-      }
-      if(rewrite) {
+      TypeNode indexType = convertType(t.getArrayIndexType(), false);
+      TypeNode constituentType = convertType(t.getArrayConstituentType(), false);
+      if(indexType != t.getArrayIndexType() || constituentType != t.getArrayConstituentType()) {
         TypeNode newType = nm->mkArrayType(indexType, constituentType);
-        Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
+        Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
                               newType, "an array variable introduced by Boolean-term conversion",
                               NodeManager::SKOLEM_EXACT_NAME);
         top.setAttribute(BooleanTermAttr(), n);
         Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
-        Node n_zero = nm->mkNode(kind::SELECT, n, zero);
-        Node n_one = nm->mkNode(kind::SELECT, n, one);
+        Node n_ff = nm->mkNode(kind::SELECT, n, d_ff);
+        Node n_tt = nm->mkNode(kind::SELECT, n, d_tt);
         Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), nm->mkConst(false).toExpr()));
         Node repl = nm->mkNode(kind::STORE,
                     nm->mkNode(kind::STORE, base, nm->mkConst(false),
-                               nm->mkNode(kind::EQUAL, n_zero, one)), nm->mkConst(true),
-                               nm->mkNode(kind::EQUAL, n_one, one));
+                               nm->mkNode(kind::EQUAL, n_ff, d_tt)), nm->mkConst(true),
+                               nm->mkNode(kind::EQUAL, n_tt, d_tt));
         Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl;
         d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl);
-        d_booleanTermCache[make_pair(top, boolParent)] = n;
+        d_termCache[make_pair(top, parentTheory)] = n;
         return n;
       }
-      d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+      d_termCache[make_pair(top, parentTheory)] = Node::null();
       return top;
-    } else if(t.isTuple()) {
-      return top;
-    } else if(t.isRecord()) {
+    } else if(t.isTuple() || t.isRecord()) {
+      TypeNode newType = convertType(t, true);
+      if(t != newType) {
+        Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
+                              newType, "a tuple/record variable introduced by Boolean-term conversion",
+                              NodeManager::SKOLEM_EXACT_NAME);
+        top.setAttribute(BooleanTermAttr(), n);
+        n.setAttribute(BooleanTermAttr(), top);
+        Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
+        d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
+        Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
+        d_termCache[make_pair(top, parentTheory)] = n;
+        return n;
+      }
+      d_termCache[make_pair(top, parentTheory)] = Node::null();
       return top;
-    } else if(t.isDatatype()) {
-      return top;// no support for datatypes at present
-      const Datatype& dt = t.getConst<Datatype>();
-      const Datatype& dt2 = booleanTermsConvertDatatype(dt);
-      if(dt != dt2) {
-        Assert(d_booleanTermCache.find(make_pair(top, boolParent)) == d_booleanTermCache.end(),
+    } else if(t.isDatatype() || t.isParametricDatatype()) {
+      Debug("boolean-terms") << "found a var of datatype type" << endl;
+      TypeNode newT = convertType(t, parentTheory == theory::THEORY_DATATYPES);
+      if(t != newT) {
+        Assert(d_termCache.find(make_pair(top, parentTheory)) == d_termCache.end(),
                "Node `%s' already in cache ?!", top.toString().c_str());
-        Assert(top.isVar());
-        TypeNode newType = TypeNode::fromType(dt2.getDatatypeType());
-        Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
-                              newType, "an array variable introduced by Boolean-term conversion",
+        Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
+                              newT, "a datatype variable introduced by Boolean-term conversion",
                               NodeManager::SKOLEM_EXACT_NAME);
+        Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
         top.setAttribute(BooleanTermAttr(), n);
-        Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
-        d_booleanTermCache[make_pair(top, boolParent)] = n;
+        d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
+        Debug("boolean-terms") << "constructed: " << n << " of type " << newT << endl;
+        d_termCache[make_pair(top, parentTheory)] = n;
         return n;
       } else {
-        d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+        d_termCache[make_pair(top, parentTheory)] = Node::null();
         return top;
       }
     } else if(t.isConstructor()) {
-      return top;// no support for datatypes at present
-      Assert(!boolParent);
-      const Datatype& dt = t[t.getNumChildren() - 1].getConst<Datatype>();
-      const Datatype& dt2 = booleanTermsConvertDatatype(dt);
+      Assert(parentTheory != theory::THEORY_BOOL);
+      Assert(t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ||
+             t[t.getNumChildren() - 1].getKind() == kind::PARAMETRIC_DATATYPE);
+      const Datatype& dt = t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ?
+                           t[t.getNumChildren() - 1].getConst<Datatype>() :
+                           t[t.getNumChildren() - 1][0].getConst<Datatype>();
+      TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
+      const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
       if(dt != dt2) {
-        Assert(d_booleanTermCache.find(make_pair(top, boolParent)) != d_booleanTermCache.end(),
+        Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(),
                "constructor `%s' not in cache", top.toString().c_str());
-        return d_booleanTermCache[make_pair(top, boolParent)];
-      } else {
-        d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
-        return top;
+        return d_termCache[make_pair(top, parentTheory)];
       }
+      d_termCache[make_pair(top, parentTheory)] = Node::null();
+      return top;
     } else if(t.isTester() || t.isSelector()) {
-      return top;// no support for datatypes at present
-      Assert(!boolParent);
-      const Datatype& dt = t[0].getConst<Datatype>();
-      const Datatype& dt2 = booleanTermsConvertDatatype(dt);
+      Assert(parentTheory != theory::THEORY_BOOL);
+      const Datatype& dt = t[0].getKind() == kind::DATATYPE_TYPE ?
+                           t[0].getConst<Datatype>() :
+                           t[0][0].getConst<Datatype>();
+      TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
+      const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
       if(dt != dt2) {
-        Assert(d_booleanTermCache.find(make_pair(top, boolParent)) != d_booleanTermCache.end(),
+        Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(),
                "tester or selector `%s' not in cache", top.toString().c_str());
-        return d_booleanTermCache[make_pair(top, boolParent)];
+        return d_termCache[make_pair(top, parentTheory)];
       } else {
-        d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+        d_termCache[make_pair(top, parentTheory)] = Node::null();
         return top;
       }
     } else if(t.getNumChildren() > 0) {
       for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) {
         if((*i).isBoolean()) {
           vector<TypeNode> argTypes(t.begin(), t.end());
-          replace(argTypes.begin(), argTypes.end(), *i, nm->mkBitVectorType(1));
+          replace(argTypes.begin(), argTypes.end(), *i, d_tt.getType());
           TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes);
           Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
                                 newType, "a variable introduced by Boolean-term conversion",
                                 NodeManager::SKOLEM_EXACT_NAME);
           Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
           top.setAttribute(BooleanTermAttr(), n);
-          d_booleanTermCache[make_pair(top, boolParent)] = n;
+          d_termCache[make_pair(top, parentTheory)] = n;
           return n;
         }
       }
@@ -385,11 +562,12 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st
           }
         }
         Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, boundVars);
-        Node body = rewriteBooleanTermsRec(top[1], true, quantBoolVars);
+        Node body = rewriteBooleanTermsRec(top[1], theory::THEORY_BOOL, quantBoolVars);
         Node quant = nm->mkNode(top.getKind(), boundVarList, body);
         Debug("bt") << "rewrote quantifier to -> " << quant << endl;
-        d_booleanTermCache[make_pair(top, true)] = quant;
-        d_booleanTermCache[make_pair(top, false)] = quant.iteNode(one, zero);
+        d_termCache[make_pair(top, theory::THEORY_BOOL)] = quant;
+        d_termCache[make_pair(top, theory::THEORY_BUILTIN)] = quant.iteNode(d_tt, d_ff);
+        d_termCache[make_pair(top, theory::THEORY_DATATYPES)] = quant.iteNode(d_tt, d_ff);
         return quant;
       }
     }
@@ -400,15 +578,20 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st
     NodeBuilder<> b(k);
     Debug("bt") << "looking at: " << top << endl;
     if(mk == kind::metakind::PARAMETERIZED) {
-      if(kindToTheoryId(k) != THEORY_BV &&
-         k != kind::APPLY_TYPE_ASCRIPTION &&
-         k != kind::TUPLE_SELECT &&
-         k != kind::TUPLE_UPDATE &&
-         k != kind::RECORD_SELECT &&
-         k != kind::RECORD_UPDATE &&
-         k != kind::RECORD) {
+      if(k == kind::RECORD) {
+        b << convertType(top.getType(), parentTheory == theory::THEORY_DATATYPES);
+      } else if(k == kind::APPLY_TYPE_ASCRIPTION) {
+        Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType()));
+        b << asc;
+        Debug("boolean-terms") << "setting " << top.getOperator() << ":" << top.getOperator().getId() << " to point to " << asc << ":" << asc.getId() << endl;
+        asc.setAttribute(BooleanTermAttr(), top.getOperator());
+      } else if(kindToTheoryId(k) != THEORY_BV &&
+                k != kind::TUPLE_SELECT &&
+                k != kind::TUPLE_UPDATE &&
+                k != kind::RECORD_SELECT &&
+                k != kind::RECORD_UPDATE) {
         Debug("bt") << "rewriting: " << top.getOperator() << endl;
-        b << rewriteBooleanTermsRec(top.getOperator(), false, quantBoolVars);
+        b << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars);
         Debug("bt") << "got: " << b.getOperator() << endl;
       } else {
         b << top.getOperator();
@@ -416,17 +599,21 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st
     }
     for(unsigned i = 0; i < top.getNumChildren(); ++i) {
       Debug("bt") << "rewriting: " << top[i] << endl;
-      b << rewriteBooleanTermsRec(top[i], isBoolean(top, i), quantBoolVars);
+      b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), quantBoolVars);
       Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl;
     }
     Node n = b;
     Debug("boolean-terms") << "constructed: " << n << endl;
-    if(boolParent &&
-       n.getType().isBitVector() &&
-       n.getType().getBitVectorSize() == 1) {
-      n = nm->mkNode(kind::EQUAL, n, one);
+    if(parentTheory == theory::THEORY_BOOL) {
+      if(n.getType().isBitVector() &&
+         n.getType().getBitVectorSize() == 1) {
+        n = nm->mkNode(kind::EQUAL, n, d_tt);
+      } else if(n.getType().isDatatype() &&
+                n.getType().hasAttribute(BooleanTermAttr())) {
+        n = nm->mkNode(kind::EQUAL, n, d_ttDt);
+      }
     }
-    d_booleanTermCache[make_pair(top, boolParent)] = n;
+    d_termCache[make_pair(top, parentTheory)] = n;
     return n;
   }
 }/* BooleanTermConverter::rewriteBooleanTermsRec() */
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h
index c53eadfa0..06f25f9ef 100644
--- a/src/smt/boolean_terms.h
+++ b/src/smt/boolean_terms.h
@@ -38,35 +38,64 @@ typedef expr::Attribute<attr::BooleanTermAttrTag, Node> BooleanTermAttr;
 
 class BooleanTermConverter {
   /** The type of the Boolean term conversion cache */
-  typedef std::hash_map< std::pair<Node, bool>, Node,
+  typedef std::hash_map< std::pair<Node, theory::TheoryId>, Node,
                          PairHashFunction< Node, bool,
-                                           NodeHashFunction, std::hash<int> > > BooleanTermCache;
+                                           NodeHashFunction, std::hash<size_t> > > BooleanTermCache;
+  /** The type of the Boolean term conversion type cache */
+  typedef std::hash_map< std::pair<TypeNode, bool>, TypeNode,
+                         PairHashFunction< TypeNode, bool,
+                                           TypeNodeHashFunction, std::hash<int> > > BooleanTermTypeCache;
+  /** The type of the Boolean term conversion datatype cache */
+  typedef std::hash_map<const Datatype*, const Datatype*, DatatypeHashFunction> BooleanTermDatatypeCache;
 
   /** The SmtEngine to which we're associated */
   SmtEngine& d_smt;
 
+  /** The conversion for "false." */
+  Node d_ff;
+  /** The conversion for "true." */
+  Node d_tt;
+  /** The conversion for "false" when in datatypes contexts. */
+  Node d_ffDt;
+  /** The conversion for "true" when in datatypes contexts. */
+  Node d_ttDt;
+
   /** The cache used during Boolean term conversion */
-  BooleanTermCache d_booleanTermCache;
+  BooleanTermCache d_termCache;
+  /** The cache used during Boolean term type conversion */
+  BooleanTermTypeCache d_typeCache;
+  /** The cache used during Boolean term datatype conversion */
+  BooleanTermDatatypeCache d_datatypeCache;
 
   /**
    * Scan a datatype for and convert as necessary.
    */
-  const Datatype& booleanTermsConvertDatatype(const Datatype& dt) throw();
+  const Datatype& convertDatatype(const Datatype& dt) throw();
+
+  /**
+   * Convert a type.
+   */
+  TypeNode convertType(TypeNode type, bool datatypesContext);
 
-  Node rewriteBooleanTermsRec(TNode n, bool boolParent, std::map<TNode, Node>& quantBoolVars) throw();
+  Node rewriteBooleanTermsRec(TNode n, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw();
 
 public:
 
-  BooleanTermConverter(SmtEngine& smt) :
-    d_smt(smt) {
-  }
+  /**
+   * Construct a Boolean-term converter associated to the given
+   * SmtEngine.
+   */
+  BooleanTermConverter(SmtEngine& smt);
 
   /**
-   * We rewrite Boolean terms in assertions as bitvectors of length 1.
+   * Rewrite Boolean terms under a node.  The node itself is not converted
+   * if boolParent is true, but its Boolean subterms appearing in a
+   * non-Boolean context will be rewritten.
    */
-  Node rewriteBooleanTerms(TNode n, bool boolParent = true) throw() {
+  Node rewriteBooleanTerms(TNode n, bool boolParent = true, bool dtParent = false) throw() {
     std::map<TNode, Node> quantBoolVars;
-    return rewriteBooleanTermsRec(n, boolParent, quantBoolVars);
+    Assert(!(boolParent && dtParent));
+    return rewriteBooleanTermsRec(n, boolParent ? theory::THEORY_BOOL : (dtParent ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), quantBoolVars);
   }
 
 };/* class BooleanTermConverter */
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index 26f5c9c60..fb80b27f7 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -17,37 +17,170 @@
 #include "smt/model_postprocessor.h"
 #include "smt/boolean_terms.h"
 
+using namespace std;
 using namespace CVC4;
 using namespace CVC4::smt;
 
+Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
+  if(n.getType().isSubtypeOf(asType)) {
+    // good to go, we have the right type
+    return n;
+  }
+  if(!n.isConst()) {
+    // we don't handle non-const right now
+    return n;
+  }
+  if(asType.isBoolean()) {
+    if(n.getType().isBitVector(1u)) {
+      // type mismatch: should only happen for Boolean-term conversion under
+      // datatype constructor applications; rewrite from BV(1) back to Boolean
+      bool tf = (n.getConst<BitVector>().getValue() == 1);
+      return NodeManager::currentNM()->mkConst(tf);
+    }
+    if(n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())) {
+      // type mismatch: should only happen for Boolean-term conversion under
+      // datatype constructor applications; rewrite from datatype back to Boolean
+      Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
+      Assert(n.getNumChildren() == 0);
+      // we assume (by construction) false is first; see boolean_terms.cpp
+      bool tf = (Datatype::indexOf(n.getOperator().toExpr()) == 1);
+      Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << " ==> " << tf << endl;
+      return NodeManager::currentNM()->mkConst(tf);
+    }
+  }
+  Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << endl;
+  if(n.getType().isArray()) {
+    Assert(asType.isArray());
+    if(n.getKind() == kind::STORE) {
+      return NodeManager::currentNM()->mkNode(kind::STORE,
+                                              rewriteAs(n[0], asType),
+                                              rewriteAs(n[1], asType[0]),
+                                              rewriteAs(n[2], asType[1]));
+    }
+    Assert(n.getKind() == kind::STORE_ALL);
+    const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>();
+    Node val = rewriteAs(asa.getExpr(), asType[1]);
+    return NodeManager::currentNM()->mkConst(ArrayStoreAll(asType.toType(), val.toExpr()));
+  }
+  if(asType.getNumChildren() != n.getNumChildren() ||
+     n.getMetaKind() == kind::metakind::CONSTANT) {
+    return n;
+  }
+  NodeBuilder<> b(n.getKind());
+  TypeNode::iterator t = asType.begin();
+  for(TNode::iterator i = n.begin(); i != n.end(); ++i, ++t) {
+    Assert(t != asType.end());
+    b << rewriteAs(*i, *t);
+  }
+  Assert(t == asType.end());
+  Debug("boolean-terms") << "+++ constructing " << b << endl;
+  Node out = b;
+  return out;
+}
+
 void ModelPostprocessor::visit(TNode current, TNode parent) {
-  Debug("tuprec") << "visiting " << current << std::endl;
+  Debug("tuprec") << "visiting " << current << endl;
   Assert(!alreadyVisited(current, TNode::null()));
   if(current.getType().hasAttribute(expr::DatatypeTupleAttr())) {
     Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
+    TypeNode expectType = current.getType().getAttribute(expr::DatatypeTupleAttr());
     NodeBuilder<> b(kind::TUPLE);
-    for(TNode::iterator i = current.begin(); i != current.end(); ++i) {
+    TypeNode::iterator t = expectType.begin();
+    for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
       Assert(alreadyVisited(*i, TNode::null()));
+      Assert(t != expectType.end());
       TNode n = d_nodes[*i];
-      b << (n.isNull() ? *i : n);
+      n = n.isNull() ? *i : n;
+      if(!n.getType().isSubtypeOf(*t)) {
+        Assert(n.getType().isBitVector(1u) ||
+               (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
+        Assert(n.isConst());
+        Assert((*t).isBoolean());
+        if(n.getType().isBitVector(1u)) {
+          b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
+        } else {
+          // we assume (by construction) false is first; see boolean_terms.cpp
+          b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
+        }
+      } else {
+        b << n;
+      }
     }
+    Assert(t == expectType.end());
     d_nodes[current] = b;
-    Debug("tuprec") << "returning " << d_nodes[current] << std::endl;
+    Debug("tuprec") << "returning " << d_nodes[current] << endl;
+    Assert(d_nodes[current].getType() == expectType);
   } else if(current.getType().hasAttribute(expr::DatatypeRecordAttr())) {
     Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
+    TypeNode expectType = current.getType().getAttribute(expr::DatatypeRecordAttr());
+    const Record& expectRec = expectType.getConst<Record>();
     NodeBuilder<> b(kind::RECORD);
     b << current.getType().getAttribute(expr::DatatypeRecordAttr());
-    for(TNode::iterator i = current.begin(); i != current.end(); ++i) {
+    Record::const_iterator t = expectRec.begin();
+    for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
       Assert(alreadyVisited(*i, TNode::null()));
+      Assert(t != expectRec.end());
       TNode n = d_nodes[*i];
-      b << (n.isNull() ? *i : n);
+      n = n.isNull() ? *i : n;
+      if(!n.getType().isSubtypeOf(TypeNode::fromType((*t).second))) {
+        Assert(n.getType().isBitVector(1u) ||
+               (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
+        Assert(n.isConst());
+        Assert((*t).second.isBoolean());
+        if(n.getType().isBitVector(1u)) {
+          b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
+        } else {
+          // we assume (by construction) false is first; see boolean_terms.cpp
+          b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
+        }
+      } else {
+        b << n;
+      }
     }
+    Assert(t == expectRec.end());
     d_nodes[current] = b;
-    Debug("tuprec") << "returning " << d_nodes[current] << std::endl;
+    Debug("tuprec") << "returning " << d_nodes[current] << endl;
+    Assert(d_nodes[current].getType() == expectType);
+  } else if(current.getKind() == kind::APPLY_CONSTRUCTOR &&
+            ( current.getOperator().hasAttribute(BooleanTermAttr()) ||
+              ( current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION &&
+                current.getOperator()[0].hasAttribute(BooleanTermAttr()) ) )) {
+    NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
+    Node realOp;
+    if(current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION) {
+      TNode oldAsc = current.getOperator().getOperator();
+      Debug("boolean-terms") << "old asc: " << oldAsc << endl;
+      Node newCons = current.getOperator()[0].getAttribute(BooleanTermAttr());
+      Node newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().toType()));
+      Debug("boolean-terms") << "new asc: " << newAsc << endl;
+      if(newCons.getType().getRangeType().isParametricDatatype()) {
+        vector<TypeNode> oldParams = TypeNode::fromType(oldAsc.getConst<AscriptionType>().getType()).getRangeType().getParamTypes();
+        vector<TypeNode> newParams = newCons.getType().getRangeType().getParamTypes();
+        Assert(oldParams.size() == newParams.size() && oldParams.size() > 0);
+        newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().substitute(newParams.begin(), newParams.end(), oldParams.begin(), oldParams.end()).toType()));
+      }
+      realOp = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, newAsc, newCons);
+    } else {
+      realOp = current.getOperator().getAttribute(BooleanTermAttr());
+    }
+    b << realOp;
+    Debug("boolean-terms") << "+ op " << b.getOperator() << endl;
+    TypeNode::iterator j = realOp.getType().begin();
+    for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++j) {
+      Assert(j != realOp.getType().end());
+      Assert(alreadyVisited(*i, TNode::null()));
+      TNode repl = d_nodes[*i];
+      repl = repl.isNull() ? *i : repl;
+      Debug("boolean-terms") << "+ adding " << repl << " expecting " << *j << endl;
+      b << rewriteAs(repl, *j);
+    }
+    Node n = b;
+    Debug("boolean-terms") << "model-post: " << current << endl
+                           << "- returning " << n << endl;
+    d_nodes[current] = n;
   } else {
-    Debug("tuprec") << "returning self" << std::endl;
+    Debug("tuprec") << "returning self for kind " << current.getKind() << endl;
     // rewrite to self
     d_nodes[current] = Node::null();
   }
 }/* ModelPostprocessor::visit() */
-
diff --git a/src/smt/model_postprocessor.h b/src/smt/model_postprocessor.h
index 08e6168d9..f727a3483 100644
--- a/src/smt/model_postprocessor.h
+++ b/src/smt/model_postprocessor.h
@@ -25,9 +25,12 @@ namespace CVC4 {
 namespace smt {
 
 class ModelPostprocessor {
+  std::hash_map<TNode, Node, TNodeHashFunction> d_nodes;
+
 public:
   typedef Node return_type;
-  std::hash_map<TNode, Node, TNodeHashFunction> d_nodes;
+
+  Node rewriteAs(TNode n, TypeNode asType);
 
   bool alreadyVisited(TNode current, TNode parent) {
     return d_nodes.find(current) != d_nodes.end();
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e98bffc1e..147cea85b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -63,6 +63,8 @@
 #include "theory/logic_info.h"
 #include "theory/options.h"
 #include "theory/booleans/circuit_propagator.h"
+#include "theory/booleans/boolean_term_conversion_mode.h"
+#include "theory/booleans/options.h"
 #include "util/ite_removal.h"
 #include "theory/model.h"
 #include "printer/printer.h"
@@ -586,11 +588,13 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_cumulativeTimeUsed(0),
   d_cumulativeResourceUsed(0),
   d_status(),
-  d_private(new smt::SmtEnginePrivate(*this)),
-  d_statisticsRegistry(new StatisticsRegistry()),
+  d_private(NULL),
+  d_statisticsRegistry(NULL),
   d_stats(NULL) {
 
   SmtScope smts(this);
+  d_private = new smt::SmtEnginePrivate(*this);
+  d_statisticsRegistry = new StatisticsRegistry();
   d_stats = new SmtEngineStatistics();
 
   // We have mutual dependency here, so we add the prop engine to the theory
@@ -2636,10 +2640,26 @@ void SmtEnginePrivate::processAssertions() {
     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
     for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
       Node n = d_booleanTermConverter.rewriteBooleanTerms(d_assertionsToPreprocess[i]);
-      if(n != d_assertionsToPreprocess[i] && !d_smt.d_logic.isTheoryEnabled(theory::THEORY_BV)) {
-        d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
-        d_smt.d_logic.enableTheory(theory::THEORY_BV);
-        d_smt.d_logic.lock();
+      if(n != d_assertionsToPreprocess[i]) {
+        switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) {
+        case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS:
+        case booleans::BOOLEAN_TERM_CONVERT_NATIVE:
+          if(!d_smt.d_logic.isTheoryEnabled(theory::THEORY_BV)) {
+            d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+            d_smt.d_logic.enableTheory(theory::THEORY_BV);
+            d_smt.d_logic.lock();
+          }
+          break;
+        case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
+          if(!d_smt.d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
+            d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+            d_smt.d_logic.enableTheory(theory::THEORY_DATATYPES);
+            d_smt.d_logic.lock();
+          }
+          break;
+        default:
+          Unhandled(mode);
+        }
       }
       d_assertionsToPreprocess[i] = n;
     }
@@ -3046,10 +3066,14 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log
   return quickCheck().asValidityResult();
 }
 
-Node SmtEngine::postprocess(TNode node) {
+Node SmtEngine::postprocess(TNode node, TypeNode expectedType) {
   ModelPostprocessor mpost;
   NodeVisitor<ModelPostprocessor> visitor;
-  return visitor.run(mpost, node);
+  Node value = visitor.run(mpost, node);
+  Debug("boolean-terms") << "postproc: got " << value << " expect type " << expectedType << endl;
+  Node realValue = mpost.rewriteAs(value, expectedType);
+  Debug("boolean-terms") << "postproc: realval " << realValue << " expect type " << expectedType << endl;
+  return realValue;
 }
 
 Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException) {
@@ -3071,7 +3095,7 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep
   // Make sure all preprocessing is done
   d_private->processAssertions();
   Node n = d_private->simplify(Node::fromExpr(e));
-  n = postprocess(n);
+  n = postprocess(n, TypeNode::fromType(e.getType()));
   return n.toExpr();
 }
 
@@ -3093,7 +3117,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L
   }
   hash_map<Node, Node, NodeHashFunction> cache;
   Node n = d_private->expandDefinitions(Node::fromExpr(e), cache);
-  n = postprocess(n);
+  n = postprocess(n, TypeNode::fromType(e.getType()));
   return n.toExpr();
 }
 
@@ -3140,8 +3164,10 @@ Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, TypeCheckingExcep
     resultNode = m->getValue(n);
   }
   Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
-  resultNode = postprocess(resultNode);
+  resultNode = postprocess(resultNode, n.getType());
   Trace("smt") << "--- model-post returned " << resultNode << endl;
+  Trace("smt") << "--- model-post returned " << resultNode.getType() << endl;
+  Trace("smt") << "--- model-post expected " << n.getType() << endl;
 
   // type-check the result we got
   Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(n.getType()));
@@ -3356,7 +3382,9 @@ void SmtEngine::checkModel(bool hardFailure) {
       // function symbol (since then the definition is recursive)
       if (val.getKind() == kind::LAMBDA) {
         // first apply the model substitutions we have so far
+        Debug("boolean-terms") << "applying subses to " << val[1] << endl;
         Node n = substitutions.apply(val[1]);
+        Debug("boolean-terms") << "++ got " << n << endl;
         // now check if n contains func by doing a substitution
         // [func->func2] and checking equality of the Nodes.
         // (this just a way to check if func is in n.)
@@ -3391,6 +3419,7 @@ void SmtEngine::checkModel(bool hardFailure) {
       }
 
       // (3) checks complete, add the substitution
+      Debug("boolean-terms") << "cm: adding subs " << func << " :=> " << val << endl;
       substitutions.addSubstitution(func, val);
     }
   }
@@ -3408,7 +3437,9 @@ void SmtEngine::checkModel(bool hardFailure) {
     Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl;
 
     // Apply our model value substitutions.
+    Debug("boolean-terms") << "applying subses to " << n << endl;
     n = substitutions.apply(n);
+    Debug("boolean-terms") << "++ got " << n << endl;
     Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl;
 
     // Simplify the result.
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index fecfba14a..525f90ffe 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -249,7 +249,7 @@ class CVC4_PUBLIC SmtEngine {
    * like turning datatypes back into tuples, length-1-bitvectors back
    * into booleans, etc.
    */
-  Node postprocess(TNode n);
+  Node postprocess(TNode n, TypeNode expectedType);
 
   /**
    * This is something of an "init" procedure, but is idempotent; call
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index b30a399e4..b3760b239 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -3,7 +3,7 @@ AM_CPPFLAGS = \
 	-I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
-SUBDIRS = builtin booleans uf arith arrays bv datatypes quantifiers rewriterules
+SUBDIRS = builtin booleans uf arith bv arrays datatypes quantifiers rewriterules
 DIST_SUBDIRS = $(SUBDIRS) example
 
 noinst_LTLIBRARIES = libtheory.la
diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am
index 8cb32de18..9d58ffa75 100644
--- a/src/theory/booleans/Makefile.am
+++ b/src/theory/booleans/Makefile.am
@@ -13,7 +13,10 @@ libbooleans_la_SOURCES = \
 	theory_bool_rewriter.h \
 	theory_bool_rewriter.cpp \
 	circuit_propagator.h \
-	circuit_propagator.cpp
+	circuit_propagator.cpp \
+	boolean_term_conversion_mode.h \
+	boolean_term_conversion_mode.cpp
 
 EXTRA_DIST = \
-	kinds
+	kinds \
+	options_handlers.h
diff --git a/src/theory/booleans/boolean_term_conversion_mode.cpp b/src/theory/booleans/boolean_term_conversion_mode.cpp
new file mode 100644
index 000000000..f9d80835c
--- /dev/null
+++ b/src/theory/booleans/boolean_term_conversion_mode.cpp
@@ -0,0 +1,41 @@
+/*********************                                                        */
+/*! \file boolean_term_conversion_mode.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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 <iostream>
+#include "theory/booleans/boolean_term_conversion_mode.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) {
+  switch(mode) {
+  case theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS:
+    out << "BOOLEAN_TERM_CONVERT_TO_BITVECTORS";
+    break;
+  case theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
+    out << "BOOLEAN_TERM_CONVERT_TO_DATATYPES";
+    break;
+  case theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE:
+    out << "BOOLEAN_TERM_CONVERT_NATIVE";
+    break;
+  default:
+    out << "BooleanTermConversionMode!UNKNOWN";
+  }
+
+  return out;
+}
+
+}/* CVC4 namespace */
diff --git a/src/theory/booleans/boolean_term_conversion_mode.h b/src/theory/booleans/boolean_term_conversion_mode.h
new file mode 100644
index 000000000..6ca908df4
--- /dev/null
+++ b/src/theory/booleans/boolean_term_conversion_mode.h
@@ -0,0 +1,53 @@
+/*********************                                                        */
+/*! \file boolean_term_conversion_mode.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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_private.h"
+
+#ifndef __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H
+#define __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H
+
+#include <iostream>
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+typedef enum {
+  /**
+   * Convert Boolean terms to bitvectors of size 1.
+   */
+  BOOLEAN_TERM_CONVERT_TO_BITVECTORS,
+  /**
+   * Convert Boolean terms to enumerations in the Datatypes theory.
+   */
+  BOOLEAN_TERM_CONVERT_TO_DATATYPES,
+  /**
+   * Convert Boolean terms to enumerations in the Datatypes theory IF
+   * used in a datatypes context, otherwise to a bitvector of size 1.
+   */
+  BOOLEAN_TERM_CONVERT_NATIVE
+
+} BooleanTermConversionMode;
+
+}/* CVC4::theory::booleans namespace */
+}/* CVC4::theory namespace */
+
+std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H */
diff --git a/src/theory/booleans/options b/src/theory/booleans/options
index ae14de58b..6c571f30e 100644
--- a/src/theory/booleans/options
+++ b/src/theory/booleans/options
@@ -5,4 +5,7 @@
 
 module BOOLEANS "theory/booleans/options.h" Boolean theory
 
+option booleanTermConversionMode boolean-term-conversion-mode --boolean-term-conversion-mode=MODE CVC4::theory::booleans::BooleanTermConversionMode :default CVC4::theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS :include "theory/booleans/boolean_term_conversion_mode.h" :handler CVC4::theory::booleans::stringToBooleanTermConversionMode :handler-include "theory/booleans/options_handlers.h"
+ policy for converting Boolean terms
+
 endmodule
diff --git a/src/theory/booleans/options_handlers.h b/src/theory/booleans/options_handlers.h
new file mode 100644
index 000000000..2bf53b3d2
--- /dev/null
+++ b/src/theory/booleans/options_handlers.h
@@ -0,0 +1,65 @@
+/*********************                                                        */
+/*! \file options_handlers.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-2012  New York University and The University of Iowa
+ ** 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_private.h"
+
+#ifndef __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H
+
+#include <string>
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+static const std::string booleanTermConversionModeHelp = "\
+Boolean term conversion modes currently supported by the\n\
+--boolean-term-conversion-mode option:\n\
+\n\
+bitvectors [default]\n\
++ Boolean terms are converted to bitvectors of size 1.\n\
+\n\
+datatypes\n\
++ Boolean terms are converted to enumerations in the Datatype theory.\n\
+\n\
+native\n\
++ Boolean terms are converted in a \"natural\" way depending on where they\n\
+  are used.  If in a datatype context, they are converted to an enumeration.\n\
+  Elsewhere, they are converted to a bitvector of size 1.\n\
+";
+
+inline BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg ==  "bitvectors") {
+    return BOOLEAN_TERM_CONVERT_TO_BITVECTORS;
+  } else if(optarg ==  "datatypes") {
+    return BOOLEAN_TERM_CONVERT_TO_DATATYPES;
+  } else if(optarg ==  "native") {
+    return BOOLEAN_TERM_CONVERT_NATIVE;
+  } else if(optarg ==  "help") {
+    puts(booleanTermConversionModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --boolean-term-conversion-mode: `") +
+                          optarg + "'.  Try --boolean-term-conversion-mode help.");
+  }
+}
+
+}/* CVC4::theory::booleans namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H */
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 352868f7b..a369fb572 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -79,7 +79,7 @@ class EqualityTypeRule {
 
       if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) {
         std::stringstream ss;
-        ss << "Subtypes must have a common type:" << std::endl;
+        ss << "Subexpressions must have a common base type:" << std::endl;
         ss << "Equation: " << n << std::endl;
         ss << "Type 1: " << lhsType << std::endl;
         ss << "Type 2: " << rhsType << std::endl;
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index cc589c5c3..6da3b8efc 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -438,7 +438,7 @@ Node Bitblaster::getVarValue(TNode a) {
     if (d_cnfStream->hasLiteral(bits[i])) { 
       SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
       bit_value = d_satSolver->value(bit);
-      Assert (bit_value != SAT_VALUE_UNKNOWN);
+      Assert (bit_value != SAT_VALUE_UNKNOWN); 
     } else {
       // the bit is unconstrainted so we can give it an arbitrary value 
       bit_value = SAT_VALUE_FALSE;
@@ -453,7 +453,7 @@ void Bitblaster::collectModelInfo(TheoryModel* m) {
   __gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin();
   for (; it!= d_variables.end(); ++it) {
     TNode var = *it;
-    if ((Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) && hasValue(var))  {
+    if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var))  {
       Node const_value = getVarValue(var);
       Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= "
                                 << var << " "
diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index 3dfeba140..6d2ed0cf6 100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -458,3 +458,15 @@ BitVector InequalityGraph::getValueInModel(TNode node) const {
   Assert (hasModelValue(id));
   return getValue(id); 
 }
+
+void InequalityGraph::getAllValuesInModel(std::vector<Node>& assignments) {
+  for (ModelValues::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
+    TermId id = (*it).first;
+    BitVector value = (*it).second.value;
+    TNode var = getTermNode(id);
+    Node constant = utils::mkConst(value);
+    Node assignment = utils::mkNode(kind::EQUAL, var, constant);
+    assignments.push_back(assignment); 
+    Debug("bitvector-model") << "   " << var <<" => " << constant << "\n"; 
+  }
+}
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index b23ea7704..860302aa4 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -88,11 +88,11 @@ class InequalityGraph : public context::ContextNotifyObj{
     {}
   };
   
-  typedef context::CDHashMap<TermId, ModelValue> Model;
+  typedef context::CDHashMap<TermId, ModelValue> ModelValues;
 
   struct QueueComparator {
-    const Model* d_model;
-    QueueComparator(const Model* model)
+    const ModelValues* d_model;
+    QueueComparator(const ModelValues* model)
       : d_model(model)
     {}
     bool operator() (TermId left, TermId right) const {
@@ -128,7 +128,7 @@ class InequalityGraph : public context::ContextNotifyObj{
   std::vector<TNode> d_conflict;
   bool d_signed; 
 
-  Model  d_modelValues;
+  ModelValues  d_modelValues;
   void initializeModelValue(TNode node); 
   void setModelValue(TermId term, const ModelValue& mv);
   ModelValue getModelValue(TermId term) const;
@@ -290,7 +290,9 @@ public:
    * 
    * @return 
    */
-  BitVector getValueInModel(TNode a) const; 
+  BitVector getValueInModel(TNode a) const;
+
+  void getAllValuesInModel(std::vector<Node>& assignments); 
 }; 
 
 }
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 4389dc50d..ed90e0ebe 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -91,6 +91,7 @@ public:
   virtual void preRegister(TNode node) {}
   virtual void propagate(Theory::Effort e) {}
   virtual void collectModelInfo(TheoryModel* m) = 0;
+  virtual Node getModelValue(TNode var) = 0; 
   virtual bool isComplete() = 0;
   virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0;
   virtual void addSharedTerm(TNode node) {} 
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index c7387daf8..9c4a5c5b6 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -64,6 +64,7 @@ void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
 
 
 bool BitblastSolver::check(Theory::Effort e) {
+  Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n"; 
   ++(d_statistics.d_numCallstoCheck); 
   //// Eager bit-blasting
   if (options::bitvectorEagerBitblast()) {
@@ -87,7 +88,8 @@ bool BitblastSolver::check(Theory::Effort e) {
 
   // Processing assertions  
   while (!done()) {
-    TNode fact = get(); 
+    TNode fact = get();
+    Debug("bv-bitblast") << "  fact " << fact << ")\n"; 
     if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) {
       // Some atoms have not been bit-blasted yet
       d_bitblaster->bbAtom(fact);
@@ -137,3 +139,7 @@ EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) {
 void BitblastSolver::collectModelInfo(TheoryModel* m) {
   return d_bitblaster->collectModelInfo(m); 
 }
+
+Node BitblastSolver::getModelValue(TNode node) {
+  return d_bitblaster->getVarValue(node);
+}
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index b05ac74cd..b6be84df5 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -50,6 +50,7 @@ public:
   void  explain(TNode literal, std::vector<TNode>& assumptions);
   EqualityStatus getEqualityStatus(TNode a, TNode b);
   void collectModelInfo(TheoryModel* m); 
+  Node getModelValue(TNode node);
   bool isComplete() { return true; }
 };
 
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 112f73083..15720885d 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -222,9 +222,92 @@ bool CoreSolver::check(Theory::Effort e) {
   //   if (!ok)
   //     return false; 
   // }
+
+  // if we are sat and in full check attempt to construct a model
+  if (Theory::fullEffort(e) && isComplete()) {
+    buildModel();
+  }
+  
   return true;
 }
 
+void CoreSolver::buildModel() {
+  Debug("bv-core") << "CoreSolver::buildModel() \n"; 
+  d_modelValues.clear(); 
+  TNodeSet constants;
+  TNodeSet constants_in_eq_engine; 
+  // collect constants in equality engine
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine); 
+  while (!eqcs_i.isFinished()) {
+    TNode repr = *eqcs_i;
+    if  (repr.getKind() == kind::CONST_BITVECTOR) {
+      // must check if it's just the constant
+      eq::EqClassIterator it(repr, &d_equalityEngine);
+      if (!(++it).isFinished()) {
+        constants.insert(repr);
+        constants_in_eq_engine.insert(repr); 
+      }
+    }
+    ++eqcs_i; 
+  }
+  // build repr to value map
+  
+  eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
+  while (!eqcs_i.isFinished()) {
+    TNode repr = *eqcs_i;
+    ++eqcs_i; 
+    TypeNode type = repr.getType(); 
+    if (type.isBitVector() && repr.getKind()!= kind::CONST_BITVECTOR) {
+      Debug("bv-core-model") << "   processing " << repr <<"\n"; 
+      // we need to assign a value for it
+      TypeEnumerator te(type);
+      Node val; 
+      do {
+        val = *te; 
+        ++te;
+        // Debug("bv-core-model") << "  trying value " << val << "\n";
+        // Debug("bv-core-model") << "  is in set? " << constants.count(val) << "\n";
+        // Debug("bv-core-model") << "  enumerator done? " << te.isFinished() << "\n"; 
+      } while (constants.count(val) != 0 && !(te.isFinished()));
+      
+      if (te.isFinished() && constants.count(val) != 0) {
+        // if we cannot enumerate anymore values we just return the lemma stating that
+        // at least two of the representatives are equal.
+        std::vector<TNode> representatives;
+        representatives.push_back(repr);
+
+        for (TNodeSet::const_iterator it = constants_in_eq_engine.begin();
+             it != constants_in_eq_engine.end(); ++it) {
+          TNode constant = *it; 
+          if (utils::getSize(constant) == utils::getSize(repr)) {
+            representatives.push_back(constant); 
+          }
+        }
+        for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
+          representatives.push_back(it->first);
+        }
+        std::vector<Node> equalities; 
+        for (unsigned i = 0; i < representatives.size(); ++i) {
+          for (unsigned j = i + 1; j < representatives.size(); ++j) {
+            TNode a = representatives[i];
+            TNode b = representatives[j];
+            if (utils::getSize(a) == utils::getSize(b)) {
+              equalities.push_back(utils::mkNode(kind::EQUAL, a, b));
+            }
+          }
+        }
+        Node lemma = utils::mkOr(equalities);
+        d_bv->lemma(lemma);
+        Debug("bv-core") << "  lemma: " << lemma << "\n"; 
+        return; 
+      }
+      Debug("bv-core-model") << "   " << repr << " => " << val <<"\n" ;
+      constants.insert(val);
+      d_modelValues[repr] = val; 
+    }
+  }
+}
+
 bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
   // Notify the equality engine 
   if (d_useEqualityEngine && !d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) {
@@ -297,8 +380,6 @@ void CoreSolver::conflict(TNode a, TNode b) {
   d_bv->setConflict(conflict);
 }
 
-
-
 void CoreSolver::collectModelInfo(TheoryModel* m) {
   if (Debug.isOn("bitvector-model")) {
     context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin();
@@ -310,6 +391,20 @@ void CoreSolver::collectModelInfo(TheoryModel* m) {
   set<Node> termSet;
   d_bv->computeRelevantTerms(termSet);
   m->assertEqualityEngine(&d_equalityEngine, &termSet);
+  if (isComplete()) {
+    Debug("bitvector-model") << "CoreSolver::collectModelInfo complete."; 
+    for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
+      Node a = it->first;
+      Node b = it->second;
+      m->assertEquality(a, b, true); 
+    }
+  }
+}
+
+Node CoreSolver::getModelValue(TNode var) {
+  Assert (isComplete());
+  Assert (d_modelValues.find(var) != d_modelValues.end()); 
+  return d_modelValues[d_equalityEngine.getRepresentative(var)]; 
 }
 
 CoreSolver::Statistics::Statistics()
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 4a9d84f79..d04dc164f 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -31,6 +31,9 @@ class Base;
  * Bitvector equality solver
  */
 class CoreSolver : public SubtheorySolver {
+  typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> ModelValue;
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; 
+
   struct Statistics {
     IntStat d_numCallstoCheck;
     Statistics();
@@ -69,7 +72,9 @@ class CoreSolver : public SubtheorySolver {
   Slicer* d_slicer;
   context::CDO<bool> d_isCoreTheory;
   /** To make sure we keep the explanations */
-  context::CDHashSet<Node, NodeHashFunction> d_reasons; 
+  context::CDHashSet<Node, NodeHashFunction> d_reasons;
+  ModelValue d_modelValues;
+  void buildModel(); 
   bool assertFactToEqualityEngine(TNode fact, TNode reason);  
   bool decomposeFact(TNode fact);
   Node getBaseDecomposition(TNode a, std::vector<TNode>& explanation);
@@ -83,6 +88,7 @@ public:
   bool  check(Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions);
   void  collectModelInfo(TheoryModel* m);
+  Node  getModelValue(TNode var); 
   void  addSharedTerm(TNode t) {
     d_equalityEngine.addTriggerTerm(t, THEORY_BV);
   }
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 3d7339e88..27047f6af 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -153,6 +153,23 @@ void InequalitySolver::propagate(Theory::Effort e) {
   Assert (false); 
 }
 
+void InequalitySolver::collectModelInfo(TheoryModel* m) {
+  Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n"; 
+  std::vector<Node> model;
+  d_inequalityGraph.getAllValuesInModel(model);
+  for (unsigned i = 0; i < model.size(); ++i) {
+    Assert (model[i].getKind() == kind::EQUAL); 
+    m->assertEquality(model[i][0], model[i][1], true); 
+  }
+}
+
+Node InequalitySolver::getModelValue(TNode var) {
+  Assert (isComplete());
+  Assert (d_inequalityGraph.hasValueInModel(var)); 
+  BitVector val = d_inequalityGraph.getValueInModel(var);
+  return utils::mkConst(val); 
+}
+
 InequalitySolver::Statistics::Statistics()
   : d_numCallstoCheck("theory::bv::InequalitySolver::NumCallsToCheck", 0)
 {
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index bcf94dc8b..b19ebb381 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -54,7 +54,8 @@ public:
   void propagate(Theory::Effort e); 
   void explain(TNode literal, std::vector<TNode>& assumptions);
   bool isComplete() { return d_isComplete; }
-  void collectModelInfo(TheoryModel* m) {}
+  void collectModelInfo(TheoryModel* m); 
+  Node getModelValue(TNode var); 
   EqualityStatus getEqualityStatus(TNode a, TNode b);
   void assertFact(TNode fact); 
 }; 
diff --git a/src/theory/bv/options b/src/theory/bv/options
index 72db63c09..8e01c6572 100644
--- a/src/theory/bv/options
+++ b/src/theory/bv/options
@@ -14,4 +14,6 @@ option bitvectorShareLemmas --bitblast-share-lemmas bool
 option bitvectorEagerFullcheck --bitblast-eager-fullcheck bool
  check the bitblasting eagerly
 
+option bitvectorInequalitySolver --bv-inequality-solver bool
+ turn on the inequality solver for the bit-vector theory 
 endmodule
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 43e290175..8245fdbdc 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -52,10 +52,12 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
     d_subtheories.push_back(core_solver);
     d_subtheoryMap[SUB_CORE] = core_solver;
 
-    SubtheorySolver* ineq_solver = new InequalitySolver(c, this); 
-    d_subtheories.push_back(ineq_solver);
-    d_subtheoryMap[SUB_INEQUALITY] = ineq_solver;
-
+    if (options::bitvectorInequalitySolver()) {
+      SubtheorySolver* ineq_solver = new InequalitySolver(c, this); 
+      d_subtheories.push_back(ineq_solver);
+      d_subtheoryMap[SUB_INEQUALITY] = ineq_solver;
+    }
+    
     SubtheorySolver* bb_solver = new BitblastSolver(c, this); 
     d_subtheories.push_back(bb_solver);
     d_subtheoryMap[SUB_BITBLAST] = bb_solver;
@@ -164,8 +166,21 @@ void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
   Assert(!inConflict());
   //  Assert (fullModel); // can only query full model
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-    d_subtheories[i]->collectModelInfo(m); 
+    if (d_subtheories[i]->isComplete()) {
+      d_subtheories[i]->collectModelInfo(m);
+      return; 
+    }
+  }
+}
+
+Node TheoryBV::getModelValue(TNode var) {
+  Assert(!inConflict());
+  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+    if (d_subtheories[i]->isComplete()) {
+      return d_subtheories[i]->getModelValue(var); 
+    }
   }
+  Unreachable(); 
 }
 
 void TheoryBV::propagate(Effort e) {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 5d139e11f..6bc4bdaf6 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -125,6 +125,8 @@ private:
 
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
+  Node getModelValue(TNode var);
+
   inline std::string indent()
   {
     std::string indentStr(getSatContext()->getLevel(), ' ');
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 98bc8041d..f8b9f010e 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -249,6 +249,32 @@ inline unsigned isPow2Const(TNode node) {
 
 typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
 
+inline Node mkOr(const std::vector<Node>& nodes) {
+  std::set<TNode> all;
+  all.insert(nodes.begin(), nodes.end());
+
+  if (all.size() == 0) {
+    return mkTrue(); 
+  }
+  
+  if (all.size() == 1) {
+    // All the same, or just one
+    return nodes[0];
+  }
+  
+
+  NodeBuilder<> disjunction(kind::OR);
+  std::set<TNode>::const_iterator it = all.begin();
+  std::set<TNode>::const_iterator it_end = all.end();
+  while (it != it_end) {
+    disjunction << *it;
+    ++ it;
+  }
+
+  return disjunction; 
+}/* mkOr() */
+
+                 
 inline Node mkAnd(const std::vector<TNode>& conjunctions) {
   std::set<TNode> all;
   all.insert(conjunctions.begin(), conjunctions.end());
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 9e4f0de75..a3bec7af0 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -24,6 +24,7 @@
 #include "theory/datatypes/theory_datatypes_type_rules.h"
 #include "theory/model.h"
 #include "smt/options.h"
+#include "smt/boolean_terms.h"
 #include "theory/quantifiers/options.h"
 
 #include <map>
@@ -311,15 +312,28 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
     return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
   }
 
+  TypeNode t = in.getType();
+
   // we only care about tuples and records here
   if(in.getKind() != kind::TUPLE && in.getKind() != kind::TUPLE_UPDATE &&
      in.getKind() != kind::RECORD && in.getKind() != kind::RECORD_UPDATE) {
+    if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) {
+      Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl;
+      Debug("tuprec") << "so " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl;
+      if(t.isTuple()) {
+        Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeTupleAttr()) << endl;
+        Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl;
+        NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()));
+      } else {
+        Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeRecordAttr()) << endl;
+        Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl;
+        NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()));
+      }
+    }
     // nothing to do
     return in;
   }
 
-  TypeNode t = in.getType();
-
   if(t.hasAttribute(expr::DatatypeTupleAttr())) {
     t = t.getAttribute(expr::DatatypeTupleAttr());
   } else if(t.hasAttribute(expr::DatatypeRecordAttr())) {
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 2a74f6d15..a4facdefe 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -176,7 +176,7 @@ class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> {
   void newEnumerators() {
     d_enumerators = new TypeEnumerator*[getType().getNumChildren()];
     for(size_t i = 0; i < getType().getNumChildren(); ++i) {
-      d_enumerators[i] = NULL;
+      d_enumerators[i] = new TypeEnumerator(getType()[i]);
     }
   }
 
@@ -205,9 +205,7 @@ public:
     if(te.d_enumerators != NULL) {
       newEnumerators();
       for(size_t i = 0; i < getType().getNumChildren(); ++i) {
-        if(te.d_enumerators[i] != NULL) {
-          d_enumerators[i] = new TypeEnumerator(*te.d_enumerators[i]);
-        }
+        *d_enumerators[i] = TypeEnumerator(*te.d_enumerators[i]);
       }
     }
   }
@@ -292,9 +290,7 @@ public:
     if(re.d_enumerators != NULL) {
       newEnumerators();
       for(size_t i = 0; i < getType().getNumChildren(); ++i) {
-        if(re.d_enumerators[i] != NULL) {
-          d_enumerators[i] = new TypeEnumerator(*re.d_enumerators[i]);
-        }
+        *d_enumerators[i] = TypeEnumerator(*re.d_enumerators[i]);
       }
     }
   }
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index bbc51c9e0..42a5380e4 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -57,7 +57,7 @@ Node TheoryModel::getValue( TNode n ) const{
 Expr TheoryModel::getValue( Expr expr ) const{
   Node n = Node::fromExpr( expr );
   Node ret = getValue( n );
-  return d_smt.postprocess(ret).toExpr();
+  return d_smt.postprocess(ret, TypeNode::fromType(expr.getType())).toExpr();
 }
 
 /** get cardinality for sort */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 5b2032430..94cf9accd 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -516,6 +516,11 @@ public:
   virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; }
 
   /**
+   * Return the model value of the give shared term (or null if not avalilable.
+   */
+  virtual Node getModelValue(TNode var) { return Node::null(); }
+
+  /**
    * Check the current assignment's consistency.
    *
    * An implementation of check() is required to either:
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f7f689850..b89ca8fa4 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1129,6 +1129,11 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
   return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
 }
 
+Node TheoryEngine::getModelValue(TNode var) {
+  Assert(d_sharedTerms.isShared(var));
+  return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
+}
+
 static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
 
   std::set<TNode> all;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index a3779f0e8..a8fe52498 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -709,6 +709,12 @@ public:
    */
   theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
 
+  /**
+   * Retruns the value that a theory that owns the type of var currently
+   * has (or null if none);
+   */
+  Node getModelValue(TNode var);
+
 private:
 
   /** Default visitor for pre-registration */
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 389a17461..c5d2845bd 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -83,6 +83,11 @@ EqualityStatus Valuation::getEqualityStatus(TNode a, TNode b) {
   return d_engine->getEqualityStatus(a, b);
 }
 
+Node Valuation::getModelValue(TNode var) {
+  return d_engine->getModelValue(var);
+}
+
+
 Node Valuation::ensureLiteral(TNode n) {
   Debug("ensureLiteral") << "rewriting: " << n << std::endl;
   Node rewritten = Rewriter::rewrite(n);
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index f69bacc19..36e62a402 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -97,6 +97,11 @@ public:
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
   /**
+   * Returns the model value of the shared term (or null if not available).
+   */
+  Node getModelValue(TNode var);
+
+  /**
    * Ensure that the given node will have a designated SAT literal
    * that is definitionally equal to it.  The result of this function
    * is a Node that can be queried via getSatValue().
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 18ecbc316..574a57f19 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -820,7 +820,18 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) {
   // can only output datatypes in the CVC4 native language
   Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
 
-  os << "DATATYPE " << dt.getName() << " =" << endl;
+  os << "DATATYPE " << dt.getName();
+  if(dt.isParametric()) {
+    os << '[';
+    for(size_t i = 0; i < dt.getNumParameters(); ++i) {
+      if(i > 0) {
+        os << ',';
+      }
+      os << dt.getParameter(i);
+    }
+    os << ']';
+  }
+  os << " =" << endl;
   Datatype::const_iterator i = dt.begin(), i_end = dt.end();
   if(i != i_end) {
     os << "  ";
diff --git a/src/util/datatype.h b/src/util/datatype.h
index de38d8835..4b6894ef8 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -450,7 +450,7 @@ public:
    * Create a new Datatype of the given name, with the given
    * parameterization.
    */
-  inline Datatype(std::string name, std::vector<Type>& params);
+  inline Datatype(std::string name, const std::vector<Type>& params);
 
   /**
    * Add a constructor to this Datatype.  Constructor names need not
@@ -620,7 +620,7 @@ inline Datatype::Datatype(std::string name) :
   d_self() {
 }
 
-inline Datatype::Datatype(std::string name, std::vector<Type>& params) :
+inline Datatype::Datatype(std::string name, const std::vector<Type>& params) :
   d_name(name),
   d_params(params),
   d_constructors(),
diff --git a/src/util/dense_map.h b/src/util/dense_map.h
index 222a761c3..b7d690811 100644
--- a/src/util/dense_map.h
+++ b/src/util/dense_map.h
@@ -98,7 +98,7 @@ public:
       return false;
     }else{
       Assert(x <  allocated());
-      return d_posVector[x] != POSITION_SENTINEL;
+      return d_posVector[x] != +POSITION_SENTINEL;
     }
   }
 
@@ -160,7 +160,7 @@ public:
   void pop_back() {
     Assert(!empty());
     Key atBack = back();
-    d_posVector[atBack] = POSITION_SENTINEL;
+    d_posVector[atBack] = +POSITION_SENTINEL;
     d_image[atBack] = T();
     d_list.pop_back();
   }
@@ -195,7 +195,7 @@ public:
 
   void increaseSize(Key max){
     Assert(max >= allocated());
-    d_posVector.resize(max+1, POSITION_SENTINEL);
+    d_posVector.resize(max+1, +POSITION_SENTINEL);
     d_image.resize(max+1);
   }
 
diff --git a/src/util/hash.h b/src/util/hash.h
index 4d4094143..913358512 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -48,7 +48,7 @@ namespace CVC4 {
 
 struct StringHashFunction {
   size_t operator()(const std::string& str) const {
-    return std::hash<const char*>()(str.c_str());
+    return __gnu_cxx::hash<const char*>()(str.c_str());
   }
 };/* struct StringHashFunction */
 
diff --git a/src/util/statistics.i b/src/util/statistics.i
index 74cee5f37..7f3bbe526 100644
--- a/src/util/statistics.i
+++ b/src/util/statistics.i
@@ -4,7 +4,7 @@
 #ifdef SWIGJAVA
 
 #include "bindings/java_iterator_adapter.h"
-#include "bindings/java_output_stream_adapter.h"
+#include "bindings/java_stream_adapters.h"
 
 #endif /* SWIGJAVA */
 %}
@@ -72,7 +72,7 @@
 #ifdef SWIGJAVA
 
 %include "bindings/java_iterator_adapter.h"
-%include "bindings/java_output_stream_adapter.h"
+%include "bindings/java_stream_adapters.h"
 
 %template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>;
 
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 08462d51b..8e992c03e 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -38,6 +38,12 @@ TESTS =	\
 	typed_v2l30079.cvc \
 	typed_v3l20092.cvc \
 	typed_v5l30069.cvc \
+	boolean-terms-datatype.cvc \
+	boolean-terms-parametric-datatype-1.cvc \
+	boolean-terms-parametric-datatype-2.cvc \
+	boolean-terms-tuple.cvc \
+	boolean-terms-record.cvc \
+	some-boolean-tests.cvc \
 	v10l40099.cvc \
 	v2l40025.cvc \
 	v3l60006.cvc \
@@ -48,6 +54,7 @@ TESTS =	\
 	wrong-sel-simp.cvc
 
 FAILING_TESTS = \
+	pair-real-bool.smt2 \
 	datatype-dump.cvc
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/datatypes/boolean-terms-datatype.cvc b/test/regress/regress0/datatypes/boolean-terms-datatype.cvc
new file mode 100644
index 000000000..490574b35
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-terms-datatype.cvc
@@ -0,0 +1,12 @@
+% EXPECT: sat
+% EXIT: 10
+
+DATATYPE List =
+  cons(car:BOOLEAN, cdr:List) | nil
+END;
+
+x : List;
+
+ASSERT x /= nil;
+
+CHECKSAT;
diff --git a/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc
new file mode 100644
index 000000000..b667d0bbc
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc
@@ -0,0 +1,13 @@
+% EXPECT: sat
+% EXIT: 10
+
+DATATYPE RightistTree[T] =
+  node(left:BOOLEAN, right:RightistTree[T]) |
+  leaf(data:T)
+END;
+
+x : RightistTree[INT];
+
+ASSERT x /= leaf(0);
+
+CHECKSAT;
diff --git a/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc
new file mode 100644
index 000000000..b667d0bbc
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc
@@ -0,0 +1,13 @@
+% EXPECT: sat
+% EXIT: 10
+
+DATATYPE RightistTree[T] =
+  node(left:BOOLEAN, right:RightistTree[T]) |
+  leaf(data:T)
+END;
+
+x : RightistTree[INT];
+
+ASSERT x /= leaf(0);
+
+CHECKSAT;
diff --git a/test/regress/regress0/datatypes/boolean-terms-record.cvc b/test/regress/regress0/datatypes/boolean-terms-record.cvc
new file mode 100644
index 000000000..ec757d042
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-terms-record.cvc
@@ -0,0 +1,8 @@
+% EXPECT: sat
+% EXIT: 10
+
+x : [# i:INT, b:BOOLEAN #];
+
+ASSERT x /= (# i := 0, b := FALSE #);
+
+CHECKSAT;
diff --git a/test/regress/regress0/datatypes/boolean-terms-tuple.cvc b/test/regress/regress0/datatypes/boolean-terms-tuple.cvc
new file mode 100644
index 000000000..c2d95ce8f
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-terms-tuple.cvc
@@ -0,0 +1,8 @@
+% EXPECT: sat
+% EXIT: 10
+
+x : [ INT, BOOLEAN ];
+
+ASSERT x /= ( 0, FALSE );
+
+CHECKSAT;
diff --git a/test/regress/regress0/datatypes/pair-real-bool.smt2 b/test/regress/regress0/datatypes/pair-real-bool.smt2
new file mode 100644
index 000000000..5d028d723
--- /dev/null
+++ b/test/regress/regress0/datatypes/pair-real-bool.smt2
@@ -0,0 +1,25 @@
+;(set-option :produce-models true)
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes () (
+  ( RealTree 
+    ( Node 
+      (left RealTree) 
+		  (elem Real) 
+		  (right RealTree)) 
+    (Leaf)
+   )
+))
+
+(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))
+
+( declare-fun SumeAndPositiveTree ( RealTree ) (Pair Real Bool) )
+
+(declare-fun l1 () RealTree)
+(declare-fun l2 () RealTree)
+(declare-const result (Pair Real Bool))
+(assert (= l1 (Node l2 5.0 l2)))
+(assert (= result (SumeAndPositiveTree l1)))
+(assert (= (first result) 5))
+(assert (= (second result) true))
+(check-sat)
diff --git a/test/regress/regress0/datatypes/some-boolean-tests.cvc b/test/regress/regress0/datatypes/some-boolean-tests.cvc
new file mode 100644
index 000000000..ac6ef1137
--- /dev/null
+++ b/test/regress/regress0/datatypes/some-boolean-tests.cvc
@@ -0,0 +1,12 @@
+% EXPECT: sat
+% EXIT: 10
+DATATYPE list[T] = cons(car:T, care:BOOLEAN, cdr:list[T]) | nil END;
+x : list[REAL];
+
+y : [INT,BOOLEAN,INT];
+ASSERT y = (5,TRUE,4);
+
+ASSERT y.1;
+
+ASSERT x = cons(1.1,TRUE,nil::list[REAL])::list[REAL];
+CHECKSAT;