diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-06-08 13:25:13 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-06-08 13:25:13 -0700 |
| commit | dcbd349c069a423dd631d4a5bc049f3721d5cc83 (patch) | |
| tree | 12e2ccb50c3dd907c095a50d60ebf157bafc01a9 /contrib | |
| parent | e0bdf8d71dca4af530273ede2bdd252ca6d8e6b1 (diff) | |
Disable BV-abstraction in the competition script. (#2061)
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/run-script-smtcomp2018 | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018 index ff06fb933..849df0a6b 100644 --- a/contrib/run-script-smtcomp2018 +++ b/contrib/run-script-smtcomp2018 @@ -38,11 +38,11 @@ QF_NIA) trywith 300 --nl-ext-tplanes --decision=internal 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 - trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig - trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig - trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig - finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig + 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 + finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction ;; QF_NRA) trywith 300 --nl-ext-tplanes --decision=internal @@ -120,7 +120,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-abstraction --bv-eq-slicer=auto + 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 ;; QF_AUFLIA) finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification |