From fcb0935524a9f6d68fc3bfcd477727893c39ccda Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 7 May 2013 17:38:47 -0400 Subject: BV strategy for SMT-EVAL --- contrib/run-script-smteval2013 | 6 ++++++ 1 file changed, 6 insertions(+) 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 -- cgit v1.2.3