Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.

7 files changed, 97 insertions, 1228 deletions

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index bcacd4bd4..442355580 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -38,824 +38,5 @@ 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_varCache(smt.d_userContext),
-  d_termCache(smt.d_userContext),
-  d_typeCache(),
-  d_datatypeCache(),
-  d_datatypeReverseCache() {
-
-  // 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:
-  case kind::AND:
-  case kind::IFF:
-  case kind::IMPLIES:
-  case kind::OR:
-  case kind::XOR:
-  case kind::FORALL:
-  case kind::EXISTS:
-  case kind::REWRITE_RULE:
-  case kind::RR_REWRITE:
-  case kind::RR_DEDUCTION:
-  case kind::RR_REDUCTION:
-  case kind::INST_PATTERN:
-    return true;
-
-  case kind::ITE:
-    if(i == 0) {
-      return true;
-    }
-    return top.getType().isBoolean();
-
-  default:
-    return false;
-  }
-}
-
-// This function rewrites "in" as an "as"---this is actually expected
-// to be for model-substitution, so the "in" is a Boolean-term-converted
-// node, and "as" is the original.  See how it's used in function
-// handling, below.
-//
-// Note this isn't the case any longer, and parts of what's below have
-// been repurposed for *forward* conversion, meaning this works in either
-// direction.
-Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, bool >& processing) throw() {
-  Debug("boolean-terms2") << "Rewrite as " << in << " " << as << std::endl;
-  if(in.getType() == as) {
-    return in;
-  }
-  if(in.getType().isBoolean()) {
-    Assert(d_tt.getType() == as);
-    return NodeManager::currentNM()->mkNode(kind::ITE, in, d_tt, d_ff);
-  }
-  if(as.isBoolean() && in.getType().isBitVector() && in.getType().getBitVectorSize() == 1) {
-    return NodeManager::currentNM()->mkNode(kind::EQUAL, NodeManager::currentNM()->mkConst(BitVector(1u, 1u)), in);
-  }
-  TypeNode in_t = in.getType();
-  if( processing.find( in_t )==processing.end() ){
-    processing[in_t] = true;
-    if(in.getType().isParametricDatatype() &&
-      in.getType().isInstantiatedDatatype()) {
-      // We have something here like (Pair Bool Bool)---need to dig inside
-      // and make it (Pair BV1 BV1)
-      Assert(as.isParametricDatatype() && as.isInstantiatedDatatype());
-      const Datatype* dt2 = &as[0].getDatatype();
-      std::vector<TypeNode> fromParams, toParams;
-      for(unsigned i = 0; i < dt2->getNumParameters(); ++i) {
-        fromParams.push_back(TypeNode::fromType(dt2->getParameter(i)));
-        toParams.push_back(as[i + 1]);
-      }
-      const Datatype* dt1;
-      if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) {
-        dt1 = d_datatypeCache[dt2];
-      } else {
-        dt1 = d_datatypeReverseCache[dt2];
-      }
-      Assert(dt1 != NULL, "expected datatype in cache");
-      Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes");
-      Node out;
-      for(size_t i = 0; i < dt1->getNumConstructors(); ++i) {
-        DatatypeConstructor ctor = (*dt1)[i];
-        NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
-        appctorb << (*dt2)[i].getConstructor();
-        for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
-          TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType());
-          asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end());
-          appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType, processing);
-        }
-        Node appctor = appctorb;
-        if(i == 0) {
-          out = appctor;
-        } else {
-          Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out);
-          out = newOut;
-        }
-      }
-      processing.erase( in_t );
-      return out;
-    }
-    if(in.getType().isDatatype()) {
-      if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
-        processing.erase( in_t );
-        return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in);
-      }
-      Assert(as.isDatatype());
-      const Datatype* dt2 = &as.getDatatype();
-      const Datatype* dt1;
-      if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) {
-        dt1 = d_datatypeCache[dt2];
-      } else {
-        dt1 = d_datatypeReverseCache[dt2];
-      }
-      Assert(dt1 != NULL, "expected datatype in cache");
-      Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes");
-      Node out;
-      for(size_t i = 0; i < dt1->getNumConstructors(); ++i) {
-        DatatypeConstructor ctor = (*dt1)[i];
-        NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
-        appctorb << (*dt2)[i].getConstructor();
-        for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
-          appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()), processing);
-        }
-        Node appctor = appctorb;
-        if(i == 0) {
-          out = appctor;
-        } else {
-          Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out);
-          out = newOut;
-        }
-      }
-      processing.erase( in_t );
-      return out;
-    }
-    if(in.getType().isArray()) {
-      // convert in to in'
-      // e.g. in : (Array Int Bool)
-      // for in' : (Array Int (_ BitVec 1))
-      // then subs  in  |=>  \array_lambda ( \lambda (x:Int) . [convert (read a' x) x]
-      Assert(as.isArray());
-      Assert(as.getArrayIndexType() == in.getType().getArrayIndexType());
-      Assert(as.getArrayConstituentType() != in.getType().getArrayConstituentType());
-      Node x = NodeManager::currentNM()->mkBoundVar(as.getArrayIndexType());
-      Node boundvars = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, x);
-      Node sel = NodeManager::currentNM()->mkNode(kind::SELECT, in, x);
-      Node selprime = rewriteAs(sel, as.getArrayConstituentType(), processing);
-      Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundvars, selprime);
-      Node out = NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA, lam);
-      Assert(out.getType() == as);
-      processing.erase( in_t );
-      return out;
-    }
-    Unhandled(in);
-  }else{
-    Message() << "Type " << in_t << " involving Boolean sort is not supported." << std::endl;
-    exit( 0 );
-  }
-}
-
-const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw() {
-  const Datatype*& out = d_datatypeCache[&dt];
-  if(out != NULL) {
-    return *out;
-  }
-
-  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) {
-      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(), false));
-        } else {
-          newDtVector.push_back(Datatype(dt.getName() + "'", false));
-        }
-        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) {
-            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);
-              }
-            }
-          }
-          newDt.addConstructor(ctor);
-        }
-        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;
-          const DatatypeConstructor *newC;
-          Node::fromExpr((*(newC = &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_varCache[Node::fromExpr((*c).getConstructor())] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
-          d_varCache[Node::fromExpr((*c).getTester())] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
-          for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
-            Node::fromExpr((*newC)[(*a).getName() + "'"].getSelector()).setAttribute(BooleanTermAttr(), Node::fromExpr((*a).getSelector()));// other attr?
-            d_varCache[Node::fromExpr((*a).getSelector())] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
-          }
-        }
-        out = &newD;
-        d_datatypeReverseCache[&newD] = &dt;
-        return newD;
-      }
-    }
-  }
-
-  // this is identity; don't need the reverse cache
-  out = &dt;
-  return dt;
-
-}/* 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].getDatatype() : type.getDatatype();
-    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.isSort() && 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) {
-  if(vars.empty()) {
-    return;
-  }
-  const pair<TNode, bool> cacheKey(n, boolParent);
-  if(alreadySeen.find(cacheKey) != alreadySeen.end()) {
-    return;
-  }
-  alreadySeen.insert(cacheKey);
-
-  if(n.isVar() && vars.find(n) != vars.end() && !boolParent) {
-    vars.erase(n);
-    output.insert(n);
-    if(vars.empty()) {
-      return;
-    }
-  }
-  for(size_t i = 0; i < n.getNumChildren(); ++i) {
-    collectVarsInTermContext(n[i], vars, output, isBoolean(n, i), alreadySeen);
-    if(vars.empty()) {
-      return;
-    }
-  }
-}
-
-Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw() {
-
-  stack< triple<TNode, theory::TheoryId, bool> > worklist;
-  worklist.push(triple<TNode, theory::TheoryId, bool>(top, parentTheory, false));
-  stack< NodeBuilder<> > result;
-  //AJR: not sure what the significance of "TUPLE" is here, seems to be a placeholder.  Since TUPLE is no longer a kind, replacing this with "AND".
-  //result.push(NodeBuilder<>(kind::TUPLE));
-  result.push(NodeBuilder<>(kind::AND));
-
-  NodeManager* nm = NodeManager::currentNM();
-
-  while(!worklist.empty()) {
-    top = worklist.top().first;
-    parentTheory = worklist.top().second;
-    bool& childrenPushed = worklist.top().third;
-
-    Kind k = top.getKind();
-    kind::MetaKind mk = top.getMetaKind();
-
-    // 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;
-      }
-    }
-
-    if(!childrenPushed) {
-      Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - parentTheory=" << parentTheory << endl;
-
-      BooleanTermVarCache::iterator i = d_varCache.find(top);
-      if(i != d_varCache.end()) {
-        result.top() << ((*i).second.isNull() ? Node(top) : (*i).second);
-        worklist.pop();
-        goto next_worklist;
-      }
-      BooleanTermCache::iterator j = d_termCache.find(pair<Node, theory::TheoryId>(top, parentTheory));
-      if(j != d_termCache.end()) {
-        result.top() << ((*j).second.isNull() ? Node(top) : (*j).second);
-        worklist.pop();
-        goto next_worklist;
-      }
-
-      if(quantBoolVars.find(top) != quantBoolVars.end()) {
-        // this Bool variable is quantified over and we're changing it to a BitVector var
-        if(parentTheory == theory::THEORY_BOOL) {
-          result.top() << quantBoolVars[top].eqNode(d_tt);
-        } else {
-          result.top() << quantBoolVars[top];
-        }
-        worklist.pop();
-        goto next_worklist;
-      }
-
-      if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean() && top.getKind()!=kind::SEP_STAR && top.getKind()!=kind::SEP_WAND) {
-        // still need to rewrite e.g. function applications over boolean
-        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;
-        result.top() << n;
-        worklist.pop();
-        goto next_worklist;
-      }
-
-      if(mk == kind::metakind::CONSTANT) {
-        if(k == kind::STORE_ALL) {
-          const ArrayStoreAll& asa = top.getConst<ArrayStoreAll>();
-          ArrayType arrType = asa.getType();
-          TypeNode indexType = TypeNode::fromType(arrType.getIndexType());
-          Type constituentType = arrType.getConstituentType();
-          if(constituentType.isBoolean()) {
-            // we have store_all(true) or store_all(false)
-            // just turn it into store_all(1) or store_all(0)
-            if(indexType.isBoolean()) {
-              // change index type to BV(1) also
-              indexType = d_tt.getType();
-            }
-            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;
-            result.top() << n;
-            worklist.pop();
-            goto next_worklist;
-          }
-          if(indexType.isBoolean()) {
-            // must change index type to BV(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;
-            result.top() << n;
-            worklist.pop();
-            goto next_worklist;
-          }
-        }
-        result.top() << top;
-        worklist.pop();
-        goto next_worklist;
-      } else if(mk == kind::metakind::VARIABLE) {
-        TypeNode t = top.getType();
-        if(t.isFunction()) {
-          for(unsigned i = 0; i < t.getNumChildren(); ++i) {
-            TypeNode newType = convertType(t[i], false);
-            // is this the return type?  (allowed to be Bool)
-            bool returnType = (i == t.getNumChildren() - 1);
-            if(newType != t[i] && (!t[i].isBoolean() || !returnType)) {
-              vector<TypeNode> argTypes = t.getArgTypes();
-              for(unsigned j = 0; j < argTypes.size(); ++j) {
-                argTypes[j] = convertType(argTypes[j], false);
-              }
-              TypeNode rangeType = t.getRangeType();
-              if(!rangeType.isBoolean()) {
-                rangeType = convertType(rangeType, false);
-              }
-              TypeNode newType = nm->mkFunctionType(argTypes, rangeType);
-              Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "__boolterm__",
-                                    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);
-              NodeBuilder<> boundVarsBuilder(kind::BOUND_VAR_LIST);
-              NodeBuilder<> bodyBuilder(kind::APPLY_UF);
-              bodyBuilder << n;
-              for(unsigned j = 0; j < t.getNumChildren() - 1; ++j) {
-                Node var = nm->mkBoundVar(t[j]);
-                boundVarsBuilder << var;
-                if(t[j] != argTypes[j]) {
-                  std::map< TypeNode, bool > processing;
-                  bodyBuilder << rewriteAs(var, argTypes[j], processing);
-                } else {
-                  bodyBuilder << var;
-                }
-              }
-              Node boundVars = boundVarsBuilder;
-              Node body = bodyBuilder;
-              if(t.getRangeType() != rangeType) {
-                std::map< TypeNode, bool > processing;
-                Node convbody = rewriteAs(body, t.getRangeType(), processing);
-                body = convbody;
-              }
-              Node lam = nm->mkNode(kind::LAMBDA, boundVars, body);
-              Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl;
-              d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam);
-              d_varCache[top] = n;
-              result.top() << n;
-              worklist.pop();
-              goto next_worklist;
-            }
-          }
-        } else if(t.isArray()) {
-          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()) + "'",
-                                  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_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()), (*TypeEnumerator(n_ff.getType())).toExpr()));
-            Node repl = nm->mkNode(kind::STORE,
-                                   nm->mkNode(kind::STORE, base, nm->mkConst(true),
-                                              n_tt),
-                                   nm->mkConst(false), n_ff);
-            Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl;
-            d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl);
-            d_varCache[top] = n;
-            result.top() << n;
-            worklist.pop();
-            goto next_worklist;
-          } else if(indexType == t.getArrayIndexType() && constituentType != t.getArrayConstituentType()) {
-            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_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
-            d_varCache[top] = n;
-            result.top() << n;
-            worklist.pop();
-            goto next_worklist;
-          } else if(indexType != t.getArrayIndexType() && constituentType != t.getArrayConstituentType()) {
-            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;
-            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_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_varCache[top] = n;
-            result.top() << n;
-            worklist.pop();
-            goto next_worklist;
-          }
-          d_varCache[top] = Node::null();
-          result.top() << top;
-          worklist.pop();
-          goto next_worklist;
-        } 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_varCache.find(top) == d_varCache.end(),
-                   "Node `%s' already in cache ?!", top.toString().c_str());
-            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);
-            d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
-            Debug("boolean-terms") << "constructed: " << n << " of type " << newT << endl;
-            d_varCache[top] = n;
-            result.top() << n;
-            worklist.pop();
-            goto next_worklist;
-          } else {
-            d_varCache[top] = Node::null();
-            result.top() << top;
-            worklist.pop();
-            goto next_worklist;
-          }
-        } else if(t.isConstructor()) {
-          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].getDatatype() :
-            t[t.getNumChildren() - 1][0].getDatatype();
-          TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
-          const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getDatatype();
-          if(dt != dt2) {
-            Assert(d_varCache.find(top) != d_varCache.end(),
-                   "constructor `%s' not in cache", top.toString().c_str());
-            result.top() << d_varCache[top].get();
-            worklist.pop();
-            goto next_worklist;
-          }
-          d_varCache[top] = Node::null();
-          result.top() << top;
-          worklist.pop();
-          goto next_worklist;
-        } else if(t.isTester() || t.isSelector()) {
-          Assert(parentTheory != theory::THEORY_BOOL);
-          const Datatype& dt = t[0].getKind() == kind::DATATYPE_TYPE ?
-            t[0].getDatatype() :
-            t[0][0].getDatatype();
-          TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
-          const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getDatatype();
-          if(dt != dt2) {
-            Assert(d_varCache.find(top) != d_varCache.end(),
-                   "tester or selector `%s' not in cache", top.toString().c_str());
-            result.top() << d_varCache[top].get();
-            worklist.pop();
-            goto next_worklist;
-          } else {
-            d_varCache[top] = Node::null();
-            result.top() << top;
-            worklist.pop();
-            goto next_worklist;
-          }
-        } else if(!t.isSort() && t.getNumChildren() > 0) {
-          if( t.getKind()!=kind::SEP_STAR && t.getKind()!=kind::SEP_WAND ){
-            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, 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_varCache[top] = n;
-                result.top() << n;
-                worklist.pop();
-                goto next_worklist;
-              }
-            }
-          }
-        }
-        result.top() << top;
-        worklist.pop();
-        goto next_worklist;
-      }
-      switch(k) {
-      //case kind::INST_ATTRIBUTE:
-      case kind::BOUND_VAR_LIST:
-        result.top() << top;
-        worklist.pop();
-        goto next_worklist;
-
-      case kind::REWRITE_RULE:
-      case kind::RR_REWRITE:
-      case kind::RR_DEDUCTION:
-      case kind::RR_REDUCTION:
-      case kind::SEP_STAR:
-      case kind::SEP_WAND:
-        // not yet supported
-        result.top() << top;
-        worklist.pop();
-        goto next_worklist;
-
-      case kind::FORALL:
-      case kind::EXISTS: {
-        Debug("bt") << "looking at quantifier -> " << top << endl;
-        set<TNode> ourVars;
-        set<TNode> output;
-        for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) {
-          if((*i).getType().isBoolean()) {
-            ourVars.insert(*i);
-          } else if(convertType((*i).getType(), false) != (*i).getType()) {
-            output.insert(*i);
-          }
-        }
-        if(ourVars.empty() && output.empty()) {
-          // Simple case, quantifier doesn't quantify over Boolean vars,
-          // no special handling needed for quantifier.  Fall through.
-          Debug("bt") << "- quantifier simple case (1), no Boolean vars bound" << endl;
-        } else {
-          hash_set< pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> > alreadySeen;
-          collectVarsInTermContext(top[1], ourVars, output, true, alreadySeen);
-          if(output.empty()) {
-            // Simple case, quantifier quantifies over Boolean vars, but they
-            // don't occur in term context.  Fall through.
-            Debug("bt") << "- quantifier simple case (2), Boolean vars bound but not used in term context" << endl;
-          } else {
-            Debug("bt") << "- quantifier case (3), Boolean vars bound and used in term context" << endl;
-            // We have Boolean vars appearing in term context.  Convert their
-            // types in the quantifier.
-            for(set<TNode>::const_iterator i = output.begin(); i != output.end(); ++i) {
-              Node newVar = nm->mkBoundVar((*i).toString(), convertType((*i).getType(), false));
-              Assert(quantBoolVars.find(*i) == quantBoolVars.end(), "bad quantifier: shares a bound var with another quantifier (don't do that!)");
-              quantBoolVars[*i] = newVar;
-            }
-            vector<TNode> boundVars;
-            for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) {
-              map<TNode, Node>::const_iterator j = quantBoolVars.find(*i);
-              if(j == quantBoolVars.end()) {
-                boundVars.push_back(*i);
-              } else {
-                boundVars.push_back((*j).second);
-              }
-            }
-            Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, boundVars);
-            Node body = rewriteBooleanTermsRec(top[1], theory::THEORY_BOOL, quantBoolVars);
-            Node quant;
-            if( top.getNumChildren()==3 ){
-              Node ipl = rewriteBooleanTermsRec(top[2], theory::THEORY_BOOL, quantBoolVars);
-              quant = nm->mkNode(top.getKind(), boundVarList, body, ipl );
-            }else{
-              quant = nm->mkNode(top.getKind(), boundVarList, body);
-            }
-            Debug("bt") << "rewrote quantifier to -> " << quant << endl;
-            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);
-            result.top() << quant;
-            worklist.pop();
-            goto next_worklist;
-          }
-        }
-        /* intentional fall-through for some cases above */
-      }
-
-      default:
-        result.push(NodeBuilder<>(k));
-        Debug("bt") << "looking at: " << top << endl;
-        // rewrite the operator, as necessary
-        if(mk == kind::metakind::PARAMETERIZED) {
-          if(k == kind::APPLY_TYPE_ASCRIPTION) {
-            Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType()));
-            result.top() << 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_UPDATE &&
-                    k != kind::RECORD_UPDATE &&
-                    k != kind::DIVISIBLE &&
-        // Theory parametric functions go here
-        k != kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR &&
-        k != kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT &&
-        k != kind::FLOATINGPOINT_TO_FP_REAL &&
-        k != kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR &&
-        k != kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR &&
-        k != kind::FLOATINGPOINT_TO_UBV &&
-        k != kind::FLOATINGPOINT_TO_SBV &&
-        k != kind::FLOATINGPOINT_TO_REAL
-        ) {
-            Debug("bt") << "rewriting: " << top.getOperator() << endl;
-            result.top() << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars);
-            Debug("bt") << "got: " << result.top().getOperator() << endl;
-          } else {
-            result.top() << top.getOperator();
-          }
-        }
-        // push children
-        for(int i = top.getNumChildren() - 1; i >= 0; --i) {
-          Debug("bt") << "rewriting: " << top[i] << endl;
-          worklist.push(triple<TNode, theory::TheoryId, bool>(top[i], top.getKind() == kind::CHAIN ? parentTheory : ((isBoolean(top, i) || top.getKind()==kind::INST_ATTRIBUTE) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN)), false));
-          //b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? , quantBoolVars);
-          //Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl;
-        }
-        childrenPushed = true;
-      }
-    } else {
-      Node n = result.top();
-      result.pop();
-      Debug("boolean-terms") << "constructed: " << n << " of type " << n.getType() << endl;
-      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_termCache[make_pair(top, parentTheory)] = n;
-      result.top() << n;
-      worklist.pop();
-      goto next_worklist;
-    }
-
-  next_worklist:
-    ;
-  }
-
-  Assert(worklist.size() == 0);
-  Assert(result.size() == 1);
-  Node retval = result.top()[0];
-  result.top().clear();
-  result.pop();
-  return retval;
-
-}/* BooleanTermConverter::rewriteBooleanTermsRec() */
-
 }/* CVC4::smt namespace */
 }/* CVC4 namespace */
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h
index 0a63f7fd8..0fb82aafe 100644
--- a/src/smt/boolean_terms.h
+++ b/src/smt/boolean_terms.h
@@ -28,84 +28,5 @@
 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 variable cache */
