[SMT-COMP 2019] Use lazy BV as backup for QF_UFBV (#3037)

We cannot Ackermannize all the QF_UFBV benchmarks due to uninterpreted
sorts. This commit adds lazy bit-blasting as a backup strategy.

diff --git a/contrib/run-script-smtcomp2019 b/contrib/run-script-smtcomp2019
index 15bae8d0d405af257db06e89b65b99f2550f6648..d917d9c5a122f88d013c1319d85d08ff267d0e8f 100755 (executable)
--- a/contrib/run-script-smtcomp2019
+++ b/contrib/run-script-smtcomp2019
@@ -119,7 +119,10 @@ QF_ABV)
   finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
   ;;
 QF_UFBV)
-  finishwith --bitblast=eager --bv-sat-solver=cadical
+  # Benchmarks with uninterpreted sorts cannot be solved with eager
+  # bit-blasting currently
+  trywith 2400 --bitblast=eager --bv-sat-solver=cadical
+  finishwith
   ;;
 QF_BV)
   finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction