diff options
| -rwxr-xr-x[-rw-r--r--] | contrib/run-script-smtcomp2019 | 0 | ||||
| -rwxr-xr-x | contrib/run-script-smtcomp2019-incremental (renamed from contrib/run-script-smtcomp2019-application) | 2 | ||||
| -rwxr-xr-x | contrib/run-script-smtcomp2019-model-validation | 25 | ||||
| -rwxr-xr-x[-rw-r--r--] | contrib/run-script-smtcomp2019-unsat-cores | 0 |
4 files changed, 26 insertions, 1 deletions
diff --git a/contrib/run-script-smtcomp2019 b/contrib/run-script-smtcomp2019 index d25783453..d25783453 100644..100755 --- a/contrib/run-script-smtcomp2019 +++ b/contrib/run-script-smtcomp2019 diff --git a/contrib/run-script-smtcomp2019-application b/contrib/run-script-smtcomp2019-incremental index a7d4d985c..12c91a036 100755 --- a/contrib/run-script-smtcomp2019-application +++ b/contrib/run-script-smtcomp2019-incremental @@ -1,6 +1,6 @@ #!/bin/bash -cvc4=./cvc4-application +cvc4=./cvc4 line="" while [[ -z "$line" ]]; do 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 + diff --git a/contrib/run-script-smtcomp2019-unsat-cores b/contrib/run-script-smtcomp2019-unsat-cores index 1454e7a8a..1454e7a8a 100644..100755 --- a/contrib/run-script-smtcomp2019-unsat-cores +++ b/contrib/run-script-smtcomp2019-unsat-cores |