From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 9 Jun 2014 18:56:42 +0000 (-0400)
Subject: Tim's options for QF_LIA and QF_LRA---SOI+approx.
X-Git-Tag: cvc5-1.0.0~6846
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=19634b3e34ee4984136b61f8374a45242919085b;p=cvc5.git

Tim's options for QF_LIA and QF_LRA---SOI+approx.
---

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.