diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-01 23:34:18 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-01 23:34:18 -0600 |
commit | a39f1719ede136579cbd15c34b6a763a2b08a464 (patch) | |
tree | 4bc0f72f191167c400d42011f2bd062d7b4103ba /src/smt | |
parent | ac9808bdc0c6d5619f636691bd737079b50b9ea5 (diff) |
Ensure quantifiers options are set with --no-strings-lazy-pp (#3515)
Diffstat (limited to 'src/smt')
-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(); |