[SMT-COMP] Redirect non-answers to /dev/null (#4528)

Commit 00badd3a63a2fa568373d5c58553944b579d42bb changed our run script
to write output other than `sat`/`unsat` to a file if `$2` is passed to
it. However, it looks like StarExec does not pass that parameter to our
script despite the documentation claiming that it does [0]. This commit
makes our check more defensive by redirecting our unnecessary output to
`/dev/null` if `STAREXEC_WALLCLOCK_LIMIT` is set. I've done a quick test
run on StarExec and it looks like this does the trick.

[0]
https://wiki.uiowa.edu/display/stardev/User+Guide#UserGuide-SpecialVariables

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index bdc94b0bcedb0265c38ea45b5dd0cb7bc6c39e26..3ca8bd32b2d53a6ea18b732b3033290b3ad46274 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -7,6 +7,13 @@ bench="$1"
 # in the directory specified by $2 if it has been set (e.g. when running on
 # StarExec).
 out_file=/dev/stderr
+
+if [ -n "$STAREXEC_WALLCLOCK_LIMIT" ]; then
+  # If we are running on StarExec, don't print to `/dev/stderr/` even when $2
+  # is not provided.
+  out_file="/dev/null"
+fi
+
 if [ -n "$2" ]; then
   out_file="$2/err.log"
 fi