[ 0:00] + cat [ 0:00] + cat [ 0:00] + divcc -c foo.c [ 0:00] + ar r libfoo.a foo.o [ 0:00] ar: creating libfoo.a [ 0:00] + nm libfoo.a [ 0:00] + grep 'T foo' [ 0:00] 00000000 T foo [ 0:00] + cat [ 0:00] + divcc main.c libfoo.a [ 0:00] + ./a.out [ 0:00] + divine check a.out [ 0:00] states per second: 90.9091 [ 0:01] state count: 3 [ 0:01] mips: 0.22 [ 0:01] error found: no [ 0:01] a report was written to a.report [ 0:01] + rm a.out [ 0:02] + divcc main.c -L. -lfoo [ 0:02] + ./a.out [ 0:02] + divine check a.out [ 0:02] states per second: 83.3333 [ 0:03] state count: 3 [ 0:03] mips: 0.2 [ 0:03] error found: no [ 0:03] a report was written to a.report [ 0:03] + check debris [ 0:03] + test -e warning