diff options
| author | Andres Noetzli <noetzli@stanford.edu> | 2019-06-02 21:23:52 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-06-02 21:23:52 -0700 |
| commit | 52a910f728f399e782b3ac036e4476f1fb3c27fa (patch) | |
| tree | f71207f20a825d88890f5367979ae56919d246b9 | |
| parent | 9ccf3c01a736a9f6d5c6889b51c4589221044c97 (diff) | |
[SMT-COMP 2019] Use lazy BV as backup for QF_UFBV (#3037)
We cannot Ackermannize all the QF_UFBV benchmarks due to uninterpreted
sorts. This commit adds lazy bit-blasting as a backup strategy.
| -rwxr-xr-x | contrib/run-script-smtcomp2019 | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/contrib/run-script-smtcomp2019 b/contrib/run-script-smtcomp2019 index 15bae8d0d..d917d9c5a 100755 --- a/contrib/run-script-smtcomp2019 +++ b/contrib/run-script-smtcomp2019 @@ -119,7 +119,10 @@ QF_ABV) finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv ;; QF_UFBV) - finishwith --bitblast=eager --bv-sat-solver=cadical + # Benchmarks with uninterpreted sorts cannot be solved with eager + # bit-blasting currently + trywith 2400 --bitblast=eager --bv-sat-solver=cadical + finishwith ;; QF_BV) finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction |