diff options
Diffstat (limited to 'contrib/run-script-smtcomp2019-model-validation')
-rwxr-xr-x | contrib/run-script-smtcomp2019-model-validation | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/contrib/run-script-smtcomp2019-model-validation b/contrib/run-script-smtcomp2019-model-validation new file mode 100755 index 000000000..f4b812fd6 --- /dev/null +++ b/contrib/run-script-smtcomp2019-model-validation @@ -0,0 +1,25 @@ +#!/bin/bash + +cvc4=./cvc4 +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. +function finishwith { + $cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench +} + +case "$logic" in + +QF_BV) + finishwith --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cadical --bv-eq-slicer=auto --no-bv-abstraction + ;; +*) + # just run the default + finishwith + ;; + +esac + |