From fcb0935524a9f6d68fc3bfcd477727893c39ccda Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 7 May 2013 17:38:47 -0400
Subject: [PATCH] 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
-- 
2.30.2