diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-03 12:24:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-03 12:24:08 -0500 |
| commit | 64e7ff24ad33a1fb297adfda8ec5aa4631ed9dba (patch) | |
| tree | 7c302cf375acc9a8beadf25561c18a46b2f9e657 /contrib | |
| parent | 4251c330cc2e9e87ffaaf4dd2c1bc9db6f1046a5 (diff) | |
Option to interleave tangent plane inferences (#1833)
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/run-script-smtcomp2018 | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018 index 403f6c8a8..b920152b2 100644 --- a/contrib/run-script-smtcomp2018 +++ b/contrib/run-script-smtcomp2018 @@ -34,7 +34,8 @@ 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 ;; QF_NIA) - trywith 300 --nl-ext --nl-ext-tplanes --decision=internal + 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 @@ -43,10 +44,10 @@ QF_NIA) finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat ;; QF_NRA) - trywith 300 --nl-ext --nl-ext-tplanes --decision=internal - trywith 300 --nl-ext --nl-ext-tplanes --decision=justification --no-nl-ext-factor - trywith 30 --nl-ext --nl-ext-tplanes --decision=internal --solve-real-as-int - finishwith --nl-ext --nl-ext-tplanes --decision=justification + 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 ;; # 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) |