[ 0:00] + cat
[ 0:00] + divine cc testcase.c
[ 0:00] compiling testcase.c
[ 0:00] + divine verify testcase.bc
[ 0:00] loading bitcode … DiOS … LART … RR … constants … ERROR: unresolved symbol (function): exp2
[ 0:02] + divine cc testcase.c -lm
[ 0:02] compiling testcase.c
[ 0:02] + divine verify testcase.bc
[ 0:02] loading bitcode … DiOS … LART … RR … constants … done
[ 0:04] booting … done
[ 0:04] states per second: 93.75
[ 0:04] state count: 3
[ 0:04] mips: 0.2
[ 0:04] error found: no
[ 0:04] a report was written to testcase.report
[ 0:04] + divine cc testcase.c -l m
[ 0:04] compiling testcase.c
[ 0:04] + divine verify testcase.bc
[ 0:05] loading bitcode … DiOS … LART … RR … constants … done
[ 0:07] booting … done
[ 0:07] states per second: 78.9474
[ 0:07] state count: 3
[ 0:07] mips: 0.17
[ 0:07] error found: no
[ 0:07] a report was written to testcase.report
[ 0:07] + divine verify -C,-lm testcase.c
[ 0:07] compiling testcase.c
[ 0:08] loading bitcode … DiOS … LART … RR … constants … done
[ 0:09] booting … done
[ 0:09] states per second: 81.0811
[ 0:09] state count: 3
[ 0:09] mips: 0.17
[ 0:09] error found: no
[ 0:09] a report was written to testcase.report
[ 0:09] + divine verify -C,-l,m testcase.c
[ 0:10] compiling testcase.c
[ 0:10] loading bitcode … DiOS … LART … RR … constants … done
[ 0:12] booting … done
[ 0:12] states per second: 103.448
[ 0:12] state count: 3
[ 0:12] mips: 0.22
[ 0:12] error found: no
[ 0:12] a report was written to testcase.report
[ 0:12] + check debris
[ 0:12] + test -e warning