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

67 files changed, 367 insertions, 400 deletions

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index cb8cd8dca..da69436f1 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -109,11 +109,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) {
   d_acm.eqNotifyNewClass(t);
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 7946fea59..f9b97d524 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -247,16 +247,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);
@@ -356,8 +354,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);
@@ -403,7 +400,7 @@ void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions, eq::E
   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, proof);
   } else {
     d_equalityEngine.explainPredicate(atom, polarity, assumptions, proof);
@@ -2235,11 +2232,7 @@ void TheoryArrays::conflict(TNode a, TNode b) {
   Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl;
   eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL;
 
-  if (a.getKind() == kind::CONST_BOOLEAN) {
-    d_conflictNode = explain(a.iffNode(b), proof);
-  } else {
-    d_conflictNode = explain(a.eqNode(b), proof);
-  }
+  d_conflictNode = explain(a.eqNode(b), proof);
 
   if (!d_inCheckModel) {
     ProofArray* proof_array = NULL;
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 77c5928f0..a1d275364 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -296,7 +296,13 @@ class TheoryArrays : public Theory {
     }
 
     bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
-      Unreachable();
+      Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
+      // Just forward to arrays
+      if (value) {
+        return d_arrays.propagate(predicate);
+      } else {
+        return d_arrays.propagate(predicate.notNode());
+      }
     }
 
     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 2726f386b..e63c224a0 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 {
@@ -377,8 +377,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));
@@ -483,8 +482,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/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 297ff6d9f..8e9116543 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..9d7b3fbd6 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -30,7 +30,6 @@ enumerator BOOLEAN_TYPE \
 
 operator NOT 1 "logical not"
 operator AND 2: "logical and (N-ary)"
-operator IFF 2 "logical equivalence (exactly two parameters)"
 operator IMPLIES 2 "logical implication (exactly two parameters)"
 operator OR 2: "logical or (N-ary)"
 operator XOR 2 "exclusive or (exactly two parameters)"
@@ -40,7 +39,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/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index d483ba105..b0f2efcda 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -56,6 +56,22 @@ Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubsti
   return PP_ASSERT_STATUS_SOLVED;
 }
 
+/*
+void TheoryBool::check(Effort level) {
+  if (done() && !fullEffort(level)) {
+    return;
+  }
+  while (!done())
+  {
+    // Get all the assertions
+    Assertion assertion = get();
+    TNode fact = assertion.assertion;
+    Trace("ajr-bool") << "Assert : " << fact << std::endl;
+  }
+  if( Theory::fullEffort(level) ){
+  }
+}  
+*/
 
 }/* CVC4::theory::booleans namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index eef379bf9..353143c43 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -35,6 +35,8 @@ public:
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
 
+  //void check(Effort);
+  
   std::string identify() const { return std::string("TheoryBool"); }
 };/* class TheoryBool */
 
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index dc5f655aa..32f69e037 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 300a2b0d4..a2fb3f3f6 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -32,7 +32,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;
   }
@@ -42,7 +42,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 af25feaa5..85adfb41c 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 bb2c403aa..934e2fffd 100644
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -194,15 +194,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]);
@@ -247,6 +238,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 a63c548a2..baa85f64b 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 b7e973928..60515b2d1 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -507,7 +507,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 36772406d..b38352b77 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -101,7 +101,7 @@ 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); 
+  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 2ceca7423..053986b8c 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -109,7 +109,7 @@ void EagerBitblaster::bbAtom(TNode node) {
   }
 
   // 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_bb);
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index fd21456ee..1477f183e 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -125,7 +125,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;
@@ -141,7 +141,7 @@ void TLazyBitblaster::bbAtom(TNode node) {
   }
 
   // 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 7200d1dec..aaa3c561d 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -383,12 +383,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 e58289568..0d58233c9 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -251,7 +251,7 @@ public:
         Trace("datatypes-rewrite-debug") << "Clash constants : " << n1 << " " << n2 << std::endl;
         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 fe07e44da..f5ae05bc3 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -492,10 +492,11 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
           rt.d_req_kind = OR;reqk = NOT;
         }else if( k==OR ){
           rt.d_req_kind = AND;reqk = NOT;
-        }else if( k==IFF ) {
+        //AJR : eliminate this if we eliminate xor
+        }else if( k==EQUAL ) {
           rt.d_req_kind = XOR;
         }else if( k==XOR ) {
-          rt.d_req_kind = IFF;
+          rt.d_req_kind = EQUAL;
         }else if( k==ITE ){
           rt.d_req_kind = ITE;reqkc[1] = NOT;reqkc[2] = NOT;
           rt.d_children[0].d_req_type = d_tds->getArgType( dt[c], 0 );
@@ -1331,7 +1332,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 3d114f9f1..8d2e5618f 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -422,7 +422,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++;
     }
@@ -507,15 +507,9 @@ void TheoryDatatypes::preRegisterTerm(TNode n) {
     d_equalityEngine.addTriggerPredicate(n);
     break;
   default:
-    // Maybe it's a predicate
-    if (n.getType().isBoolean()) {
-      // Get triggered for both equal and dis-equal
-      d_equalityEngine.addTriggerPredicate(n);
-    } else {
-      // Function applications/predicates
-      d_equalityEngine.addTerm(n);
-      //d_equalityEngine.addTriggerTerm(n, THEORY_DATATYPES);
-    }
+    // Function applications/predicates
+    d_equalityEngine.addTerm(n);
+    //d_equalityEngine.addTriggerTerm(n, THEORY_DATATYPES);
     break;
   }
   flushPendingFacts();
@@ -634,11 +628,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
 void TheoryDatatypes::addSharedTerm(TNode t) {
   Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
                      << t << " " << t.getType().isBoolean() << endl;
-  //if( t.getType().isBoolean() ){
-    //d_equalityEngine.addTriggerPredicate(t, THEORY_DATATYPES);
-  //}else{
   d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES);
-  //}
   Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl;
 }
 
@@ -703,7 +693,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++ ){
@@ -731,11 +721,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;
@@ -812,8 +798,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() );
               }
             }
@@ -835,7 +820,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;
@@ -1284,7 +1269,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
   if( !r.isNull() ){
     Node rr = Rewriter::rewrite( r );
     if( use_s!=rr ){
-      Node eq = rr.getType().isBoolean() ? use_s.iffNode( rr ) : use_s.eqNode( rr );
+      Node eq = use_s.eqNode( rr );
       Node eq_exp;
       if( options::dtRefIntro() ){
         eq_exp = d_true;
@@ -1697,7 +1682,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 );
@@ -1716,7 +1701,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;
@@ -2053,7 +2038,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
       addLemma = dt.involvesExternalType();
     }
-  }else if( n.getKind()==LEQ || n.getKind()==IFF || n.getKind()==OR ){
+  }else if( n.getKind()==LEQ || n.getKind()==OR ){
     addLemma = true;
   }
   if( addLemma ){
@@ -2110,7 +2095,7 @@ void TheoryDatatypes::printModelDebug( const char* c ){
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ){
     Node eqc = (*eqcs_i);
-    if( !eqc.getType().isBoolean() ){
+    //if( !eqc.getType().isBoolean() ){
       if( eqc.getType().isDatatype() ){
         Trace( c ) << "DATATYPE : ";
       }
@@ -2155,7 +2140,7 @@ void TheoryDatatypes::printModelDebug( const char* c ){
           Trace( c ) << std::endl;
         }
       }
-    }
+    //}
     ++eqcs_i;
   }
 }
diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp
index 126f3bfb8..419e5b4dd 100644
--- a/src/theory/ite_utilities.cpp
+++ b/src/theory/ite_utilities.cpp
@@ -313,7 +313,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/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index a00d6d8a1..a5fd34c64 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -72,7 +72,7 @@ Node AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE
       Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
       Trace("alpha-eq") << "  " << q << std::endl;
       Trace("alpha-eq") << "  " << aen->d_quant << std::endl;
