diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-05-23 20:52:29 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-05-23 20:52:29 -0700 |
| commit | 08a178c7456ed824925a1eeaaff01d6adccacb52 (patch) | |
| tree | 6dac3b67a92a3f8d0bc69fe2d2c891d845abade2 /contrib | |
| parent | f831e2116c210bee79aeae7d26527ac62e3dd92d (diff) | |
[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
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/competitions/smt-comp/run-script-smtcomp-current | 7 |
1 files changed, 7 insertions, 0 deletions
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 |