diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-15 19:54:19 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-15 19:54:19 -0400 |
commit | 39a863a248db14d3956b975d0e9c531b96f2baa4 (patch) | |
tree | ecde58a054ece263f5d38379955a400217c73d8c /contrib | |
parent | 84f7eeae9d3713c99fcc8b2d33f5c004574a1c57 (diff) |
Application trace executor (if they end up using that) requires --print-success.
Diffstat (limited to 'contrib')
-rwxr-xr-x | contrib/run-script-smtcomp2014-application | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application index 16ee64bff..ae1d9e1ec 100755 --- a/contrib/run-script-smtcomp2014-application +++ b/contrib/run-script-smtcomp2014-application @@ -9,7 +9,7 @@ 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 --no-checking --no-interactive --tear-down-incremental "$@" + cat "$bench" | $cvc4 -L smt2 --print-success --no-checking --no-interactive --tear-down-incremental "$@" } case "$logic" in |