BV strategy for SMT-EVAL

diff --git a/contrib/run-script-smteval2013 b/contrib/run-script-smteval2013
index 6210ca17e8432b1b737042f08479e2675f786ae0..6a2af96c79623f482660094c20527b863345818f 100755 (executable)
--- 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