From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 19 Jun 2014 00:44:09 +0000 (-0400)
Subject: Version of the run script that works with trace executor; waiting on StarExec infrast... 
X-Git-Tag: cvc5-1.0.0~6758^2~4
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=34f2e94c6a4263637fb2de06eb2ca55adc987644;p=cvc5.git

Version of the run script that works with trace executor; waiting on StarExec infrastructure for testing.
---

diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application
index 2decdb98a..fb4ebe259 100755
--- a/contrib/run-script-smtcomp2014-application
+++ b/contrib/run-script-smtcomp2014-application
@@ -1,15 +1,25 @@
 #!/bin/bash
 
 cvc4=./cvc4
-bench="$1"
 
-logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
+read line
+if [ "$line" != '(set-option :print-success true)' ]; then
+  echo 'ERROR: first line supposed to be set-option :print-success, but got: "'"$line"'"' >&2
+  exit 1
+fi
+echo success
+read line
+logic=$(expr "$line" : ' *(set-logic  *\([A-Z_]*\) *) *$')
+if [ -z "$logic" ]; then
+  echo 'ERROR: second line supposed to be set-logic, but got: "'"$line"'"' >&2
+  exit 1
+fi
 
 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 --no-incremental --tear-down-incremental "$@"
+  (echo "(set-logic $logic)"; cat) | $cvc4 -L smt2 --print-success --no-checking --no-interactive --tear-down-incremental "$@"
 }
 
 case "$logic" in