Fixes for relational triggers (#2967)

[cvc5.git] / src / theory / quantifiers / ematching / inst_strategy_e_matching.cpp

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 8f671fb55eae3c3dfee5bca060953ed7fefa982a..ce328df2e5df9d4791fe07839181715ca00b7523 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -325,7 +325,10 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         }
       }
       int curr_w = Trigger::getTriggerWeight( patTermsF[i] );
-      if( ntrivTriggers && !newVar && last_weight!=-1 && curr_w>last_weight ){
+      // triggers whose value is maximum (2) are considered expendable.
+      if (ntrivTriggers && !newVar && last_weight != -1 && curr_w > last_weight
+          && curr_w >= 2)
+      {
         Trace("auto-gen-trigger-debug") << "...exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl;
         rmPatTermsF[patTermsF[i]] = true;
       }else{