From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 30 May 2018 19:04:38 +0000 (-0700)
Subject: [SMT-COMP] Print non-(un)sat output to stderr (#2019)
X-Git-Tag: cvc5-1.0.0~4995
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=551a914cf9c09353712089bb0d7ad33b56adcc3f;p=cvc5.git

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