From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 7 May 2013 03:07:28 +0000 (-0400)
Subject: Change SMT-EVAL run-script to use Tim's best QF_LRA command-line parameters
X-Git-Tag: cvc5-1.0.0~7287^2~149
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a5f13935cd4a861c134a1e741cc81248b012eaaf;p=cvc5.git

Change SMT-EVAL run-script to use Tim's best QF_LRA command-line parameters
---

diff --git a/contrib/run-script-smteval2013 b/contrib/run-script-smteval2013
index 3c71b28e7..6210ca17e 100755
--- a/contrib/run-script-smteval2013
+++ b/contrib/run-script-smteval2013
@@ -25,10 +25,7 @@ function finishwith {
 case "$logic" in
 
 QF_LRA)
-  # 3 minutes with default decision heuristic
-  trywith --tlimit-per=180000
-  # switch to internal decision heuristic
-  finishwith --decision=internal
+  finishwith --no-restrict-pivots --enable-miplib-trick --miplib-trick-subs=2 --fc-penalties --collect-pivot-stats --use-soi --new-prop --dio-decomps --unconstrained-simp --fancy-final
   ;;
 AUFLIA)
   # 60 seconds with default decision heuristic