diff options
| -rwxr-xr-x | contrib/competitions/smt-comp/run-script-smtcomp-current | 5 | ||||
| -rwxr-xr-x | contrib/competitions/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 |