[ 0:01] + cat
[ 0:01] + divine cc testcase.c
[ 0:01] compiling testcase.c
[ 0:01] + divine verify testcase.bc
[ 0:06] ERROR: Program::insert: Unresolved symbol (function): exp2
[ 0:11] + divine cc testcase.c -lm
[ 0:11] compiling testcase.c
[ 0:12] + divine verify testcase.bc
[ 0:17] states per second: 1.65769
[ 0:28] state count: 4
[ 0:28] mips: 0.25
[ 0:28] error found: no
[ 0:28] a report was written to testcase.report
[ 0:28] + divine cc testcase.c -l m
[ 0:29] compiling testcase.c
[ 0:29] + divine verify testcase.bc
[ 0:35] states per second: 1.40056
[ 0:46] state count: 4
[ 0:46] mips: 0.21
[ 0:46] error found: no
[ 0:46] a report was written to testcase.report
[ 0:46] + divine verify -C,-lm testcase.c
[ 0:47] compiling testcase.c
[ 0:47] states per second: 1.35685
[ 1:01] state count: 4
[ 1:01] mips: 0.2
[ 1:01] error found: no
[ 1:01] a report was written to testcase.report
[ 1:01] + divine verify -C,-l,m testcase.c
[ 1:02] compiling testcase.c
[ 1:02] states per second: 1.4477
[ 1:15] state count: 4
[ 1:15] mips: 0.21
[ 1:15] error found: no
[ 1:15] a report was written to testcase.report
[ 1:15] + check debris
[ 1:17]      1	#include <math.h>
[ 1:17]      2	#include <assert.h>
[ 1:17]      3	
[ 1:17]      4	int main() {
[ 1:17]      5	    int x = exp2( 2 );
[ 1:17]      6	    assert( x == 4 );
[ 1:17]      7	}
[ 1:17]