Update QF_BV options for SMT-COMP 2019. (#3033)

diff --git a/contrib/run-script-smtcomp2019 b/contrib/run-script-smtcomp2019
index d2578345385a0728b07416d13ceaa135dbadccfd..a87cefb965be61c5f2609f449c848be3e8a27fd8 100755 (executable)
--- a/contrib/run-script-smtcomp2019
+++ b/contrib/run-script-smtcomp2019
@@ -39,11 +39,11 @@ QF_NIA)
   trywith 30 --nl-ext-tplanes --decision=justification
   trywith 30 --no-nl-ext-tplanes --decision=internal
   # this totals up to more than 20 minutes, although notice that smaller bit-widths may quickly fail
-  trywith 300 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction
-  trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction
-  trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction
-  trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction
-  trywith 600 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction
+  trywith 300 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 600 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
   finishwith --nl-ext-tplanes --decision=internal
   ;;
 QF_NRA)
@@ -122,7 +122,7 @@ QF_UFBV)
   finishwith --bitblast=eager --bv-sat-solver=cadical
   ;;
 QF_BV)
-  finishwith --unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --bv-eq-slicer=auto --no-bv-abstraction
+  finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
   ;;
 QF_AUFLIA)
   finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification

diff --git a/contrib/run-script-smtcomp2019-model-validation b/contrib/run-script-smtcomp2019-model-validation
index f4b812fd619fef21c3ec0f034e4ae7b3698c2222..eec17294d0b3c5b25c7cff64869e989e2dff0c5f 100755 (executable)
--- a/contrib/run-script-smtcomp2019-model-validation
+++ b/contrib/run-script-smtcomp2019-model-validation
@@ -14,7 +14,7 @@ function finishwith {
 case "$logic" in
 
 QF_BV)
-  finishwith --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cadical --bv-eq-slicer=auto --no-bv-abstraction
+  finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
   ;;
 *)
   # just run the default