Initial work on boolean term reorganization. IFF replaced by EQUAL. Boolean term conversion removed. Currently 149 total regressions fail on debug build.

69 files changed, 247 insertions, 1420 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 08146760f..6efa76fd3 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -269,7 +269,7 @@ Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const {
 }
 
 Expr Expr::iffExpr(const Expr& right) const {
-  return getEM()->mkExpr(CVC4::kind::IFF, *this, right);
+  return getEM()->mkExpr(CVC4::kind::EQUAL, *this, right);
 }
 
 Expr Expr::impExpr(const Expr& right) const {
@@ -413,9 +413,11 @@ bool Expr::isAtomicFormula() const {
     case CVC4::kind::AND:
     case CVC4::kind::OR:
     case CVC4::kind::ITE:
-    case CVC4::kind::IFF:
     case CVC4::kind::IMPLIES:
       return false;
+    case CVC4::kind::EQUAL:
+      return !(*this)[0].getType().isBool();
+      break;
     default:
       ; /* fall through */
   }
@@ -448,10 +450,12 @@ bool Expr::isBoolConnective() const {
   case CVC4::kind::AND:
   case CVC4::kind::OR:
   case CVC4::kind::IMPLIES:
-  case CVC4::kind::IFF:
   case CVC4::kind::XOR:
   case CVC4::kind::ITE:
     return true;
+  case CVC4::kind::EQUAL:
+    return (*this)[0].getType().isBool();
+    break;
   default:
     return false;
   }
@@ -526,7 +530,8 @@ bool Expr::isITE() const {
 }
 
 bool Expr::isIff() const {
-  return getKind() == CVC4::kind::IFF;
+  //IFF to EQUAL : is this function necessary?
+  return getKind() == CVC4::kind::EQUAL && (*this)[0].getType().isBool();
 }
 
 bool Expr::isImpl() const {
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index c9a6b7e1b..786788dcd 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -143,10 +143,10 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D
 inline void computeXorIffDesiredValues
 (Kind k, SatValue desiredVal, SatValue &desiredVal1, SatValue &desiredVal2)
 {
-  Assert(k == kind::IFF || k == kind::XOR);
+  Assert(k == kind::EQUAL || k == kind::XOR);
 
   bool shouldInvert =
-    (desiredVal == SAT_VALUE_TRUE && k == kind::IFF) ||
+    (desiredVal == SAT_VALUE_TRUE && k == kind::EQUAL) ||
     (desiredVal == SAT_VALUE_FALSE && k == kind::XOR);
 
   if(desiredVal1 == SAT_VALUE_UNKNOWN &&
@@ -517,7 +517,7 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal)
     break;
 
   case kind::XOR:
-  case kind::IFF: {
+  case kind::EQUAL: {
     SatValue desiredVal1 = tryGetSatValue(node[0]);
     SatValue desiredVal2 = tryGetSatValue(node[1]);
     computeXorIffDesiredValues(k, desiredVal, desiredVal1, desiredVal2);
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 47042b458..069c8aa51 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -532,11 +532,12 @@ Expr Expr::xorExpr(const Expr& e) const {
 }
 
 Expr Expr::iffExpr(const Expr& e) const {
+  //IFF to EQUAL : remove this function?
   Assert(d_exprManager != NULL,
          "Don't have an expression manager for this expression!");
   CheckArgument(d_exprManager == e.d_exprManager, e,
                 "Different expression managers!");
-  return d_exprManager->mkExpr(IFF, *this, e);
+  return d_exprManager->mkExpr(EQUAL, *this, e);
 }
 
 Expr Expr::impExpr(const Expr& e) const {
diff --git a/src/expr/node.h b/src/expr/node.h
index 080034e70..d11d51b9c 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -891,8 +891,6 @@ public:
   NodeTemplate<true> iteNode(const NodeTemplate<ref_count2>& thenpart,
                              const NodeTemplate<ref_count3>& elsepart) const;
   template <bool ref_count2>
-  NodeTemplate<true> iffNode(const NodeTemplate<ref_count2>& right) const;
-  template <bool ref_count2>
   NodeTemplate<true> impNode(const NodeTemplate<ref_count2>& right) const;
   template <bool ref_count2>
   NodeTemplate<true> xorNode(const NodeTemplate<ref_count2>& right) const;
@@ -1201,14 +1199,6 @@ NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count2>& thenpart,
 template <bool ref_count>
 template <bool ref_count2>
 NodeTemplate<true>
-NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count2>& right) const {
-  assertTNodeNotExpired();
-  return NodeManager::currentNM()->mkNode(kind::IFF, *this, right);
-}
-
-template <bool ref_count>
-template <bool ref_count2>
-NodeTemplate<true>
 NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count2>& right) const {
   assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right);
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 0c356ca57..a2e6c0af2 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -320,7 +320,7 @@ Kind getOperatorKind(int type, bool& negate) {
 
   switch(type) {
     // booleanBinop
-  case IFF_TOK: return kind::IFF;
+  case IFF_TOK: return kind::EQUAL;
   case IMPLIES_TOK: return kind::IMPLIES;
   case OR_TOK: return kind::OR;
   case XOR_TOK: return kind::XOR;
@@ -403,8 +403,6 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em,
     if(lhs.getType().isBoolean()) {
       if(parser->strictModeEnabled()) {
         WarningOnce() << "Warning: in strict parsing mode, will not convert BOOL = BOOL to BOOL <=> BOOL" << std::endl;
-      } else {
-        k = kind::IFF;
       }
     }
     break;
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index a885fe990..8bff38f47 100644
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -351,7 +351,7 @@ builtinOp[CVC4::Kind& kind]
   | AND_TOK      { $kind = CVC4::kind::AND;     }
   | OR_TOK       { $kind = CVC4::kind::OR;      }
   | XOR_TOK      { $kind = CVC4::kind::XOR;     }
-  | IFF_TOK      { $kind = CVC4::kind::IFF;     }
+  | IFF_TOK      { $kind = CVC4::kind::EQUAL;     }
   | EQUAL_TOK    { $kind = CVC4::kind::EQUAL;   }
   | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
   // Arithmetic
diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index 8d827b17e..4857aa9da 100644
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -77,7 +77,6 @@ Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode, bool parseOn
   // Boolean symbols are always defined
   addOperator(kind::AND);
   addOperator(kind::EQUAL);
-  addOperator(kind::IFF);
   addOperator(kind::IMPLIES);
   addOperator(kind::ITE);
   addOperator(kind::NOT);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 902e745ea..ce7e03351 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1277,13 +1277,6 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   : /* a built-in operator application */
     LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
     {
-      if( kind == CVC4::kind::EQUAL &&
-          args.size() > 0 &&
-          args[0].getType() == EXPR_MANAGER->booleanType() ) {
-        /* Use IFF for boolean equalities. */
-        kind = CVC4::kind::IFF;
-      }
-
       if( !PARSER_STATE->strictModeEnabled() &&
           (kind == CVC4::kind::AND || kind == CVC4::kind::OR) &&
           args.size() == 1) {
@@ -1309,7 +1302,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         for(size_t i = args.size() - 1; i > 0;) {
           expr = MK_EXPR(kind, args[--i], expr);
         }
-      } else if( ( kind == CVC4::kind::IFF || kind == CVC4::kind::EQUAL ||
+      } else if( ( kind == CVC4::kind::EQUAL ||
                    kind == CVC4::kind::LT || kind == CVC4::kind::GT ||
                    kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) &&
                  args.size() > 2 ) {
@@ -1511,7 +1504,6 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         Expr guard;
         Expr body;
         if(expr[1].getKind() == kind::IMPLIES ||
-           expr[1].getKind() == kind::IFF ||
            expr[1].getKind() == kind::EQUAL) {
           guard = expr[0];
           body = expr[1];
@@ -1526,10 +1518,13 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
           args.push_back(f2);
         }
 
-        if     ( body.getKind()==kind::IMPLIES )    kind = kind::RR_DEDUCTION;
-        else if( body.getKind()==kind::IFF )        kind = kind::RR_REDUCTION;
-        else if( body.getKind()==kind::EQUAL )      kind = kind::RR_REWRITE;
-        else PARSER_STATE->parseError("Error parsing rewrite rule.");
+        if     ( body.getKind()==kind::IMPLIES ){
+          kind = kind::RR_DEDUCTION;
+        }else if( body.getKind()==kind::EQUAL ){
+          kind = body[0].getType() == EXPR_MANAGER->booleanType() ? kind::RR_REDUCTION : kind::RR_REWRITE;
+        }else{
+          PARSER_STATE->parseError("Error parsing rewrite rule.");
+        }
 
         expr = MK_EXPR( kind, args );
       } else if(! patexprs.empty()) {
@@ -1648,7 +1643,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       }
       bool success = true;
       if( attr==":fun-def" ){
-        if( ( expr.getKind()!=kind::EQUAL && expr.getKind()!=kind::IFF ) || expr[0].getKind()!=kind::APPLY_UF ){
+        if( expr.getKind()!=kind::EQUAL || expr[0].getKind()!=kind::APPLY_UF ){
           success = false;
         }else{
           FunctionType t = (FunctionType)expr[0].getOperator().getType();
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 3db2e252d..db5b73d4b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -149,7 +149,6 @@ void Smt2::addTheory(Theory theory) {
     Parser::addOperator(kind::AND);
     Parser::addOperator(kind::DISTINCT);
     Parser::addOperator(kind::EQUAL);
-    Parser::addOperator(kind::IFF);
     Parser::addOperator(kind::IMPLIES);
     Parser::addOperator(kind::ITE);
     Parser::addOperator(kind::NOT);
@@ -594,7 +593,7 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec
     builtTerm = ops[i][j];
   }
   Debug("parser-sygus") << "...made built term " << builtTerm << std::endl;
-  Expr assertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
+  Expr assertion = getExprManager()->mkExpr(kind::EQUAL, evalApply, builtTerm);
   Expr pattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
   pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern);
   assertion = getExprManager()->mkExpr(kind::FORALL, bvl, assertion, pattern);
@@ -644,7 +643,7 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec
               Debug("parser-sygus") << "builtApply " << builtApply[k] << std::endl;
               builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
               Debug("parser-sygus") << "builtTerm " << builtTerm << std::endl;
-              Expr eassertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
+              Expr eassertion = getExprManager()->mkExpr(kind::EQUAL, evalApply, builtTerm);
               Expr epattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
               epattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, epattern);
               eassertion = getExprManager()->mkExpr(kind::FORALL, nbvl, eassertion, epattern);
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 62dcc70f5..290f4f808 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -517,7 +517,7 @@ fofLogicFormula[CVC4::Expr& expr]
       ( fofBinaryNonAssoc[na] fofUnitaryFormula[expr2]
         { switch(na) {
            case tptp::NA_IFF:
-             expr = MK_EXPR(kind::IFF,expr,expr2);
+             expr = MK_EXPR(kind::EQUAL,expr,expr2);
              break;
            case tptp::NA_REVIFF:
              expr = MK_EXPR(kind::XOR,expr,expr2);
@@ -652,7 +652,7 @@ tffLogicFormula[CVC4::Expr& expr]
       ( fofBinaryNonAssoc[na] tffUnitaryFormula[expr2]
         { switch(na) {
            case tptp::NA_IFF:
-             expr = MK_EXPR(kind::IFF,expr,expr2);
+             expr = MK_EXPR(kind::EQUAL,expr,expr2);
              break;
            case tptp::NA_REVIFF:
              expr = MK_EXPR(kind::XOR,expr,expr2);
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index b674b12dc..477e8142a 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -71,7 +71,6 @@ void Tptp::addTheory(Theory theory) {
     defineVar("$false", em->mkConst(false));
     addOperator(kind::AND);
     addOperator(kind::EQUAL);
-    addOperator(kind::IFF);
     addOperator(kind::IMPLIES);
     //addOperator(kind::ITE); //only for tff thf
     addOperator(kind::NOT);
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 2e1170666..9e9e2a9e4 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -200,7 +200,11 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
 
     // BUILTIN
     case kind::EQUAL:
-      op << '=';
+      if( n[0].getType().isBoolean() ){
+        op << "<=>";
+      }else{
+        op << '=';
+      }
       opType = INFIX;
       break;
     case kind::ITE:
@@ -270,10 +274,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       op << "XOR";
       opType = INFIX;
       break;
-    case kind::IFF:
-      op << "<=>";
-      opType = INFIX;
-      break;
     case kind::IMPLIES:
       op << "=>";
       opType = INFIX;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 999dc870f..6dd911279 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -320,7 +320,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     // bool theory
   case kind::NOT:
   case kind::AND:
-  case kind::IFF:
   case kind::IMPLIES:
   case kind::OR:
   case kind::XOR:
@@ -652,7 +651,6 @@ static string smtKindString(Kind k) throw() {
     // bool theory
   case kind::NOT: return "not";
   case kind::AND: return "and";
-  case kind::IFF: return "=";
   case kind::IMPLIES: return "=>";
   case kind::OR: return "or";
   case kind::XOR: return "xor";
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 52989d722..bdf158e68 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -53,7 +53,6 @@ std::string toLFSCKind(Kind kind) {
   case kind::AND: return "and";
   case kind::XOR: return "xor";
   case kind::EQUAL: return "=";
-  case kind::IFF: return "iff";
   case kind::IMPLIES: return "impl";
   case kind::NOT: return "not";
   default:
@@ -103,8 +102,12 @@ void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) {
 
   case kind::EQUAL:
     os << "(";
-    os << "= ";
-    os << term[0].getType() << " ";
+    if( term[0].getType().isBoolean() ){
+      os << "iff ";
+    }else{
+      os << "= ";
+      os << term[0].getType() << " ";
+    }
     printTerm(term[0], os);
     os << " ";
     printTerm(term[1], os);
@@ -123,7 +126,6 @@ void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) {
   case kind::OR:
   case kind::AND:
   case kind::XOR:
-  case kind::IFF:
   case kind::IMPLIES:
   case kind::NOT:
     // print the Boolean operators
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index fd30cd997..2f7f2a30a 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -370,7 +370,7 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
 
 SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
   Assert(!hasLiteral(iffNode), "Atom already mapped!");
-  Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!");
+  Assert(iffNode.getKind() == EQUAL, "Expecting an EQUAL expression!");
   Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!");
 
   Debug("cnf") << "handleIff(" << iffNode << ")" << endl;
@@ -469,9 +469,6 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
     case ITE:
       nodeLit = handleIte(node);
       break;
-    case IFF:
-      nodeLit = handleIff(node);
-      break;
     case IMPLIES:
       nodeLit = handleImplies(node);
       break;
@@ -484,7 +481,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
     case EQUAL:
       if(node[0].getType().isBoolean()) {
         // normally this is an IFF, but EQUAL is possible with pseudobooleans
-        nodeLit = handleIff(node[0].iffNode(node[1]));
+        nodeLit = handleIff(node);
       } else {
         nodeLit = convertAtom(node);
       }
@@ -680,9 +677,6 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
   case OR:
     convertAndAssertOr(node, negated);
     break;
-  case IFF:
-    convertAndAssertIff(node, negated);
-    break;
   case XOR:
     convertAndAssertXor(node, negated);
     break;
@@ -695,6 +689,11 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
   case NOT:
     convertAndAssert(node[0], !negated);
     break;
+  case EQUAL:
+    if( node[0].getType().isBoolean() ){
+      convertAndAssertIff(node, negated);
+      break;
+    }
   default:
     // Atoms
     assertClause(node, toCNF(node, negated));
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 54a6b5416..977ce95c5 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -37,879 +37,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) throw() {
-  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);
-  }
-  if(in.getType().isRecord()) {
-    Assert(as.isRecord());
-    const Record& inRec = in.getType().getConst<Record>();
-    const Record& asRec = as.getConst<Record>();
-    Assert(inRec.getNumFields() == asRec.getNumFields());
-    NodeBuilder<> nb(kind::RECORD);
-    nb << NodeManager::currentNM()->mkConst(asRec);
-    for(size_t i = 0; i < asRec.getNumFields(); ++i) {
-      Assert(inRec[i].first == asRec[i].first);
-      Node arg = NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(RecordSelect(inRec[i].first)), in);
-      if(inRec[i].second != asRec[i].second) {
-        arg = rewriteAs(arg, TypeNode::fromType(asRec[i].second));
-      }
-      nb << arg;
-    }
-    Node out = nb;
-    return out;
-  }
-  if(in.getType().isTuple()) {
-    Assert(as.isTuple());
-    Assert(in.getType().getNumChildren() == as.getNumChildren());
-    NodeBuilder<> nb(kind::TUPLE);
-    for(size_t i = 0; i < as.getNumChildren(); ++i) {
-      Node arg = NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(TupleSelect(i)), in);
-      if(in.getType()[i] != as[i]) {
-        arg = rewriteAs(arg, as[i]);
-      }
-      nb << arg;
-    }
-    Node out = nb;
-    return out;
-  }
-  if(in.getType().isDatatype()) {
-    if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
-      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()));
-      }
-      Node appctor = appctorb;
-      if(i == 0) {
-        out = appctor;
-      } else {
-        Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out);
-        out = newOut;
-      }
-    }
-    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());
-    Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundvars, selprime);
-    Node out = NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA, lam);
-    Assert(out.getType() == as);
-    return out;
-  }
-  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);
-      }
-      Node appctor = appctorb;
-      if(i == 0) {
-        out = appctor;
-      } else {
-        Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out);
-        out = newOut;
-      }
-    }
-    return out;
-  }
-
-  Unhandled(in);
-}
-
-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].getConst<Datatype>() : type.getConst<Datatype>();
-    TypeNode out = TypeNode::fromType(convertDatatype(dt).getDatatypeType());
-    Debug("boolean-terms") << "AFTER, got "<< out << " param:" << parametric << endl;
-    if(parametric) {
-      // re-parameterize the translation
-      vector<TypeNode> params = type.getParamTypes();
-      for(size_t i = 0; i < params.size(); ++i) {
-        Debug("boolean-terms") << "in loop, got "<< params[i] << endl;
-        params[i] = convertType(params[i], true);
-        Debug("boolean-terms") << "in loop, convert to "<< params[i] << endl;
-      }
-      params.insert(params.begin(), out[0]);
-      out = NodeManager::currentNM()->mkTypeNode(kind::PARAMETRIC_DATATYPE, params);
-      Debug("boolean-terms") << "got OUT: " << out << endl;
-    }
-    if(out != type) {
-      outNode = out;// cache it
-      Debug("boolean-terms") << "OUT is same as TYPE" << endl;
-    } else Debug("boolean-terms") << "OUT is DIFFERENT FROM TYPE" << endl;
-    return out;
-  }
-  if(type.isRecord()) {
-    const Record& rec = type.getConst<Record>();
-    vector< pair<string, Type> > flds;
-    for(Record::const_iterator i = rec.begin(); i != rec.end(); ++i) {
-      TypeNode converted = convertType(TypeNode::fromType((*i).second), true);
-      if(TypeNode::fromType((*i).second) != converted) {
-        flds.push_back(make_pair((*i).first, converted.toType()));
-      } else {
-        flds.push_back(*i);
-      }
-    }
-    TypeNode newRec = NodeManager::currentNM()->mkRecordType(Record(flds));
-    Debug("tuprec") << "converted " << type << " to " << newRec << endl;
-    if(newRec != type) {
-      outNode = newRec;// cache it
-    }
-    return newRec;
-  }
-  if(!type.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;
-  result.push(NodeBuilder<>(kind::TUPLE));
-
-  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()) {
-        // 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]) {
-                  bodyBuilder << rewriteAs(var, argTypes[j]);
-                } else {
-                  bodyBuilder << var;
-                }
-              }
-              Node boundVars = boundVarsBuilder;
-              Node body = bodyBuilder;
-              if(t.getRangeType() != rangeType) {
-                Node convbody = rewriteAs(body, t.getRangeType());
-                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.isTuple() || t.isRecord()) {
-          TypeNode newType = convertType(t, true);
-          if(t != newType) {
-            Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
-                                  newType, "a tuple/record variable introduced by Boolean-term conversion",
-                                  NodeManager::SKOLEM_EXACT_NAME);
-            top.setAttribute(BooleanTermAttr(), n);
-            n.setAttribute(BooleanTermAttr(), top);
-            Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
-            d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
-            Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
-            d_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].getConst<Datatype>() :
-            t[t.getNumChildren() - 1][0].getConst<Datatype>();
-          TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
-          const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
-          if(dt != dt2) {
-            Assert(d_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].getConst<Datatype>() :
-            t[0][0].getConst<Datatype>();
-          TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
-          const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
-          if(dt != dt2) {
-            Assert(d_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) {
-          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:
-        // 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::RECORD) {
-            result.top() << convertType(top.getType(), parentTheory == theory::THEORY_DATATYPES);
-          } else if(k == kind::APPLY_TYPE_ASCRIPTION) {
-            Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType()));
-            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_SELECT &&
-                    k != kind::TUPLE_UPDATE &&
-                    k != kind::RECORD_SELECT &&
-                    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) ? 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 << 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 ed676c667..fa58b2452 100644
--- a/src/smt/boolean_terms.h
+++ b/src/smt/boolean_terms.h
@@ -28,84 +28,7 @@
 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) 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/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index 44b56fdd4..7a543f715 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -40,34 +40,6 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
     // 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.getConst<Datatype>();
