diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-07-03 12:11:57 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-03 19:11:57 +0000 |
| commit | 698d244a00618a0399bce9e15eddef52f68b8c94 (patch) | |
| tree | 65acbab5671dc90bec6790f6a70be76e16fe037a /src/theory/quantifiers_engine.cpp | |
| parent | c56eaf4423fbf65663a4e03c8a60ed937c99de7d (diff) | |
Fix performance of string regression (#6832)
Regression cmu-dis-0707-3.smt2 has been timing out when using an ASan
build after commit a4f38d6. Before that
commit --strings-exp implicitly enabled --fmf-bound. After the
commit, the solver was supposed to apply the same reasoning but only to
interal quantifiers and without enabling --fmf-bound. However, the
commit missed some options checks that now also have to check whether
--strings-exp is enabled. This commit updates those option checks.
With this fix, we get a slightly different value for bug590.smt2 after
replying unknown. This commit updates the regression to be more lenient
with the value returned.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 6214737ad..ccd177b7d 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -19,6 +19,7 @@ #include "options/printer_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" +#include "options/strings_options.h" #include "options/uf_options.h" #include "smt/smt_engine_scope.h" #include "theory/quantifiers/equality_query.h" @@ -67,7 +68,7 @@ QuantifiersEngine::QuantifiersEngine( // Finite model finding requires specialized ways of building the model. // We require constructing the model here, since it is required for // initializing the CombinationEngine and the rest of quantifiers engine. - if (options::fmfBound() + if (options::fmfBound() || options::stringExp() || (options::finiteModelFind() && (options::mbqiMode() == options::MbqiMode::FMC || options::mbqiMode() == options::MbqiMode::TRUST))) |