diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-30 12:04:38 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-30 12:04:38 -0700 |
| commit | 551a914cf9c09353712089bb0d7ad33b56adcc3f (patch) | |
| tree | 3babb2c463fdebde1a0ccd79cf4a936b011df9ea /contrib | |
| parent | 47dbf8d8b3e04810f79fd3069eb15ee1b2fb176d (diff) | |
[SMT-COMP] Print non-(un)sat output to stderr (#2019)
In the SMT-COMP runscript, we are currently discarding output on stdout
that is not "sat" or "unsat" when using `trywith` (this is not the case
with `finishwith`). Due to this, our tests might miss cases where CVC4
fails and prints an error on stdout when using `trywith`. This commit
changes the script to print output other than "sat" or "unsat" to
stderr.
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/run-script-smtcomp2018 | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018 index c44c81235..6bcc5f3d3 100644 --- a/contrib/run-script-smtcomp2018 +++ b/contrib/run-script-smtcomp2018 @@ -6,14 +6,15 @@ bench="$1" logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$') # use: trywith [params..] -# to attempt a run. Only thing printed on stdout is "sat" or "unsat", in -# which case this run script terminates immediately. Otherwise, this -# function returns normally. +# to attempt a run. Only thing printed on stdout is "sat" or "unsat", in which +# case this run script terminates immediately. Otherwise, this function +# 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)" case "$result" in sat|unsat) echo "$result"; exit 0;; + *) echo "$result" >&2;; esac } |