First chunk of boolean-terms support.

Passes simple tests and doesn't break existing functionality.
Still need some work merged in for models.

This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV).  Tonight's nightly regression run should tell us if/how that hurts performance.

(this commit was certified error- and warning-free by the test-and-commit script.)

21 files changed, 557 insertions, 101 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 5be612b20..8ded902b7 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -231,12 +231,6 @@ void PopCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
-/* class CheckSatCommand */
-
-CheckSatCommand::CheckSatCommand() throw() :
-  d_expr() {
-}
-
 Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
   return new PopCommand();
 }
@@ -247,6 +241,10 @@ Command* PopCommand::clone() const {
 
 /* class CheckSatCommand */
 
+CheckSatCommand::CheckSatCommand() throw() :
+  d_expr() {
+}
+
 CheckSatCommand::CheckSatCommand(const Expr& expr) throw() :
   d_expr(expr) {
 }
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 7cb5eb459..5159f6b5a 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -700,10 +700,6 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
       // CVC4::Datatype class, but this actually needs to be checked.
       AlwaysAssert(!SelectorType(selectorType).getRangeType().d_typeNode->isFunctionLike(),
                    "cannot put function-like things in datatypes");
-      // currently don't play well with Boolean terms
-      if(SelectorType(selectorType).getRangeType().d_typeNode->isBoolean()) {
-        WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a datatype containing a Boolean)" << std::endl;
-      }
     }
   }
 }
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 6e08a9bc2..5cf591f9d 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1055,9 +1055,6 @@ NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) {
   for (unsigned i = 0; i < sorts.size(); ++ i) {
     CheckArgument(!sorts[i].isFunctionLike(), sorts,
                   "cannot create higher-order function types");
-    if(i + 1 < sorts.size() && sorts[i].isBoolean()) {
-      WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a function type with a Boolean argument)" << std::endl;
-    }
     sortNodes.push_back(sorts[i]);
   }
   return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
@@ -1070,9 +1067,6 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
   for (unsigned i = 0; i < sorts.size(); ++ i) {
     CheckArgument(!sorts[i].isFunctionLike(), sorts,
                   "cannot create higher-order function types");
-    if(i + 1 < sorts.size() && sorts[i].isBoolean()) {
-      WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a predicate type with a Boolean argument)" << std::endl;
-    }
     sortNodes.push_back(sorts[i]);
   }
   sortNodes.push_back(booleanType());
@@ -1085,9 +1079,6 @@ inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
   for (unsigned i = 0; i < types.size(); ++ i) {
     CheckArgument(!types[i].isFunctionLike(), types,
                   "cannot put function-like types in tuples");
-    if(types[i].isBoolean()) {
-      WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a tuple type with a Boolean argument)" << std::endl;
-    }
     typeNodes.push_back(types[i]);
   }
   return mkTypeNode(kind::TUPLE_TYPE, typeNodes);
@@ -1119,9 +1110,6 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
                 "cannot index arrays by a function-like type");
   CheckArgument(!constituentType.isFunctionLike(), constituentType,
                 "cannot store function-like types in arrays");
