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--isdn--hardware--eicon--divadidd.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.: 82 105 583 2854
INFO: Compilation, preparation and instrumentation time: 0.232316017151
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Defining function printk as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function proc_mkdir as symbolic
Defining function proc_create_data 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:
  strchr
  strcpy
  strlen
  __memcpy
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.192873001099
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 147 103 442 2104
INFO: Starting verification
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 14556 states (over memory cap)
KLEE: WARNING: killing 14470 states (over memory cap)
KLEE: WARNING: killing 14677 states (over memory cap)
KLEE: WARNING: killing 15017 states (over memory cap)
KLEE: WARNING: killing 15075 states (over memory cap)
KLEE: WARNING: killing 15409 states (over memory cap)
KLEE: WARNING: killing 15329 states (over memory cap)
KLEE: WARNING: killing 15658 states (over memory cap)
KLEE: WARNING: killing 15581 states (over memory cap)
KLEE: WARNING: killing 15774 states (over memory cap)
KLEE: WARNING: killing 16105 states (over memory cap)
KLEE: WARNING: killing 16035 states (over memory cap)
KLEE: WARNING: killing 16097 states (over memory cap)
KLEE: WARNING: killing 16420 states (over memory cap)
KLEE: WARNING: killing 16471 states (over memory cap)
KLEE: WARNING: killing 16658 states (over memory cap)
KLEE: WARNING: killing 16723 states (over memory cap)
KLEE: WARNING: killing 16774 states (over memory cap)
KLEE: WARNING: killing 16953 states (over memory cap)
KLEE: WARNING: killing 16876 states (over memory cap)
KLEE: WARNING: killing 17185 states (over memory cap)
KLEE: WARNING: killing 17239 states (over memory cap)
KLEE: WARNING: killing 17290 states (over memory cap)
KLEE: WARNING: killing 17210 states (over memory cap)
KLEE: WARNING: killing 17264 states (over memory cap)
KLEE: WARNING: killing 17561 states (over memory cap)
KLEE: WARNING: killing 17489 states (over memory cap)
KLEE: WARNING: killing 12756 states (over memory cap)
KLEE: WARNING: killing 16975 states (over memory cap)
KLEE: WARNING: killing 17399 states (over memory cap)
KLEE: WARNING: killing 12471 states (over memory cap)
KLEE: WARNING: killing 17015 states (over memory cap)
KLEE: WARNING: killing 12627 states (over memory cap)
KLEE: WARNING: killing 16892 states (over memory cap)
KLEE: WARNING: killing 12539 states (over memory cap)
KLEE: WARNING: killing 17135 states (over memory cap)
KLEE: WARNING: killing 12684 states (over memory cap)
KLEE: WARNING: killing 12164 states (over memory cap)
KLEE: WARNING: killing 17097 states (over memory cap)
KLEE: WARNING: killing 12920 states (over memory cap)
KLEE: WARNING: killing 12160 states (over memory cap)
KLEE: WARNING: killing 16794 states (over memory cap)
KLEE: WARNING: killing 12552 states (over memory cap)
KLEE: WARNING: killing 12031 states (over memory cap)
KLEE: WARNING: killing 11888 states (over memory cap)
KLEE: WARNING: killing 11971 states (over memory cap)
KLEE: WARNING: killing 12057 states (over memory cap)
KLEE: WARNING: killing 12027 states (over memory cap)
KLEE: WARNING: killing 11875 states (over memory cap)
KLEE: WARNING: killing 12079 states (over memory cap)
KLEE: WARNING: killing 12044 states (over memory cap)
KLEE: WARNING: killing 11892 states (over memory cap)
KLEE: WARNING: killing 11858 states (over memory cap)
KLEE: WARNING: killing 11946 states (over memory cap)
KLEE: WARNING: killing 12144 states (over memory cap)
KLEE: WARNING: killing 11884 states (over memory cap)
KLEE: WARNING: killing 11848 states (over memory cap)
KLEE: WARNING: killing 11821 states (over memory cap)
KLEE: WARNING: killing 12018 states (over memory cap)
KLEE: WARNING: killing 12104 states (over memory cap)
KLEE: WARNING: killing 12067 states (over memory cap)
KLEE: WARNING: killing 11922 states (over memory cap)
KLEE: WARNING: killing 11891 states (over memory cap)
KLEE: WARNING: killing 11861 states (over memory cap)
KLEE: WARNING: killing 11943 states (over memory cap)
KLEE: WARNING: killing 12026 states (over memory cap)
KLEE: WARNING: killing 12001 states (over memory cap)
KLEE: WARNING: killing 12190 states (over memory cap)
KLEE: WARNING: killing 11830 states (over memory cap)
KLEE: WARNING: killing 12132 states (over memory cap)
KLEE: WARNING: killing 12100 states (over memory cap)
KLEE: WARNING: killing 11850 states (over memory cap)
KLEE: WARNING: killing 12037 states (over memory cap)
KLEE: WARNING: killing 11899 states (over memory cap)
KLEE: WARNING: killing 11976 states (over memory cap)
KLEE: WARNING: killing 11949 states (over memory cap)
KLEE: WARNING: killing 11807 states (over memory cap)
KLEE: WARNING: killing 11886 states (over memory cap)
KLEE: WARNING: killing 11967 states (over memory cap)
KLEE: WARNING: killing 12053 states (over memory cap)
KLEE: WARNING: killing 11915 states (over memory cap)
KLEE: WARNING: killing 11997 states (over memory cap)
KLEE: WARNING: killing 12180 states (over memory cap)
KLEE: WARNING: killing 12046 states (over memory cap)
KLEE: WARNING: killing 11910 states (over memory cap)
KLEE: WARNING: killing 11882 states (over memory cap)
KLEE: WARNING: killing 11854 states (over memory cap)
KLEE: WARNING: killing 11930 states (over memory cap)
KLEE: WARNING: killing 12009 states (over memory cap)
KLEE: WARNING: killing 11871 states (over memory cap)
KLEE: WARNING: killing 11736 states (over memory cap)
KLEE: WARNING: killing 11706 states (over memory cap)
KLEE: WARNING: killing 11995 states (over memory cap)
KLEE: WARNING: killing 11759 states (over memory cap)
KLEE: WARNING: killing 12046 states (over memory cap)
