gib# out run test/svcomp/product-lines/minepump_spec2_product42_false.cil.chk.c gib# cmd /usr/bin/env gib# srcdir=/home/xrockai/src/divine/nightly gib# PATH=/home/xrockai/src/divine/nightly/test/lib:/usr/bin:/bin:/opt/klee/bin gib# sh gib# /home/xrockai/src/divine/nightly/test/lib/check gib# test/svcomp/product-lines/minepump_spec2_product42_false.cil.chk.c expect --result error --location-comment ERROR cc -o test.bc /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec2_product42_false.cil.chk.c verify --symbolic --solver stp -o nofail:malloc test.bc compiling /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec2_product42_false.cil.chk.c /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec2_product42_false.cil.chk.c:49:44: warning: incompatible redeclaration of library function 'malloc' extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ; ^ /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec2_product42_false.cil.chk.c:49:44: note: 'malloc' is a builtin with type 'void *(unsigned long)' 1 warning generated. loading bitcode … DiOS … LART … RR … constants … done booting … done searching: 145 states in 1:00, avg 2.4/s @ 158.5 kips, queued: 2 searching: 721 states in 2:00, avg 6.0/s @ 260.3 kips, queued: 36 searching: 1297 states in 3:00, avg 7.2/s @ 291.1 kips, queued: 52 states per second: 7.46279 state count: 1659 mips: 0.31 symbolic: 1 error found: yes error trace: | ASSUME (not (not (= var_1 #x00000000))) ASSUME (not (not (= var_2 #x00000000))) ASSUME (not (not (= var_3 #x00000000))) ASSUME (not (not (= var_4 #x00000000))) ASSUME (not (= var_5 #x00000000)) ASSUME (not (not (= var_6 #x00000000))) ASSUME (not (not (= var_7 #x00000000))) ASSUME (not (not (= var_8 #x00000000))) ASSUME (not (not (= var_9 #x00000000))) ASSUME (not (= var_10 #x00000000)) ASSUME (not (not (= var_11 #x00000000))) ASSUME (not (not (= var_12 #x00000000))) ASSUME (not (not (= var_13 #x00000000))) ASSUME (not (not (= var_14 #x00000000))) ASSUME (not (not (= var_15 #x00000000))) ASSUME (not (not (= var_16 #x00000000))) FAULT: verifier error called [0] FATAL: dios assertion violation in userspace active stack: - symbol: void __dios::FaultBase::handler<__dios::Context>(_VM_Fault, _VM_Frame*, void (*)()) location: /dios/sys/fault.hpp:118 - symbol: __dios_fault location: /dios/arch/divm/fault.c:12 - symbol: __VERIFIER_error location: /dios/libc/svcomp/svcomp-error.cpp:5 - symbol: __automaton_fail location: /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec2_product42_false.cil.chk.c:849 - symbol: __utac_acc__Specification2_spec__2 location: /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec2_product42_false.cil.chk.c:695 - symbol: timeShift location: /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec2_product42_false.cil.chk.c:514 - symbol: test location: /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec2_product42_false.cil.chk.c:471 - symbol: runTest location: /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec2_product42_false.cil.chk.c:816 - symbol: main location: /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec2_product42_false.cil.chk.c:834 - symbol: __dios_start location: /dios/libc/sys/start.cpp:94