diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-05-30 11:17:35 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-30 11:17:35 -0700 |
| commit | c32348d5527a92894da44848297079a2797e6590 (patch) | |
| tree | 4ebef5a21902f5043ee1c48a2155947f6f9d9598 | |
| parent | 3b110a7a599011deca7bececb3622507f31c3527 (diff) | |
Use CaDiCaL for eager bit-blasting in QF_NIA and QF_UFBV. (#2018)
| -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 6034fb83b..c44c81235 100644 --- a/contrib/run-script-smtcomp2018 +++ b/contrib/run-script-smtcomp2018 @@ -37,11 +37,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=cryptominisat - trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cryptominisat - trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cryptominisat - trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cryptominisat - finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat + 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 ;; QF_NRA) trywith 300 --nl-ext-tplanes --decision=internal @@ -113,7 +113,7 @@ QF_ABV) finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv ;; QF_UFBV) - finishwith --bitblast=eager --bv-sat-solver=cryptominisat + 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 |