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--edac--i7300_edac.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.: 166 59 566 2945
INFO: Compilation, preparation and instrumentation time: 0.230020999908
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'edac_mc_free' (function is undefined)
Removed calls to 'edac_pci_release_generic_ctl' (function is undefined)
Defining function printk as symbolic
Defining function __pci_register_driver as symbolic
Defining function edac_mc_del_mc as symbolic
Removed calls to 'pci_dev_put' (function is undefined)
Defining function pci_enable_device as symbolic
Defining function edac_mc_alloc as symbolic
Removed calls to 'edac_mc_handle_error' (function is undefined)
Defining function edac_mc_add_mc as symbolic
Defining function edac_pci_create_generic_ctl as symbolic
Defining function pci_bus_write_config_dword as symbolic
Defining function pci_bus_read_config_dword as symbolic
Defining function snprintf as symbolic
Defining function pci_bus_read_config_word as symbolic
Defining function find_first_bit as symbolic
Defining function pci_get_device as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.233528852463
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 219 58 333 1847
INFO: Starting verification
KLEE: ERROR: /tmp/symbiotic-V9dqPg/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--edac--i7300_edac.ko-main.cil.out.c:4237: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-V9dqPg/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--edac--i7300_edac.ko-main.cil.out.c:4241: 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 17984 states (over memory cap)
KLEE: WARNING: killing 17952 states (over memory cap)
KLEE: WARNING: killing 17784 states (over memory cap)
KLEE: WARNING: killing 17907 states (over memory cap)
KLEE: WARNING: killing 17893 states (over memory cap)
KLEE: WARNING: killing 17896 states (over memory cap)
KLEE: WARNING: killing 18310 states (over memory cap)
KLEE: WARNING: killing 18183 states (over memory cap)
KLEE: WARNING: killing 18340 states (over memory cap)
KLEE: WARNING: killing 18627 states (over memory cap)
KLEE: WARNING: killing 18387 states (over memory cap)
KLEE: WARNING: killing 18407 states (over memory cap)
KLEE: WARNING: killing 18287 states (over memory cap)
KLEE: WARNING: killing 18314 states (over memory cap)
KLEE: WARNING: killing 18209 states (over memory cap)
KLEE: WARNING: killing 17969 states (over memory cap)
KLEE: WARNING: killing 12911 states (over memory cap)
KLEE: WARNING: killing 17150 states (over memory cap)
KLEE: WARNING: killing 12782 states (over memory cap)
KLEE: WARNING: killing 17629 states (over memory cap)
KLEE: WARNING: killing 12798 states (over memory cap)
KLEE: WARNING: killing 17478 states (over memory cap)
KLEE: WARNING: killing 12939 states (over memory cap)
KLEE: WARNING: killing 17333 states (over memory cap)
KLEE: WARNING: killing 12826 states (over memory cap)
KLEE: WARNING: killing 12291 states (over memory cap)
KLEE: WARNING: killing 17139 states (over memory cap)
KLEE: WARNING: killing 12809 states (over memory cap)
KLEE: WARNING: killing 12277 states (over memory cap)
KLEE: WARNING: killing 12237 states (over memory cap)
KLEE: WARNING: killing 12198 states (over memory cap)
KLEE: WARNING: killing 12046 states (over memory cap)
KLEE: WARNING: killing 12249 states (over memory cap)
KLEE: WARNING: killing 11970 states (over memory cap)
KLEE: WARNING: killing 12044 states (over memory cap)
KLEE: WARNING: killing 12124 states (over memory cap)
KLEE: WARNING: killing 12085 states (over memory cap)
KLEE: WARNING: killing 11935 states (over memory cap)
KLEE: WARNING: killing 12250 states (over memory cap)
KLEE: WARNING: killing 11746 states (over memory cap)
KLEE: WARNING: killing 11944 states (over memory cap)
KLEE: WARNING: killing 12023 states (over memory cap)
KLEE: WARNING: killing 12104 states (over memory cap)
KLEE: WARNING: killing 11959 states (over memory cap)
KLEE: WARNING: killing 12150 states (over memory cap)
KLEE: WARNING: killing 12005 states (over memory cap)
KLEE: WARNING: killing 12194 states (over memory cap)
KLEE: WARNING: killing 12161 states (over memory cap)
KLEE: WARNING: killing 12011 states (over memory cap)
KLEE: WARNING: killing 11863 states (over memory cap)
KLEE: WARNING: killing 11708 states (over memory cap)
KLEE: WARNING: killing 11908 states (over memory cap)
KLEE: WARNING: killing 11982 states (over memory cap)
KLEE: WARNING: killing 11949 states (over memory cap)
KLEE: WARNING: killing 11693 states (over memory cap)
KLEE: WARNING: killing 11995 states (over memory cap)
KLEE: WARNING: killing 12077 states (over memory cap)
KLEE: WARNING: killing 11708 states (over memory cap)
KLEE: WARNING: killing 11785 states (over memory cap)
KLEE: WARNING: killing 11869 states (over memory cap)
KLEE: WARNING: killing 11730 states (over memory cap)
KLEE: WARNING: killing 11810 states (over memory cap)
KLEE: WARNING: killing 11887 states (over memory cap)
KLEE: WARNING: killing 12076 states (over memory cap)
KLEE: WARNING: killing 11836 states (over memory cap)
KLEE: WARNING: killing 12240 states (over memory cap)
KLEE: WARNING: killing 11666 states (over memory cap)
KLEE: WARNING: killing 11749 states (over memory cap)
KLEE: WARNING: killing 11935 states (over memory cap)
KLEE: WARNING: killing 11906 states (over memory cap)
KLEE: WARNING: killing 11763 states (over memory cap)
KLEE: WARNING: killing 11945 states (over memory cap)
KLEE: WARNING: killing 11809 states (over memory cap)
KLEE: WARNING: killing 11672 states (over memory cap)
KLEE: WARNING: killing 11745 states (over memory cap)
KLEE: WARNING: killing 11827 states (over memory cap)
KLEE: WARNING: killing 11795 states (over memory cap)
KLEE: WARNING: killing 11766 states (over memory cap)
KLEE: WARNING: killing 11847 states (over memory cap)
KLEE: WARNING: killing 11819 states (over memory cap)
KLEE: WARNING: killing 11890 states (over memory cap)
KLEE: WARNING: killing 11753 states (over memory cap)
KLEE: WARNING: killing 11730 states (over memory cap)
KLEE: WARNING: killing 12010 states (over memory cap)
KLEE: WARNING: killing 11665 states (over memory cap)
KLEE: WARNING: killing 11752 states (over memory cap)
