diff options
Diffstat (limited to 'contrib/competitions/smt-comp/run-script-smtcomp-current')
| -rwxr-xr-x | contrib/competitions/smt-comp/run-script-smtcomp-current | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index f2168398f..d4a257395 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -11,7 +11,7 @@ logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_] # returns normally and prints the output of the solver to stderr. function trywith { limit=$1; shift; - result="$(ulimit -S -t "$limit";$cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench)" + result="$(ulimit -S -t "$limit";$cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench)" case "$result" in sat|unsat) echo "$result"; exit 0;; *) echo "$result" >&2;; @@ -21,7 +21,7 @@ function trywith { # 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 + $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench } # the following is designed for a run time of 20 min. |