-      lem = q.iffNode( aen->d_quant );
+      lem = q.eqNode( aen->d_quant );
     }else{
       //do not reduce annotated quantified formulas based on alpha equivalence 
     }
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index c488e8c23..37fbff03a 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -138,7 +138,7 @@ bool BoundedIntegers::IntRangeModel::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/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 8e8f34cac..7c9a6196f 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -227,7 +227,7 @@ Node CandidateGeneratorQELitEq::getNextCandidate(){
 CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) :
 CandidateGenerator( qe ), d_match_pattern( mpat ){
 
-  Assert( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF );
+  Assert( d_match_pattern.getKind()==EQUAL );
   d_match_pattern_type = d_match_pattern[0].getType();
 }
 
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index f4b63f929..9903f14aa 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -710,13 +710,13 @@ Node CegInstantiation::getEagerUnfold( Node n, std::map< Node, Node >& visited )
           }
           for( unsigned j=1; j<n.getNumChildren(); j++ ){
             Node nc = getEagerUnfold( n[j], visited );
-            if( var_list[j-1].getType().isBoolean() ){   
-              //TODO: remove this case when boolean term conversion is eliminated
-              Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
-              subs.push_back( nc.eqNode( c ) );
-            }else{
-              subs.push_back( nc );
-            }
+            //if( var_list[j-1].getType().isBoolean() ){   
+            //  //TODO: remove this case when boolean term conversion is eliminated
+            //  Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+            //  subs.push_back( nc.eqNode( c ) );
+            //}else{
+            subs.push_back( nc );
+            //}
             Assert( subs[j-1].getType()==var_list[j-1].getType() );
           }
           Assert( vars.size()==subs.size() );
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 44ac135a7..92d62a177 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -758,13 +758,13 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
     Assert( d_single_inv_arg_sk.size()==varList.getNumChildren() );
     for( unsigned i=0; i<d_single_inv_arg_sk.size(); i++ ){
       Trace("csi-sol") << d_single_inv_arg_sk[i] << " ";
-      if( varList[i].getType().isBoolean() ){
-        //TODO force boolean term conversion mode
-        Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
-        vars.push_back( d_single_inv_arg_sk[i].eqNode( c ) );
-      }else{
-        vars.push_back( d_single_inv_arg_sk[i] );
-      }
+      //if( varList[i].getType().isBoolean() ){
+      //  //TODO force boolean term conversion mode
+      //  Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+      //  vars.push_back( d_single_inv_arg_sk[i].eqNode( c ) );
+      //}else{
+      vars.push_back( d_single_inv_arg_sk[i] );
+      //}
       d_sol->d_varList.push_back( varList[i] );
     }
     Trace("csi-sol") << std::endl;
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index 5cc46d163..d93898a1e 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -215,7 +215,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{
@@ -271,7 +271,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 );
     }
   }
@@ -279,7 +279,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() ){
@@ -492,7 +492,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 ) ){
@@ -567,7 +567,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;
@@ -848,15 +848,19 @@ 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 ){
+                      if( 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] ) );
+                      }else if( curr[0].getType().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{
+                        new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) );
+                      }
                     }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/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 61a20ad42..3dacfca3a 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -753,6 +753,12 @@ void CegInstantiator::processAssertions() {
               Trace("cbqi-proc") << "......add substitution : " << itae2->first << " -> " << itae2->second << std::endl;
             }
           }
+        }else if( atom.getKind()==BOOLEAN_TERM_VARIABLE ){
+          if( std::find( d_aux_vars.begin(), d_aux_vars.end(), atom )!=d_aux_vars.end() ){
+            Node val = NodeManager::currentNM()->mkConst( lit.getKind()!=NOT );
+            aux_subs[ atom ] = val;
+            Trace("cbqi-proc") << "......add substitution : " << atom << " -> " << val << std::endl;
+          }
         }
       }
     }
@@ -884,7 +890,7 @@ void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited )
     d_is_nested_quant = true;
   }else if( visited.find( n )==visited.end() ){
     visited[n] = true;
-    if( TermDb::isBoolConnective( n.getKind() ) ){
+    if( TermDb::isBoolConnectiveTerm( n ) ){
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
         collectCeAtoms( n[i], visited );
       }
@@ -940,7 +946,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
 
   //remove ITEs
   IteSkolemMap iteSkolemMap;
-  d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
+  d_qe->getTheoryEngine()->getTermFormulaRemover()->run(lems, iteSkolemMap);
   //Assert( d_aux_vars.empty() );
   d_aux_vars.clear();
   d_aux_eq.clear();
@@ -965,6 +971,14 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
         }
       }
     }
+    /*else if( lems[i].getKind()==EQUAL && lems[i][0].getType().isBoolean() ){
+      //Boolean terms
+      if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][0] )!=d_aux_vars.end() ){
+        Node v = lems[i][0];
+        d_aux_eq[rlem][v] = lems[i][1];
+         Trace("cbqi-debug") << "  " << rlem << " implies " << v << " = " << lems[i][1] << std::endl;
+      } 
+    }*/
     lems[i] = rlem;
   }
   //collect atoms from all lemmas: we will only do bounds coming from original body
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index b6743724b..88b5f5fb1 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -327,7 +327,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 9109aab8a..1172fb92c 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -49,7 +49,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
       Trace("fmf-fun-def-debug") << "Process function " << n << ", body = " << bd << std::endl;
       if( !bd.isNull() ){
         d_funcs.push_back( f );
-        bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd );
+        bd = NodeManager::currentNM()->mkNode( EQUAL, n, bd );
 
         //create a sort S that represents the inputs of the function
         std::stringstream ss;
@@ -97,7 +97,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
   for( unsigned i=0; i<assertions.size(); i++ ){
     int is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end() ? 1 : 0;
     //constant boolean function definitions do not add domain constraints
-    if( is_fd==0 || ( is_fd==1 && ( assertions[i][1].getKind()==EQUAL || assertions[i][1].getKind()==IFF ) ) ){
+    if( is_fd==0 || ( is_fd==1 && assertions[i][1].getKind()==EQUAL ) ){
       std::vector< Node > constraints;
       Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is_fd = " << is_fd << std::endl;
       Node n = simplifyFormula( assertions[i], true, true, constraints, is_fd==1 ? subs_head[i] : Node::null(), is_fd );
@@ -201,11 +201,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 2a940f1fd..7cf9868bd 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -76,7 +76,7 @@ int InstMatchGenerator::getActiveScore( QuantifiersEngine * qe ) {
     unsigned ngtt = qe->getTermDatabase()->getNumTypeGroundTerms( tn );
     Trace("trigger-active-sel-debug") << "Number of ground terms for " << tn << " is " << ngtt << std::endl;
     return ngtt;
-//  }else if( d_match_pattern_getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
+//  }else if( d_match_pattern_getKind()==EQUAL ){
     
   }else{
     return -1;
@@ -90,7 +90,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       //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
       for( unsigned i=0; i<2; i++ ){
@@ -150,7 +150,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       //we will be scanning lists trying to find d_match_pattern.getOperator()
       d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern );
       //if matching on disequality, inform the candidate generator not to match on eqc
-      if( d_pattern.getKind()==NOT && ( d_pattern[0].getKind()==IFF || d_pattern[0].getKind()==EQUAL ) ){
+      if( d_pattern.getKind()==NOT && d_pattern[0].getKind()==EQUAL ){
         ((inst::CandidateGeneratorQE*)d_cg)->excludeEqc( d_eq_class_rel );
         d_eq_class_rel = Node::null();
       }
@@ -166,7 +166,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       }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 &&
               d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT ){
       //we will be producing candidates via literal matching heuristics
       if( d_pattern.getKind()!=NOT ){
@@ -253,10 +253,12 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
         }
       }else{
         if( pat.getKind()==EQUAL ){
-          Assert( t.getType().isReal() );
-          t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one);
-        }else if( pat.getKind()==IFF ){
-          t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermDatabase()->d_true, t ) );
+          if( t.getType().isBoolean() ){
+            t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermDatabase()->d_true, t ) );
+          }else{
+            Assert( t.getType().isReal() );
+            t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one);
+          }
         }else if( pat.getKind()==GEQ ){
           t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one);
         }else if( pat.getKind()==GT ){
@@ -706,7 +708,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat, Quantifier
   }else{
     d_pol = true;
   }
