From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sun, 15 Jun 2014 05:29:53 +0000 (-0400)
Subject: better bv args for smtcomp
X-Git-Tag: cvc5-1.0.0~6809
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6e7b111b9b38fb69ab10fbca11bd9144346fafd8;p=cvc5.git

better bv args for smtcomp
---

diff --git a/contrib/run-script-smtcomp2014 b/contrib/run-script-smtcomp2014
index cd81a3f52..55f274234 100755
--- a/contrib/run-script-smtcomp2014
+++ b/contrib/run-script-smtcomp2014
@@ -72,8 +72,8 @@ QF_AUFBV)
 QF_BV)
   exec ./pcvc4 -L smt2 --no-incremental --no-checking --no-interactive \
          --threads 2 \
-         --thread0 '--unconstrained-simp --bv-eq-slicer=auto' \
-         --thread1 '--bitblast=eager --unconstrained-simp' \
+         --thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --no-bv-abstraction' \
+         --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto ' \
          --no-wait-to-join \
          "$bench"
   #trywith 10 --bv-eq-slicer=auto --decision=justification