[ 0:00] + divine cc -o testcase.bc /home/xrockai/src/divine/nightly/test/svcomp/pthread/buggy_simple_loop1_vf_false.c [ 0:00] compiling /home/xrockai/src/divine/nightly/test/svcomp/pthread/buggy_simple_loop1_vf_false.c [ 0:00] + divine verify --max-memory 4GiB --max-time 600 --threads 2 --report-filename verify.out --solver z3 --symbolic --svcomp -o nofail:malloc testcase.bc [ 0:00] loading bitcode … DiOS … LART … RR … constants … done [ 0:03] booting … done [ 0:03] searching: 1645 states in 1:00, avg 27.4/s @ 27.4 kips, queued: 30 [ 1:03] searching: 2729 states in 2:00, avg 22.7/s @ 25.4 kips, queued: 50 [ 2:03] searching: 3829 states in 3:00, avg 21.3/s @ 23.0 kips, queued: 76 [ 3:03] searching: 4463 states in 4:00, avg 18.6/s @ 19.9 kips, queued: 92 [ 4:03] searching: 4781 states in 5:00, avg 15.9/s @ 17.2 kips, queued: 100 [ 5:03] searching: 4998 states in 6:00, avg 13.9/s @ 14.9 kips, queued: 100 [ 6:03] searching: 5220 states in 7:00, avg 12.4/s @ 13.3 kips, queued: 108 [ 7:03] searching: 5752 states in 8:00, avg 12.0/s @ 12.7 kips, queued: 120 [ 8:03] searching: 6359 states in 9:00, avg 11.8/s @ 13.0 kips, queued: 132 [ 9:03] searching: 6914 states in 10:00, avg 11.5/s @ 13.0 kips, queued: 140 [10:03] states per second: 11.5232 [10:03] state count: 6914 [10:03] mips: 0.013 [10:03] E: resource exhausted: time limit (600s / 600s) [10:03] /home/xrockai/src/divine/nightly/test/lib/verify: line 15: 16507 Aborted divine "$@"