Add lazy strategy for bounded integers to avoid non-terminating unsat cases. Add regressions.

1 files changed, 6 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0604988d3..4deb43f42 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -941,6 +941,9 @@ void SmtEngine::setDefaults() {
       Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl;
     }
     if(! options::fmfBoundInt.wasSetByUser()) {
+      if(! options::fmfBoundIntLazy.wasSetByUser()) {
+        options::fmfBoundIntLazy.set( true );
+      }
       options::fmfBoundInt.set( true );
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
     }
@@ -1178,6 +1181,9 @@ void SmtEngine::setDefaults() {
   if( options::recurseCbqi() ){
     options::cbqi.set( true );
   }
+  if(options::fmfBoundIntLazy.wasSetByUser() && options::fmfBoundIntLazy()) {
+    options::fmfBoundInt.set( true );
+  }
   if( options::fmfBoundInt() ){
     //must have finite model finding on
     options::finiteModelFind.set( true );