diff options
| author | Andres Noetzli <noetzli@stanford.edu> | 2017-06-15 14:11:29 -0700 |
|---|---|---|
| committer | Andres Nötzli <andres.noetzli@gmail.com> | 2017-06-15 14:54:02 -0700 |
| commit | 06b31fab6b9968ea1d6a58435cf210af5e6f540a (patch) | |
| tree | 7a7f5204049ba4e9fc94c10c6dff89fc6c07e3bd /contrib/run-script-smtcomp2017-application | |
| parent | 209b08887bc55349880b9ed6d858e23637267dee (diff) | |
Make comp script more robust
In certain cases, the trace executor inserts empty lines, which threw off
our competition script. This commit adds code to ignores empty lines.
Diffstat (limited to 'contrib/run-script-smtcomp2017-application')
| -rwxr-xr-x[-rw-r--r--] | contrib/run-script-smtcomp2017-application | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/contrib/run-script-smtcomp2017-application b/contrib/run-script-smtcomp2017-application index 528a5deab..ddcc1f0c6 100644..100755 --- a/contrib/run-script-smtcomp2017-application +++ b/contrib/run-script-smtcomp2017-application @@ -2,13 +2,19 @@ cvc4=./cvc4-application -read line +line="" +while [[ -z "$line" ]]; do + read line +done if [ "$line" != '(set-option :print-success true)' ]; then echo 'ERROR: first line supposed to be set-option :print-success, but got: "'"$line"'"' >&2 exit 1 fi echo success -read line +line="" +while [[ -z "$line" ]]; do + read line +done logic=$(expr "$line" : ' *(set-logic *\([A-Z_]*\) *) *$') if [ -z "$logic" ]; then echo 'ERROR: second line supposed to be set-logic, but got: "'"$line"'"' >&2 |