diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-06-01 16:40:33 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-06-01 16:40:33 -0700 |
| commit | 2d9f552b86cf75a95187541699612ea1331ec990 (patch) | |
| tree | 3a57fa9737ca413e78a2c124fa8cbccc972bf69f /contrib | |
| parent | 9b6985b4427aff888f07ecc84079452c11113cb6 (diff) | |
Update QF_BV options for SMT-COMP 2019. (#3033)
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/run-script-smtcomp2019 | 12 | ||||
| -rwxr-xr-x | contrib/run-script-smtcomp2019-model-validation | 2 |
2 files changed, 7 insertions, 7 deletions
diff --git a/contrib/run-script-smtcomp2019 b/contrib/run-script-smtcomp2019 index d25783453..a87cefb96 100755 --- a/contrib/run-script-smtcomp2019 +++ b/contrib/run-script-smtcomp2019 @@ -39,11 +39,11 @@ QF_NIA) trywith 30 --nl-ext-tplanes --decision=justification trywith 30 --no-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 --bitblast-aig --no-bv-abstraction - trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction - trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction - trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction - trywith 600 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction + 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 finishwith --nl-ext-tplanes --decision=internal ;; QF_NRA) @@ -122,7 +122,7 @@ QF_UFBV) finishwith --bitblast=eager --bv-sat-solver=cadical ;; QF_BV) - finishwith --unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --bv-eq-slicer=auto --no-bv-abstraction + finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction ;; QF_AUFLIA) finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification diff --git a/contrib/run-script-smtcomp2019-model-validation b/contrib/run-script-smtcomp2019-model-validation index f4b812fd6..eec17294d 100755 --- a/contrib/run-script-smtcomp2019-model-validation +++ b/contrib/run-script-smtcomp2019-model-validation @@ -14,7 +14,7 @@ function finishwith { case "$logic" in QF_BV) - finishwith --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cadical --bv-eq-slicer=auto --no-bv-abstraction + finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction ;; *) # just run the default |