From: Andres Noetzli <noetzli@stanford.edu>
Date: Mon, 3 Jun 2019 04:23:52 +0000 (-0700)
Subject: [SMT-COMP 2019] Use lazy BV as backup for QF_UFBV (#3037)
X-Git-Tag: cvc5-1.0.0~4129
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=52a910f728f399e782b3ac036e4476f1fb3c27fa;p=cvc5.git

[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 15bae8d0d..d917d9c5a 100755
--- 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