Fix performance of string regression (#6832)
authorAndres Noetzli <andres.noetzli@gmail.com>
Sat, 3 Jul 2021 19:11:57 +0000 (12:11 -0700)
committerGitHub <noreply@github.com>
Sat, 3 Jul 2021 19:11:57 +0000 (19:11 +0000)
commit698d244a00618a0399bce9e15eddef52f68b8c94
tree65acbab5671dc90bec6790f6a70be76e16fe037a
parentc56eaf4423fbf65663a4e03c8a60ed937c99de7d
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.
src/theory/quantifiers/fmf/full_model_check.cpp
src/theory/quantifiers/fmf/model_builder.cpp
src/theory/quantifiers_engine.cpp
test/regress/regress1/bug590.smt2