-      return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, (tf ? asDatatype[0] : asDatatype[1]).getConstructor());
-    }
-  }
   if(n.getType().isRecord() && asType.isRecord()) {
     Debug("boolean-terms") << "+++ got a record - rewriteAs " << n << " : " << asType << endl;
     const Record& rec CVC4_UNUSED = n.getType().getConst<Record>();
@@ -154,20 +126,8 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
       Assert(t != expectType.end());
       TNode n = d_nodes[*i];
       n = n.isNull() ? *i : n;
-      if(!n.getType().isSubtypeOf(*t)) {
-        Assert(n.getType().isBitVector(1u) ||
-               (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
-        Assert(n.isConst());
-        Assert((*t).isBoolean());
-        if(n.getType().isBitVector(1u)) {
-          b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
-        } else {
-          // we assume (by construction) false is first; see boolean_terms.cpp
-          b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
-        }
-      } else {
-        b << n;
-      }
+      Assert( n.getType().isSubtypeOf(*t) );
+      b << n;
     }
     Assert(t == expectType.end());
     d_nodes[current] = b;
@@ -188,63 +148,14 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
       Assert(t != expectRec.end());
       TNode n = d_nodes[*i];
       n = n.isNull() ? *i : n;
-      if(!n.getType().isSubtypeOf(TypeNode::fromType((*t).second))) {
-        Assert(n.getType().isBitVector(1u) ||
-               (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
-        Assert(n.isConst());
-        Assert((*t).second.isBoolean());
-        if(n.getType().isBitVector(1u)) {
-          b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
-        } else {
-          // we assume (by construction) false is first; see boolean_terms.cpp
-          b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
-        }
-      } else {
-        b << n;
-      }
+      Assert(n.getType().isSubtypeOf(TypeNode::fromType((*t).second)));
+      b << n;
     }
     Assert(t == expectRec.end());
     d_nodes[current] = b;
     Debug("tuprec") << "returning " << d_nodes[current] << endl;
     Assert(d_nodes[current].getType() == expectType);
-  } else if(current.getKind() == kind::APPLY_CONSTRUCTOR &&
-            ( current.getOperator().hasAttribute(BooleanTermAttr()) ||
-              ( current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION &&
-                current.getOperator()[0].hasAttribute(BooleanTermAttr()) ) )) {
-    NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
-    Node realOp;
-    if(current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION) {
-      TNode oldAsc = current.getOperator().getOperator();
-      Debug("boolean-terms") << "old asc: " << oldAsc << endl;
-      Node newCons = current.getOperator()[0].getAttribute(BooleanTermAttr());
-      Node newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().toType()));
-      Debug("boolean-terms") << "new asc: " << newAsc << endl;
-      if(newCons.getType().getRangeType().isParametricDatatype()) {
-        vector<TypeNode> oldParams = TypeNode::fromType(oldAsc.getConst<AscriptionType>().getType()).getRangeType().getParamTypes();
-        vector<TypeNode> newParams = newCons.getType().getRangeType().getParamTypes();
-        Assert(oldParams.size() == newParams.size() && oldParams.size() > 0);
-        newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().substitute(newParams.begin(), newParams.end(), oldParams.begin(), oldParams.end()).toType()));
-      }
-      realOp = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, newAsc, newCons);
-    } else {
-      realOp = current.getOperator().getAttribute(BooleanTermAttr());
-    }
-    b << realOp;
-    Debug("boolean-terms") << "+ op " << b.getOperator() << endl;
-    TypeNode::iterator j = realOp.getType().begin();
-    for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++j) {
-      Assert(j != realOp.getType().end());
-      Assert(alreadyVisited(*i, TNode::null()));
-      TNode repl = d_nodes[*i];
-      repl = repl.isNull() ? *i : repl;
-      Debug("boolean-terms") << "+ adding " << repl << " expecting " << *j << endl;
-      b << rewriteAs(repl, *j);
-    }
-    Node n = b;
-    Debug("boolean-terms") << "model-post: " << current << endl
-                           << "- returning " << n << endl;
-    d_nodes[current] = n;
-  } else if(current.getKind() == kind::LAMBDA) {
+  }else if(current.getKind() == kind::LAMBDA) {
     // rewrite based on children
     bool self = true;
     for(size_t i = 0; i < current.getNumChildren(); ++i) {
@@ -262,13 +173,7 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
       // 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;
-        }
+        nb << current.getOperator();
       }
       for(size_t i = 0; i < current.getNumChildren(); ++i) {
         Assert(d_nodes.find(current[i]) != d_nodes.end());
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3aec77a45..1ac209d01 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -168,8 +168,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 */
@@ -214,7 +212,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),
@@ -238,7 +235,6 @@ struct SmtEngineStatistics {
  {
 
     StatisticsRegistry::registerStat(&d_definitionExpansionTime);
-    StatisticsRegistry::registerStat(&d_rewriteBooleanTermsTime);
     StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
     StatisticsRegistry::registerStat(&d_miplibPassTime);
     StatisticsRegistry::registerStat(&d_numMiplibAssertionsRemoved);
@@ -263,7 +259,6 @@ struct SmtEngineStatistics {
 
   ~SmtEngineStatistics() {
     StatisticsRegistry::unregisterStat(&d_definitionExpansionTime);
-    StatisticsRegistry::unregisterStat(&d_rewriteBooleanTermsTime);
     StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
     StatisticsRegistry::unregisterStat(&d_miplibPassTime);
     StatisticsRegistry::unregisterStat(&d_numMiplibAssertionsRemoved);
@@ -314,10 +309,7 @@ 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;
@@ -455,7 +447,6 @@ public:
     d_resourceManager(NULL),
     d_nonClausalLearnedLiterals(),
     d_realAssertionsEnd(0),
-    d_booleanTermConverter(NULL),
     d_propagator(d_nonClausalLearnedLiterals, true, true),
     d_propagatorNeedsFinish(false),
     d_assertions(),
@@ -480,10 +471,6 @@ public:
       d_propagator.finish();
       d_propagatorNeedsFinish = false;
     }
-    if(d_booleanTermConverter != NULL) {
-      delete d_booleanTermConverter;
-      d_booleanTermConverter = NULL;
-    }
     d_smt.d_nodeManager->unsubscribeEvents(this);
   }
 
@@ -583,11 +570,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.
    */
@@ -2109,7 +2091,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;
     }
@@ -2965,6 +2947,7 @@ 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);
 
