Ensure quantifiers options are set with --no-strings-lazy-pp (#3515)

1 files changed, 5 insertions, 3 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ca5558e87..eb10f580a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1251,10 +1251,12 @@ void SmtEngine::setDefaults() {
     }
   }
 
-  // set default options associated with strings-exp
-  if (options::stringExp())
+  // Set default options associated with strings-exp. We also set these options
+  // if we are using eager string preprocessing, which may introduce quantified
+  // formulas at preprocess time.
+  if (options::stringExp() || !options::stringLazyPreproc())
   {
-    // We require quantifiers since extended functions reduce using them
+    // We require quantifiers since extended functions reduce using them.
     if (!d_logic.isQuantified())
     {
       d_logic = d_logic.getUnlockedCopy();