X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Ftheory%2Fquantifiers%2Fematching%2Finst_strategy_e_matching.cpp;h=ce328df2e5df9d4791fe07839181715ca00b7523;hb=9e26baaaa717a5075984c63878e8bc1aa4e78b16;hp=8f671fb55eae3c3dfee5bca060953ed7fefa982a;hpb=1694c6b45dfa02ca22146755c89078bfa6b851ef;p=cvc5.git

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 8f671fb55..ce328df2e 100644
--- 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{