From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 8 May 2013 02:12:35 +0000 (-0400)
Subject: fix for smt-eval run script
X-Git-Tag: cvc5-1.0.0~7287^2~139
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3b1f1148158efbb8e1785754baf1465776c39eae;p=cvc5.git

fix for smt-eval run script
---

diff --git a/contrib/run-script-smteval2013 b/contrib/run-script-smteval2013
index 6a2af96c7..fbdf4e039 100755
--- a/contrib/run-script-smteval2013
+++ b/contrib/run-script-smteval2013
@@ -1,16 +1,16 @@
 #!/bin/bash
 
-cat >bench-$$.smt2
-trap 'rm bench-$$.smt2' EXIT
+cvc4=./cvc4
+bench="$1"
 
-logic=$(expr "$(head -n 1 bench-$$.smt2)" : ' *(set-logic  *\([A-Z_]*\) *) *$')
+logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
 
 # use: trywith [params..]
 # to attempt a run.  Only thing printed on stdout is "sat" or "unsat", in
 # which case this run script terminates immediately.  Otherwise, this
 # function returns normally.
 function trywith {
-  result="$(./cvc4 -L smt2 --no-checking --no-interactive "$@" bench-$$.smt2)"
+  result="$($cvc4 --stats -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 -L smt2 --no-checking --no-interactive "$@" bench-$$.smt2
+  $cvc4 --stats -L smt2 --no-checking --no-interactive "$@" $bench
 }
 
 case "$logic" in