@@ -3000,6 +2983,7 @@ Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) {
   }
   return retval;
 }
+*/
 
 void SmtEnginePrivate::processAssertions() {
   TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
@@ -3066,6 +3050,7 @@ void SmtEnginePrivate::processAssertions() {
     dumpAssertions("post-bv-abstraction", d_assertions);
   }
 
+  /*
   dumpAssertions("pre-boolean-terms", d_assertions);
   {
     Chat() << "rewriting Boolean terms..." << endl;
@@ -3074,6 +3059,7 @@ void SmtEnginePrivate::processAssertions() {
     }
   }
   dumpAssertions("post-boolean-terms", d_assertions);
+  */
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
@@ -3736,7 +3722,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin
   // 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]
   if(!n.getType().isFunction()) {
-    n = d_private->rewriteBooleanTerms(n);
+    //n = d_private->rewriteBooleanTerms(n);
     n = Rewriter::rewrite(n);
   }
 
@@ -3838,7 +3824,7 @@ 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 = d_private->rewriteBooleanTerms(n);
     n = Rewriter::rewrite(n);
 
     Trace("smt") << "--- getting value of " << n << endl;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 7c5c45e42..cd05d736c 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -91,7 +91,6 @@ namespace smt {
   struct SmtEngineStatistics;
   class SmtEnginePrivate;
   class SmtScope;
-  class BooleanTermConverter;
 
   void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
   ProofManager* currentProofManager();
@@ -334,7 +333,6 @@ class CVC4_PUBLIC SmtEngine {
 
   friend class ::CVC4::smt::SmtEnginePrivate;
   friend class ::CVC4::smt::SmtScope;
-  friend class ::CVC4::smt::BooleanTermConverter;
   friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*);
   friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
   friend ProofManager* ::CVC4::smt::currentProofManager();
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 90029495b..28eb40e95 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -91,11 +91,7 @@ bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerTermEquality(
 }
 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
   Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
-  if (t1.getKind() == kind::CONST_BOOLEAN) {
-    d_acm.propagate(t1.iffNode(t2));
-  } else {
-    d_acm.propagate(t1.eqNode(t2));
-  }
+  d_acm.propagate(t1.eqNode(t2));
 }
 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyNewClass(TNode t) {
 }
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 94f3f573e..c2e200dec 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -224,16 +224,14 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck
         for (j = leftWrites - 1; j > i; --j) {
           index_j = write_j[1];
           if (!ppCheck || !ppDisequal(index_i, index_j)) {
-            Node hyp2(index_i.getType() == nm->booleanType()?
-                      index_i.iffNode(index_j) : index_i.eqNode(index_j));
+            Node hyp2(index_i.eqNode(index_j));
             hyp << hyp2.notNode();
           }
           write_j = write_j[0];
         }
 
         Node r1 = nm->mkNode(kind::SELECT, e1, index_i);
-        conc = (r1.getType() == nm->booleanType())?
-          r1.iffNode(write_i[2]) : r1.eqNode(write_i[2]);
+        conc = r1.eqNode(write_i[2]);
         if (hyp.getNumChildren() != 0) {
           if (hyp.getNumChildren() == 1) {
             conc = hyp.getChild(0).impNode(conc);
@@ -333,8 +331,7 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs
     case kind::NOT:
     {
       d_ppFacts.push_back(in);
-      Assert(in[0].getKind() == kind::EQUAL ||
-             in[0].getKind() == kind::IFF );
+      Assert(in[0].getKind() == kind::EQUAL);
       Node a = in[0][0];
       Node b = in[0][1];
       d_ppEqualityEngine.assertEquality(in[0], false, in);
@@ -380,7 +377,7 @@ void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) {
   TNode atom = polarity ? literal : literal[0];
   //eq::EqProof * eqp = new eq::EqProof;
   eq::EqProof * eqp = NULL;
-  if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+  if (atom.getKind() == kind::EQUAL) {
     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, eqp);
   } else {
     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
@@ -2666,11 +2663,7 @@ bool TheoryArrays::dischargeLemmas()
 }
 
 void TheoryArrays::conflict(TNode a, TNode b) {
-  if (a.getKind() == kind::CONST_BOOLEAN) {
-    d_conflictNode = explain(a.iffNode(b));
-  } else {
-    d_conflictNode = explain(a.eqNode(b));
-  }
+  d_conflictNode = explain(a.eqNode(b));
   if (!d_inCheckModel) {
     d_out->conflict(d_conflictNode);
   }
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 7753e11b9..35b56cbd4 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -33,7 +33,7 @@ void setMostFrequentValue(TNode store, TNode value);
 void setMostFrequentValueCount(TNode store, uint64_t count);
 
 static inline Node mkEqNode(Node a, Node b) {
-  return a.getType().isBoolean() ? a.iffNode(b) : a.eqNode(b);
+  return a.eqNode(b);
 }
 
 class TheoryArraysRewriter {
@@ -376,8 +376,7 @@ public:
         }
         break;
       }
-      case kind::EQUAL:
-      case kind::IFF: {
+      case kind::EQUAL: {
         if(node[0] == node[1]) {
           Trace("arrays-postrewrite") << "Arrays::postRewrite returning true" << std::endl;
           return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
@@ -482,8 +481,7 @@ public:
         }
         break;
       }
-      case kind::EQUAL:
-      case kind::IFF: {
+      case kind::EQUAL: {
         if(node[0] == node[1]) {
           Trace("arrays-prerewrite") << "Arrays::preRewrite returning true" << std::endl;
           return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
diff --git a/src/theory/booleans/boolean_term_conversion_mode.cpp b/src/theory/booleans/boolean_term_conversion_mode.cpp
index b8647eb3c..14633e274 100644
--- a/src/theory/booleans/boolean_term_conversion_mode.cpp
+++ b/src/theory/booleans/boolean_term_conversion_mode.cpp
@@ -20,22 +20,6 @@
 
 namespace CVC4 {
 
-std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) {
-  switch(mode) {
-  case theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS:
-    out << "BOOLEAN_TERM_CONVERT_TO_BITVECTORS";
-    break;
-  case theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
-    out << "BOOLEAN_TERM_CONVERT_TO_DATATYPES";
-    break;
-  case theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE:
-    out << "BOOLEAN_TERM_CONVERT_NATIVE";
-    break;
-  default:
-    out << "BooleanTermConversionMode!UNKNOWN";
-  }
 
-  return out;
-}
 
 }/* CVC4 namespace */
diff --git a/src/theory/booleans/boolean_term_conversion_mode.h b/src/theory/booleans/boolean_term_conversion_mode.h
index 5671dea13..35853de2a 100644
--- a/src/theory/booleans/boolean_term_conversion_mode.h
+++ b/src/theory/booleans/boolean_term_conversion_mode.h
@@ -26,28 +26,9 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-typedef enum {
-  /**
-   * Convert Boolean terms to bitvectors of size 1.
-   */
-  BOOLEAN_TERM_CONVERT_TO_BITVECTORS,
-  /**
-   * Convert Boolean terms to enumerations in the Datatypes theory.
-   */
-  BOOLEAN_TERM_CONVERT_TO_DATATYPES,
-  /**
-   * Convert Boolean terms to enumerations in the Datatypes theory IF
-   * used in a datatypes context, otherwise to a bitvector of size 1.
-   */
-  BOOLEAN_TERM_CONVERT_NATIVE
-
-} BooleanTermConversionMode;
 
 }/* CVC4::theory::booleans namespace */
 }/* CVC4::theory namespace */
-
-std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) CVC4_PUBLIC;
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H */
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index cd6b8dc53..dafb7767c 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -135,7 +135,8 @@ void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) {
       }
     }
     break;
-  case kind::IFF:
+  case kind::EQUAL:
+    Assert( parent[0].getType().isBoolean() );
     if (parentAssignment) {
       // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment [resp x = y.assignment])
       if (isAssigned(parent[0])) {
@@ -285,7 +286,8 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) {
         }
       }
       break;
-    case kind::IFF:
+    case kind::EQUAL:
+      Assert( parent[0].getType().isBoolean() );
       if (isAssigned(parent[0]) && isAssigned(parent[1])) {
         // IFF x y: if x or y is assigned, assign(IFF = (x.assignment <=> y.assignment))
         assignAndEnqueue(parent, getAssignment(parent[0]) == getAssignment(parent[1]));
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index ad45e3cbb..eea3a9fa6 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -40,7 +40,6 @@ typerule CONST_BOOLEAN ::CVC4::theory::boolean::BooleanTypeRule
 
 typerule NOT ::CVC4::theory::boolean::BooleanTypeRule
 typerule AND ::CVC4::theory::boolean::BooleanTypeRule
-typerule IFF ::CVC4::theory::boolean::BooleanTypeRule
 typerule IMPLIES ::CVC4::theory::boolean::BooleanTypeRule
 typerule OR ::CVC4::theory::boolean::BooleanTypeRule
 typerule XOR ::CVC4::theory::boolean::BooleanTypeRule
diff --git a/src/theory/booleans/options b/src/theory/booleans/options
index 6c571f30e..fbcea2433 100644
--- a/src/theory/booleans/options
+++ b/src/theory/booleans/options
@@ -5,7 +5,6 @@
 
 module BOOLEANS "theory/booleans/options.h" Boolean theory
 
-option booleanTermConversionMode boolean-term-conversion-mode --boolean-term-conversion-mode=MODE CVC4::theory::booleans::BooleanTermConversionMode :default CVC4::theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS :include "theory/booleans/boolean_term_conversion_mode.h" :handler CVC4::theory::booleans::stringToBooleanTermConversionMode :handler-include "theory/booleans/options_handlers.h"
- policy for converting Boolean terms
+
 
 endmodule
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 05bb99680..4483d4248 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -173,7 +173,6 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
     break;
   }
-  case kind::IFF:
   case kind::EQUAL: {
     // rewrite simple cases of IFF
     if(n[0] == tt) {
@@ -318,7 +317,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
 
     int parityTmp;
     if ((parityTmp = equalityParity(n[1], n[2])) != 0) {
-      Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].iffNode(n[1]);
+      Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].eqNode(n[1]);
       Debug("bool-ite") << "equalityParity n[1], n[2] " << parityTmp
                         << " " << n << ": " << resp << std::endl;
       return RewriteResponse(REWRITE_AGAIN, resp);
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index 516d6a06b..1fb6a9d9e 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -31,7 +31,7 @@ Node TheoryBuiltinRewriter::blastDistinct(TNode in) {
   if(in.getNumChildren() == 2) {
     // if this is the case exactly 1 != pair will be generated so the
     // AND is not required
-    Node eq = NodeManager::currentNM()->mkNode(in[0].getType().isBoolean() ? kind::IFF : kind::EQUAL, in[0], in[1]);
+    Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, in[0], in[1]);
     Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
     return neq;
   }
@@ -41,7 +41,7 @@ Node TheoryBuiltinRewriter::blastDistinct(TNode in) {
   for(TNode::iterator i = in.begin(); i != in.end(); ++i) {
     TNode::iterator j = i;
     while(++j != in.end()) {
-      Node eq = NodeManager::currentNM()->mkNode((*i).getType().isBoolean() ? kind::IFF : kind::EQUAL, *i, *j);
+      Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, *i, *j);
       Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
       diseqs.push_back(neq);
     }
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 977a097d0..30ed7af39 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -86,10 +86,6 @@ class EqualityTypeRule {
 
         throw TypeCheckingExceptionPrivate(n, ss.str());
       }
-
-      if ( lhsType == booleanType && rhsType == booleanType ) {
-        throw TypeCheckingExceptionPrivate(n, "equality between two boolean terms (use IFF instead)");
-      }
     }
     return booleanType;
   }
diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index 6270995ef..e26d166ed 100644
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -180,15 +180,6 @@ Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
       }
       break;
     }