-  typedef context::CDHashMap<Node, Node, NodeHashFunction> BooleanTermVarCache;
-
-  /** The type of the Boolean term conversion cache */
-  typedef context::CDHashMap< std::pair<Node, theory::TheoryId>, Node,
-                              PairHashFunction< Node, bool,
-                                                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 variable conversion */
-  BooleanTermVarCache d_varCache;
-  /** The cache used during Boolean term conversion */
-  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;
-  /** A (reverse) cache for Boolean term datatype conversion */
-  BooleanTermDatatypeCache d_datatypeReverseCache;
-
-  Node rewriteAs(TNode in, TypeNode as, std::map< TypeNode, bool >& processing) throw();
-
-  /**
-   * Scan a datatype for and convert as necessary.
-   */
-  const Datatype& convertDatatype(const Datatype& dt) throw();
-
-  /**
-   * Convert a type.
-   */
-  TypeNode convertType(TypeNode type, bool datatypesContext);
-
-  Node rewriteBooleanTermsRec(TNode n, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw();
-
-public:
-
-  /**
-   * Construct a Boolean-term converter associated to the given
-   * SmtEngine.
-   */
-  BooleanTermConverter(SmtEngine& smt);
-
-  /**
-   * 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, bool dtParent = false) throw() {
-    std::map<TNode, Node> quantBoolVars;
-    Assert(!(boolParent && dtParent));
-    return rewriteBooleanTermsRec(n, boolParent ? theory::THEORY_BOOL : (dtParent ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), quantBoolVars);
-  }
-
-};/* class BooleanTermConverter */
-
 }/* CVC4::smt namespace */
 }/* CVC4 namespace */
