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.

23 files changed, 164 insertions, 153 deletions

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];