Bug fixes for bounded integer quantification. Current best strategy is to turn off MBQI. Disable relevant triggers by default.

1 files changed, 10 insertions, 0 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 628f8b14a..fa7b4e342 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -181,6 +181,16 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){
   }else{
     d_performCheck = true;
   }
+  static int ierCounter2 = 0;
+  if( e==Theory::EFFORT_LAST_CALL ){
+    ierCounter2++;
+    //with bounded integers, skip every other last call,
+    // since matching loops may occur with infinite quantification
+    if( ierCounter2%2==0 && options::fmfBoundInt() ){
+      d_performCheck = false;
+    }
+  }
+
   return d_performCheck;
 }