summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2014-06-16 19:59:24 -0400
committerlianah <lianahady@gmail.com>2014-06-19 18:24:39 -0400
commitae182dad751cb2a8955904a373ef3d2960557506 (patch)
treed462b4b919f1d5b77ec0b85c00f1a701cb303701 /contrib
parent00ae9a7eba6648f957011cc250ba8707cce029c3 (diff)
Some fixes for tear-down-incremental and "success" output.
Diffstat (limited to 'contrib')
-rwxr-xr-xcontrib/run-script-smtcomp2014-application2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application
index b04b33775..2decdb98a 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 --print-success --no-checking --no-interactive --tear-down-incremental "$@"
+ cat "$bench" | $cvc4 -L smt2 --print-success --no-checking --no-interactive --no-incremental --tear-down-incremental "$@"
}
case "$logic" in
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback