diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-06-13 01:21:28 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-06-13 01:21:28 -0400 |
| commit | e39bd1a347ae22f0cc22bd3a3172acfa6d1f8e75 (patch) | |
| tree | 1e2e937f28c986a30c3a1bb0ccb878259abeaa73 | |
| parent | 46492b22e1fa6ba0c5d5256ece6ba82e76755fce (diff) | |
sync assertions run script with default
| -rwxr-xr-x | contrib/run-script-smtcomp2015-assertions | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/contrib/run-script-smtcomp2015-assertions b/contrib/run-script-smtcomp2015-assertions index 328646326..40a31fc45 100755 --- a/contrib/run-script-smtcomp2015-assertions +++ b/contrib/run-script-smtcomp2015-assertions @@ -38,7 +38,10 @@ QF_LIA) # same as QF_LRA but add --pb-rewrites finishwith --enable-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 ;; -ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) +AUFLIA) + finishwith --no-e-matching --full-saturate-quant + ;; +ALIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) # the following is designed for a run time of 1800s. # initial runs 1min (30) trywith 10 --simplification=none --full-saturate-quant @@ -102,8 +105,18 @@ QF_BV) #trywith 600 --decision=internal --bitblast-eager #finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1 ;; -QF_AUFLIA|QF_AX) - finishwith --no-arrays-eager-index --arrays-eager-lemmas +QF_AUFLIA) + finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification + ;; +QF_AX) + finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=internal + ;; +QF_AUFNIA) + finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas + ;; +QF_ALIA) + trywith 30 --decision=justification --arrays-weak-equiv + finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas ;; *) # just run the default |