Fix to ignore a case of triggers with no free variables.

2 files changed, 8 insertions, 4 deletions

diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index c91194239..214a4d055 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -284,7 +284,7 @@ bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) {
         return true;
       }
     }
-  }else if( isAtomicTrigger( n1 ) && isUsable( n1, q ) ){
+  }else if( isUsableAtomicTrigger( n1, q ) ){
     if( options::relationalTriggers() && n2.getKind()==INST_CONSTANT && !quantifiers::TermDb::containsTerm( n1, n2 ) ){
       return true;
     }else if( !quantifiers::TermDb::hasInstConstAttr(n2) ){
@@ -339,15 +339,18 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) {
       return rtr2;
     }
   }else{
-    bool usable = quantifiers::TermDb::getInstConstAttr(n)==q && isAtomicTrigger( n ) && isUsable( n, q );
-    Trace("trigger-debug") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==q) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl;
-    if( usable ){
+    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 Node::null();
 }
 
+bool Trigger::isUsableAtomicTrigger( Node n, Node q ) {
+  return quantifiers::TermDb::getInstConstAttr( n )==q && isAtomicTrigger( n ) && isUsable( n, q );
+}
+
 bool Trigger::isUsableTrigger( Node n, Node q ){
   Node nu = getIsUsableTrigger( n, q );
   return !nu.isNull();
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 902f73e75..a3da4d398 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -107,6 +107,7 @@ class Trigger {
   /** is usable trigger */
   static bool isUsableTrigger( Node n, Node q );
   static Node getIsUsableTrigger( Node n, Node q );
+  static bool isUsableAtomicTrigger( Node n, Node q );
   static bool isAtomicTrigger( Node n );
   static bool isAtomicTriggerKind( Kind k );
   static bool isRelationalTrigger( Node n );