diff options
Diffstat (limited to 'contrib/competitions/smt-comp/run-script-smtcomp2021-model-validation')
-rwxr-xr-x | contrib/competitions/smt-comp/run-script-smtcomp2021-model-validation | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2021-model-validation b/contrib/competitions/smt-comp/run-script-smtcomp2021-model-validation new file mode 100755 index 000000000..0998e9949 --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2021-model-validation @@ -0,0 +1,30 @@ +#!/bin/bash + +cvc5=$(dirname "$(readlink -f "$0")")/cvc5 +bench="$1" + +logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$') + +# use: finishwith [params..] +# to run cvc5 and let it output whatever it will to stdout. +function finishwith { + $cvc5 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench +} + +case "$logic" in + +QF_LRA) + finishwith --no-restrict-pivots --use-soi --new-prop + ;; +QF_LIA) + finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --use-soi --pb-rewrites --ite-simp --simp-ite-compress + ;; +QF_BV) + finishwith --bv-assert-input + ;; +*) + # just run the default + finishwith + ;; + +esac |