diff --git a/src/smt/ite_removal.cpp b/src/smt/ite_removal.cpp
index d31d54121..0202a5a2d 100644
--- a/src/smt/ite_removal.cpp
+++ b/src/smt/ite_removal.cpp
@@ -25,36 +25,36 @@ using namespace std;
 
 namespace CVC4 {
 
-RemoveITE::RemoveITE(context::UserContext* u)
+RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u)
   : d_iteCache(u)
 {
   d_containsVisitor = new theory::ContainsTermITEVisitor();
 }
 
-RemoveITE::~RemoveITE(){
+RemoveTermFormulas::~RemoveTermFormulas(){
   delete d_containsVisitor;
 }
 
-void RemoveITE::garbageCollect(){
+void RemoveTermFormulas::garbageCollect(){
   d_containsVisitor->garbageCollect();
 }
 
-theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() {
+theory::ContainsTermITEVisitor* RemoveTermFormulas::getContainsVisitor() {
   return d_containsVisitor;
 }
 
-size_t RemoveITE::collectedCacheSizes() const{
+size_t RemoveTermFormulas::collectedCacheSizes() const{
   return d_containsVisitor->cache_size() + d_iteCache.size();
 }
 
-void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
+void RemoveTermFormulas::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
 {
   size_t n = output.size();
   for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
     // Do this in two steps to avoid Node problems(?)
     // Appears related to bug 512, splitting this into two lines
     // fixes the bug on clang on Mac OS
-    Node itesRemoved = run(output[i], output, iteSkolemMap, false);
+    Node itesRemoved = run(output[i], output, iteSkolemMap, false, false);
     // In some calling contexts, not necessary to report dependence information.
     if (reportDeps &&
         (options::unsatCores() || options::fewerPreprocessingHoles())) {
@@ -69,22 +69,27 @@ void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool
   }
 }
 
-bool RemoveITE::containsTermITE(TNode e) const {
+bool RemoveTermFormulas::containsTermITE(TNode e) const {
   return d_containsVisitor->containsTermITE(e);
 }
 
-Node RemoveITE::run(TNode node, std::vector<Node>& output,
-                    IteSkolemMap& iteSkolemMap, bool inQuant) {
+Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
+                    IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm) {
   // Current node
-  Debug("ite") << "removeITEs(" << node << ")" << endl;
-
-  if(node.isVar() || node.isConst() ||
-     (options::biasedITERemoval() && !containsTermITE(node))){
+  Debug("ite") << "removeITEs(" << node << ")" << " " << inQuant << " " << inTerm << endl;
+
+  //if(node.isVar() || node.isConst()){
+  //   (options::biasedITERemoval() && !containsTermITE(node))){
+  //if(node.isVar()){
+  //  return Node(node);
+  //}
+  if( node.getKind()==kind::INST_PATTERN_LIST ){
     return Node(node);
   }
 
   // The result may be cached already
-  std::pair<Node, bool> cacheKey(node, inQuant);
+  int cv = cacheVal( inQuant, inTerm );
+  std::pair<Node, int> cacheKey(node, cv);
   NodeManager *nodeManager = NodeManager::currentNM();
   ITECache::const_iterator i = d_iteCache.find(cacheKey);
   if(i != d_iteCache.end()) {
@@ -93,14 +98,10 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
     return cached.isNull() ? Node(node) : cached;
   }
 
-  // Remember that we're inside a quantifier
-  if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
-    inQuant = true;
-  }
 
-  // If an ITE replace it
+  // If an ITE, replace it
+  TypeNode nodeType = node.getType();
   if(node.getKind() == kind::ITE) {
-    TypeNode nodeType = node.getType();
     if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) {
       Node skolem;
       // Make the skolem to represent the ITE
@@ -116,7 +117,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
       d_iteCache.insert(cacheKey, skolem);
 
       // Remove ITEs from the new assertion, rewrite it and push it to the output
-      newAssertion = run(newAssertion, output, iteSkolemMap, inQuant);
+      newAssertion = run(newAssertion, output, iteSkolemMap, false, false);
 
       iteSkolemMap[skolem] = output.size();
       output.push_back(newAssertion);
@@ -125,6 +126,40 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
       return skolem;
     }
   }
+  //if a non-variable Boolean term, replace it
+  if(node.getKind()!=kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() && inTerm && !inQuant ){//(!inQuant || !node.hasBoundVar())){
+    Node skolem;
+    // Make the skolem to represent the Boolean term
+    //skolem = nodeManager->mkSkolem("termBT", nodeType, "a variable introduced due to Boolean term removal");
+    skolem = nodeManager->mkBooleanTermVariable();
+
+    // The new assertion
+    Node newAssertion = skolem.eqNode( node );
+    Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
+
+    // Attach the skolem
+    d_iteCache.insert(cacheKey, skolem);
+
+    // Remove ITEs from the new assertion, rewrite it and push it to the output
+    newAssertion = run(newAssertion, output, iteSkolemMap, false, false);
+
+    iteSkolemMap[skolem] = output.size();
+    output.push_back(newAssertion);
+
+    // The representation is now the skolem
+    return skolem;
+  }
+  
+  if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+    // Remember if we're inside a quantifier
+    inQuant = true;
+  }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && 
+            node.getKind()!=kind::EQUAL && node.getKind()!=kind::SEP_STAR && 
+            node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL ){
+    // Remember if we're inside a term
+    Debug("ite") << "In term because of " << node << " " << node.getKind() << std::endl;
+    inTerm = true;
+  }
 
   // If not an ITE, go deep
   vector<Node> newChildren;
@@ -134,7 +169,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
   }
   // Remove the ITEs from the children
   for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
-    Node newChild = run(*it, output, iteSkolemMap, inQuant);
+    Node newChild = run(*it, output, iteSkolemMap, inQuant, inTerm);
     somethingChanged |= (newChild != *it);
     newChildren.push_back(newChild);
   }
@@ -150,24 +185,32 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
   }
 }
 
