projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: f7118b2)
minor update to application track config in QF_BV
authorMorgan Deters <mdeters@cs.nyu.edu>
Mon, 16 Jun 2014 03:08:50 +0000 (23:08 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Mon, 16 Jun 2014 03:08:50 +0000 (23:08 -0400)
contrib/run-script-smtcomp2014-application patch | blob | history

diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application
index ae1d9e1ecdf17062ba3abddf0be08e421b83ffd9..b04b3377546d9fb773ccade0c3a8474b32a92937 100755 (executable)
--- a/contrib/run-script-smtcomp2014-application
+++ b/contrib/run-script-smtcomp2014-application
@@ -28,7 +28,7 @@ LIA|LRA|NIA|NRA)
   runcvc4 --enable-cbqi --full-saturate-quant
   ;;
 QF_BV)
-  runcvc4 --bv-eq-slicer=auto --decision=justification
+  runcvc4 --unconstrained-simp --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2
   ;;
 QF_AUFLIA|QF_AX)
   runcvc4 --no-arrays-eager-index --arrays-eager-lemmas