diff options
Diffstat (limited to 'contrib/competitions/smt-comp/run-script-smtcomp-current-incremental')
| -rwxr-xr-x | contrib/competitions/smt-comp/run-script-smtcomp-current-incremental | 40 |
1 files changed, 5 insertions, 35 deletions
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental index 21bb2f6e0..79df91d69 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental @@ -1,6 +1,6 @@ #!/bin/bash -cvc5=./cvc5 +cvc5=$(dirname "$(readlink -f "$0")")/cvc5 line="" while [[ -z "$line" ]]; do @@ -26,50 +26,20 @@ function runcvc5 { # we run in this way for line-buffered input, otherwise memory's a # concern (plus it mimics what we'll end up getting from an # application-track trace runner?) - $cvc5 --force-logic="$logic" -L smt2.6 --print-success --no-type-checking --no-interactive "$@" <&0- + $cvc5 --incremental --force-logic="$logic" -L smt2.6 --print-success --no-type-checking --no-interactive "$@" <&0- } case "$logic" in -ALIA|ANIA|AUFNIRA|LIA|LRA|QF_ALIA|QF_ANIA|QF_AUFBVLIA|QF_AUFBVNIA|QF_LIA|QF_LRA|QF_NIA|QF_UFBVLIA|QF_UFLIA|QF_UFLRA|QF_UFNIA|UFLRA) - runcvc5 --tear-down-incremental=1 - ;; QF_AUFLIA) - runcvc5 --tear-down-incremental=1 --no-arrays-eager-index --arrays-eager-lemmas + runcvc5 --no-arrays-eager-index --arrays-eager-lemmas ;; QF_BV) - runcvc5 --incremental --bitblast=eager --bv-assert-input - ;; -QF_UFBV) - runcvc5 --incremental --bv-assert-input - ;; -QF_UF) - runcvc5 --incremental - ;; -QF_AUFBV) - runcvc5 --incremental --bv-assert-input - ;; -QF_ABV) - runcvc5 --incremental --bv-assert-input - ;; -ABVFP) - runcvc5 --incremental - ;; -BVFP) - runcvc5 --incremental - ;; -QF_ABVFP) - runcvc5 --incremental - ;; -QF_BVFP) - runcvc5 --incremental - ;; -QF_FP) - runcvc5 --incremental + runcvc5 --bitblast=eager ;; *) # just run the default - runcvc5 --incremental + runcvc5 ;; esac |