1 files changed, 6 insertions, 6 deletions

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