-  if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
+  if( d_match_pattern.getKind()==EQUAL ){
     d_eqc = d_match_pattern[1];
     d_match_pattern = d_match_pattern[0];
     Assert( !quantifiers::TermDb::hasInstConstAttr( d_eqc ) );
diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index 1f68fb787..41099552d 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -366,8 +366,13 @@ bool EqualityQueryInstProp::isPropagateLiteral( Node n ) {
     return false;
   }else{
     Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();
-    Assert( ak!=NOT );
-    return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE;
+    if( ak==EQUAL ){
+      Node atom = n.getKind() ? n[0] : n;
+      return !atom[0].getType().isBoolean();
+    }else{
+      Assert( ak!=NOT );
+      return ak!=AND && ak!=OR && ak!=ITE;
+    }
   }
 }
 
@@ -466,7 +471,7 @@ Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, s
                 addArgument( c, args, watch, is_watch );
                 abort_i = i;
                 break;
-              }else if( k==kind::AND || k==kind::OR || k==kind::ITE || k==IFF ){
+              }else if( k==kind::AND || k==kind::OR || k==kind::ITE || ( k==EQUAL && n[0].getType().isBoolean() ) ){
                 Trace("qip-eval-debug") << "Adding argument " << c << " to " << k << ", isProp = " << newHasPol << std::endl;
                 if( ( k==kind::AND || k==kind::OR  ) && c.getKind()==k ){
                   //flatten
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 895a0c93c..0023f7d0f 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -193,7 +193,7 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
                 Assert( index<(int)d_nested_qe_waitlist[q].size() );
                 Node nq = d_nested_qe_waitlist[q][index];
                 Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts );
-                Node dqelem = nq.iffNode( nqeqn ); 
+                Node dqelem = nq.eqNode( nqeqn ); 
                 Trace("cbqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl;
                 d_quantEngine->getOutputChannel().lemma( dqelem );
                 d_nested_qe_waitlist_proc[q] = index + 1;
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index c4bf61b28..f2ed81d8c 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -361,9 +361,9 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
             Assert( Trigger::isAtomicTrigger( pat ) );
             if( pat.getType().isBoolean() && rpoleq.isNull() ){
               if( options::literalMatchMode()==LITERAL_MATCH_USE ){
-                pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
+                pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
               }else if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){
-                pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==1 ) );
+                pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==1 ) );
               }
             }else{
               Assert( !rpoleq.isNull() );
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 976b81e60..96d682a77 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -147,7 +147,7 @@ bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc,
 }
 
 bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
-  return pol && ( n.getKind()==EQUAL || n.getKind()==IFF );
+  return pol && n.getKind()==EQUAL;
 }
 
 bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
@@ -211,7 +211,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 a5ec16e3a..090f2735a 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -674,7 +674,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 1e484311c..420a3d2f7 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -622,7 +622,8 @@ bool QuantInfo::isPropagatingInstance( QuantConflictFind * p, Node n ) {
   if( n.getKind()==FORALL ){
     //TODO?
     return true;
-  }else if( n.getKind()==NOT || n.getKind()==AND || n.getKind()==OR || n.getKind()==EQUAL || n.getKind()==ITE || n.getKind()==IFF ){
+  }else if( n.getKind()==NOT || n.getKind()==AND || n.getKind()==OR || n.getKind()==EQUAL || n.getKind()==ITE || 
+            ( n.getKind()==EQUAL && n[0].getType().isBoolean() ) ){
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       if( !isPropagatingInstance( p, n[i] ) ){
         return false;
@@ -1098,7 +1099,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 << ", #bvars = " << bvars.size() << std::endl;
-  bool isComm = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF );
+  bool isComm = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==EQUAL );
   if( isComm ){
     std::map< int, std::vector< int > > c_to_vars;
     std::map< int, std::vector< int > > vars_to_c;
@@ -1563,7 +1564,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 ) ){
@@ -1660,7 +1661,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;
@@ -1861,7 +1862,7 @@ void MatchGen::setInvalid() {
 }
 
 bool MatchGen::isHandledBoolConnective( TNode n ) {
-  return TermDb::isBoolConnective( n.getKind() ) && ( n.getKind()!=ITE || n.getType().isBoolean() ) && n.getKind()!=SEP_STAR;
+  return TermDb::isBoolConnectiveTerm( n ) && n.getKind()!=SEP_STAR;
 }
 
 bool MatchGen::isHandledUfTerm( TNode n ) {
@@ -1904,11 +1905,7 @@ d_conflict( c, false ) {
 }
 
 Node QuantConflictFind::mkEqNode( Node a, Node b ) {
-  if( a.getType().isBoolean() ){
-    return a.iffNode( b );
-  }else{
-    return a.eqNode( b );
-  }
+  return a.eqNode( b );
 }
 
 //-------------------------------------------------- registration
diff --git a/src/theory/quantifiers/quant_equality_engine.cpp b/src/theory/quantifiers/quant_equality_engine.cpp
index 3f89a799c..46a8b7ce2 100644
--- a/src/theory/quantifiers/quant_equality_engine.cpp
+++ b/src/theory/quantifiers/quant_equality_engine.cpp
@@ -93,7 +93,7 @@ void QuantEqualityEngine::assertNode( Node n ) {
     bool success = true;
     Node t1;
     Node t2;
-    if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL || lit.getKind()==IFF ){
+    if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL ){
       lit = getTermDatabase()->getCanonicalTerm( lit );
       Trace("qee-debug") << "Canonical :  " << lit << ", pol = " << pol << std::endl;
       if( lit.getKind()==APPLY_UF ){
@@ -102,28 +102,30 @@ void QuantEqualityEngine::assertNode( Node n ) {
         pol = true;
         lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 );
       }else if( lit.getKind()==EQUAL ){
-        t1 = lit[0];
-        t2 = lit[1];
-      }else if( lit.getKind()==IFF ){
-        if( lit[0].getKind()==NOT ){
-          t1 = lit[0][0];
-          pol = !pol;
+        if( lit[0].getType().isBoolean() ){
+          if( lit[0].getKind()==NOT ){
+            t1 = lit[0][0];
+            pol = !pol;
+          }else{
+            t1 = lit[0];
+          }
+          if( lit[1].getKind()==NOT ){
+            t2 = lit[1][0];
+            pol = !pol;
+          }else{
+            t2 = lit[1];
+          }
+          if( t1.getKind()==APPLY_UF && t2.getKind()==APPLY_UF ){
+            t1 = getFunctionAppForPredicateApp( t1 );
+            t2 = getFunctionAppForPredicateApp( t2 );
+            lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 );
+          }else{
+            success = false;
+          }
         }else{
           t1 = lit[0];
-        }
-        if( lit[1].getKind()==NOT ){
-          t2 = lit[1][0];
-          pol = !pol;
-        }else{
           t2 = lit[1];
         }
-        if( t1.getKind()==APPLY_UF && t2.getKind()==APPLY_UF ){
-          t1 = getFunctionAppForPredicateApp( t1 );
-          t2 = getFunctionAppForPredicateApp( t2 );
-          lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 );
-        }else{
-          success = false;
-        }
       }
     }else{
       success = false;
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index c0595d3d9..163c576f7 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -201,7 +201,7 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind
 }
 
 Node QuantArith::solveEqualityFor( Node lit, Node v ) {
-  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++ ){
@@ -513,7 +513,7 @@ Node QuantEPR::mkEPRAxiom( TypeNode tn ) {
     std::vector< Node > disj;
     Node x = NodeManager::currentNM()->mkBoundVar( tn );
     for( unsigned i=0; i<d_consts[tn].size(); i++ ){
-      disj.push_back( NodeManager::currentNM()->mkNode( tn.isBoolean() ? IFF : EQUAL, x, d_consts[tn][i] ) );
+      disj.push_back( NodeManager::currentNM()->mkNode( EQUAL, x, d_consts[tn][i] ) );
     }
     Assert( !disj.empty() );
     d_epr_axiom[tn] = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ), disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ) );
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index fcd8d1829..2b7e19c48 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -55,7 +55,6 @@ bool QuantifiersRewriter::isLiteral( Node n ){
   case IMPLIES:
   case XOR:
   case ITE:
-  case IFF:
     return false;
     break;
   case EQUAL:
@@ -251,7 +250,7 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) {
     k = OR;
     negCh1 = true;
   }else if( ok==XOR ){
-    k = IFF;
+    k = EQUAL;
     negCh1 = true;
   }else if( ok==NOT ){
     if( body[0].getKind()==NOT ){
@@ -265,9 +264,9 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) {
       k = OR;
       negAllCh = true;
       body = body[0];
-    }else if( body[0].getKind()==XOR || body[0].getKind()==IFF ){
-      k = IFF;
-      negCh1 = ( body[0].getKind()==IFF );
+    }else if( body[0].getKind()==XOR || ( body[0].getKind()==EQUAL && body[0][0].getType().isBoolean() ) ){
+      k = EQUAL;
+      negCh1 = ( body[0].getKind()==EQUAL );
       body = body[0];
     }else if( body[0].getKind()==ITE ){
       k = body[0].getKind();
@@ -277,7 +276,7 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) {
     }else{
       return body;
     }
-  }else if( ok!=IFF && ok!=ITE && ok!=AND && ok!=OR ){
+  }else if( ( ok!=EQUAL || !body[0].getType().isBoolean() ) && ok!=ITE && ok!=AND && ok!=OR ){
     //a literal
     return body;
   }
