fix for smt-eval run script
authorMorgan Deters <mdeters@cs.nyu.edu>
Wed, 8 May 2013 02:12:35 +0000 (22:12 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Wed, 8 May 2013 02:13:03 +0000 (22:13 -0400)
contrib/run-script-smteval2013

index 6a2af96c79623f482660094c20527b863345818f..fbdf4e039b2612729f2dcf85d600b71982780501 100755 (executable)
@@ -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