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 | |
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.
-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 |