From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sun, 24 May 2020 03:52:29 +0000 (-0700)
Subject: [SMT-COMP] Redirect non-answers to /dev/null (#4528)
X-Git-Tag: cvc5-1.0.0~3291
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=08a178c7456ed824925a1eeaaff01d6adccacb52;p=cvc5.git

[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 bdc94b0bc..3ca8bd32b 100755
--- 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