@@ -410,8 +409,8 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){
     }else if( res==-1 ){
       return getEntailedCond( n[2], currCond );
     }
-  }else if( n.getKind()==IFF || n.getKind()==ITE ){
-    unsigned start = n.getKind()==IFF ? 0 : 1;
+  }else if( ( n.getKind()==EQUAL && n[0].getType().isBoolean() ) || n.getKind()==ITE ){
+    unsigned start = n.getKind()==EQUAL ? 0 : 1;
     int res1 = 0;
     for( unsigned j=start; j<=(start+1); j++ ){
       int res = getEntailedCond( n[j], currCond );
@@ -423,7 +422,7 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){
         Assert( res!=0 );
         if( n.getKind()==ITE ){
           return res1==res ? res : 0;
-        }else if( n.getKind()==IFF ){
+        }else if( n.getKind()==EQUAL ){
           return res1==res ? 1 : -1;
         }
       }
@@ -512,7 +511,7 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n
     Assert( !body.isNull() );
     Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl;
     Node r = computeProcessTerms2( fbody, true, true, curr_cond, 0, cache, icache, new_vars, new_conds );
-    return Rewriter::rewrite( NodeManager::currentNM()->mkNode( h.getType().isBoolean() ? IFF : EQUAL, h, r ) );
+    return Rewriter::rewrite( NodeManager::currentNM()->mkNode( EQUAL, h, r ) );
   }else{
     return computeProcessTerms2( body, true, true, curr_cond, 0, cache, icache, new_vars, new_conds );
   }
@@ -773,7 +772,7 @@ Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){
     }
   }
   if( options::condVarSplitQuant() ){
-    if( body.getKind()==ITE || ( body.getKind()==IFF && options::condVarSplitQuantAgg() ) ){
+    if( body.getKind()==ITE || ( body.getKind()==EQUAL && body[0].getType().isBoolean() && options::condVarSplitQuantAgg() ) ){
       Assert( !qa.isFunDef() );
       Trace("quantifiers-rewrite-debug") << "Conditional var elim split " << body << "?" << std::endl;
       bool do_split = false;
@@ -1100,7 +1099,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s
               NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ),
               NodeManager::currentNM()->mkNode( kind::OR, body[0], body[2] ) );
     return computePrenex( nn, args, nargs, pol, prenexAgg );
-  }else if( prenexAgg && body.getKind()==kind::IFF ){
+  }else if( prenexAgg && body.getKind()==kind::EQUAL && body[0].getType().isBoolean() ){
     Node nn = NodeManager::currentNM()->mkNode( kind::AND,
               NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ),
               NodeManager::currentNM()->mkNode( kind::OR, body[0], body[1].notNode() ) );
@@ -1631,11 +1630,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:
@@ -1780,7 +1775,7 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
     //check if it contains a quantifier as a subterm
     //if so, we will write this node
     if( containsQuantifiers( n ) ){
-      if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || n.getKind()==kind::IFF ){
+      if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || ( n.getKind()==kind::EQUAL && n[0].getType().isBoolean() ) ){
         if( options::preSkolemQuantAgg() ){
           Node nn;
           //must remove structure
@@ -1788,12 +1783,10 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
             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 ){
             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() ) );
-          }else if( n.getKind()==kind::IMPLIES ){
-            nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
           }
           return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs );
         }
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index ec1b41a98..3e6b0ffa9 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -230,27 +230,14 @@ 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 );
-        //head_eq = head_eq.negate();
-        //cc.push_back( head_eq );
-        //Trace("rr-register-debug") << "  head eq is " << head_eq << std::endl;
-      //}
       //add patterns
       for( unsigned i=1; i<f[2].getNumChildren(); i++ ){
         std::vector< Node > nc;
         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 );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 0bdfa2d24..d394c8fef 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -267,10 +267,10 @@ void TermDb::computeUfTerms( TNode f ) {
             }else{
               if( at!=n && ee->areDisequal( at, n, false ) ){
                 std::vector< Node > lits;
-                lits.push_back( NodeManager::currentNM()->mkNode( at.getType().isBoolean() ? IFF : EQUAL, at, n ) );
+                lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at, n ) );
                 for( unsigned i=0; i<at.getNumChildren(); i++ ){
                   if( at[i]!=n[i] ){
-                    lits.push_back( NodeManager::currentNM()->mkNode( at[i].getType().isBoolean() ? IFF : EQUAL, at[i], n[i] ).negate() );
+                    lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at[i], n[i] ).negate() );
                   }
                 }
                 Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits );
@@ -484,7 +484,7 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
   Assert( !qy->extendsEngine() );
   Trace("term-db-entail") << "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 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy );
     if( !n1.isNull() ){
       TNode n2 = getEntailedTerm2( n[1], subs, subsRep, hasSubs, qy );
@@ -518,10 +518,11 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
       }
     }
     return !simPol;
