From 52a910f728f399e782b3ac036e4476f1fb3c27fa Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sun, 2 Jun 2019 21:23:52 -0700 Subject: [PATCH] [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. --- contrib/run-script-smtcomp2019 | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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 -- 2.30.2