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/theory_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/theory_engine.cpp')
0 files changed, 0 insertions, 0 deletions