diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-30 11:50:33 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-30 16:50:33 +0000 |
| commit | a4f38d64da67dda3bba7a132328e5477807837b9 (patch) | |
| tree | 8e042403dc6bf42792e2c91fa571acb566d16ef4 /test/regress/CMakeLists.txt | |
| parent | a633cd03e1fe118a0e5a7b50db25395b387173a1 (diff) | |
Do not apply fmfBound to standard quantifiers when only stringsExp is enabled (#6816)
There are compelling use cases that combine strings/sequences and quantifiers. Prior to this PR, strings enabled "bounded integer" quantifier instantiation so that internally generated quantifiers for strings reductions are handled in a complete manner. However, this enabled bounded integer quantifier instantiation globally. This degrades performance for "unsat" on quantified formulas in general.
After this PR, we do not enable bounded integer quantifier globally. Instead, we ensure that bounded integer quantification is applied to at least the internally generated quantified formulas; all other quantified formulas are handled as usual.
Notice this required ensuring that all quantified formulas generated by strings are marked properly. It also required adding --fmf-bound to a few regressions that explicitly require it.
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index da67705f5..5312e70a3 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2198,6 +2198,7 @@ set(regress_1_tests regress1/strings/rev-ex5.smt2 regress1/strings/rew-020618.smt2 regress1/strings/rew-check1.smt2 + regress1/strings/seq-quant-infinite-branch.smt2 regress1/strings/simple-re-consume.smt2 regress1/strings/stoi-400million.smt2 regress1/strings/stoi-solve.smt2 |