-  case kind::IFF:
-    {
-      Assert (node.getNumChildren() == 2); 
-      Abc_Obj_t* child1 = bbFormula(node[0]);
-      Abc_Obj_t* child2 = bbFormula(node[1]);
-
-      result = mkIff(child1, child2); 
-      break;
-    }
   case kind::XOR:
     {
       result = bbFormula(node[0]);
@@ -233,6 +224,18 @@ Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
       result = mkInput(node);
       break;
     }
+  case kind::EQUAL:
+    {
+      if( node[0].getType().isBoolean() ){
+        Assert (node.getNumChildren() == 2); 
+        Abc_Obj_t* child1 = bbFormula(node[0]);
+        Abc_Obj_t* child2 = bbFormula(node[1]);
+
+        result = mkIff(child1, child2); 
+        break;
+      }
+      //else continue...
+    }
   default:
     bbAtom(node);
     result = getBBAtom(node);
diff --git a/src/theory/bv/bitblast_utils.h b/src/theory/bv/bitblast_utils.h
index a236c69e8..fd9ea4954 100644
--- a/src/theory/bv/bitblast_utils.h
+++ b/src/theory/bv/bitblast_utils.h
@@ -119,7 +119,7 @@ Node mkXor<Node>(Node a, Node b) {
 
 template <> inline
 Node mkIff<Node>(Node a, Node b) {
-  return NodeManager::currentNM()->mkNode(kind::IFF, a, b);
+  return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
 }
 
 template <> inline
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 154f3d7f3..d11d612fb 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -498,7 +498,7 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
     bool changed = subst.addSubstitution(var, new_right, reason);
 
     if (Dump.isOn("bv-algebraic")) {
-      Node query = utils::mkNot(utils::mkNode(kind::IFF, fact, utils::mkNode(kind::EQUAL, var, new_right)));
+      Node query = utils::mkNot(utils::mkNode(kind::EQUAL, fact, utils::mkNode(kind::EQUAL, var, new_right)));
       Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation"); 
       Dump("bv-algebraic") << PushCommand(); 
       Dump("bv-algebraic") << AssertCommand(query.toExpr());
diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index 06a1d4a44..dc31912c0 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -101,7 +101,8 @@ Node BvToBoolPreprocessor::convertBvAtom(TNode node) {
   Assert (utils::getSize(node[1]) == 1);
   Node a = convertBvTerm(node[0]);
   Node b = convertBvTerm(node[1]);
-  Node result = utils::mkNode(kind::IFF, a, b); 
+  //IFF to EQUAL : this function may be unecessary in some cases?
+  Node result = utils::mkNode(kind::EQUAL, a, b); 
   Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvAtom " << node <<" => " << result << "\n";
 
   ++(d_statistics.d_numAtomsLifted);
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 065d5d5ef..f16b56cc1 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -81,7 +81,7 @@ void EagerBitblaster::bbAtom(TNode node) {
       Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) :
       normalized;
   // asserting that the atom is true iff the definition holds
-  Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
+  Node atom_definition = utils::mkNode(kind::EQUAL, node, atom_bb);
 
   AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); 
   storeBBAtom(node, atom_definition);
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index fbebcd952..50e5b7aa2 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -115,7 +115,7 @@ void TLazyBitblaster::bbAtom(TNode node) {
       atom_bb = utils::mkAnd(atoms);
     }
     Assert (!atom_bb.isNull()); 
-    Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
+    Node atom_definition = utils::mkNode(kind::EQUAL, node, atom_bb);
     storeBBAtom(node, atom_bb);
     d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
     return; 
@@ -127,7 +127,7 @@ void TLazyBitblaster::bbAtom(TNode node) {
     Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) :
     normalized;
   // asserting that the atom is true iff the definition holds
-  Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
+  Node atom_definition = utils::mkNode(kind::EQUAL, node, atom_bb);
   storeBBAtom(node, atom_bb);
   d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
 }
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 3cc1c323c..bef60c6f3 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -377,12 +377,7 @@ public:
           std::ostringstream os;
           os << "RewriteRule <"<<rule<<">; expect unsat";
 
-          Node condition;
-          if (result.getType().isBoolean()) {
-            condition = node.iffNode(result).notNode();
-          } else {
-            condition = node.eqNode(result).notNode();
-          }
+          Node condition = node.eqNode(result).notNode();
 
           Dump("bv-rewrites")
             << CommentCommand(os.str())
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index ec9318e99..74b95d0e2 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -296,7 +296,7 @@ public:
       if( n1.isConst() && n2.isConst() ){
         return true;
       }else{
-        Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 );
+        Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, n1, n2 );
         rew.push_back( eq );
       }
     }
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 19aacd0df..a3cc19c06 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -432,10 +432,10 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
         nk = OR;reqk = NOT;
       }else if( k==OR ){
         nk = AND;reqk = NOT;
-      }else if( k==IFF ) {
+      }else if( k==EQUAL ) {
         nk = XOR;
       }else if( k==XOR ) {
-        nk = IFF;
+        nk = EQUAL;
       }
     }
     if( parent==BITVECTOR_NOT ){
@@ -1166,7 +1166,7 @@ Node SygusSymBreak::getSeparationTemplate( TypeNode tn,  Node rep_prog, Node anc
 bool SygusSymBreak::processConstantArg( TypeNode tnp, const Datatype & pdt, int pc,
                                         Kind k, int i, Node arg, std::map< unsigned, bool >& rlv ) {
   Assert( d_tds->hasKind( tnp, k ) );
-  if( k==AND || k==OR || k==IFF || k==XOR || k==IMPLIES || ( k==ITE && i==0 ) ){
+  if( k==AND || k==OR || ( k==EQUAL && arg.getType().isBoolean() ) || k==XOR || k==IMPLIES || ( k==ITE && i==0 ) ){
     return false;
   }else if( d_tds->isIdempotentArg( arg, k, i ) ){
     if( pdt[pc].getNumArgs()==2 ){
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 6aa8b71dd..a4463250b 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -382,7 +382,7 @@ void TheoryDatatypes::doPendingMerges(){
     //do all pending merges
     int i=0;
     while( i<(int)d_pending_merge.size() ){
-      Assert( d_pending_merge[i].getKind()==EQUAL || d_pending_merge[i].getKind()==IFF );
+      Assert( d_pending_merge[i].getKind()==EQUAL );
       merge( d_pending_merge[i][0], d_pending_merge[i][1] );
       i++;
     }
@@ -540,19 +540,6 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
   // we only care about tuples and records here
   if(in.getKind() != kind::TUPLE && in.getKind() != kind::TUPLE_UPDATE &&
      in.getKind() != kind::RECORD && in.getKind() != kind::RECORD_UPDATE) {
-    if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) {
-      Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl;
-      Debug("tuprec") << "so " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl;
-      if(t.isTuple()) {
-        Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeTupleAttr()) << endl;
-        Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl;
-        NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()));
-      } else {
-        Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeRecordAttr()) << endl;
-        Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl;
-        NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()));
-      }
-    }
 
     if( in.getKind()==EQUAL ){
       Node nn;
@@ -696,7 +683,7 @@ void TheoryDatatypes::explain(TNode literal, std::vector<TNode>& assumptions){
   Debug("datatypes-explain") << "Explain " << literal << std::endl;
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
-  if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+  if (atom.getKind() == kind::EQUAL) {
     explainEquality( atom[0], atom[1], polarity, assumptions );
   } else if( atom.getKind() == kind::AND && polarity ){
     for( unsigned i=0; i<atom.getNumChildren(); i++ ){
@@ -724,11 +711,7 @@ Node TheoryDatatypes::explain( std::vector< Node >& lits ) {
 
 /** Conflict when merging two constants */
 void TheoryDatatypes::conflict(TNode a, TNode b){
-  if (a.getKind() == kind::CONST_BOOLEAN) {
-    d_conflictNode = explain( a.iffNode(b) );
-  } else {
-    d_conflictNode = explain( a.eqNode(b) );
-  }
+  d_conflictNode = explain( a.eqNode(b) );
   Trace("dt-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode << std::endl;
   d_out->conflict( d_conflictNode );
   d_conflict = true;
@@ -803,8 +786,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
             for( unsigned i=0; i<deq_cand.size(); i++ ){
               if( d_equalityEngine.areDisequal( deq_cand[i].first, deq_cand[i].second, true ) ){
                 conf = true;
-                Node eq = NodeManager::currentNM()->mkNode( deq_cand[i].first.getType().isBoolean() ? kind::IFF : kind::EQUAL,
-                                                            deq_cand[i].first, deq_cand[i].second );
+                Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, deq_cand[i].first, deq_cand[i].second );
                 exp.push_back( eq.negate() );
               }
             }
@@ -825,7 +807,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
             //do unification
             for( int i=0; i<(int)cons1.getNumChildren(); i++ ) {
               if( !areEqual( cons1[i], cons2[i] ) ){
-                Node eq = cons1[i].getType().isBoolean() ? cons1[i].iffNode( cons2[i] ) : cons1[i].eqNode( cons2[i] );
+                Node eq = cons1[i].eqNode( cons2[i] );
                 d_pending.push_back( eq );
                 d_pending_exp[ eq ] = unifEq;
                 Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq << " by " << unifEq << std::endl;
@@ -1172,7 +1154,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
     Node rr = Rewriter::rewrite( r );
     if( s!=rr ){
       Node eq_exp = c.eqNode( s[0] );
-      Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr );
+      Node eq = s.eqNode( rr );
       Trace("datatypes-infer") << "DtInfer : collapse sel";
       Trace("datatypes-infer") << ( wrong ? " wrong" : "");
       Trace("datatypes-infer") << " : " << eq << " by " << eq_exp << std::endl;
@@ -1540,7 +1522,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
           if( children.empty() ){
             lem = n.negate();
           }else{
-            lem = NodeManager::currentNM()->mkNode( IFF, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) );
+            lem = NodeManager::currentNM()->mkNode( EQUAL, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) );
           }
           Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl;
           d_pending.push_back( lem );
@@ -1557,7 +1539,7 @@ void TheoryDatatypes::processNewTerm( Node n ){
   //see if it is rewritten to be something different
   Node rn = Rewriter::rewrite( n );
   if( rn!=n && !areEqual( rn, n ) ){
-    Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n );
+    Node eq = rn.eqNode( n );
     d_pending.push_back( eq );
     d_pending_exp[ eq ] = d_true;
     Trace("datatypes-infer") << "DtInfer : rewrite : " << eq << std::endl;
@@ -1896,7 +1878,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
   //We may need to communicate outwards if the conclusions involve other theories.  Also communicate (6) and OR conclusions.
   Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl;
   bool addLemma = false;
-  if( n.getKind()==EQUAL || n.getKind()==IFF ){
+  if( n.getKind()==EQUAL ){
     /*
     for( unsigned i=0; i<2; i++ ){
       if( !n[i].isVar() && n[i].getKind()!=APPLY_SELECTOR_TOTAL && n[i].getKind()!=APPLY_CONSTRUCTOR ){
diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp
index dcb75a44a..4f34c03c4 100644
--- a/src/theory/ite_utilities.cpp
+++ b/src/theory/ite_utilities.cpp
@@ -312,7 +312,7 @@ Node ITECompressor::push_back_boolean(Node original, Node compressed){
     d_compressed[original] = skolem;
     d_compressed[compressed] = skolem;
 
-    Node iff = skolem.iffNode(rewritten);
+    Node iff = skolem.eqNode(rewritten);
     d_assertions->push_back(iff);
     ++(d_statistics.d_skolemsAdded);
     return skolem;
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index dda3b1be4..217f7079a 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -137,7 +137,7 @@ bool BoundedIntegers::RangeModel::proxyCurrentRange() {
     if( d_ranges_proxied.find( curr )==d_ranges_proxied.end() ){
       d_ranges_proxied[curr] = true;
       Assert( d_range_literal.find( curr )!=d_range_literal.end() );
-      Node lem = NodeManager::currentNM()->mkNode( IFF, d_range_literal[curr].negate(),
+      Node lem = NodeManager::currentNM()->mkNode( EQUAL, d_range_literal[curr].negate(),
                    NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(curr) ) ) );
       Trace("bound-int-lemma") << "*** bound int : proxy lemma : " << lem << std::endl;
       d_bi->getQuantifiersEngine()->addLemma( lem );
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 1a1169578..27a52ab30 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -147,7 +147,7 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
 
             for( unsigned i=0; i<single_invoke_args[prog][k-1].size(); i++ ){
               Node arg = single_invoke_args[prog][k-1][i];
-              Node asum = NodeManager::currentNM()->mkNode( arg.getType().isBoolean() ? IFF : EQUAL, v, arg ).negate();
+              Node asum = NodeManager::currentNM()->mkNode( EQUAL, v, arg ).negate();
               Trace("cegqi-si-debug") << "  ..." << arg << " occurs in ";
               Trace("cegqi-si-debug") << single_invoke_args_from[prog][k-1][arg].size() << " invocations at position " << (k-1) << " of " << prog << "." << std::endl;
               for( unsigned j=0; j<single_invoke_args_from[prog][k-1][arg].size(); j++ ){
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index 7cefb0aec..4a86cbcd8 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -207,7 +207,7 @@ Node CegConjectureSingleInvSol::flattenITEs( Node n, bool rec ) {
       if( n0.getKind()==ITE ){
         n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ),
                                                    NodeManager::currentNM()->mkNode( AND, n0.negate(), n2 ) );
-      }else if( n0.getKind()==IFF ){
+      }else if( n0.getKind()==EQUAL ){
         n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ),
                                                    NodeManager::currentNM()->mkNode( AND, n0.negate(), n1.negate() ) );
       }else{
@@ -263,7 +263,7 @@ bool CegConjectureSingleInvSol::getAssign( bool pol, Node n, std::map< Node, boo
       }
     }else if( n.getKind()==NOT ){
       return getAssign( !pol, n[0], assign, new_assign, vars, new_vars, new_subs );
-    }else if( pol && ( n.getKind()==IFF || n.getKind()==EQUAL ) ){
+    }else if( pol && n.getKind()==EQUAL ){
       getAssignEquality( n, vars, new_vars, new_subs );
     }
   }
@@ -271,7 +271,7 @@ bool CegConjectureSingleInvSol::getAssign( bool pol, Node n, std::map< Node, boo
 }
 
 bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs ) {
-  Assert( eq.getKind()==IFF || eq.getKind()==EQUAL );
+  Assert( eq.getKind()==EQUAL );
   //try to find valid argument
   for( unsigned r=0; r<2; r++ ){
     if( std::find( d_varList.begin(), d_varList.end(), eq[r] )!=d_varList.end() ){
@@ -484,7 +484,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st
           std::map< Node, bool >::iterator it = atoms.find( atom );
           if( it==atoms.end() ){
             atoms[atom] = pol;
-            if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){
+            if( status==0 && atom.getKind()==EQUAL ){
               if( pol==( sol.getKind()==AND ) ){
                 Trace("csi-simp") << "  ...equality." << std::endl;
                 if( getAssignEquality( atom, vars, new_vars, new_subs ) ){
@@ -559,7 +559,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st
         bool red = false;
         Node atom = children[i].getKind()==NOT ? children[i][0] : children[i];
         bool pol = children[i].getKind()!=NOT;
-        if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){
+        if( status==0 && atom.getKind()==EQUAL ){
           if( pol!=( sol.getKind()==AND ) ){
             std::vector< Node > tmp_vars;
             std::vector< Node > tmp_subs;
@@ -801,15 +801,18 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in
               Node new_t;
               do{
                 new_t = Node::null();
-                if( curr.getKind()==EQUAL && ( curr[0].getType().isInteger() || curr[0].getType().isReal() ) ){
-                  new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, curr[0], curr[1] ),
-                                                                NodeManager::currentNM()->mkNode( LEQ, curr[1], curr[0] ) );
+                if( curr.getKind()==EQUAL ){
+                  TypeNode tn = curr[0].getType();
+                  if( tn.isInteger() || tn.isReal() ){
+                    new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, curr[0], curr[1] ),
+                                                                  NodeManager::currentNM()->mkNode( LEQ, curr[1], curr[0] ) );
+                  }else if( tn.isBoolean() ){
+                    new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
+                                                                  NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[1].negate() ) );
+                  }
                 }else if( curr.getKind()==ITE ){
                   new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
                                                                 NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[2] ) );
-                }else if( curr.getKind()==IFF ){
-                  new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
-                                                                NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[1].negate() ) );
                 }else if( curr.getKind()==OR || curr.getKind()==AND ){
                   new_t = TermDb::simpleNegate( curr ).negate();
                 }else if( curr.getKind()==NOT ){
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index eef354e75..50acb8834 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -251,7 +251,7 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
     }else{
       return 0;
     }
-  }else if( n.getKind()==IFF ){
+  }else if( n.getKind()==EQUAL && n[0].getType().isBoolean() ){
     int depIndex1;
     int eVal = evaluate( n[0], depIndex1, ri );
     if( eVal!=0 ){
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index cb772a31f..09fec7981 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -34,7 +34,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
   for( unsigned i=0; i<assertions.size(); i++ ){
     if( assertions[i].getKind()==FORALL ){
       if( quantifiers::TermDb::isFunDef( assertions[i] ) ){
-        Assert( assertions[i][1].getKind()==EQUAL || assertions[i][1].getKind()==IFF );
+        Assert( assertions[i][1].getKind()==EQUAL );
         Node n = assertions[i][1][0];
         Assert( n.getKind()==APPLY_UF );
         Node f = n.getOperator();
@@ -176,11 +176,7 @@ void FunDefFmf::simplifyTerm( Node n, std::vector< Node >& constraints ) {
         std::vector< Node > children;
         for( unsigned j=0; j<n.getNumChildren(); j++ ){
           Node uz = NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], z );
-          if( !n[j].getType().isBoolean() ){
-            children.push_back( uz.eqNode( n[j] ) );
-          }else{
-            children.push_back( uz.iffNode( n[j] ) );
-          }
+          children.push_back( uz.eqNode( n[j] ) );
         }
         Node bd = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );
         bd = bd.negate();
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index de8e45a84..ca4b27f1c 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -63,7 +63,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
       //we want to add the children of the NOT
       d_match_pattern = d_pattern[0];
     }
-    if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){
+    if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){
       //make sure the matching portion of the equality is on the LHS of d_pattern
       //  and record what d_match_pattern is
       if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) ||
@@ -135,7 +135,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
       }else{
         d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern );
       }
-    }else if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
+    }else if( d_match_pattern.getKind()==EQUAL ){
       //we will be producing candidates via literal matching heuristics
       if( d_pattern.getKind()!=NOT ){
         //candidates will be all equalities
@@ -144,7 +144,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
         //candidates will be all disequalities
         d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );
       }
-    }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF ||
+    }else if( d_pattern.getKind()==EQUAL || 
               d_pattern.getKind()==GEQ || d_pattern.getKind()==GT || d_pattern.getKind()==NOT ){
       Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
       if( d_pattern.getKind()==NOT ){
@@ -238,11 +238,13 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
           t_match = t;
         }
       }else{
-        if(pat.getKind()==EQUAL) {
-          Node r = NodeManager::currentNM()->mkConst( Rational(1) );
-          t_match = NodeManager::currentNM()->mkNode(PLUS, t, r);
-        }else if( pat.getKind()==IFF ){
-          t_match = NodeManager::currentNM()->mkConst( !q->areEqual( NodeManager::currentNM()->mkConst(true), t ) );
+        if( pat.getKind()==EQUAL) {
+          if( !pat[0].getType().isBoolean() ){
+            Node r = NodeManager::currentNM()->mkConst( Rational(1) );
+            t_match = NodeManager::currentNM()->mkNode(PLUS, t, r);
+          }else{
+            t_match = NodeManager::currentNM()->mkConst( !q->areEqual( NodeManager::currentNM()->mkConst(true), t ) );
+          }
         }else if( pat.getKind()==GEQ ){
           Node r = NodeManager::currentNM()->mkConst( Rational(1) );
           t_match = NodeManager::currentNM()->mkNode(PLUS, t, r);
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 249b71130..017d793e4 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -242,7 +242,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
     //well-defined function: can assume LHS is only trigger
     Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
     if( d_quantEngine->getTermDatabase()->isQAttrFunDef( f ) && options::quantFunWellDefined() ){
-      Assert( bd.getKind()==EQUAL || bd.getKind()==IFF );
+      Assert( bd.getKind()==EQUAL );
       Assert( bd[0].getKind()==APPLY_UF );
       patTermsF.push_back( bd[0] );
     }else{
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 81cd5948a..16b46b27d 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -92,7 +92,7 @@ bool QuantifierMacros::containsBadOp( Node n, Node op ){
 }
 
 bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
-  return pol && ( n.getKind()==EQUAL || n.getKind()==IFF );
+  return pol && n.getKind()==EQUAL;
 }
 
 bool QuantifierMacros::isBoundVarApplyUf( Node n ) {
@@ -132,7 +132,7 @@ void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidat
 }
 
 Node QuantifierMacros::solveInEquality( Node n, Node lit ){
-  if( lit.getKind()==IFF || lit.getKind()==EQUAL ){
+  if( lit.getKind()==EQUAL ){
     //return the opposite side of the equality if defined that way
     for( int i=0; i<2; i++ ){
       if( lit[i]==n ){
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 53f55e70b..a7d303950 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -642,7 +642,7 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
       std::vector< Node > tr_terms;
       if( lit.getKind()==APPLY_UF ){
         //only match predicates that are contrary to this one, use literal matching
-        Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false );
+        Node eq = NodeManager::currentNM()->mkNode( EQUAL, lit, !phase ? fm->d_true : fm->d_false );
         tr_terms.push_back( eq );
       }else if( lit.getKind()==EQUAL ){
         //collect trigger terms
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index d465df4c0..4e5890584 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -898,7 +898,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
         //for( unsigned i=0; i<d_children.size(); i++ ){

         //  d_children_order.push_back( i );

         //}

-        //if( !d_n.isNull() && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ) ){

+        //if( !d_n.isNull() && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==EQUAL ) ){

           //sort based on the type of the constraint : ground comes first, then literals, then others

           //MatchGenSort mgs;

           //mgs.d_mg = this;

@@ -926,7 +926,7 @@ void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbva
 

 void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ) {

   Trace("qcf-qregister-debug") << "Determine variable order " << d_n << std::endl;

-  bool isCom = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF );

+  bool isCom = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==EQUAL );

   std::map< int, std::vector< int > > c_to_vars;

   std::map< int, std::vector< int > > vars_to_c;

   std::map< int, int > vb_count;

@@ -1353,7 +1353,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
               success = true;

             }

           }

-        }else if( d_n.getKind()==IFF ){

+        }else if( d_n.getKind()==EQUAL ){

           //construct match based on both children

           if( d_child_counter%2==0 ){

             if( getChild( 0 )->getNextMatch( p, qi ) ){

@@ -1450,7 +1450,7 @@ bool MatchGen::getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vecto
       }else{

         return getChild( d_child_counter )->getExplanation( p, qi, exp );

       }

-    }else if( d_n.getKind()==IFF ){

+    }else if( d_n.getKind()==EQUAL ){

       for( unsigned i=0; i<2; i++ ){

         if( !getChild( i )->getExplanation( p, qi, exp ) ){

           return false;

@@ -1651,7 +1651,7 @@ void MatchGen::setInvalid() {
 }

 

 bool MatchGen::isHandledBoolConnective( TNode n ) {

-  return n.getType().isBoolean() && ( n.getKind()==OR || n.getKind()==AND || n.getKind()==IFF || n.getKind()==ITE || n.getKind()==FORALL || n.getKind()==NOT );

+  return n.getType().isBoolean() && ( n.getKind()==OR || n.getKind()==AND || ( n.getKind()==EQUAL && n[0].getType().isBoolean() ) || n.getKind()==ITE || n.getKind()==FORALL || n.getKind()==NOT );

 }

 

 bool MatchGen::isHandledUfTerm( TNode n ) {

@@ -1692,14 +1692,6 @@ d_qassert( c ) {
   d_false = NodeManager::currentNM()->mkConst<bool>(false);

 }

 

-Node QuantConflictFind::mkEqNode( Node a, Node b ) {

-  if( a.getType().isBoolean() ){

-    return a.iffNode( b );

-  }else{

-    return a.eqNode( b );

-  }

-}

-

 //-------------------------------------------------- registration

 

 void QuantConflictFind::registerQuantifier( Node q ) {

@@ -1733,7 +1725,7 @@ void QuantConflictFind::registerQuantifier( Node q ) {
 

 int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {

   int ret = 0;

-  if( n.getKind()==EQUAL ){

+  if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){

     Node n1 = evaluateTerm( n[0] );

     Node n2 = evaluateTerm( n[1] );

     Debug("qcf-eval") << "Evaluate : Normalize " << n << " to " << n1 << " = " << n2 << std::endl;

@@ -1775,7 +1767,8 @@ int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {
     if( ret==0 && cevc[0]!=0 && cevc[0]==cevc[1] ){

       ret = cevc[0];

     }

-  }else if( n.getKind()==IFF ){

+  //IFF to EQUAL : also evaluate as above?

+  }else if( n.getKind()==EQUAL ){

     int cev1 = evaluate( n[0] );

     if( cev1!=0 ){

       int cev2 = evaluate( n[1] );

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index b2dc680f2..f82866d7b 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -174,7 +174,6 @@ private:
   std::map< Node, Node > d_op_node;

   int d_fid_count;

   std::map< Node, int > d_fid;

-  Node mkEqNode( Node a, Node b );

 public:  //for ground terms

   Node d_true;

   Node d_false;

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 1d3bf7c2a..599b6bddb 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -198,13 +198,13 @@ void QuantArith::debugPrintMonomialSum( std::map< Node, Node >& msum, const char
 }
 
 bool QuantArith::solveEqualityFor( Node lit, Node v, Node & veq ) {
-  Assert( lit.getKind()==EQUAL || lit.getKind()==IFF );
+  Assert( lit.getKind()==EQUAL );
   //first look directly at sides
   TypeNode tn = lit[0].getType();
   for( unsigned r=0; r<2; r++ ){
     if( lit[r]==v ){
       Node olitr = lit[r==0 ? 1 : 0];
-      veq = tn.isBoolean() ? lit[r].iffNode( olitr ) : lit[r].eqNode( olitr );
+      veq = lit[r].eqNode( olitr );
       return true;
     }
   }
@@ -353,7 +353,7 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool&
   newPol = pol;
   if( n.getKind()==NOT ){
     newPol = !pol;
-  }else if( n.getKind()==IFF ){
+  }else if( n.getKind()==EQUAL ){
     newHasPol = false;
   }else if( n.getKind()==ITE ){
     if( child==0 ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index a78fa8d7b..9dc8d9225 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -53,11 +53,10 @@ bool QuantifiersRewriter::isLiteral( Node n ){
   case IMPLIES:
   case XOR:
   case ITE:
-  case IFF:
     return false;
     break;
   case EQUAL:
-    return n[0].getType()!=NodeManager::currentNM()->booleanType();
+    return !n[0].getType().isBoolean();
     break;
   default:
     break;
@@ -267,7 +266,7 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) {
     if( body.getKind()==IMPLIES ){
       return NodeManager::currentNM()->mkNode( OR, children );
     }else if( body.getKind()==XOR ){
-      return NodeManager::currentNM()->mkNode( IFF, children );
+      return NodeManager::currentNM()->mkNode( EQUAL, children );
     }else if( childrenChanged ){
       return NodeManager::currentNM()->mkNode( body.getKind(), children );
     }else{
@@ -298,7 +297,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){
             children.push_back( nc );
           }
         }
-      }else if( body[0].getKind()==IFF ){
+      }else if( body[0].getKind()==EQUAL ){
         for( int i=0; i<2; i++ ){
           Node nn = i==0 ? body[0][i] : body[0][i].notNode();
           children.push_back( computeNNF( nn ) );
@@ -592,8 +591,8 @@ Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBui
         }
         tt << pred;
         defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-      }else if( nt.getKind()==IFF ){
-        //case for IFF
+      }else if( nt.getKind()==EQUAL && nt[0].getType().isBoolean() ){
+        //case for EQUAL
         for( int i=0; i<4; i++ ){
           NodeBuilder<> tt(OR);
           tt << ( ( i==0 || i==3 ) ? nt[0].notNode() : nt[0] );
@@ -1103,11 +1102,7 @@ Node QuantifiersRewriter::rewriteRewriteRule( Node r ) {
   case kind::RR_REWRITE:
     // Equality
     pattern.push_back( head );
-    if( head.getType().isBoolean() ){
-      body = head.iffNode(body);
-    }else{
-      body = head.eqNode(body);
-    }
+    body = head.eqNode(body);
     break;
   case kind::RR_REDUCTION:
   case kind::RR_DEDUCTION:
@@ -1244,14 +1239,14 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
     //if so, we will write this node
     if( containsQuantifiers( n ) ){
       if( n.getType().isBoolean() ){
-        if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){
+        if( n.getKind()==kind::ITE || ( n.getKind()==kind::EQUAL && n[0].getType().isBoolean() ) || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){
           Node nn;
           //must remove structure
           if( n.getKind()==kind::ITE ){
             nn = NodeManager::currentNM()->mkNode( kind::AND,
                    NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
                    NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
-          }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
+          }else if( n.getKind()==kind::EQUAL || n.getKind()==kind::XOR ){
             nn = NodeManager::currentNM()->mkNode( kind::AND,
                    NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
                    NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 05e33c7b2..201d3e53d 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -234,7 +234,7 @@ void RewriteEngine::registerQuantifier( Node f ) {
       std::vector< Node > cc;
       //Node head = rr[2][0];
       //if( head!=d_true ){
-        //Node head_eq = head.getType().isBoolean() ? head.iffNode( head ) : head.eqNode( head );
+        //Node head_eq = head.eqNode( head );
         //head_eq = head_eq.negate();
         //cc.push_back( head_eq );
         //Trace("rr-register-debug") << "  head eq is " << head_eq << std::endl;
@@ -245,18 +245,13 @@ void RewriteEngine::registerQuantifier( Node f ) {
         for( unsigned j=0; j<f[2][i].getNumChildren(); j++ ){
           Node nn;
           Node nbv = NodeManager::currentNM()->mkBoundVar( f[2][i][j].getType() );
-          if( f[2][i][j].getType().isBoolean() ){
-            if( f[2][i][j].getKind()!=APPLY_UF ){
-              nn = f[2][i][j].negate();
-            }else{
-              nn = f[2][i][j].iffNode( nbv ).negate();
-              bvl.push_back( nbv );
-            }
-            //nn = f[2][i][j].negate();
+          if( f[2][i][j].getType().isBoolean() && f[2][i][j].getKind()!=APPLY_UF ){
+            nn = f[2][i][j].negate();
           }else{
             nn = f[2][i][j].eqNode( nbv ).negate();
             bvl.push_back( nbv );
           }
+          //nn = f[2][i][j].negate();
           nc.push_back( nn );
         }
         if( !nc.empty() ){
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 2e2007c0a..17cfc6618 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -279,7 +279,7 @@ TNode TermDb::evaluateTerm( TNode n ) {
 bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ) {
   Trace("term-db-eval") << "Check entailed : " << n << ", pol = " << pol << std::endl;
   Assert( n.getType().isBoolean() );
-  if( n.getKind()==EQUAL ){
+  if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
     TNode n1 = evaluateTerm( n[0], subs, subsRep );
     if( !n1.isNull() ){
       TNode n2 = evaluateTerm( n[1], subs, subsRep );
@@ -320,10 +320,11 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
       }
     }
     return !simPol;
-  }else if( n.getKind()==IFF || n.getKind()==ITE ){
+  //IFF to EQUAL: also use entailment check above?
+  }else if( n.getKind()==EQUAL || n.getKind()==ITE ){
     for( unsigned i=0; i<2; i++ ){
       if( isEntailed( n[0], subs, subsRep, i==0 ) ){
-        unsigned ch = ( n.getKind()==IFF || i==0 ) ? 1 : 2;
+        unsigned ch = ( n.getKind()==EQUAL || i==0 ) ? 1 : 2;
         bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
         return isEntailed( n[ch], subs, subsRep, reqPol );
       }
@@ -1187,7 +1188,7 @@ Node TermDb::getRewriteRule( Node q ) {
 }
 
 bool TermDb::isFunDef( Node q ) {
-  if( q.getKind()==FORALL && ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF && q.getNumChildren()==3 ){
+  if( q.getKind()==FORALL && q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF && q.getNumChildren()==3 ){
     for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
       if( q[2][i].getKind()==INST_ATTRIBUTE ){
         if( q[2][i][0].getAttribute(FunDefAttribute()) ){
@@ -1217,7 +1218,7 @@ void TermDb::computeAttributes( Node q ) {
         if( avar.getAttribute(FunDefAttribute()) ){
           Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
           d_qattr_fundef[q] = true;
-          Assert( q[1].getKind()==EQUAL || q[1].getKind()==IFF );
+          Assert( q[1].getKind()==EQUAL );
           Assert( q[1][0].getKind()==APPLY_UF );
           Node f = q[1][0].getOperator();
           if( d_fun_defs.find( f )!=d_fun_defs.end() ){
@@ -1650,12 +1651,12 @@ int TermDbSygus::getTermSize( Node n ){
 }
 
 bool TermDbSygus::isAssoc( Kind k ) {
-  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
+  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==EQUAL ||
          k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT;
 }
 
 bool TermDbSygus::isComm( Kind k ) {
-  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
+  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==EQUAL ||
          k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
 }
 
@@ -1698,7 +1699,7 @@ bool TermDbSygus::isIdempotentArg( Node n, Kind ik, int arg ) {
       return arg==1;
     }
   }else if( n==getTypeMaxValue( tn ) ){
-    if( ik==IFF || ik==BITVECTOR_AND || ik==BITVECTOR_XNOR ){
+    if( ik==EQUAL || ik==BITVECTOR_AND || ik==BITVECTOR_XNOR ){
       return true;
     }
   }
@@ -1985,15 +1986,18 @@ Node TermDbSygus::minimizeBuiltinTerm( Node n ) {
 }
 
 Node TermDbSygus::expandBuiltinTerm( Node t ){
-  if( t.getKind()==EQUAL && ( t[0].getType().isInteger() || t[0].getType().isReal() ) ){
-    return NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ),
-                                                  NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) );
+  if( t.getKind()==EQUAL ){
+    TypeNode tn = t[0].getType();
+    if( tn.isInteger() || tn.isReal() ){
+      return NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ),
+                                                    NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) );
+    }else if( tn.isBoolean() ){
+      return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
+                                                  NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) );
+    }
   }else if( t.getKind()==ITE && t.getType().isBoolean() ){
     return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
                                                  NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[2] ) );
-  }else if( t.getKind()==IFF ){
-    return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
-                                                 NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) );
   }
   return Node::null();
 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index e953e90b2..1ebcb31ef 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -248,7 +248,7 @@ bool nodeContainsVar( Node n, Node v ){
 
 Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
   if( options::relationalTriggers() ){
-    if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){
+    if( n.getKind()==EQUAL || n.getKind()==GEQ ){
       Node rtr;
       for( unsigned i=0; i<2; i++) {
         unsigned j = (i==0) ? 1 : 0;
@@ -331,7 +331,7 @@ bool Trigger::isSimpleTrigger( Node n ){
 bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ){
   if( patMap.find( n )==patMap.end() ){
     patMap[ n ] = false;
-    bool newHasPol = n.getKind()==IFF ? false : hasPol;
+    bool newHasPol = n.getKind()==EQUAL ? false : hasPol;
     bool newPol = n.getKind()==NOT ? !pol : pol;
     if( tstrt==TS_MIN_TRIGGER ){
       if( n.getKind()==FORALL ){
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 890f04aad..6e0c4681b 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -848,8 +848,7 @@ bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
 bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool reqPhasePol ){
   //Assert( !areEqual( n1, n2 ) );
   //Assert( !areDisequal( n1, n2 ) );
-  Kind knd = n1.getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
-  Node fm = NodeManager::currentNM()->mkNode( knd, n1, n2 );
+  Node fm = NodeManager::currentNM()->mkNode( EQUAL, n1, n2 );
   return addSplit( fm );
 }
 
@@ -902,7 +901,7 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
       bool nodeChanged = false;
       if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){
         bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] );
-        nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) );
+        nodes[i] = NodeManager::currentNM()->mkNode( EQUAL, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) );
         nodeChanged = true;
       }
       //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 1892ecceb..902c643a4 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1189,11 +1189,7 @@ void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
 
 void TheorySetsPrivate::conflict(TNode a, TNode b)
 {
-  if (a.getKind() == kind::CONST_BOOLEAN) {
-    d_conflictNode = explain(a.iffNode(b));
-  } else {
-    d_conflictNode = explain(a.eqNode(b));
-  }
+  d_conflictNode = explain(a.eqNode(b));
   d_external.d_out->conflict(d_conflictNode);
   Debug("sets") << "[sets] conflict: " << a << " iff " << b
                 << ", explaination " << d_conflictNode << std::endl;
@@ -1209,7 +1205,7 @@ Node TheorySetsPrivate::explain(TNode literal)
   TNode atom = polarity ? literal : literal[0];
   std::vector<TNode> assumptions;
 
-  if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+  if(atom.getKind() == kind::EQUAL) {
     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
   } else if(atom.getKind() == kind::MEMBER) {
     if( !d_equalityEngine.hasTerm(atom)) {
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 635f9856a..71a5467b1 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -79,8 +79,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
                                       B) );
   }//kind::SUBSET
 
-  case kind::EQUAL:
-  case kind::IFF: {
+  case kind::EQUAL:{
     //rewrite: t = t with true (t term)
     //rewrite: c = c' with c different from c' false (c, c' constants)
     //otherwise: sort them
@@ -98,7 +97,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
       return RewriteResponse(REWRITE_DONE, newNode);
     }
     break;
-  }//kind::IFF
+  }//kind::EQUAL
 
   case kind::SETMINUS: {
     if(node[0] == node[1]) {
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 3e705d213..23670cd9b 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -218,7 +218,7 @@ void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions){
   TNode atom = polarity ? literal : literal[0];
   unsigned ps = assumptions.size();
   std::vector< TNode > tassumptions;
-  if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+  if (atom.getKind() == kind::EQUAL) {
     if( atom[0]!=atom[1] ){
       d_equalityEngine.explainEquality(atom[0], atom[1], polarity, tassumptions);
     }
@@ -679,12 +679,7 @@ void TheoryStrings::conflict(TNode a, TNode b){
   if( !d_conflict ){
     Debug("strings-conflict") << "Making conflict..." << std::endl;
     d_conflict = true;
-    Node conflictNode;
-    if (a.getKind() == kind::CONST_BOOLEAN) {
-      conflictNode = explain( a.iffNode(b) );
-    } else {
-      conflictNode = explain( a.eqNode(b) );
-    }
+    Node conflictNode = explain( a.eqNode(b) );
     Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl;
     d_out->conflict( conflictNode );
   }
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index a8cbcfac0..4cb9b8d10 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -283,7 +283,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
         new_nodes.push_back(lencond);
       }
 
-      Node lem = NodeManager::currentNM()->mkNode(kind::IFF, nonneg.negate(),
+      Node lem = NodeManager::currentNM()->mkNode(kind::EQUAL, nonneg.negate(),
         pret.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") ))//lenp.eqNode(d_zero)
         );
       new_nodes.push_back(lem);
@@ -409,7 +409,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
         str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))),
         pret.eqNode(negone));
       new_nodes.push_back(lem);
-      /*lem = NodeManager::currentNM()->mkNode(kind::IFF,
+      /*lem = NodeManager::currentNM()->mkNode(kind::EQUAL,
         t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))),
         t.eqNode(d_zero));
       new_nodes.push_back(lem);*/
@@ -460,7 +460,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
       for(unsigned i=0; i<=9; i++) {
         chtmp[0] = i + '0';
         std::string stmp(chtmp);
-        c3cc = NodeManager::currentNM()->mkNode(kind::IFF,
+        c3cc = NodeManager::currentNM()->mkNode(kind::EQUAL,
           ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(i))),
           sx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(stmp))));
         vec_c3b.push_back(c3cc);
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index bd85b735d..2a3ac7f40 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -242,8 +242,7 @@ Node SymmetryBreaker::normInternal(TNode n, size_t level) {
         } else {
           if( (*i).getKind() == kind::OR ) {
             kids.push_back(normInternal(*i, level));
-          } else if((*i).getKind() == kind::IFF ||
-                    (*i).getKind() == kind::EQUAL) {
+          } else if((*i).getKind() == kind::EQUAL) {
             kids.push_back(normInternal(*i, level));
             if((*i)[0].isVar() ||
                (*i)[1].isVar()) {
@@ -287,8 +286,7 @@ Node SymmetryBreaker::normInternal(TNode n, size_t level) {
             first = false;
             matchingTerm = TNode::null();
             kids.push_back(normInternal(*i, level + 1));
-          } else if((*i).getKind() == kind::IFF ||
-                    (*i).getKind() == kind::EQUAL) {
+          } else if((*i).getKind() == kind::EQUAL) {
             kids.push_back(normInternal(*i, level + 1));
             if((*i)[0].isVar() ||
                (*i)[1].isVar()) {
@@ -358,7 +356,6 @@ Node SymmetryBreaker::normInternal(TNode n, size_t level) {
     return result = NodeManager::currentNM()->mkNode(k, kids);
   }
 
-  case kind::IFF:
   case kind::EQUAL:
     if(n[0].isVar() ||
        n[1].isVar()) {
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 11242569a..a7ed83482 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -207,7 +207,7 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
   eq::EqProof * eqp = d_proofEnabled ? new eq::EqProof : NULL;
-  if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+  if (atom.getKind() == kind::EQUAL) {
     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, eqp);
   } else {
     d_equalityEngine.explainPredicate(atom, polarity, assumptions, eqp);
@@ -313,10 +313,10 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
     if(n.getKind() == kind::OR && n.getNumChildren() == 2 &&
        n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 &&
        n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 &&
-       (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) &&
-       (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) &&
-       (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) &&
-       (n[1][1].getKind() == kind::EQUAL || n[1][1].getKind() == kind::IFF)) {
+       n[0][0].getKind() == kind::EQUAL &&
+       n[0][1].getKind() == kind::EQUAL &&
+       n[1][0].getKind() == kind::EQUAL &&
+       n[1][1].getKind() == kind::EQUAL) {
       // now we have (a = b && c = d) || (e = f && g = h)
 
       Debug("diamonds") << "has form of a diamond!" << endl;
@@ -373,7 +373,7 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
           (a == h && d == e) ) {
         // learn: n implies a == d
         Debug("diamonds") << "+ C holds" << endl;
-        Node newEquality = a.getType().isBoolean() ? a.iffNode(d) : a.eqNode(d);
+        Node newEquality = a.eqNode(d);
         Debug("diamonds") << "  ==> " << newEquality << endl;
         learned << n.impNode(newEquality);
       } else {
@@ -504,11 +504,7 @@ void TheoryUF::computeCareGraph() {
 
 void TheoryUF::conflict(TNode a, TNode b) {
   //TODO: create EqProof at this level if d_proofEnabled = true
-  if (a.getKind() == kind::CONST_BOOLEAN) {
-    d_conflictNode = explain(a.iffNode(b));
-  } else {
-    d_conflictNode = explain(a.eqNode(b));
-  }
+  d_conflictNode = explain(a.eqNode(b));
   d_out->conflict(d_conflictNode);
   d_conflict = true;
 }
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index 82dacb6c2..f8ffe42c5 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -32,7 +32,7 @@ class TheoryUfRewriter {
 public:
 
   static RewriteResponse postRewrite(TNode node) {
-    if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) {
+    if(node.getKind() == kind::EQUAL) {
       if(node[0] == node[1]) {
         return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
       } else if(node[0].isConst() && node[1].isConst()) {
@@ -76,7 +76,7 @@ public:
   }
 
   static RewriteResponse preRewrite(TNode node) {
-    if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) {
+    if(node.getKind() == kind::EQUAL) {
       if(node[0] == node[1]) {
         return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
       } else if(node[0].isConst() && node[1].isConst()) {
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 9cb2b5b53..37b4b6f31 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1475,6 +1475,7 @@ int StrongSolverTheoryUF::SortModel::getNumRegions(){
 }
 
 Node StrongSolverTheoryUF::SortModel::getCardinalityLiteral( int c ) {
+  Assert( c>0 );
   if( d_cardinality_literal.find( c )==d_cardinality_literal.end() ){
     d_cardinality_literal[c] = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, d_cardinality_term,
                                                                  NodeManager::currentNM()->mkConst( Rational( c ) ) );
@@ -1610,8 +1611,9 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){
       //otherwise, make equal via lemma
       if( d_card_assertions_eqv_lemma.find( lit )==d_card_assertions_eqv_lemma.end() ){
         Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] );
-        Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << lit.iffNode( eqv_lit ) << std::endl;
-        getOutputChannel().lemma( lit.iffNode( eqv_lit ) );
+        eqv_lit = lit.eqNode( eqv_lit );
+        Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl;
+        getOutputChannel().lemma( eqv_lit );
         d_card_assertions_eqv_lemma[lit] = true;
       }
     }
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index 244cb303d..aae136e84 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -168,13 +168,7 @@ void UnconstrainedSimplifier::processUnconstrained()
             if (card.isFinite() && !card.isLargeFinite() && card.getFiniteCardinality() == 2) {
               // Special case: condition is unconstrained, then and else are different, and total cardinality of the type is 2, then the result
               // is unconstrained
-              Node test;
-              if (parent.getType().isBoolean()) {
-                test = Rewriter::rewrite(parent[1].iffNode(parent[2]));
-              }
-              else {
-                test = Rewriter::rewrite(parent[1].eqNode(parent[2]));
-              }
+              Node test = Rewriter::rewrite(parent[1].eqNode(parent[2]));
               if (test == NodeManager::currentNM()->mkConst<bool>(false)) {
                 ++d_numUnconstrainedElim;
                 if (currentSub.isNull()) {
@@ -191,20 +185,37 @@ void UnconstrainedSimplifier::processUnconstrained()
         // Comparisons that return a different type - assuming domains are larger than 1, any
         // unconstrained child makes parent unconstrained as well
         case kind::EQUAL:
-          if (parent[0].getType() != parent[1].getType()) {
-            TNode other = (parent[0] == current) ? parent[1] : parent[0];
-            if (current.getType().isSubtypeOf(other.getType())) {
-              break;
+        {
+          TypeNode tn = parent[0].getType();
+          if( !tn.isBoolean() ){
+            if (tn != parent[1].getType()) {
+              TNode other = (parent[0] == current) ? parent[1] : parent[0];
+              if (current.getType().isSubtypeOf(other.getType())) {
+                break;
+              }
             }
-          }
-          if( parent[0].getType().isDatatype() ){
-            TypeNode tn = parent[0].getType();
-            const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-            if( dt.isRecursiveSingleton() ){
-              //domain size may be 1
-              break;
+            if( tn.isDatatype() ){
+              const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+              if( dt.isRecursiveSingleton() ){
+                //domain size may be 1
+                break;
+              }
+            }
+          }else{
+            if (d_unconstrained.find(parent) == d_unconstrained.end() &&
+                !d_substitutions.hasSubstitution(parent)) {
+              ++d_numUnconstrainedElim;
+              if (currentSub.isNull()) {
+                currentSub = current;
+              }
+              current = parent;
+            }
+            else {
+              currentSub = Node();
             }
+            break;
           }
+        }
         case kind::BITVECTOR_COMP:
         case kind::LT:
         case kind::LEQ:
@@ -364,7 +375,6 @@ void UnconstrainedSimplifier::processUnconstrained()
               !parent.getType().isInteger()) {
             break;
           }
-        case kind::IFF:
         case kind::XOR:
         case kind::BITVECTOR_XOR:
         case kind::BITVECTOR_XNOR:
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index dbd1dcd16..68866dfaf 100644
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -24,6 +24,7 @@
 #include "smt/options.h"
 #include "theory/rewriter.h"
 #include "theory/quantifiers/options.h"
+#include "theory/quantifiers/quant_util.h"
 
 using namespace CVC4;
 using namespace std;
@@ -433,7 +434,7 @@ void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< N
     for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
       var_bound.erase( n[0][i] );
     }
-  }else if( n.getKind()==kind::EQUAL ){
+  }else if( n.getKind()==kind::EQUAL && !n[0].getType().isBoolean() ){
     if( !hasPol || pol ){
       for( unsigned i=0; i<2; i++ ){
         if( var_bound.find( n[i] )!=var_bound.end() ){
@@ -445,14 +446,8 @@ void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< N
     }
   }
   for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    bool npol = pol;
-    bool nhasPol = hasPol;
-    if( n.getKind()==kind::NOT || ( n.getKind()==kind::IMPLIES && i==0 ) ){
-      npol = !npol;
-    }
-    if( ( n.getKind()==kind::ITE && i==0 ) || n.getKind()==kind::XOR || n.getKind()==kind::IFF ){
-      nhasPol = false;
-    }
+    bool npol, nhasPol;
+    theory::QuantPhaseReq::getPolarity( n, i, hasPol, pol, nhasPol, npol );
     processMonotonic( n[i], npol, nhasPol, var_bound );
   }
 }