From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 7 May 2013 21:38:47 +0000 (-0400)
Subject: BV strategy for SMT-EVAL
X-Git-Tag: cvc5-1.0.0~7287^2~140
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fcb0935524a9f6d68fc3bfcd477727893c39ccda;p=cvc5.git

BV strategy for SMT-EVAL
---

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