diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-06 23:07:28 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-06 23:07:28 -0400 |
| commit | a5f13935cd4a861c134a1e741cc81248b012eaaf (patch) | |
| tree | 9066915198f2d3c82d0099ec36a7f7dbba7e1910 /contrib | |
| parent | 9b035b4aedd977213a5f5acb6e8cb01bf160c415 (diff) | |
Change SMT-EVAL run-script to use Tim's best QF_LRA command-line parameters
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/run-script-smteval2013 | 5 |
1 files changed, 1 insertions, 4 deletions
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 |