Run script updates: no --stats, also application-track version.

diff --git a/contrib/run-script-smtcomp2014 b/contrib/run-script-smtcomp2014
index 5ba3506cdc25b757db1985a1f6c94c93e125b351..a4737142a08126d15bb4392b619b8a2db5a4b1b9 100755 (executable)
--- a/contrib/run-script-smtcomp2014
+++ b/contrib/run-script-smtcomp2014
@@ -10,7 +10,7 @@ logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]
 # which case this run script terminates immediately.  Otherwise, this
 # function returns normally.
 function trywith {
-  result="$($cvc4 --stats -L smt2 --no-checking --no-interactive "$@" $bench)"
+  result="$($cvc4 -L smt2 --no-checking --no-interactive "$@" $bench)"
   case "$result" in
     sat|unsat) echo "$result"; exit 0;;
   esac
@@ -19,7 +19,7 @@ function trywith {
 # use: finishwith [params..]
 # to run cvc4 and let it output whatever it will to stdout.
 function finishwith {
-  $cvc4 --stats -L smt2 --no-checking --no-interactive "$@" $bench
+  $cvc4 -L smt2 --no-checking --no-interactive "$@" $bench
 }
 
 case "$logic" in

diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application
new file mode 100755 (executable)
index 0000000..94e80b9
--- /dev/null
+++ b/contrib/run-script-smtcomp2014-application
@@ -0,0 +1,29 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
+
+case "$logic" in
+
+QF_BV)
+  # run tear-down incremental
+  #
+  # 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
+  ;;
+
+*)
+  # just run the default --incremental
+  #
+  # 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 --incremental
+  ;;
+
+esac
+