-Node RemoveITE::replace(TNode node, bool inQuant) const {
-  if(node.isVar() || node.isConst() ||
-     (options::biasedITERemoval() && !containsTermITE(node))){
+Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const {
+  //if(node.isVar() || node.isConst()){
+  //   (options::biasedITERemoval() && !containsTermITE(node))){
+  //if(node.isVar()){
+  //  return Node(node);
+  //}
+  if( node.getKind()==kind::INST_PATTERN_LIST ){
     return Node(node);
   }
 
   // Check the cache
   NodeManager *nodeManager = NodeManager::currentNM();
-  ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant));
+  int cv = cacheVal( inQuant, inTerm );
+  ITECache::const_iterator i = d_iteCache.find(make_pair(node, cv));
   if(i != d_iteCache.end()) {
     Node cached = (*i).second;
     return cached.isNull() ? Node(node) : cached;
   }
 
-  // Remember that we're inside a quantifier
   if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+    // Remember if we're inside a quantifier
     inQuant = true;
-  }
+  }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && node.getKind()!=kind::EQUAL ){
+    // Remember if we're inside a term
+    inTerm = true;
+  }  
 
   vector<Node> newChildren;
   bool somethingChanged = false;
@@ -176,7 +219,7 @@ Node RemoveITE::replace(TNode node, bool inQuant) const {
   }
   // Replace in children
   for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
