diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-07 17:38:47 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-07 17:39:00 -0400 |
| commit | fcb0935524a9f6d68fc3bfcd477727893c39ccda (patch) | |
| tree | fc4302c03849c57d0d621fdbea9275dd66d3b0ca | |
| parent | d46b3638e09cd4e6f2c939386d686ed7ac2d8fdb (diff) | |
BV strategy for SMT-EVAL
| -rwxr-xr-x | contrib/run-script-smteval2013 | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/contrib/run-script-smteval2013 b/contrib/run-script-smteval2013 index 6210ca17e..6a2af96c7 100755 --- a/contrib/run-script-smteval2013 +++ b/contrib/run-script-smteval2013 @@ -39,6 +39,12 @@ QF_AUFBV) trywith --tlimit-per=600000 finishwith --decision=justification-stoponly ;; +QF_BV) + trywith --bv-core --decision=justification --tlimit-per=10000 + trywith --decision=justification --tlimit-per=60000 + trywith --decision=internal --bitblast-eager --tlimit-per=600000 + finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1 + ;; QF_AX) trywith --tlimit-per=2000 finishwith --no-arrays-model-based |