1 files changed, 0 insertions, 11 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index abd44dac7..4ce4b8db8 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -852,17 +852,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     options::finiteModelFind.set(true);
   }
 
-  // if it contains a theory with non-termination, do not strictly enforce that
-  // quantifiers and theory combination must be interleaved
-  if (logic.isTheoryEnabled(THEORY_STRINGS)
-      || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()))
-  {
-    if (!options::instWhenStrictInterleave.wasSetByUser())
-    {
-      options::instWhenStrictInterleave.set(false);
-    }
-  }
-
   if (options::instMaxLevel() != -1)
   {
     Notice() << "SmtEngine: turning off cbqi to support instMaxLevel"