-    Node newChild = replace(*it, inQuant);
+    Node newChild = replace(*it, inQuant, inTerm);
     somethingChanged |= (newChild != *it);
     newChildren.push_back(newChild);
   }
diff --git a/src/smt/ite_removal.h b/src/smt/ite_removal.h
index c0a46c316..e629c93d7 100644
--- a/src/smt/ite_removal.h
+++ b/src/smt/ite_removal.h
@@ -35,15 +35,15 @@ namespace theory {
 
 typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
 
-class RemoveITE {
-  typedef context::CDInsertHashMap< std::pair<Node, bool>, Node, PairHashFunction<Node, bool, NodeHashFunction, BoolHashFunction> > ITECache;
+class RemoveTermFormulas {
+  typedef context::CDInsertHashMap< std::pair<Node, int>, Node, PairHashFunction<Node, int, NodeHashFunction, BoolHashFunction> > ITECache;
   ITECache d_iteCache;
 
-
+  static inline int cacheVal( bool inQuant, bool inTerm ) { return (inQuant ? 1 : 0) + 2*(inTerm ? 1 : 0); }
 public:
 
-  RemoveITE(context::UserContext* u);
-  ~RemoveITE();
+  RemoveTermFormulas(context::UserContext* u);
+  ~RemoveTermFormulas();
 
   /**
    * Removes the ITE nodes by introducing skolem variables. All
@@ -65,13 +65,13 @@ public:
    * ite created in conjunction with that skolem variable.
    */
   Node run(TNode node, std::vector<Node>& additionalAssertions,
-           IteSkolemMap& iteSkolemMap, bool inQuant);
+           IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm);
 
   /**
    * Substitute under node using pre-existing cache.  Do not remove
    * any ITEs not seen during previous runs.
    */
-  Node replace(TNode node, bool inQuant = false) const;
+  Node replace(TNode node, bool inQuant = false, bool inTerm = false) const;
 
   /** Returns true if e contains a term ite. */
   bool containsTermITE(TNode e) const;
@@ -82,7 +82,7 @@ public:
   /** Garbage collects non-context dependent data-structures. */
   void garbageCollect();
 
-  /** Return the RemoveITE's containsVisitor. */
+  /** Return the RemoveTermFormulas's containsVisitor. */
   theory::ContainsTermITEVisitor* getContainsVisitor();
 
 private:
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index 5988d81f9..0076b9de9 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -25,209 +25,6 @@ using namespace std;
 namespace CVC4 {
 namespace 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.getKind() == kind::LAMBDA) {
-    Assert(asType.isFunction());
-    Node rhs = rewriteAs(n[1], asType[1]);
-    Node out = NodeManager::currentNM()->mkNode(kind::LAMBDA, n[0], rhs);
-    Debug("boolean-terms") << "rewrote " << n << " as " << out << std::endl;
-    Debug("boolean-terms") << "need type " << asType << endl;
-    // Assert(out.getType() == asType);
-    return out;
-  }
-  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);
-    }
-  }
-  if(n.getType().isBoolean()) {
-    bool tf = n.getConst<bool>();
-    if(asType.isBitVector(1u)) {
-      return NodeManager::currentNM()->mkConst(BitVector(1u, tf ? 1u : 0u));
-    }
-    if(asType.isDatatype() && asType.hasAttribute(BooleanTermAttr())) {
-      const Datatype& asDatatype = asType.getDatatype();
-      return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, (tf ? asDatatype[0] : asDatatype[1]).getConstructor());
-    }
-  }
-  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( n.getType().isSet() ){
-    if( n.getKind()==kind::UNION ){
-      std::vector< Node > children;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        children.push_back( rewriteAs( n[i], asType ) );
-      }
-      return NodeManager::currentNM()->mkNode(kind::UNION,children);
-    }
-  }
-  if(n.getType().isParametricDatatype() &&
-     n.getType().isInstantiatedDatatype() &&
-     asType.isParametricDatatype() &&
-     asType.isInstantiatedDatatype() &&
-     n.getType()[0] == asType[0]) {
-    // Here, we're doing something like rewriting a (Pair BV1 BV1) as a
-    // (Pair Bool Bool).
-    const Datatype* dt2 = &asType[0].getDatatype();
-    std::vector<TypeNode> fromParams, toParams;
-    for(unsigned i = 0; i < dt2->getNumParameters(); ++i) {
-      fromParams.push_back(TypeNode::fromType(dt2->getParameter(i)));
-      toParams.push_back(asType[i + 1]);
-    }
-    Assert(dt2 == &Datatype::datatypeOf(n.getOperator().toExpr()));
-    size_t ctor_ix = Datatype::indexOf(n.getOperator().toExpr());
-    NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
-    appctorb << (*dt2)[ctor_ix].getConstructor();
-    for(size_t j = 0; j < n.getNumChildren(); ++j) {
-      TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[ctor_ix][j].getSelector().getType()).getRangeType());
-      asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end());
-      appctorb << rewriteAs(n[j], asType);
-    }
-    Node out = appctorb;
-    return out;
-  }
-  if(asType.getNumChildren() != n.getNumChildren() ||
-     n.getMetaKind() == kind::metakind::CONSTANT) {
-    return n;
-  }
-  NodeBuilder<> b(n.getKind());
-  if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
-    b << n.getOperator();
-  }
-  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 << endl;
-  Assert(!alreadyVisited(current, TNode::null()));
-  bool rewriteChildren = false;
-  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;
-    return;
-  //all kinds with children that can occur in nodes in a model go here
-  } else if(current.getKind() == kind::LAMBDA || current.getKind() == kind::SINGLETON || current.getKind() == kind::UNION || 
-            current.getKind()==kind::STORE || current.getKind()==kind::STORE_ALL || current.getKind()==kind::APPLY_CONSTRUCTOR ) {
-    rewriteChildren = true;
-  }
-  if( rewriteChildren ){
-    // rewrite based on children
-    bool self = true;
-    for(size_t i = 0; i < current.getNumChildren(); ++i) {
-      Assert(d_nodes.find(current[i]) != d_nodes.end());
-      if(!d_nodes[current[i]].isNull()) {
-        self = false;
-        break;
-      }
-    }
-    if(self) {
-      Debug("tuprec") << "returning self for kind " << current.getKind() << endl;
-      // rewrite to self
-      d_nodes[current] = Node::null();
-    } else {
-      // rewrite based on children
-      NodeBuilder<> nb(current.getKind());
-      if(current.getMetaKind() == kind::metakind::PARAMETERIZED) {
-        TNode op = current.getOperator();
-        Node realOp;
-        if(op.getAttribute(BooleanTermAttr(), realOp)) {
-          nb << realOp;
-        } else {
-          nb << op;
-        }
-      }
-      for(size_t i = 0; i < current.getNumChildren(); ++i) {
-        Assert(d_nodes.find(current[i]) != d_nodes.end());
-        TNode rw = d_nodes[current[i]];
-        if(rw.isNull()) {
-          rw = current[i];
-        }
-        nb << rw;
-      }
-      d_nodes[current] = nb;
-      Debug("tuprec") << "rewrote children for kind " << current.getKind() << " got " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
-    }
-  } else {
-    Debug("tuprec") << "returning self for kind " << current.getKind() << endl;
-    // rewrite to self
-    d_nodes[current] = Node::null();
-  }
-}/* ModelPostprocessor::visit() */
 
 } /* namespace smt */
 } /* namespace CVC4 */
diff --git a/src/smt/model_postprocessor.h b/src/smt/model_postprocessor.h
index d9e749677..a354315ef 100644
--- a/src/smt/model_postprocessor.h
+++ b/src/smt/model_postprocessor.h
@@ -24,28 +24,6 @@
 namespace CVC4 {
 namespace smt {
 
-class ModelPostprocessor {
-  std::hash_map<TNode, Node, TNodeHashFunction> d_nodes;
-
-public:
-  typedef Node return_type;
-
-  Node rewriteAs(TNode n, TypeNode asType);
-
-  bool alreadyVisited(TNode current, TNode parent) {
-    return d_nodes.find(current) != d_nodes.end();
-  }
-
-  void visit(TNode current, TNode parent);
-
-  void start(TNode n) { }
-
-  Node done(TNode n) {
-    Assert(alreadyVisited(n, TNode::null()));
-    TNode retval = d_nodes[n];
-    return retval.isNull() ? n : retval;
-  }
-};/* class ModelPostprocessor */
 
 }/* CVC4::smt namespace */
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e647c45d1..cefef9345 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -185,8 +185,6 @@ 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;
   /** time spent in miplib pass */
@@ -233,7 +231,6 @@ struct SmtEngineStatistics {
 
   SmtEngineStatistics() :
     d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
-    d_rewriteBooleanTermsTime("smt::SmtEngine::rewriteBooleanTermsTime"),
     d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
     d_miplibPassTime("smt::SmtEngine::miplibPassTime"),
     d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0),
@@ -258,7 +255,6 @@ struct SmtEngineStatistics {
  {
 
     smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
-    smtStatisticsRegistry()->registerStat(&d_rewriteBooleanTermsTime);
     smtStatisticsRegistry()->registerStat(&d_nonclausalSimplificationTime);
     smtStatisticsRegistry()->registerStat(&d_miplibPassTime);
     smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved);
@@ -284,7 +280,6 @@ struct SmtEngineStatistics {
 
   ~SmtEngineStatistics() {
     smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime);
-    smtStatisticsRegistry()->unregisterStat(&d_rewriteBooleanTermsTime);
     smtStatisticsRegistry()->unregisterStat(&d_nonclausalSimplificationTime);
     smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime);
     smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved);
@@ -510,9 +505,6 @@ 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;
   bool d_propagatorNeedsFinish;
@@ -567,7 +559,7 @@ public:
   IteSkolemMap d_iteSkolemMap;
 
   /** Instance of the ITE remover */
-  RemoveITE d_iteRemover;
+  RemoveTermFormulas d_iteRemover;
 
 private:
 
@@ -676,7 +668,6 @@ public:
     d_listenerRegistrations(new ListenerRegistrationList()),
     d_nonClausalLearnedLiterals(),
     d_realAssertionsEnd(0),
-    d_booleanTermConverter(NULL),
     d_propagator(d_nonClausalLearnedLiterals, true, true),
     d_propagatorNeedsFinish(false),
     d_assertions(),
@@ -756,10 +747,6 @@ public:
       d_propagator.finish();
       d_propagatorNeedsFinish = false;
     }
