diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-08 16:51:54 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-08 16:52:20 -0400 |
commit | a2c0fd92782ce942a6f25f2561a4918fb2c5b020 (patch) | |
tree | c976291b6aa9cc76244bb761c3db68cf7856a217 /contrib/run-script-smteval2013 | |
parent | 3f8927c16764151ed217b509a60e22336a2981de (diff) |
final updates for smt-eval script
Diffstat (limited to 'contrib/run-script-smteval2013')
-rwxr-xr-x | contrib/run-script-smteval2013 | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/contrib/run-script-smteval2013 b/contrib/run-script-smteval2013 index fbdf4e039..2212f71c7 100755 --- a/contrib/run-script-smteval2013 +++ b/contrib/run-script-smteval2013 @@ -27,13 +27,16 @@ 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 --fancy-final ;; -AUFLIA) +AUFLIA|AUFLIRA|AUFNIRA|UFLRA|UFNIA) # 60 seconds with default decision heuristic - trywith --tlimit-per=60000 + trywith --simplification=none --tlimit-per=60000 # try simplification for 60 seconds, default decision heuristic - trywith --simplification=batch --tlimit-per=60000 + trywith --tlimit-per=60000 # switch to internal decision heuristic - finishwith --decision=internal + finishwith --simplification=none --decision=internal + ;; +LRA) + finishwith --enable-cbqi ;; QF_AUFBV) trywith --tlimit-per=600000 |