diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-06-09 16:44:19 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-09 16:44:19 -0300 |
commit | b1dda1f5013ce688e80664dc3cd1029b1f4df1cd (patch) | |
tree | d5621d35271a7ae39ea1542d9722dfabee4404ad /contrib/competitions/smt-comp/run-script-smtcomp-current | |
parent | ba41b7306cf93717e41946e2044e29f0fb63bbf5 (diff) | |
parent | 181a175839e3af50a8cf7f80adf635fe612aeaba (diff) |
Merge branch 'master' into issue6717issue6717
Diffstat (limited to 'contrib/competitions/smt-comp/run-script-smtcomp-current')
-rwxr-xr-x | contrib/competitions/smt-comp/run-script-smtcomp-current | 33 |
1 files changed, 15 insertions, 18 deletions
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index ea3b2dde1..db72b3a6b 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -56,23 +56,23 @@ QF_LIA) finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites --ite-simp --simp-ite-compress ;; QF_NIA) - trywith 480 --nl-ext-tplanes --decision=internal - trywith 60 --nl-ext-tplanes --decision=justification + trywith 420 --nl-ext-tplanes --decision=justification + trywith 60 --nl-ext-tplanes --decision=internal + trywith 60 --nl-ext-tplanes --decision=justification-old trywith 60 --no-nl-ext-tplanes --decision=internal trywith 60 --no-arith-brab --nl-ext-tplanes --decision=internal # this totals up to more than 20 minutes, although notice that smaller bit-widths may quickly fail - trywith 300 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 600 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + trywith 300 --solve-int-as-bv=2 --bitblast=eager + trywith 300 --solve-int-as-bv=4 --bitblast=eager + trywith 300 --solve-int-as-bv=8 --bitblast=eager + trywith 300 --solve-int-as-bv=16 --bitblast=eager + trywith 600 --solve-int-as-bv=32 --bitblast=eager finishwith --nl-ext-tplanes --decision=internal ;; QF_NRA) - trywith 300 --nl-ext-tplanes --decision=internal - trywith 300 --nl-ext-tplanes --decision=justification --no-nl-ext-factor - trywith 30 --nl-ext-tplanes --decision=internal --solve-real-as-int - finishwith --nl-ext-tplanes --decision=justification + trywith 600 --decision=justification + trywith 300 --decision=internal --no-nl-cad --nl-ext=full --nl-ext-tplanes + finishwith --decision=internal --nl-ext=none ;; # all logics with UF + quantifiers should either fall under this or special cases below ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA|UFFPDTLIRA|UFFPDTNIRA) @@ -140,13 +140,10 @@ QF_ABV) finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv ;; QF_UFBV) - # Benchmarks with uninterpreted sorts cannot be solved with eager - # bit-blasting currently - trywith 1200 --bitblast=eager --bv-sat-solver=cadical - finishwith + finishwith --bitblast=eager ;; QF_BV) - finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + finishwith --bitblast=eager --bv-assert-input ;; QF_AUFLIA) finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification @@ -162,8 +159,8 @@ QF_ALIA) finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas ;; QF_S|QF_SLIA) - trywith 300 --strings-exp --rewrite-divk --strings-fmf --no-jh-rlv-order - finishwith --strings-exp --rewrite-divk --no-jh-rlv-order + trywith 300 --strings-exp --strings-fmf --no-jh-rlv-order + finishwith --strings-exp --no-jh-rlv-order ;; QF_ABVFP|QF_ABVFPLRA) finishwith --fp-exp |