summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-06-18 21:55:25 +0000
committerMorgan Deters <mdeters@gmail.com>2012-06-18 21:55:25 +0000
commita850215587ed07a536f77333c729b32966881716 (patch)
tree023a4b304d56a3fc98e86f786de659828778f9b2 /contrib
parent3b14e8b30e9fe46c1919e7e732a4641698f61778 (diff)
unnecessary ^ in regular expression; warning produced on smt-exec
Diffstat (limited to 'contrib')
-rwxr-xr-xcontrib/run-script-smtcomp20122
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/run-script-smtcomp2012 b/contrib/run-script-smtcomp2012
index 2183df8ce..bb4a9305f 100755
--- a/contrib/run-script-smtcomp2012
+++ b/contrib/run-script-smtcomp2012
@@ -3,7 +3,7 @@
cat >bench-$$.smt2
trap 'rm bench-$$.smt2' EXIT
-logic=$(expr "$(head -n 1 bench-$$.smt2)" : '^ *(set-logic *\([A-Z_]*\) *) *$')
+logic=$(expr "$(head -n 1 bench-$$.smt2)" : ' *(set-logic *\([A-Z_]*\) *) *$')
# use: trywith [params..]
# to attempt a run. Only thing printed on stdout is "sat" or "unsat", in
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback