[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.

diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018
index c44c81235f9d283ee0b4e5c379104c31e5737e37..6bcc5f3d3b0faca49d5add2db3bfcae859575d24 100644 (file)
--- 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
 }