From 4a5b4545080f0bf576830893d7dafa8f56a26a0f Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 30 May 2014 15:00:38 -0400
Subject: [PATCH] Run script updates: no --stats, also application-track
 version.

---
 contrib/run-script-smtcomp2014             |  4 +--
 contrib/run-script-smtcomp2014-application | 29 ++++++++++++++++++++++
 2 files changed, 31 insertions(+), 2 deletions(-)
 create mode 100755 contrib/run-script-smtcomp2014-application

diff --git a/contrib/run-script-smtcomp2014 b/contrib/run-script-smtcomp2014
index 5ba3506cd..a4737142a 100755
--- 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
index 000000000..94e80b940
--- /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
+
-- 
2.30.2