diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-18 20:44:09 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-19 18:24:40 -0400 |
commit | dd5dee0a40a03ea5fc7c3685aa2ce17d073a22ab (patch) | |
tree | 452b19b7f7ab12eeb8230f1a201bd94301dd31cc | |
parent | 5cb4e490bc222d1e8a3853b2f975a64af2976baf (diff) |
Version of the run script that works with trace executor; waiting on StarExec infrastructure for testing.
-rwxr-xr-x | contrib/run-script-smtcomp2014-application | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application index 2decdb98a..fb4ebe259 100755 --- a/contrib/run-script-smtcomp2014-application +++ b/contrib/run-script-smtcomp2014-application @@ -1,15 +1,25 @@ #!/bin/bash cvc4=./cvc4 -bench="$1" -logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$') +read line +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 +logic=$(expr "$line" : ' *(set-logic *\([A-Z_]*\) *) *$') +if [ -z "$logic" ]; then + echo 'ERROR: second line supposed to be set-logic, but got: "'"$line"'"' >&2 + exit 1 +fi function runcvc4 { # we run in this way for line-buffered input, otherwise memory's a # concern (plus it mimics what we'll end up getting from an # application-track trace runner?) - cat "$bench" | $cvc4 -L smt2 --print-success --no-checking --no-interactive --no-incremental --tear-down-incremental "$@" + (echo "(set-logic $logic)"; cat) | $cvc4 -L smt2 --print-success --no-checking --no-interactive --tear-down-incremental "$@" } case "$logic" in |