diff options
Diffstat (limited to 'contrib/competitions/smt-comp')
4 files changed, 26 insertions, 26 deletions
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index 3ca8bd32b..715f3fc6c 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -1,6 +1,6 @@ #!/bin/bash -cvc4=./cvc4 +cvc5=./cvc5 bench="$1" # Output other than "sat"/"unsat" is either written to stderr or to "err.log" @@ -26,7 +26,7 @@ logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_] # returns normally and prints the output of the solver to $out_file. function trywith { limit=$1; shift; - result="$({ ulimit -S -t "$limit"; $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench; } 2>&1)" + result="$({ ulimit -S -t "$limit"; $cvc5 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench; } 2>&1)" case "$result" in sat|unsat) echo "$result"; exit 0;; *) echo "$result" &> "$out_file";; @@ -34,10 +34,10 @@ function trywith { } # use: finishwith [params..] -# to run cvc4. Only "sat" or "unsat" are output. Other outputs are written to +# to run cvc5. Only "sat" or "unsat" are output. Other outputs are written to # $out_file. function finishwith { - result="$({ $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench; } 2>&1)" + result="$({ $cvc5 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench; } 2>&1)" case "$result" in sat|unsat) echo "$result"; exit 0;; *) echo "$result" &> "$out_file";; diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental index 7861a4c85..e0b51bc46 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 -cvc4=./cvc4 +cvc5=./cvc5 line="" while [[ -z "$line" ]]; do @@ -22,54 +22,54 @@ if [ -z "$logic" ]; then fi echo success -function runcvc4 { +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?) - $cvc4 --force-logic="$logic" -L smt2.6 --print-success --no-type-checking --no-interactive "$@" <&0- + $cvc5 --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) - runcvc4 --tear-down-incremental=1 + runcvc5 --tear-down-incremental=1 ;; QF_AUFLIA) - runcvc4 --tear-down-incremental=1 --no-arrays-eager-index --arrays-eager-lemmas + runcvc5 --tear-down-incremental=1 --no-arrays-eager-index --arrays-eager-lemmas ;; QF_BV) - runcvc4 --incremental --bitblast=eager --bv-sat-solver=cadical + runcvc5 --incremental --bitblast=eager --bv-sat-solver=cadical ;; QF_UFBV) - runcvc4 --incremental + runcvc5 --incremental ;; QF_UF) - runcvc4 --incremental + runcvc5 --incremental ;; QF_AUFBV) - runcvc4 --incremental + runcvc5 --incremental ;; QF_ABV) - runcvc4 --incremental + runcvc5 --incremental ;; ABVFP) - runcvc4 --incremental + runcvc5 --incremental ;; BVFP) - runcvc4 --incremental + runcvc5 --incremental ;; QF_ABVFP) - runcvc4 --incremental + runcvc5 --incremental ;; QF_BVFP) - runcvc4 --incremental + runcvc5 --incremental ;; QF_FP) - runcvc4 --incremental + runcvc5 --incremental ;; *) # just run the default - runcvc4 --incremental + runcvc5 --incremental ;; esac diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation index 9982a9e29..338215a52 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation @@ -1,14 +1,14 @@ #!/bin/bash -cvc4=./cvc4 +cvc5=./cvc5 bench="$1" logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$') # use: finishwith [params..] -# to run cvc4 and let it output whatever it will to stdout. +# to run cvc5 and let it output whatever it will to stdout. function finishwith { - $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench + $cvc5 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench } case "$logic" in diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores index 5cb2ab610..ab6e2a6fc 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores @@ -1,14 +1,14 @@ #!/bin/bash -cvc4=./cvc4 +cvc5=./cvc5 bench="$1" logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$') # use: finishwith [params..] -# to run cvc4 and let it output whatever it will to stdout. +# to run cvc5 and let it output whatever it will to stdout. function finishwith { - $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench + $cvc5 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench } case "$logic" in |