diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/smt/smt_engine.cpp | 8 |
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(); |