From 6394bf6ffa2486587d1726271769117f7dc227a8 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Thu, 10 Jun 2021 11:27:10 -0700 Subject: [PATCH] smtcomp: Change some BV configs for SQ and INC track. (#6721) --- contrib/competitions/smt-comp/run-script-smtcomp-current | 5 +---- .../smt-comp/run-script-smtcomp-current-incremental | 6 +++--- 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index db72b3a6b..ecc6ce5fe 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -139,10 +139,7 @@ QF_ABV) trywith 500 --arrays-weak-equiv finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv ;; -QF_UFBV) - finishwith --bitblast=eager - ;; -QF_BV) +QF_BV|QF_UFBV) finishwith --bitblast=eager --bv-assert-input ;; QF_AUFLIA) diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental index c6901ff5b..21bb2f6e0 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental @@ -41,16 +41,16 @@ QF_BV) runcvc5 --incremental --bitblast=eager --bv-assert-input ;; QF_UFBV) - runcvc5 --incremental + runcvc5 --incremental --bv-assert-input ;; QF_UF) runcvc5 --incremental ;; QF_AUFBV) - runcvc5 --incremental + runcvc5 --incremental --bv-assert-input ;; QF_ABV) - runcvc5 --incremental + runcvc5 --incremental --bv-assert-input ;; ABVFP) runcvc5 --incremental -- 2.30.2