-    if(d_booleanTermConverter != NULL) {
-      delete d_booleanTermConverter;
-      d_booleanTermConverter = NULL;
-    }
     d_smt.d_nodeManager->unsubscribeEvents(this);
   }
 
@@ -859,11 +846,6 @@ public:
       throw(TypeCheckingException, LogicException, UnsafeInterruptException);
 
   /**
-   * Rewrite Boolean terms in a Node.
-   */
-  Node rewriteBooleanTerms(TNode n);
-
-  /**
    * Simplify node "in" by expanding definitions and applying any
    * substitutions learned from preprocessing.
    */
@@ -1447,6 +1429,15 @@ void SmtEngine::setDefaults() {
     d_logic = log;
     d_logic.lock();
   }
+  if(d_logic.isTheoryEnabled(THEORY_ARRAY) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_SETS)) {
+    if(!d_logic.isTheoryEnabled(THEORY_UF)) {
+      LogicInfo log(d_logic.getUnlockedCopy());
+      Trace("smt") << "because a theory that permits Boolean terms is enabled, also enabling UF" << endl;
+      log.enableTheory(THEORY_UF);
+      d_logic = log;
+      d_logic.lock();
+    }
+  }
 
   // by default, symmetry breaker is on only for QF_UF
   if(! options::ufSymmetryBreaker.wasSetByUser()) {
@@ -2918,7 +2909,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
     for (; pos != newSubstitutions.end(); ++pos) {
       // Add back this substitution as an assertion
       TNode lhs = (*pos).first, rhs = newSubstitutions.apply((*pos).second);
-      Node n = NodeManager::currentNM()->mkNode(lhs.getType().isBoolean() ? kind::IFF : kind::EQUAL, lhs, rhs);
+      Node n = NodeManager::currentNM()->mkNode(kind::EQUAL, lhs, rhs);
       substitutionsBuilder << n;
       Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl;
     }
@@ -3775,42 +3766,6 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node,
   return false;
 }
 
-Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) {
-  TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
-
-  spendResource(options::preprocessStep());
-
-  if(d_booleanTermConverter == NULL) {
-    // This needs to be initialized _after_ the whole SMT framework is in place, subscribed
-    // to ExprManager notifications, etc.  Otherwise we might miss the "BooleanTerm" datatype
-    // definition, and not dump it properly.
-    d_booleanTermConverter = new BooleanTermConverter(d_smt);
-  }
-  Node retval = d_booleanTermConverter->rewriteBooleanTerms(n);
-  if(retval != n) {
-    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_BV)) {
-        d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
-        d_smt.d_logic.enableTheory(THEORY_BV);
-        d_smt.d_logic.lock();
-      }
-      break;
-    case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
-      if(!d_smt.d_logic.isTheoryEnabled(THEORY_DATATYPES)) {
-        d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
-        d_smt.d_logic.enableTheory(THEORY_DATATYPES);
-        d_smt.d_logic.lock();
-      }
-      break;
-    default:
-      Unhandled(mode);
-    }
-  }
-  return retval;
-}
-
 void SmtEnginePrivate::processAssertions() {
   TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
   spendResource(options::preprocessStep());
@@ -3904,15 +3859,6 @@ void SmtEnginePrivate::processAssertions() {
     dumpAssertions("post-bv-abstraction", d_assertions);
   }
 
-  dumpAssertions("pre-boolean-terms", d_assertions);
-  {
-    Chat() << "rewriting Boolean terms..." << endl;
-    for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) {
-      d_assertions.replace(i, rewriteBooleanTerms(d_assertions[i]));
-    }
-  }
-  dumpAssertions("post-boolean-terms", d_assertions);
-
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
   dumpAssertions("pre-constrain-subtypes", d_assertions);
@@ -4523,6 +4469,7 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec
 }/* SmtEngine::assertFormula() */
 
 Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
+/*
   ModelPostprocessor mpost;
   NodeVisitor<ModelPostprocessor> visitor;
   Node value = visitor.run(mpost, node);
@@ -4534,6 +4481,8 @@ Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
     Debug("boolean-terms") << "postproc: after rewrite " << realValue << endl;
   }
   return realValue;
+  */
+  return node;
 }
 
 Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
@@ -4627,8 +4576,9 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin
   // used by the Model classes.  It's not clear to me exactly how these
   // two are different, but they need to be unified.  This ugly hack here
   // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
+  
+  //AJR : necessary?
   if(!n.getType().isFunction()) {
-    n = d_private->rewriteBooleanTerms(n);
     n = Rewriter::rewrite(n);
   }
 
@@ -4732,7 +4682,6 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, UnsafeInterruptExce
     // Expand, then normalize
     hash_map<Node, Node, NodeHashFunction> cache;
     Node n = d_private->expandDefinitions(*i, cache);
-    n = d_private->rewriteBooleanTerms(n);
     n = Rewriter::rewrite(n);
 
     Trace("smt") << "--- getting value of " << n << endl;