diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-05-17 23:07:48 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-05-17 21:07:48 -0700 |
| commit | 3d79c9b5813eda2f6f55822e193e36a660435e10 (patch) | |
| tree | 454e66ccc024534d52dd01d0ec4ae5ffa569c166 /contrib | |
| parent | 437191609061acbc76b92bab79df31334a489e82 (diff) | |
Update QF_NIA strategy (#3012)
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/run-script-smtcomp2019 | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/contrib/run-script-smtcomp2019 b/contrib/run-script-smtcomp2019 index 4138decd6..d25783453 100644 --- a/contrib/run-script-smtcomp2019 +++ b/contrib/run-script-smtcomp2019 @@ -36,13 +36,15 @@ QF_LIA) ;; QF_NIA) trywith 300 --nl-ext-tplanes --decision=internal + 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 - finishwith --solve-int-as-bv=32 --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 + finishwith --nl-ext-tplanes --decision=internal ;; QF_NRA) trywith 300 --nl-ext-tplanes --decision=internal |