diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-09 14:56:42 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-09 14:56:49 -0400 |
| commit | 19634b3e34ee4984136b61f8374a45242919085b (patch) | |
| tree | d213b4af6b12655b2bd7966904384fb188492034 /contrib | |
| parent | e2f91c1242015aaf74286fe45987afaaea5a6806 (diff) | |
Tim's options for QF_LIA and QF_LRA---SOI+approx.
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/run-script-smtcomp2014 | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/contrib/run-script-smtcomp2014 b/contrib/run-script-smtcomp2014 index 3af41545a..e723df9c7 100755 --- a/contrib/run-script-smtcomp2014 +++ b/contrib/run-script-smtcomp2014 @@ -25,8 +25,9 @@ function finishwith { case "$logic" in -QF_LRA) - finishwith --no-restrict-pivots --enable-miplib-trick --miplib-trick-subs=2 --fc-penalties --collect-pivot-stats --use-soi --new-prop --dio-decomps --unconstrained-simp --use-approx +QF_LRA|QF_LIA) + # need also --pb-rewrites after tim's merge + finishwith --enable-miplib-trick --miplib-trick-subs=4 --use-approx --stats --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi ;; AUFLIA|AUFLIRA|AUFNIRA|UFLRA|UFNIA) # the following is designed for a run time of 1500s. |