From 19634b3e34ee4984136b61f8374a45242919085b Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 9 Jun 2014 14:56:42 -0400 Subject: [PATCH] Tim's options for QF_LIA and QF_LRA---SOI+approx. --- contrib/run-script-smtcomp2014 | 5 +++-- 1 file 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. -- 2.30.2