summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2021-07-03 12:11:57 -0700
committerGitHub <noreply@github.com>2021-07-03 19:11:57 +0000
commit698d244a00618a0399bce9e15eddef52f68b8c94 (patch)
tree65acbab5671dc90bec6790f6a70be76e16fe037a /src/theory/theory_engine.cpp
parentc56eaf4423fbf65663a4e03c8a60ed937c99de7d (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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback