diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ae20fa156..747fc3ac8 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -68,6 +68,7 @@ #include "options/set_language.h" #include "options/smt_options.h" #include "options/strings_options.h" +#include "options/strings_process_loop_mode.h" #include "options/theory_options.h" #include "options/uf_options.h" #include "preprocessing/preprocessing_pass.h" @@ -2262,6 +2263,15 @@ void SmtEngine::setDefaults() { "--sygus-expr-miner-check-use-export"); } } + + if (options::stringFMF() && !options::stringProcessLoopMode.wasSetByUser()) + { + Trace("smt") << "settting stringProcessLoopMode to 'simple' since " + "--strings-fmf enabled" + << endl; + options::stringProcessLoopMode.set( + theory::strings::ProcessLoopMode::SIMPLE); + } } void SmtEngine::setProblemExtended(bool value) |