From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Fri, 25 May 2018 18:02:32 +0000 (-0700)
Subject: Add QF_BV configuration for SMTCOMP'18. (#1981)
X-Git-Tag: cvc5-1.0.0~5008
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d7e4d90e547427f511dfabb66bf3686cb987324b;p=cvc5.git

Add QF_BV configuration for SMTCOMP'18. (#1981)
---

diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018
index b920152b2..5264bc26c 100644
--- a/contrib/run-script-smtcomp2018
+++ b/contrib/run-script-smtcomp2018
@@ -116,16 +116,7 @@ QF_UFBV)
   finishwith --bitblast=eager --bv-sat-solver=cryptominisat
   ;;
 QF_BV)
-  exec ./pcvc4 -L smt2.6 --no-incremental --no-checking --no-interactive --thread-stack=1024 \
-         --threads 2 \
-         --thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager  --bv-sat-solver=cryptominisat --bitblast-aig --no-bv-abstraction' \
-         --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto --no-bv-abstraction' \
-         --no-wait-to-join \
-         "$bench"
-  #trywith 10 --bv-eq-slicer=auto --decision=justification
-  #trywith 60 --decision=justification
-  #trywith 600 --decision=internal --bitblast-eager
-  #finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1
+  finishwith --unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --bv-abstraction --bv-eq-slicer=auto
   ;;
 QF_AUFLIA)
   finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification