diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-06-10 11:27:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-10 18:27:10 +0000 |
commit | 6394bf6ffa2486587d1726271769117f7dc227a8 (patch) | |
tree | 1645abca1035e9c8a086cadddceb61f9ccbe098b /contrib | |
parent | 226244a0bdb68655c06d6d1b55b31be013bf7fa6 (diff) |
smtcomp: Change some BV configs for SQ and INC track. (#6721)
Diffstat (limited to 'contrib')
-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 |