-  }else if( n.getKind()==IFF || n.getKind()==ITE ){
+  //Boolean equality here
+  }else if( n.getKind()==EQUAL || n.getKind()==ITE ){
     for( unsigned i=0; i<2; i++ ){
       if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
-        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 isEntailed2( n[ch], subs, subsRep, hasSubs, reqPol, qy );
       }
@@ -1956,18 +1957,24 @@ Node TermDb::simpleNegate( Node n ){
 }
 
 bool TermDb::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==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT ||
          k==STRING_CONCAT;
 }
 
 bool TermDb::isComm( Kind k ) {
-  return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
+  return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR || 
          k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
 }
 
 bool TermDb::isBoolConnective( Kind k ) {
-  return k==OR || k==AND || k==IFF || k==ITE || k==FORALL || k==NOT || k==SEP_STAR;
+  return k==OR || k==AND || k==EQUAL || k==ITE || k==FORALL || k==NOT || k==SEP_STAR;
+}
+
+bool TermDb::isBoolConnectiveTerm( TNode n ) {
+  return isBoolConnective( n.getKind() ) &&
+         ( n.getKind()!=EQUAL || n[0].getType().isBoolean() ) && 
+         ( n.getKind()!=ITE || n.getType().isBoolean() );
 }
 
 void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
@@ -2018,7 +2025,7 @@ bool TermDb::isFunDefAnnotation( Node ipl ) {
 }
 
 Node TermDb::getFunDefHead( Node q ) {
-  //&& ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF &&
+  //&& q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF &&
   if( q.getKind()==FORALL && q.getNumChildren()==3 ){
 
     for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
@@ -2034,7 +2041,7 @@ Node TermDb::getFunDefHead( Node q ) {
 Node TermDb::getFunDefBody( Node q ) {
   Node h = getFunDefHead( q );
   if( !h.isNull() ){
-    if( q[1].getKind()==EQUAL || q[1].getKind()==IFF ){
+    if( q[1].getKind()==EQUAL ){
       if( q[1][0]==h ){
         return q[1][1];
       }else if( q[1][1]==h ){
@@ -2718,7 +2725,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;
     }
   }
@@ -3063,15 +3070,17 @@ 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 ){
+    if( 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] ) );
+    }else if( t[0].getType().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();
 }
@@ -3248,13 +3257,13 @@ void TermDbSygus::registerEvalTerm( Node n ) {
             Assert( dt.isSygus() );
             d_eval_args[n[0]].push_back( std::vector< Node >() );
             for( unsigned j=1; j<n.getNumChildren(); j++ ){
-              if( var_list[j-1].getType().isBoolean() ){
-                //TODO: remove this case when boolean term conversion is eliminated
-                Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
-                d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) );
-              }else{
+              //if( var_list[j-1].getType().isBoolean() ){
+              //  //TODO: remove this case when boolean term conversion is eliminated
+              //  Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+              //  d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) );
+              //}else{
                 d_eval_args[n[0]].back().push_back( n[j] );
-              }
+              //}
             }
             Node a = getAnchor( n[0] );
             d_subterms[a][n[0]] = true;
@@ -3297,7 +3306,7 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems
         for( unsigned i=start; i<it->second.size(); i++ ){
           Assert( vars.size()==it->second[i].size() );
           Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() );
-          Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, d_evals[n][i], sBTerm ); 
+          Node lem = NodeManager::currentNM()->mkNode(EQUAL, d_evals[n][i], sBTerm ); 
           lem = NodeManager::currentNM()->mkNode( OR, antec, lem );
           Trace("sygus-eager") << "Lemma : " << lem << std::endl;
           lems.push_back( lem );
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index d4fdaa5e5..9f43c1d35 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -499,6 +499,8 @@ public:
   static bool isComm( Kind k );
   /** is bool connective */
   static bool isBoolConnective( Kind k );
+  /** is bool connective term */
+  static bool isBoolConnectiveTerm( TNode n );
 
 //for sygus
 private:
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 7ab9f7065..cca6543b6 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -255,7 +255,7 @@ Node Trigger::getIsUsableEq( Node q, Node n ) {
   Assert( isRelationalTrigger( n ) );
   for( unsigned i=0; i<2; i++) {
     if( isUsableEqTerms( q, n[i], n[1-i] ) ){
-      if( i==1 && ( n.getKind()==EQUAL || n.getKind()==IFF ) && !quantifiers::TermDb::hasInstConstAttr(n[0]) ){
+      if( i==1 && n.getKind()==EQUAL && !quantifiers::TermDb::hasInstConstAttr(n[0]) ){
         return NodeManager::currentNM()->mkNode( n.getKind(), n[1], n[0] );  
       }else{
         return n;
@@ -292,7 +292,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) {
     n = n[0];
   }
   if( n.getKind()==INST_CONSTANT ){
-    return pol ? n : NodeManager::currentNM()->mkNode( IFF, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
+    return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
   }else if( isRelationalTrigger( n ) ){
     Node rtr = getIsUsableEq( q, n );
     if( rtr.isNull() && n[0].getType().isReal() ){
@@ -331,7 +331,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) {
   }else{
     Trace("trigger-debug") << n << " usable : " << ( quantifiers::TermDb::getInstConstAttr(n)==q ) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl;
     if( isUsableAtomicTrigger( n, q ) ){
-      return pol ? n : NodeManager::currentNM()->mkNode( IFF, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
+      return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
     }
   }
   return Node::null();
@@ -362,7 +362,7 @@ bool Trigger::isRelationalTrigger( Node n ) {
 }
 
 bool Trigger::isRelationalTriggerKind( Kind k ) {
-  return k==EQUAL || k==IFF || k==GEQ;
+  return k==EQUAL || k==GEQ;
 }
   
 bool Trigger::isCbqiKind( Kind k ) {
@@ -377,7 +377,7 @@ bool Trigger::isCbqiKind( Kind k ) {
 
 bool Trigger::isSimpleTrigger( Node n ){
   Node t = n.getKind()==NOT ? n[0] : n;
-  if( t.getKind()==IFF || t.getKind()==EQUAL ){
+  if( t.getKind()==EQUAL ){
     if( !quantifiers::TermDb::hasInstConstAttr( t[1] ) ){
       t = t[0];
     }
@@ -416,7 +416,7 @@ bool Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited,
           Assert( nu.getKind()!=NOT );
           Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl;
           Node reqEq;
-          if( nu.getKind()==IFF || nu.getKind()==EQUAL ){
+          if( nu.getKind()==EQUAL ){
             if( isAtomicTrigger( nu[0] ) && !quantifiers::TermDb::hasInstConstAttr(nu[1]) ){
               if( hasPol ){
                 reqEq = nu[1];
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 573c97f00..ba50f9ead 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1275,8 +1275,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 );
 }
 
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 87080ec18..0df122571 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -91,7 +91,7 @@ Node Rewriter::rewrite(TNode node) {
 Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
 
 #ifdef CVC4_ASSERTIONS
-  bool isEquality = node.getKind() == kind::EQUAL;
+  bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
 
   if(s_rewriteStack == NULL) {
     s_rewriteStack = new std::hash_set<Node, NodeHashFunction>();
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 55279e485..81afc0da2 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -121,7 +121,7 @@ void TheorySep::explain(TNode literal, std::vector<TNode>& assumptions) {
     // Do the work
     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) {
       d_equalityEngine.explainEquality( atom[0], atom[1], polarity, assumptions, NULL );
     } else {
       d_equalityEngine.explainPredicate( atom, polarity, assumptions );
@@ -260,7 +260,7 @@ void TheorySep::postProcessModel( TheoryModel* m ){
     }
     Node nil = getNilRef( it->first );
     Node vnil = d_valuation.getModel()->getRepresentative( nil );
-    m_neq = NodeManager::currentNM()->mkNode( nil.getType().isBoolean() ? kind::IFF : kind::EQUAL, nil, vnil );
+    m_neq = NodeManager::currentNM()->mkNode( kind::EQUAL, nil, vnil );
     Trace("sep-model") << "sep.nil = " << vnil << std::endl;
     Trace("sep-model") << std::endl;
     if( sep_children.empty() ){
@@ -451,7 +451,7 @@ void TheorySep::check(Effort e) {
               d_out->requirePhase( lit, true );
               d_neg_guards.push_back( lit );
               d_guard_to_assertion[lit] = s_atom;
-              //Node lem = NodeManager::currentNM()->mkNode( kind::IFF, lit, conc );
+              //Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, lit, conc );
               Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit.negate(), conc );
               Trace("sep-lemma") << "Sep::Lemma : (neg) reduction : " << lem << std::endl;
               d_out->lemma( lem );
@@ -840,12 +840,7 @@ Node TheorySep::getNextDecisionRequest( unsigned& priority ) {
 
 void TheorySep::conflict(TNode a, TNode b) {
   Trace("sep-conflict") << "Sep::conflict : " << a << " " << b << std::endl;
-  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));
   d_conflict = true;
   d_out->conflict( conflictNode );
 }
@@ -1164,7 +1159,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
         Node e = d_type_references_card[tn][r];
         //ensure that it is distinct from all other references so far
         for( unsigned j=0; j<d_type_references_all[tn].size(); j++ ){
-          Node eq = NodeManager::currentNM()->mkNode( e.getType().isBoolean() ? kind::IFF : kind::EQUAL, e, d_type_references_all[tn][j] );
+          Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, e, d_type_references_all[tn][j] );
           d_out->lemma( eq.negate() );
         }
         d_type_references_all[tn].push_back( e );
@@ -1429,7 +1424,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
         std::map< Node, Node >::iterator it = pto_model.find( vr );
         if( it!=pto_model.end() ){
           if( n[1]!=it->second ){
-            children.push_back( NodeManager::currentNM()->mkNode( n[1].getType().isBoolean() ? kind::IFF : kind::EQUAL, n[1], it->second ) );
+            children.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[1], it->second ) );
           }
         }else{
           Trace("sep-inst-debug") << "Data for " << vr << " was not specified, do not add condition." << std::endl;
diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
index 48523cd06..8e9939f61 100644
--- a/src/theory/sep/theory_sep_rewriter.cpp
+++ b/src/theory/sep/theory_sep_rewriter.cpp
@@ -139,8 +139,7 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) {
       }
       break;
     }
-    case kind::EQUAL:
-    case kind::IFF: {
+    case kind::EQUAL: {
       if(node[0] == node[1]) {
         return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
       }
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index edd63bddc..c14ef02b2 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -778,7 +778,7 @@ void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) {
                       }
                       if( x!=itnm2->second[xr][0] ){
                         Assert( d_equalityEngine.areEqual( x, itnm2->second[xr][0] ) );
-                        exp.push_back( NodeManager::currentNM()->mkNode( x.getType().isBoolean() ? kind::IFF : kind::EQUAL, x, itnm2->second[xr][0] ) );
+                        exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, x, itnm2->second[xr][0] ) );
                       }
                       valid = true;
                     }
@@ -866,7 +866,7 @@ void TheorySetsPrivate::checkDisequalities( std::vector< Node >& lemmas ) {
           Node x = NodeManager::currentNM()->mkSkolem("sde_", elementType);
           Node mem1 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[0] );
           Node mem2 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[1] );
-          Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq, NodeManager::currentNM()->mkNode( kind::IFF, mem1, mem2 ).negate() );
+          Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq, NodeManager::currentNM()->mkNode( kind::EQUAL, mem1, mem2 ).negate() );
           lem = Rewriter::rewrite( lem );
           assertInference( lem, d_emp_exp, lemmas, "diseq", 1 );
           flushLemmas( lemmas );
@@ -1901,11 +1901,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;
@@ -1922,7 +1918,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_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index db29843d8..09865647e 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -992,7 +992,7 @@ int TheorySetsRels::EqcInfo::counter        = 0;
       }
       Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements);
       tuple_reduct = NodeManager::currentNM()->mkNode(kind::MEMBER,tuple_reduct, n[1]);
-      Node tuple_reduction_lemma = NodeManager::currentNM()->mkNode(kind::IFF, n, tuple_reduct);
+      Node tuple_reduction_lemma = NodeManager::currentNM()->mkNode(kind::EQUAL, n, tuple_reduct);
       sendLemma(tuple_reduction_lemma, d_trueNode, "tuple-reduction");
       d_symbolic_tuples.insert(n);
     }
@@ -1097,7 +1097,7 @@ int TheorySetsRels::EqcInfo::counter        = 0;
     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) {
       d_eqEngine->explainEquality(atom[0], atom[1], polarity, assumptions);
     } else if(atom.getKind() == kind::MEMBER) {
       if( !d_eqEngine->hasTerm(atom)) {
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index d21e3fd67..aaf71e8fc 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -191,8 +191,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
@@ -210,7 +209,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
       return RewriteResponse(REWRITE_DONE, newNode);
     }
     break;
-  }//kind::IFF
+  }
 
   case kind::SETMINUS: {
     if(node[0] == node[1]) {
diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index 1f8ec7ee4..6dabf9a13 100644
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -371,7 +371,7 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound, std::map<
     Trace("sort-inference-debug") << "...Process " << n << std::endl;
 
     int retType;
-    if( n.getKind()==kind::EQUAL ){
+    if( n.getKind()==kind::EQUAL && !n[0].getType().isBoolean() ){
       Trace("sort-inference-debug") << "For equality " << n << ", set equal types from : " << n[0].getType() << " " << n[1].getType() << std::endl;
       //if original types are mixed (e.g. Int/Real), don't commit type equality in either direction
       if( n[0].getType()!=n[1].getType() ){
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 2bce8beea..09cc3cb3b 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -257,7 +257,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] ){
       Assert( hasTerm( atom[0] ) );
       Assert( hasTerm( atom[1] ) );
@@ -402,7 +402,7 @@ int TheoryStrings::getReduction( int effort, Node n, Node& nr ) {
           std::vector< Node > new_nodes;
           Node res = d_preproc.simplify( n, new_nodes );
           Assert( res!=n );
-          new_nodes.push_back( NodeManager::currentNM()->mkNode( res.getType().isBoolean() ? kind::IFF : kind::EQUAL, res, n ) );
+          new_nodes.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, res, n ) );
           Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes );
           nnlem = Rewriter::rewrite( nnlem );
           Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl;
@@ -820,11 +820,7 @@ void TheoryStrings::conflict(TNode a, TNode b){
     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) );
-    }
+    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 c8fe1fb00..d8d8e393c 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -176,7 +176,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);
@@ -300,7 +300,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);*/
@@ -351,7 +351,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/theory.cpp b/src/theory/theory.cpp
index 2d8ea9fa8..340ab2373 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -88,7 +88,13 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
   switch(mode) {
   case THEORY_OF_TYPE_BASED:
     // Constants, variables, 0-ary constructors
-    if (node.isVar() || node.isConst()) {
+    if (node.isVar()) {
+      if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){
+        tid = THEORY_UF;
+      }else{
+        tid = Theory::theoryOf(node.getType());
+      }
+    }else if (node.isConst()) {
       tid = Theory::theoryOf(node.getType());
     } else if (node.getKind() == kind::EQUAL) {
       // Equality is owned by the theory that owns the domain
@@ -105,8 +111,13 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
         // We treat the variables as uninterpreted
         tid = s_uninterpretedSortOwner;
       } else {
-        // Except for the Boolean ones, which we just ignore anyhow
-        tid = theory::THEORY_BOOL;
+        if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){
+          //Boolean vars go to UF
+          tid = THEORY_UF;
+        }else{
+          // Except for the Boolean ones
+          tid = THEORY_BOOL;
+        }
       }
     } else if (node.isConst()) {
       // Constants go to the theory of the type
@@ -408,7 +419,7 @@ bool ExtTheory::doInferencesInternal( int effort, std::vector< Node >& terms, st
           nred.push_back( n );
         }else{
           if( !nr.isNull() && n!=nr ){
-            Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? kind::IFF : kind::EQUAL, n, nr );
+            Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, n, nr );
             if( sendLemma( lem, true ) ){
               Trace("extt-lemma") << "ExtTheory : Reduction lemma : " << lem << std::endl;
               addedLemma = true;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8da1dfc1b..7c1b02f47 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -121,13 +121,15 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori
     }
     break;
 
-  case kind::IFF:
-    if (!negated) {
-      registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1].negate()), originalLemma, false, theoryId);
-      registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId);
-    } else {
-      registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1]), originalLemma, false, theoryId);
-      registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId);
+  case kind::EQUAL:
+    if( nnLemma[0].getType().isBoolean() ){
+      if (!negated) {
+        registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1].negate()), originalLemma, false, theoryId);
+        registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId);
+      } else {
+        registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1]), originalLemma, false, theoryId);
+        registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId);
+      }
     }
     break;
 
@@ -266,7 +268,7 @@ void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
 
 TheoryEngine::TheoryEngine(context::Context* context,
                            context::UserContext* userContext,
-                           RemoveITE& iteRemover,
+                           RemoveTermFormulas& iteRemover,
                            const LogicInfo& logicInfo,
                            LemmaChannels* channels)
 : d_propEngine(NULL),
@@ -292,7 +294,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_propagatedLiterals(context),
   d_propagatedLiteralsIndex(context, 0),
   d_atomRequests(context),
-  d_iteRemover(iteRemover),
+  d_tform_remover(iteRemover),
   d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
   d_true(),
   d_false(),
@@ -327,7 +329,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   ProofManager::currentPM()->initTheoryProofEngine();
 #endif
 
-  d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor());
+  d_iteUtilities = new ITEUtilities(d_tform_remover.getContainsVisitor());
 
   smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded);
 }
@@ -1754,8 +1756,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   Node ppNode = preprocess ? this->preprocess(node) : Node(node);
 
   // Remove the ITEs
+  Debug("ite") << "Remove ITE from " << ppNode << std::endl;
   additionalLemmas.push_back(ppNode);
-  d_iteRemover.run(additionalLemmas, iteSkolemMap);
+  d_tform_remover.run(additionalLemmas, iteSkolemMap);
+  Debug("ite") << "..done " << additionalLemmas[0] << std::endl;
   additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]);
 
   if(Debug.isOn("lemma-ites")) {
@@ -1923,7 +1927,7 @@ void TheoryEngine::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
 
 Node TheoryEngine::ppSimpITE(TNode assertion)
 {
-  if (!d_iteRemover.containsTermITE(assertion)) {
+  if (!d_tform_remover.containsTermITE(assertion)) {
     return assertion;
   } else {
     Node result = d_iteUtilities->simpITE(assertion);
@@ -1964,7 +1968,7 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
         Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl;
         d_iteUtilities->clear();
         Rewriter::clearCaches();
-        d_iteRemover.garbageCollect();
+        d_tform_remover.garbageCollect();
         nm->reclaimZombiesUntil(options::zombieHuntThreshold());
         Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl;
       }
@@ -1975,7 +1979,7 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
   if(d_logicInfo.isTheoryEnabled(theory::THEORY_ARITH)
      && !options::incrementalSolving() ){
     if(!simpDidALotOfWork){
-      ContainsTermITEVisitor& contains = *d_iteRemover.getContainsVisitor();
+      ContainsTermITEVisitor& contains = *d_tform_remover.getContainsVisitor();
       arith::ArithIteUtils aiteu(contains, d_userContext, getModel());
       bool anyItes = false;
       for(size_t i = 0;  i < assertions.size(); ++i){
@@ -2109,7 +2113,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
     }
 
     Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << endl;
-    Assert(explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially");
+    Assert( explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially");
     // Mark the explanation
     NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp);
     explanationVector.push_back(newExplain);
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 3273b3d19..7ce8345f7 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -97,7 +97,7 @@ namespace theory {
 }/* CVC4::theory namespace */
 
 class DecisionEngine;
-class RemoveITE;
+class RemoveTermFormulas;
 class UnconstrainedSimplifier;
 
 /**
@@ -439,7 +439,7 @@ class TheoryEngine {
   /** Enusre that the given atoms are send to the given theory */
   void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
 
-  RemoveITE& d_iteRemover;
+  RemoveTermFormulas& d_tform_remover;
 
   /** sort inference module */
   SortInference d_sortInfer;
@@ -461,7 +461,7 @@ public:
 
   /** Constructs a theory engine */
   TheoryEngine(context::Context* context, context::UserContext* userContext,
-               RemoveITE& iteRemover, const LogicInfo& logic,
+               RemoveTermFormulas& iteRemover, const LogicInfo& logic,
                LemmaChannels* channels);
 
   /** Destroys a theory engine */
@@ -850,7 +850,7 @@ public:
 
   theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
 
-  RemoveITE* getIteRemover() { return &d_iteRemover; }
+  RemoveTermFormulas* getTermFormulaRemover() { return &d_tform_remover; }
 
   SortInference* getSortInference() { return &d_sortInfer; }
 
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 5d929a708..f7084bec3 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -230,8 +230,8 @@ EqualityNodeId EqualityEngine::newNode(TNode node) {
   d_isConstant.push_back(false);
   // No terms to evaluate by defaul
   d_subtermsToEvaluate.push_back(0);
-  // Mark Boolean nodes
-  d_isBoolean.push_back(false);
+  // Mark equality nodes
+  d_isEquality.push_back(false);
   // Mark the node as internal by default
   d_isInternal.push_back(true);
   // Add the equality node to the nodes
@@ -329,10 +329,10 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
     d_isConstant[result] = !isOperator && t.isConst();
   }
 
-  if (t.getType().isBoolean()) {
+  if (t.getKind() == kind::EQUAL) {
     // We set this here as this only applies to actual terms, not the
     // intermediate application terms
-    d_isBoolean[result] = true;
+    d_isEquality[result] = true;
   } else if (d_constantsAreTriggers && d_isConstant[result]) {
     // Non-Boolean constants are trigger terms for all tags
     EqualityNodeId tId = getNodeId(t);
@@ -613,7 +613,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
 
   // Update class2 table lookup and information if not a boolean
   // since booleans can't be in an application
-  if (!d_isBoolean[class2Id]) {
+  if (!d_isEquality[class2Id]) {
     Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl;
     do {
       // Get the current node
@@ -869,7 +869,7 @@ void EqualityEngine::backtrack() {
     d_nodeIndividualTrigger.resize(d_nodesCount);
     d_isConstant.resize(d_nodesCount);
     d_subtermsToEvaluate.resize(d_nodesCount);
-    d_isBoolean.resize(d_nodesCount);
+    d_isEquality.resize(d_nodesCount);
     d_isInternal.resize(d_nodesCount);
     d_equalityGraph.resize(d_nodesCount);
     d_equalityNodes.resize(d_nodesCount);
@@ -1268,7 +1268,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
             } else {
               eqp->d_id = MERGED_THROUGH_TRANS;
               eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() );
-              eqp->d_node = NodeManager::currentNM()->mkNode(d_nodes[t1Id].getType().isBoolean() ? kind::IFF : kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]);
+              eqp->d_node = NodeManager::currentNM()->mkNode(kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]);
             }
 
             eqp->debug_print("pf::ee", 1);
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 18e83bd1a..46ec7403b 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -464,7 +464,7 @@ private:
   /**
    * Map from ids to whether they are Boolean.
    */
-  std::vector<bool> d_isBoolean;
+  std::vector<bool> d_isEquality;
 
   /**
    * Map from ids to whether the nods is internal. An internal node is a node
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index 888fa140f..e2d740e20 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -15,6 +15,8 @@ parameterized APPLY_UF VARIABLE 1: "application of an uninterpreted function; fi
 
 typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule
 
+variable BOOLEAN_TERM_VARIABLE "Boolean term variable"
+
 operator CARDINALITY_CONSTRAINT 2 "cardinality constraint on sort S: first parameter is (any) term of sort S, second is a positive integer constant k that bounds the cardinality of S"
 typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule
 
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index ed5d99bdf..ca7284689 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -246,8 +246,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()) {
@@ -291,8 +290,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()) {
@@ -361,8 +359,7 @@ Node SymmetryBreaker::normInternal(TNode n, size_t level) {
     sort(kids.begin(), kids.end());
     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 4cdc5e240..e4a3ac78c 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -139,14 +139,14 @@ void TheoryUF::check(Effort level) {
     }
   }
 
-
-  if (d_thss != NULL && ! d_conflict) {
-    d_thss->check(level);
-    if( d_thss->isConflict() ){
-      d_conflict = true;
+  if(! d_conflict ){
+    if (d_thss != NULL) {
+      d_thss->check(level);
+      if( d_thss->isConflict() ){
+        d_conflict = true;
+      }
     }
   }
-
 }/* TheoryUF::check() */
 
 void TheoryUF::preRegisterTerm(TNode node) {
@@ -217,7 +217,7 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqPro
   // Do the work
   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) {
     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf);
   } else {
     d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf);
@@ -336,10 +336,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;
@@ -396,7 +396,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 {
@@ -533,12 +533,7 @@ void TheoryUF::computeCareGraph() {
 
 void TheoryUF::conflict(TNode a, TNode b) {
   eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL;
-
-  if (a.getKind() == kind::CONST_BOOLEAN) {
-    d_conflictNode = explain(a.iffNode(b),pf);
-  } else {
-    d_conflictNode = explain(a.eqNode(b),pf);
-  }
+  d_conflictNode = explain(a.eqNode(b),pf);
   ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL;
   d_out->conflict(d_conflictNode, puf);
   d_conflict = true;
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 0900b4c90..ce9c70ca2 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -82,27 +82,27 @@ public:
     }
 
     void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
-      Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
+      Debug("uf-notify") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
       d_uf.conflict(t1, t2);
     }
 
     void eqNotifyNewClass(TNode t) {
-      Debug("uf") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
+      Debug("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl;
       d_uf.eqNotifyNewClass(t);
     }
 
     void eqNotifyPreMerge(TNode t1, TNode t2) {
-      Debug("uf") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl;
+      Debug("uf-notify") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl;
       d_uf.eqNotifyPreMerge(t1, t2);
     }
 
     void eqNotifyPostMerge(TNode t1, TNode t2) {
-      Debug("uf") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl;
+      Debug("uf-notify") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl;
       d_uf.eqNotifyPostMerge(t1, t2);
     }
 
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
-      Debug("uf") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl;
+      Debug("uf-notify") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl;
       d_uf.eqNotifyDisequal(t1, t2, reason);
     }
 
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index 166d11451..bce6003eb 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 6b89c3524..51648fb26 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -639,7 +639,7 @@ void SortModel::assertDisequal( Node a, Node b, Node reason ){
       int bi = d_regions_map[b];
       if( !d_regions[ai]->isDisequal( a, b, ai==bi ) ){
         Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..." << std::endl;
-        //if( reason.getKind()!=NOT || ( reason[0].getKind()!=EQUAL && reason[0].getKind()!=IFF ) ||
+        //if( reason.getKind()!=NOT || reason[0].getKind()!=EQUAL ||
         //    a!=reason[0][0] || b!=reason[0][1] ){
         //  Notice() << "Assert disequal " << a << " != " << b << ", reason = " << reason << "..." << std::endl;
         //}
@@ -1861,8 +1861,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 8284f6ff4..57d95d801 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -121,6 +121,7 @@ void UnconstrainedSimplifier::processUnconstrained()
     parent = d_visitedOnce[current];
     if (!parent.isNull()) {
       swap = isSigned = strict = false;
+      bool checkParent = false;
       switch (parent.getKind()) {
 
         // If-then-else operator - any two unconstrained children makes the parent unconstrained
@@ -170,13 +171,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()) {
@@ -207,6 +202,10 @@ void UnconstrainedSimplifier::processUnconstrained()
               break;
             }
           }
+          if( parent[0].getType().isBoolean() ){
+            checkParent = true;
+            break;
+          }
         case kind::BITVECTOR_COMP:
         case kind::LT:
         case kind::LEQ:
@@ -271,17 +270,7 @@ void UnconstrainedSimplifier::processUnconstrained()
             }
           }
           if (allUnconstrained) {
-            if (d_unconstrained.find(parent) == d_unconstrained.end() &&
-                !d_substitutions.hasSubstitution(parent)) {
-              ++d_numUnconstrainedElim;
-              if (currentSub.isNull()) {
-                currentSub = current;
-              }
-              current = parent;
-            }
-            else {
-              currentSub = Node();
-            }
+            checkParent = true;
           }
         }
         break;
@@ -310,17 +299,7 @@ void UnconstrainedSimplifier::processUnconstrained()
             }
           }
           if (allUnconstrained && allDifferent) {
-            if (d_unconstrained.find(parent) == d_unconstrained.end() &&
-                !d_substitutions.hasSubstitution(parent)) {
-              ++d_numUnconstrainedElim;
-              if (currentSub.isNull()) {
-                currentSub = current;
-              }
-              current = parent;
-            }
-            else {
-              currentSub = Node();
-            }
+            checkParent = true;
           }
           break;
         }
@@ -366,23 +345,12 @@ void UnconstrainedSimplifier::processUnconstrained()
               !parent.getType().isInteger()) {
             break;
           }
-        case kind::IFF:
         case kind::XOR:
         case kind::BITVECTOR_XOR:
         case kind::BITVECTOR_XNOR:
         case kind::BITVECTOR_PLUS:
         case kind::BITVECTOR_SUB:
-          if (d_unconstrained.find(parent) == d_unconstrained.end() &&
-              !d_substitutions.hasSubstitution(parent)) {
-            ++d_numUnconstrainedElim;
-            if (currentSub.isNull()) {
-              currentSub = current;
-            }
-            current = parent;
-          }
-          else {
-            currentSub = Node();
-          }
+          checkParent = true;
           break;
 
         // Multiplication/division: must be non-integer and other operand must be non-zero
@@ -486,17 +454,7 @@ void UnconstrainedSimplifier::processUnconstrained()
           if (done) {
             break;
           }
-          if (d_unconstrained.find(parent) == d_unconstrained.end() &&
-              !d_substitutions.hasSubstitution(parent)) {
-            ++d_numUnconstrainedElim;
-            if (currentSub.isNull()) {
-              currentSub = current;
-            }
-            current = parent;
-          }
-          else {
-            currentSub = Node();
-          }
+          checkParent = true;
           break;
         }
 
@@ -671,6 +629,20 @@ void UnconstrainedSimplifier::processUnconstrained()
         default:
           break;
       }
+      if( checkParent ){
+        //run for various cases from above
+        if (d_unconstrained.find(parent) == d_unconstrained.end() &&
+            !d_substitutions.hasSubstitution(parent)) {
+          ++d_numUnconstrainedElim;
+          if (currentSub.isNull()) {
+            currentSub = current;
+          }
+          current = parent;
+        }
+        else {
+          currentSub = Node();
+        }
+      }
       if (current == parent && d_visited[parent] == 1) {
         d_unconstrained.insert(parent);
         continue;