-  if(indexType.isBoolean() || constituentType.isBoolean()) {
-    WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created an array type with a Boolean index or constituent type)" << std::endl;
-  }
   Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl;
   return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
 }
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 10ca16001..57589ec9c 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -277,66 +277,70 @@ bool Parser::isUnresolvedType(const std::string& name) {
 std::vector<DatatypeType>
 Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
 
-  std::vector<DatatypeType> types =
-    d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
-
-  assert(datatypes.size() == types.size());
-
-  for(unsigned i = 0; i < datatypes.size(); ++i) {
-    DatatypeType t = types[i];
-    const Datatype& dt = t.getDatatype();
-    const std::string& name = dt.getName();
-    Debug("parser-idt") << "define " << name << " as " << t << std::endl;
-    if(isDeclared(name, SYM_SORT)) {
-      throw ParserException(name + " already declared");
-    }
-    if( t.isParametric() ) {
-      std::vector< Type > paramTypes = t.getParamTypes();
-      defineType(name, paramTypes, t );
-    } else {
-      defineType(name, t);
-    }
-    for(Datatype::const_iterator j = dt.begin(),
-          j_end = dt.end();
-        j != j_end;
-        ++j) {
-      const DatatypeConstructor& ctor = *j;
-      Expr::printtypes::Scope pts(Debug("parser-idt"), true);
-      Expr constructor = ctor.getConstructor();
-      Debug("parser-idt") << "+ define " << constructor << std::endl;
-      string constructorName = ctor.getName();
-      if(isDeclared(constructorName, SYM_VARIABLE)) {
-        throw ParserException(constructorName + " already declared");
+  try {
+    std::vector<DatatypeType> types =
+      d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
+
+    assert(datatypes.size() == types.size());
+
+    for(unsigned i = 0; i < datatypes.size(); ++i) {
+      DatatypeType t = types[i];
+      const Datatype& dt = t.getDatatype();
+      const std::string& name = dt.getName();
+      Debug("parser-idt") << "define " << name << " as " << t << std::endl;
+      if(isDeclared(name, SYM_SORT)) {
+        throw ParserException(name + " already declared");
       }
-      defineVar(constructorName, constructor);
-      Expr tester = ctor.getTester();
-      Debug("parser-idt") << "+ define " << tester << std::endl;
-      string testerName = ctor.getTesterName();
-      if(isDeclared(testerName, SYM_VARIABLE)) {
-        throw ParserException(testerName + " already declared");
+      if( t.isParametric() ) {
+        std::vector< Type > paramTypes = t.getParamTypes();
+        defineType(name, paramTypes, t );
+      } else {
+        defineType(name, t);
       }
-      defineVar(testerName, tester);
-      for(DatatypeConstructor::const_iterator k = ctor.begin(),
-            k_end = ctor.end();
-          k != k_end;
-          ++k) {
-        Expr selector = (*k).getSelector();
-        Debug("parser-idt") << "+++ define " << selector << std::endl;
-        string selectorName = (*k).getName();
-        if(isDeclared(selectorName, SYM_VARIABLE)) {
-          throw ParserException(selectorName + " already declared");
+      for(Datatype::const_iterator j = dt.begin(),
+            j_end = dt.end();
+          j != j_end;
+          ++j) {
+        const DatatypeConstructor& ctor = *j;
+        Expr::printtypes::Scope pts(Debug("parser-idt"), true);
+        Expr constructor = ctor.getConstructor();
+        Debug("parser-idt") << "+ define " << constructor << std::endl;
+        string constructorName = ctor.getName();
+        if(isDeclared(constructorName, SYM_VARIABLE)) {
+          throw ParserException(constructorName + " already declared");
+        }
+        defineVar(constructorName, constructor);
+        Expr tester = ctor.getTester();
+        Debug("parser-idt") << "+ define " << tester << std::endl;
+        string testerName = ctor.getTesterName();
+        if(isDeclared(testerName, SYM_VARIABLE)) {
+          throw ParserException(testerName + " already declared");
+        }
+        defineVar(testerName, tester);
+        for(DatatypeConstructor::const_iterator k = ctor.begin(),
+              k_end = ctor.end();
+            k != k_end;
+            ++k) {
+          Expr selector = (*k).getSelector();
+          Debug("parser-idt") << "+++ define " << selector << std::endl;
+          string selectorName = (*k).getName();
+          if(isDeclared(selectorName, SYM_VARIABLE)) {
+            throw ParserException(selectorName + " already declared");
+          }
+          defineVar(selectorName, selector);
         }
-        defineVar(selectorName, selector);
       }
     }
-  }
 
-  // These are no longer used, and the ExprManager would have
-  // complained of a bad substitution if anything is left unresolved.
-  // Clear out the set.
-  d_unresolved.clear();
+    // These are no longer used, and the ExprManager would have
+    // complained of a bad substitution if anything is left unresolved.
+    // Clear out the set.
+    d_unresolved.clear();
 
-  return types;
+    return types;
+  } catch(IllegalArgumentException& ie) {
+    throw ParserException(ie.getMessage());
+  }
 }
 
 bool Parser::isDeclared(const std::string& name, SymbolType type) {
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index b3e16b38e..a61d2d4c0 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -20,7 +20,7 @@
 #include "expr/node_manager.h" // for VarNameAttr
 #include "expr/command.h"
 #include "theory/substitutions.h"
-
+#include "smt/boolean_terms.h"
 #include "theory/model.h"
 
 #include <iostream>
@@ -305,24 +305,23 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
     case kind::CONSTRUCTOR_TYPE:
     case kind::SELECTOR_TYPE:
-      if (n.getNumChildren() > 1) {
-        if (n.getNumChildren() > 2) {
+      if(n.getNumChildren() > 1) {
+        if(n.getNumChildren() > 2) {
           out << '(';
         }
-        for (unsigned i = 0; i < n.getNumChildren(); ++ i) {
-          if (i > 0) {
+        for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) {
+          if(i > 0) {
             out << ", ";
           }
           toStream(out, n[i], depth, types, false);
         }
-        if (n.getNumChildren() > 2) {
+        if(n.getNumChildren() > 2) {
           out << ')';
         }
+        out << " -> ";
       }
-      out << " -> ";
-      toStream(out, n[n.getNumChildren()-1], depth, types, false);
+      toStream(out, n[n.getNumChildren() - 1], depth, types, false);
       return;
-      break;
     case kind::TESTER_TYPE:
       toStream(out, n[0], depth, types, false);
       out << " -> BOOLEAN";
@@ -823,6 +822,11 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t
     Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() );
     TypeNode tn = n.getType();
     out << n << " : ";
+    /* Boolean terms functionality needs to be merged in
+    if(n.hasAttribute(smt::BooleanTermAttr())) {
+      out << "*** ";
+    }
+    */
     if( tn.isFunction() || tn.isPredicate() ){
       out << "(";
       for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
@@ -977,7 +981,7 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
 }
 
 static void toStream(std::ostream& out, const GetModelCommand* c) throw() {
-  out << "% (get-model)";
+  out << "COUNTERMODEL;";
 }
 
 static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {
@@ -985,7 +989,7 @@ static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {
 }
 
 static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() {
-  out << "% (get-assertions)";
+  out << "WHERE;";
 }
 
 static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() {
@@ -1007,9 +1011,9 @@ static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
 }
 
 static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
-  out << "% (set-option " << c->getFlag() << " ";
+  out << "OPTION \"" << c->getFlag() << "\" ";
   toStream(out, c->getSExpr());
-  out << ")";
+  out << ";";
 }
 
 static void toStream(std::ostream& out, const GetOptionCommand* c) throw() {
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 82601e3c3..75f17326d 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -15,6 +15,8 @@ libsmt_la_SOURCES = \
 	command_list.cpp \
 	command_list.h \
 	modal_exception.h \
+	boolean_terms.h \
+	boolean_terms.cpp \
 	logic_exception.h \
 	simplification_mode.h \
 	simplification_mode.cpp
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
new file mode 100644
index 000000000..c332642f1
--- /dev/null
+++ b/src/smt/boolean_terms.cpp
@@ -0,0 +1,254 @@
+/*********************                                                        */
+/*! \file boolean_terms.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-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "smt/boolean_terms.h"
+#include "smt/smt_engine.h"
+#include "theory/theory_engine.h"
+#include "theory/model.h"
+#include "expr/kind.h"
+#include <string>
+#include <algorithm>
+
+using namespace std;
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace smt {
+
+const Datatype& BooleanTermConverter::booleanTermsConvertDatatype(const Datatype& dt) throw() {
+  return dt;
+  // boolean terms not supported in datatypes, yet
+
+  Debug("boolean-terms") << "booleanTermsConvertDatatype: 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() + "'");
+        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) {
+                ctor.addArg((*a).getName() + "'", DatatypeSelfType());
+              } else {
+                ctor.addArg((*a).getName() + "'", argType);
+              }
+            }
+          }
+          newDt.addConstructor(ctor);
+        }
+        DatatypeType newDtt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(newDt);
+        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());
+          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() + "'"));
+          }
+        }
+        return newD;
+      }
+    }
+  }
+  return dt;
+}/* BooleanTermConverter::booleanTermsConvertDatatype() */
+
+Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw() {
+  Debug("boolean-terms") << "rewriteBooleanTerms: " << top << " - boolParent=" << boolParent << endl;
+
+  BooleanTermCache::iterator i = d_booleanTermCache.find(make_pair<Node, bool>(top, boolParent));
+  if(i != d_booleanTermCache.end()) {
+    return (*i).second.isNull() ? Node(top) : (*i).second;
+  }
+
+  Kind k = top.getKind();
+  kind::MetaKind mk = top.getMetaKind();
+
+  NodeManager* nm = NodeManager::currentNM();
+
+  if(!boolParent && top.getType().isBoolean()) {
+    Node one = nm->mkConst(BitVector(1u, 1u));
+    Node zero = nm->mkConst(BitVector(1u, 0u));
+    // still need to rewrite e.g. function applications over boolean
+    Node topRewritten = rewriteBooleanTerms(top, true);
+    Node n = nm->mkNode(kind::ITE, topRewritten, one, zero);
+    Debug("boolean-terms") << "constructed ITE: " << n << endl;
+    return n;
+  }
+
+  if(mk == kind::metakind::CONSTANT) {
+    Assert(k != kind::STORE_ALL, "array store-all not yet supported by Boolean-term conversion");
+    return top;
+  } else if(mk == kind::metakind::VARIABLE) {
+    TypeNode t = top.getType();
+    if(t.isFunction()) {
+      for(unsigned i = 0; i < t.getNumChildren() - 1; ++i) {
+        if(t[i].isBoolean()) {
+          vector<TypeNode> argTypes = t.getArgTypes();
+          replace(argTypes.begin(), argTypes.end(), t[i], nm->mkBitVectorType(1));
+          TypeNode newType = nm->mkFunctionType(argTypes, t.getRangeType());
+          Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "_bt",
+                                newType, "a function introduced by Boolean-term conversion",
+                                NodeManager::SKOLEM_EXACT_NAME);
+          Debug("boolean-terms") << "constructed func: " << n << " of type " << newType << endl;
+          top.setAttribute(BooleanTermAttr(), n);
+          d_booleanTermCache[make_pair(top, boolParent)] = 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 newType = nm->mkArrayType(indexType, constituentType);
+        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;
+        d_booleanTermCache[make_pair(top, boolParent)] = n;
+        return n;
+      }
+      d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+      return top;
+    } else if(t.isTuple()) {
+      return top;
+    } else if(t.isRecord()) {
+      return top;
+    } else if(t.isDatatype()) {
+      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(),
+               "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",
+                              NodeManager::SKOLEM_EXACT_NAME);
+        top.setAttribute(BooleanTermAttr(), n);
+        Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
+        d_booleanTermCache[make_pair(top, boolParent)] = n;
+        return n;
+      } else {
+        d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+        return top;
+      }
+    } else if(t.isConstructor()) {
+      Assert(!boolParent);
+      const Datatype& dt = t[t.getNumChildren() - 1].getConst<Datatype>();
+      const Datatype& dt2 = booleanTermsConvertDatatype(dt);
+      if(dt != dt2) {
+        Assert(d_booleanTermCache.find(make_pair(top, boolParent)) != d_booleanTermCache.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;
+      }
+    } else if(t.isTester() || t.isSelector()) {
+      Assert(!boolParent);
+      const Datatype& dt = t[0].getConst<Datatype>();
+      const Datatype& dt2 = booleanTermsConvertDatatype(dt);
+      if(dt != dt2) {
+        Assert(d_booleanTermCache.find(make_pair(top, boolParent)) != d_booleanTermCache.end(),
+               "tester or selector `%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;
+      }
+    } 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));
+          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;
+          return n;
+        }
+      }
+    }/* else if(t.isRecord()) {
+      Unimplemented();
+    }*/
+    return top;
+  }
+  switch(k) {
+  case kind::LAMBDA:
+  case kind::FORALL:
+  case kind::EXISTS:
+  case kind::REWRITE_RULE:
+  case kind::RR_REWRITE:
+  case kind::RR_REDUCTION:
+  case kind::RR_DEDUCTION:
+    //Assert(false, "not yet supported");
+    return top;
+
+  default:
+    NodeBuilder<> b(k);
+    Debug("bt") << "looking at: " << top << std::endl;
+    if(mk == kind::metakind::PARAMETERIZED) {
+      if(kindToTheoryId(k) != THEORY_BV &&
+         k != kind::TUPLE_SELECT &&
+         k != kind::TUPLE_UPDATE &&
+         k != kind::RECORD_SELECT &&
+         k != kind::RECORD_UPDATE &&
+         k != kind::RECORD) {
+        Debug("bt") << "rewriting: " << top.getOperator() << std::endl;
+        b << rewriteBooleanTerms(top.getOperator(), kindToTheoryId(k) == THEORY_BOOL);
+        Debug("bt") << "got: " << b.getOperator() << std::endl;
+      } else {
+        b << top.getOperator();
+      }
+    }
+    for(TNode::const_iterator i = top.begin(); i != top.end(); ++i) {
+      Debug("bt") << "rewriting: " << *i << std::endl;
+      b << rewriteBooleanTerms(*i, kindToTheoryId(k) == THEORY_BOOL);
+      Debug("bt") << "got: " << b[b.getNumChildren() - 1] << std::endl;
+    }
+    Node n = b;
+    Debug("boolean-terms") << "constructed: " << n << endl;
+    d_booleanTermCache[make_pair(top, boolParent)] = n;
+    return n;
+  }
+}/* BooleanTermConverter::rewriteBooleanTerms() */
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h
new file mode 100644
index 000000000..dea9adcf7
--- /dev/null
+++ b/src/smt/boolean_terms.h
@@ -0,0 +1,62 @@
+/*********************                                                        */
+/*! \file boolean_terms.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  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "expr/attribute.h"
+#include "expr/node.h"
+#include "util/hash.h"
+#include <utility>
+
+namespace CVC4 {
+namespace smt {
+
+namespace attr {
+  struct BooleanTermAttrTag { };
+}/* CVC4::smt::attr namespace */
+
+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,
+                         PairHashFunction< Node, bool,
+                                           NodeHashFunction, std::hash<int> > > BooleanTermCache;
+
+  /** The cache used during Boolean term conversion */
+  BooleanTermCache d_booleanTermCache;
+
+  /**
+   * Scan a datatype for and convert as necessary.
+   */
+  const Datatype& booleanTermsConvertDatatype(const Datatype& dt) throw();
+
+public:
+
+  /**
+   * We rewrite Boolean terms in assertions as bitvectors of length 1.
+   */
+  Node rewriteBooleanTerms(TNode n, bool boolParent = true) throw();
+
+};/* class BooleanTermConverter */
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 68b7222d7..a3065f29b 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -82,7 +82,7 @@ assertions\n\
 + Output the assertions after preprocessing and before clausification.\n\
   Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
   where PASS is one of the preprocessing passes: definition-expansion\n\
-  constrain-subtypes substitution skolem-quant simplify\n\
+  boolean-terms constrain-subtypes substitution skolem-quant simplify\n\
   static-learning ite-removal repeat-simplify theory-preprocessing.\n\
   PASS can also be the special value \"everything\", in which case the\n\
   assertions are printed before any preprocessing (with\n\
@@ -176,6 +176,7 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
       }
       if(!strcmp(p, "everything")) {
       } else if(!strcmp(p, "definition-expansion")) {
+      } else if(!strcmp(p, "boolean-terms")) {
       } else if(!strcmp(p, "constrain-subtypes")) {
       } else if(!strcmp(p, "substitution")) {
       } else if(!strcmp(p, "skolem-quant")) {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 07e3439fc..8e6fcccb8 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -50,6 +50,7 @@
 #include "util/configuration.h"
 #include "util/exception.h"
 #include "smt/command_list.h"
+#include "smt/boolean_terms.h"
 #include "smt/options.h"
 #include "options/option_exception.h"
 #include "util/output.h"
@@ -105,6 +106,8 @@ public:
 struct SmtEngineStatistics {
   /** time spent in definition-expansion */
   TimerStat d_definitionExpansionTime;
+  /** time spent in Boolean term rewriting */
+  TimerStat d_rewriteBooleanTermsTime;
   /** time spent in non-clausal simplification */
   TimerStat d_nonclausalSimplificationTime;
   /** Num of constant propagations found during nonclausal simp */
@@ -130,6 +133,7 @@ struct SmtEngineStatistics {
 
   SmtEngineStatistics() :
     d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
+    d_rewriteBooleanTermsTime("smt::SmtEngine::rewriteBooleanTermsTime"),
     d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
     d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
     d_staticLearningTime("smt::SmtEngine::staticLearningTime"),
@@ -143,6 +147,7 @@ struct SmtEngineStatistics {
     d_checkModelTime("smt::SmtEngine::checkModelTime") {
 
     StatisticsRegistry::registerStat(&d_definitionExpansionTime);
+    StatisticsRegistry::registerStat(&d_rewriteBooleanTermsTime);
     StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
     StatisticsRegistry::registerStat(&d_numConstantProps);
     StatisticsRegistry::registerStat(&d_staticLearningTime);
@@ -158,6 +163,7 @@ struct SmtEngineStatistics {
 
   ~SmtEngineStatistics() {
     StatisticsRegistry::unregisterStat(&d_definitionExpansionTime);
+    StatisticsRegistry::unregisterStat(&d_rewriteBooleanTermsTime);
     StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
     StatisticsRegistry::unregisterStat(&d_numConstantProps);
     StatisticsRegistry::unregisterStat(&d_staticLearningTime);
@@ -198,6 +204,9 @@ class SmtEnginePrivate : public NodeManagerListener {
   /** Size of assertions array when preprocessing starts */
   unsigned d_realAssertionsEnd;
 
+  /** The converter for Boolean terms -> BITVECTOR(1). */
+  BooleanTermConverter d_booleanTermConverter;
+
   /** A circuit propagator for non-clausal propositional deduction */
   booleans::CircuitPropagator d_propagator;
 
@@ -334,6 +343,7 @@ public:
     d_assertionsToPreprocess(),
     d_nonClausalLearnedLiterals(),
     d_realAssertionsEnd(0),
+    d_booleanTermConverter(),
     d_propagator(d_nonClausalLearnedLiterals, true, true),
     d_assertionsToCheck(),
     d_fakeContext(),
@@ -951,6 +961,13 @@ void SmtEngine::setLogicInternal() throw() {
       setOption("check-models", SExpr("false"));
     }
   }
+
+  // may need to force BV on to handle Boolean terms
+  if(!d_logic.isPure(theory::THEORY_ARITH)) {
+    d_logic = d_logic.getUnlockedCopy();
+    d_logic.enableTheory(theory::THEORY_BV);
+    d_logic.lock();
+  }
 }
 
 void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
@@ -2063,6 +2080,20 @@ void SmtEnginePrivate::processAssertions() {
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
+  dumpAssertions("pre-boolean-terms", d_assertionsToPreprocess);
+  {
+    Chat() << "rewriting Boolean terms..." << endl;
+    TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
+    for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
+      d_assertionsToPreprocess[i] =
+        d_booleanTermConverter.rewriteBooleanTerms(d_assertionsToPreprocess[i]);
+    }
+  }
+  dumpAssertions("post-boolean-terms", d_assertionsToPreprocess);
+
+  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
+  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+
   dumpAssertions("pre-constrain-subtypes", d_assertionsToPreprocess);
   {
     // Any variables of subtype types need to be constrained properly.
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 60d79e90e..42fe10cb9 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -694,7 +694,9 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa
     stringstream ss;
     ss << "The logic was specified as " << d_logicInfo.getLogicString()
        << ", which doesn't include " << Theory::theoryOf(atom)
-       << ", but got an asserted fact to that theory";
+       << ", but got a preprocessing-time fact for that theory." << endl
+       << "The fact:" << endl
+       << literal;
     throw LogicException(ss.str());
   }
 
@@ -792,7 +794,9 @@ Node TheoryEngine::preprocess(TNode assertion) {
       stringstream ss;
       ss << "The logic was specified as " << d_logicInfo.getLogicString()
          << ", which doesn't include " << Theory::theoryOf(current)
-         << ", but got an asserted fact to that theory";
+         << ", but got a preprocesing-time fact for that theory." << endl
+         << "The fact:" << endl
+         << current;
       throw LogicException(ss.str());
     }
 
@@ -882,7 +886,9 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId,
     stringstream ss;
     ss << "The logic was specified as " << d_logicInfo.getLogicString()
        << ", which doesn't include " << toTheoryId
-       << ", but got an asserted fact to that theory";
+       << ", but got an asserted fact to that theory." << endl
+       << "The fact:" << endl
+       << assertion;
     throw LogicException(ss.str());
   }
 
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index be98e40e1..18ecbc316 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -296,8 +296,8 @@ bool Datatype::operator==(const Datatype& other) const throw() {
     return false;
   }
 
-  if(d_name != other.d_name ||
-     getNumConstructors() != other.getNumConstructors()) {
+  if( d_name != other.d_name ||
+      getNumConstructors() != other.getNumConstructors() ) {
     return false;
   }
   for(const_iterator i = begin(), j = other.begin(); i != end(); ++i, ++j) {
@@ -765,7 +765,7 @@ Expr DatatypeConstructorArg::getConstructor() const {
   return d_constructor;
 }
 
-Type DatatypeConstructorArg::getType() const {
+SelectorType DatatypeConstructorArg::getType() const {
   return getSelector().getType();
 }
 
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 4006702c5..de38d8835 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -111,7 +111,7 @@ public:
    * Get the type of the selector for this constructor argument;
    * this call is only permitted after resolution.
    */
-  Type getType() const;
+  SelectorType getType() const;
 
   /**
    * Get the name of the type of this constructor argument
diff --git a/src/util/exception.cpp b/src/util/exception.cpp
index 95d307744..92f5c1840 100644
--- a/src/util/exception.cpp
+++ b/src/util/exception.cpp
@@ -19,6 +19,7 @@
 #include <cstdio>
 #include <cstdlib>
 #include <cstdarg>
+#include "util/cvc4_assert.h"
 
 using namespace std;
 using namespace CVC4;
@@ -63,7 +64,14 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
 
   setMessage(string(buf));
 
+#ifdef CVC4_DEBUG
+  if(s_debugLastException == NULL) {
+    // we leak buf[] but only in debug mode with assertions failing
+    s_debugLastException = buf;
+  }
+#else /* CVC4_DEBUG */
   delete [] buf;
+#endif /* CVC4_DEBUG */
 }
 
 void IllegalArgumentException::construct(const char* header, const char* extra,
@@ -96,5 +104,12 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
 
   setMessage(string(buf));
 
+#ifdef CVC4_DEBUG
+  if(s_debugLastException == NULL) {
+    // we leak buf[] but only in debug mode with assertions failing
+    s_debugLastException = buf;
+  }
+#else /* CVC4_DEBUG */
   delete [] buf;
+#endif /* CVC4_DEBUG */
 }
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 4789b0a55..6af6fbf70 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -49,7 +49,11 @@ SMT2_TESTS = \
 	simple-uf.smt2 \
 	simplification_bug4.smt2 \
 	parallel-let.smt2 \
-	get-value-incremental.smt2
+	get-value-incremental.smt2 \
+	hung13sdk_output1.smt2 \
+	hung10_itesdk_output2.smt2 \
+	hung10_itesdk_output1.smt2 \
+	hung13sdk_output2.smt2
 
 # Regression tests for PL inputs
 CVC_TESTS = \
@@ -116,6 +120,7 @@ BUG_TESTS = \
 	bug168.smt \
 	bug187.smt2 \
 	bug216.smt2 \
+	bug217.smt2 \
 	bug220.smt2 \
 	bug239.smt \
 	bug274.cvc \
diff --git a/test/regress/regress0/uf/bug217.smt2 b/test/regress/regress0/bug217.smt2
index 45f0f3c0c..92b72c87d 100644
--- a/test/regress/regress0/uf/bug217.smt2
+++ b/test/regress/regress0/bug217.smt2
@@ -1,10 +1,12 @@
+; EXPECT: unsat
+; EXIT: 20
 (set-logic QF_UF)
-(set-info :status unsat)
+(set-info :status sat)
+(set-option :produce-models true)
 (declare-fun f (Bool) Bool)
 (declare-fun x () Bool)
 (declare-fun y () Bool)
 (declare-fun z () Bool)
-;(assert (and x (or (f x) (f y))))
 (assert (or (f x) (f y) (f z)))
 (assert (not (f false)))
 (assert (not (f true)))
diff --git a/test/regress/regress0/hung10_itesdk_output1.smt2 b/test/regress/regress0/hung10_itesdk_output1.smt2
new file mode 100644
index 000000000..8bcdfdfbc
--- /dev/null
+++ b/test/regress/regress0/hung10_itesdk_output1.smt2
@@ -0,0 +1,30 @@
+( set-logic QF_ALL_SUPPORTED)
+( set-info :source | SMT-COMP'06 organizers |)
+( set-info :smt-lib-version 2.0)
+( set-info :category "check")
+( set-info :status sat)
+( declare-fun x1 () Bool)
+( declare-fun x2 () Real)
+( declare-fun x3 () Real)
+( declare-fun x4 () Bool)
+( declare-fun x5 () Real)
+( declare-fun x6 () Real)
+( declare-fun x7 () Real)
+( declare-fun x8 () Real)
+( declare-fun bo1 () Bool)
+( declare-fun bo2 () Bool)
+( declare-fun bo3 () Bool)
+( declare-fun r1 () Real)
+( declare-fun r2 () Real)
+( declare-fun r3 () Real)
+( define-fun myBoolIte ( ( a Real) ( b Bool) ( c Bool)) Bool
+  ( ite ( > a 0.0) b c))
+( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real
+  ( ite a1 b1 c1))
+( declare-fun f ( Real Bool) Real)
+( declare-fun fRealRealReal ( Real Real) Real)
+( declare-fun fRealReal ( Real) Real)
+( declare-fun fReal () Real)
+( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/hung10_itesdk_output2.smt2 b/test/regress/regress0/hung10_itesdk_output2.smt2
new file mode 100644
index 000000000..8bcdfdfbc
--- /dev/null
+++ b/test/regress/regress0/hung10_itesdk_output2.smt2
@@ -0,0 +1,30 @@
+( set-logic QF_ALL_SUPPORTED)
+( set-info :source | SMT-COMP'06 organizers |)
+( set-info :smt-lib-version 2.0)
+( set-info :category "check")
+( set-info :status sat)
+( declare-fun x1 () Bool)
+( declare-fun x2 () Real)
+( declare-fun x3 () Real)
+( declare-fun x4 () Bool)
+( declare-fun x5 () Real)
+( declare-fun x6 () Real)
+( declare-fun x7 () Real)
+( declare-fun x8 () Real)
+( declare-fun bo1 () Bool)
+( declare-fun bo2 () Bool)
+( declare-fun bo3 () Bool)
+( declare-fun r1 () Real)
+( declare-fun r2 () Real)
+( declare-fun r3 () Real)
+( define-fun myBoolIte ( ( a Real) ( b Bool) ( c Bool)) Bool
+  ( ite ( > a 0.0) b c))
+( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real
+  ( ite a1 b1 c1))
+( declare-fun f ( Real Bool) Real)
+( declare-fun fRealRealReal ( Real Real) Real)
+( declare-fun fRealReal ( Real) Real)
+( declare-fun fReal () Real)
+( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/hung13sdk_output1.smt2 b/test/regress/regress0/hung13sdk_output1.smt2
new file mode 100644
index 000000000..bf3ab9a26
--- /dev/null
+++ b/test/regress/regress0/hung13sdk_output1.smt2
@@ -0,0 +1,14 @@
+( set-logic QF_ALL_SUPPORTED)
+( set-info :source | SMT-COMP'06 organizers |)
+( set-info :smt-lib-version 2.0)
+( set-info :category "check")
+( set-info :status sat)
+( declare-fun x1 () Bool)
+( declare-fun x2 () Real)
+( declare-fun x3 () Real)
+( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real
+  ( ite a1 b1 c1))
+( declare-fun fReal () Real)
+( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/hung13sdk_output2.smt2 b/test/regress/regress0/hung13sdk_output2.smt2
new file mode 100644
index 000000000..bf3ab9a26
--- /dev/null
+++ b/test/regress/regress0/hung13sdk_output2.smt2
@@ -0,0 +1,14 @@
+( set-logic QF_ALL_SUPPORTED)
+( set-info :source | SMT-COMP'06 organizers |)
+( set-info :smt-lib-version 2.0)
+( set-info :category "check")
+( set-info :status sat)
+( declare-fun x1 () Bool)
+( declare-fun x2 () Real)
+( declare-fun x3 () Real)
+( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real
+  ( ite a1 b1 c1))
+( declare-fun fReal () Real)
+( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3))))
+(check-sat)
+(exit)
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 9333cdb8c..68c1e0677 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -121,12 +121,12 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
       error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
     fi
     benchmark=$tmpbenchmark
-  elif grep '^ *(set-info  *:status  *sat' "$benchmark" &>/dev/null; then
+  elif grep '^ *( *set-info  *:status  *sat' "$benchmark" &>/dev/null; then
     expected_proof=
     expected_output=sat
     expected_exit_status=10
     command_line=
-  elif grep '^ *(set-info  *:status  *unsat' "$benchmark" &>/dev/null; then
+  elif grep '^ *( *set-info  *:status  *unsat' "$benchmark" &>/dev/null; then
     expected_proof=
     expected_output=unsat
     expected_exit_status=20