bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.c


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 35 57 324 1287
INFO: Compilation, preparation and instrumentation time: 0.104088068008
Removed calls to 'i2c_del_driver' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'regulator_unregister' (function is undefined)
Defining function regulator_list_voltage_linear as symbolic
Defining function regulator_map_voltage_linear as symbolic
Defining function rdev_get_drvdata as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Defining function i2c_smbus_read_byte as symbolic
Defining function dev_err as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Defining function i2c_smbus_write_byte as symbolic
Defining function i2c_register_driver as symbolic
Defining function dev_get_drvdata as symbolic
Defining function devm_kzalloc as symbolic
Defining function regulator_register as symbolic
Defining function dev_set_drvdata as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.104480028152
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 81 64 235 844
INFO: Starting verification
KLEE: ERROR: /tmp/symbiotic-849GNC/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.c:2261: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-849GNC/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.c:2280: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-849GNC/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.c:2324: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 24761 states (over memory cap)
KLEE: WARNING: killing 24788 states (over memory cap)
KLEE: WARNING: killing 24820 states (over memory cap)
KLEE: WARNING: killing 24485 states (over memory cap)
KLEE: WARNING: killing 24168 states (over memory cap)
KLEE: WARNING: killing 25106 states (over memory cap)
KLEE: WARNING: killing 17751 states (over memory cap)
KLEE: WARNING: killing 24715 states (over memory cap)
KLEE: WARNING: killing 17777 states (over memory cap)
KLEE: WARNING: killing 24520 states (over memory cap)
KLEE: WARNING: killing 17984 states (over memory cap)
KLEE: WARNING: killing 24857 states (over memory cap)
KLEE: WARNING: killing 18027 states (over memory cap)
KLEE: WARNING: killing 17792 states (over memory cap)
KLEE: WARNING: killing 17397 states (over memory cap)
KLEE: WARNING: killing 17343 states (over memory cap)
KLEE: WARNING: killing 17297 states (over memory cap)
KLEE: WARNING: killing 17418 states (over memory cap)
KLEE: WARNING: killing 17195 states (over memory cap)
KLEE: WARNING: killing 17822 states (over memory cap)
KLEE: WARNING: killing 17768 states (over memory cap)
KLEE: WARNING: killing 17381 states (over memory cap)
KLEE: WARNING: killing 17329 states (over memory cap)
KLEE: WARNING: killing 17435 states (over memory cap)
KLEE: WARNING: killing 17041 states (over memory cap)
KLEE: WARNING: killing 17159 states (over memory cap)
KLEE: WARNING: killing 17603 states (over memory cap)
KLEE: WARNING: killing 17881 states (over memory cap)
KLEE: WARNING: killing 17003 states (over memory cap)
KLEE: WARNING: killing 17116 states (over memory cap)
KLEE: WARNING: killing 17391 states (over memory cap)
KLEE: WARNING: killing 17331 states (over memory cap)
KLEE: WARNING: killing 17439 states (over memory cap)
KLEE: WARNING: killing 17212 states (over memory cap)
KLEE: WARNING: killing 17489 states (over memory cap)
KLEE: WARNING: killing 17593 states (over memory cap)
KLEE: WARNING: killing 17859 states (over memory cap)
KLEE: WARNING: killing 17805 states (over memory cap)
KLEE: WARNING: killing 17269 states (over memory cap)
KLEE: WARNING: killing 17218 states (over memory cap)
KLEE: WARNING: killing 17480 states (over memory cap)
KLEE: WARNING: killing 17428 states (over memory cap)
KLEE: WARNING: killing 16904 states (over memory cap)
KLEE: WARNING: killing 17163 states (over memory cap)
KLEE: WARNING: killing 17274 states (over memory cap)
KLEE: WARNING: killing 17534 states (over memory cap)
KLEE: WARNING: killing 17639 states (over memory cap)
KLEE: WARNING: killing 17436 states (over memory cap)
KLEE: WARNING: killing 17547 states (over memory cap)
KLEE: WARNING: killing 17643 states (over memory cap)
KLEE: WARNING: killing 17441 states (over memory cap)
KLEE: WARNING: killing 17545 states (over memory cap)
KLEE: WARNING: killing 17192 states (over memory cap)
KLEE: WARNING: killing 17448 states (over memory cap)
KLEE: WARNING: killing 17390 states (over memory cap)
KLEE: WARNING: killing 17799 states (over memory cap)
KLEE: WARNING: killing 17452 states (over memory cap)
KLEE: WARNING: killing 17091 states (over memory cap)
KLEE: WARNING: killing 17497 states (over memory cap)
KLEE: WARNING: killing 17295 states (over memory cap)
KLEE: WARNING: killing 17556 states (over memory cap)
KLEE: WARNING: killing 17498 states (over memory cap)
KLEE: WARNING: killing 17296 states (over memory cap)
KLEE: WARNING: killing 17396 states (over memory cap)
KLEE: WARNING: killing 17347 states (over memory cap)
KLEE: WARNING: killing 17301 states (over memory cap)
KLEE: WARNING: killing 17254 states (over memory cap)
KLEE: WARNING: killing 17499 states (over memory cap)
KLEE: WARNING: killing 17454 states (over memory cap)
KLEE: WARNING: killing 17564 states (over memory cap)
KLEE: WARNING: killing 17367 states (over memory cap)
KLEE: WARNING: killing 17472 states (over memory cap)
KLEE: WARNING: killing 17419 states (over memory cap)
KLEE: WARNING: killing 17368 states (over memory cap)
KLEE: WARNING: killing 17323 states (over memory cap)
KLEE: WARNING: killing 16985 states (over memory cap)
KLEE: WARNING: killing 17372 states (over memory cap)
KLEE: WARNING: killing 17474 states (over memory cap)
KLEE: WARNING: killing 17431 states (over memory cap)
KLEE: WARNING: killing 17387 states (over memory cap)
KLEE: WARNING: killing 17334 states (over memory cap)
KLEE: WARNING: killing 17431 states (over memory cap)
KLEE: WARNING: killing 17387 states (over memory cap)
KLEE: WARNING: killing 17201 states (over memory cap)
KLEE: WARNING: killing 17437 states (over memory cap)
KLEE: WARNING: killing 17253 states (over memory cap)
KLEE: WARNING: killing 17768 states (over memory cap)
KLEE: WARNING: killing 17445 states (over memory cap)
KLEE: WARNING: killing 17120 states (over memory cap)
KLEE: WARNING: killing 17348 states (over memory cap)
KLEE: WARNING: killing 17024 states (over memory cap)
KLEE: WARNING: killing 17114 states (over memory cap)
KLEE: WARNING: killing 17350 states (over memory cap)
KLEE: WARNING: killing 17165 states (over memory cap)
KLEE: WARNING: killing 17269 states (over memory cap)
KLEE: WARNING: killing 17074 states (over memory cap)
KLEE: WARNING: killing 17175 states (over memory cap)
