Simplify quantifiers strategy for when to apply last call effort check with fmfBound (#4673)

There was a strategy in place for alternating which rounds quantifier instantiation would run on when --fmf-bound is enabled.

However, this made it so that in some cases, no instantiation strategy would be applied, if e.g. fmfBound was enabled but no quantified formulas were handled by that strategy.

It is not clear if this strategy is a good idea, considering all use cases of quantifiers, and hence this PR deletes this block of code.

This makes it so that several eqrange benchmarks are answered "unsat" quickly.

1 files changed, 0 insertions, 7 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index f38d2fbdb..6dce6ce1e 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1091,13 +1091,6 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   {
     performCheck = true;
   }
-  if( e==Theory::EFFORT_LAST_CALL ){
-    //with bounded integers, skip every other last call,
-    // since matching loops may occur with infinite quantification
-    if( d_ierCounter_lc%2==0 && options::fmfBound() ){
-      performCheck = false;
-    }
-  }
   return performCheck;
 }