diff options
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/run-script-smtcomp2014-application | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application index 1a9078994..53df6a927 100755 --- a/contrib/run-script-smtcomp2014-application +++ b/contrib/run-script-smtcomp2014-application @@ -14,12 +14,13 @@ if [ -z "$logic" ]; then echo 'ERROR: second line supposed to be set-logic, but got: "'"$line"'"' >&2 exit 1 fi +echo success function runcvc4 { # 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?) - (echo "(set-logic $logic)"; cat) | $cvc4 -L smt2 --print-success --no-checking --no-interactive --tear-down-incremental "$@" + $cvc4 --force-logic="$logic" -L smt2 --print-success --no-checking --no-interactive --tear-down-incremental "$@" <&0- } case "$logic" in |