[ 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:05] booting … done
[ 0:05] states per second: 90.9091
[ 0:05] state count: 3
[ 0:05] mips: 0.19
[ 0:05] error found: no
[ 0:05] a report was written to testcase.report
[ 0:05] + divine cc testcase.c -l m
[ 0:06] compiling testcase.c
[ 0:06] + divine verify testcase.bc
[ 0:06] loading bitcode … DiOS … LART … RR … constants … done
[ 0:08] booting … done
[ 0:08] states per second: 63.8298
[ 0:08] state count: 3
[ 0:08] mips: 0.14
[ 0:08] error found: no
[ 0:08] a report was written to testcase.report
[ 0:08] + divine verify -C,-lm testcase.c
[ 0:09] compiling testcase.c
[ 0:09] loading bitcode … DiOS … LART … RR … constants … done
[ 0:12] booting … done
[ 0:12] states per second: 76.9231
[ 0:12] state count: 3
[ 0:12] mips: 0.16
[ 0:12] error found: no
[ 0:12] a report was written to testcase.report
[ 0:12] + divine verify -C,-l,m testcase.c
[ 0:12] compiling testcase.c
[ 0:12] loading bitcode … DiOS … LART … RR … constants … done
[ 0:15] booting … done
[ 0:15] states per second: 69.7674
[ 0:15] state count: 3
[ 0:15] mips: 0.15
[ 0:15] error found: no
[ 0:15] a report was written to testcase.report
[ 0:15] + check debris
[ 0:15] + test -e warning