diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-21 22:09:17 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-21 22:09:17 -0400 |
| commit | 37e1a756c83a24322f1cb496dbd2e85a162c93b0 (patch) | |
| tree | d418ded7004cd1f97fbdae0bd52596d3e3824a20 /contrib/run-script-smtcomp2014-application | |
| parent | eb49f3939e0b47a0c1a404079a6ef108628e13d1 (diff) | |
Run in application track with --check-models.
Diffstat (limited to 'contrib/run-script-smtcomp2014-application')
| -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 fb4ebe259..165293e74 100755 --- a/contrib/run-script-smtcomp2014-application +++ b/contrib/run-script-smtcomp2014-application @@ -19,7 +19,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?) - (echo "(set-logic $logic)"; cat) | $cvc4 -L smt2 --print-success --no-checking --no-interactive --tear-down-incremental "$@" + (echo "(set-logic $logic)"; cat) | $cvc4 -L smt2 --print-success --no-checking --no-interactive --tear-down-incremental --check-models "$@" } case "$logic" in |