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/get-abc | |
| 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/get-abc')
0 files changed, 0 insertions, 0 deletions