bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-challenges/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-media-usb-dvb-usb-dvb-usb-cxusb_true-unreach-call.cil.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.: 419 368 2320 12356
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.532727956772
Defining function dib7000p_set_gpio as symbolic
Removed calls to 'vfree' (function is undefined)
Defining function usb_cypress_load_firmware as symbolic
Defining function external_allocated_data as symbolic
Removed calls to '__symbol_put' (function is undefined)
Defining function usb_set_interface as symbolic
Defining function printk as symbolic
Removed calls to 'msleep' (function is undefined)
Defining function __symbol_get as symbolic
Defining function __request_module as symbolic
Defining function dvb_usb_generic_write as symbolic
Defining function dvb_usb_generic_rw as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_lock_interruptible_nested as symbolic
Removed calls to 'ldv_after_alloc' (function is undefined)
Defining function usb_clear_halt as symbolic
Defining function usb_bulk_msg as symbolic
Removed calls to 'usb_deregister' (function is undefined)
Defining function usb_register_driver as symbolic
Defining function ldv_pre_usb_register_driver as symbolic
Removed calls to '__const_udelay' (function is undefined)
Defining function dib7000p_i2c_enumeration as symbolic
Defining function dib7000p_get_i2c_master as symbolic
Defining function dib0070_wbd_offset as symbolic
Defining function dib7000p_set_wbd_ref as symbolic
Defining function dvb_usb_device_init as symbolic
Removed calls to 'ldv_assert' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'dvb_usb_device_exit' (function is undefined)
Removed calls to 'ldv_pre_probe' (function is undefined)
Linked our definitions to these undefined functions:
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.458549022675
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 488 384 1074 7021
INFO: Starting verification
KLEE: WARNING: undefined reference to function: dvb_usb_device_exit
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_dba00afa-5092-4759-acd0-6521c90cb0c9/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 24133 states (over memory cap)
KLEE: WARNING: killing 18160 states (over memory cap)
KLEE: WARNING: killing 17612 states (over memory cap)
KLEE: WARNING: killing 17566 states (over memory cap)
KLEE: WARNING: killing 17848 states (over memory cap)
KLEE: WARNING: killing 16838 states (over memory cap)
KLEE: WARNING: killing 17770 states (over memory cap)
KLEE: WARNING: killing 17566 states (over memory cap)
KLEE: WARNING: killing 17213 states (over memory cap)
KLEE: WARNING: killing 17343 states (over memory cap)
KLEE: WARNING: killing 32707 states (over memory cap)
KLEE: WARNING: killing 17731 states (over memory cap)
KLEE: WARNING: killing 16090 states (over memory cap)
KLEE: WARNING: killing 16706 states (over memory cap)
KLEE: WARNING: killing 17314 states (over memory cap)
KLEE: WARNING: killing 17774 states (over memory cap)
KLEE: WARNING: killing 17269 states (over memory cap)
KLEE: WARNING: killing 17398 states (over memory cap)
KLEE: WARNING: killing 17528 states (over memory cap)
KLEE: WARNING: killing 16862 states (over memory cap)
KLEE: WARNING: killing 17466 states (over memory cap)
KLEE: WARNING: killing 17752 states (over memory cap)
KLEE: WARNING: killing 18672 states (over memory cap)
KLEE: WARNING: killing 18483 states (over memory cap)
KLEE: WARNING: killing 19083 states (over memory cap)
KLEE: WARNING: killing 18742 states (over memory cap)
KLEE: WARNING: killing 19341 states (over memory cap)
KLEE: WARNING: killing 19155 states (over memory cap)
KLEE: WARNING: killing 19591 states (over memory cap)
KLEE: WARNING: killing 19417 states (over memory cap)
KLEE: WARNING: killing 20003 states (over memory cap)
KLEE: WARNING: killing 20757 states (over memory cap)
KLEE: WARNING: killing 19800 states (over memory cap)
KLEE: WARNING: killing 20393 states (over memory cap)
KLEE: WARNING: killing 20998 states (over memory cap)
KLEE: WARNING: killing 20040 states (over memory cap)
KLEE: WARNING: killing 19388 states (over memory cap)
KLEE: WARNING: killing 20133 states (over memory cap)
KLEE: WARNING: killing 20105 states (over memory cap)
KLEE: WARNING: killing 19466 states (over memory cap)
KLEE: WARNING: killing 19905 states (over memory cap)
KLEE: WARNING: killing 19727 states (over memory cap)
KLEE: WARNING: killing 20168 states (over memory cap)
KLEE: WARNING: killing 20307 states (over memory cap)
KLEE: WARNING: killing 20131 states (over memory cap)
KLEE: WARNING: killing 19644 states (over memory cap)
KLEE: WARNING: killing 18396 states (over memory cap)
KLEE: WARNING: killing 18072 states (over memory cap)
KLEE: WARNING: killing 18349 states (over memory cap)
KLEE: WARNING: killing 19541 states (over memory cap)
KLEE: WARNING: killing 19683 states (over memory cap)
KLEE: WARNING: killing 18590 states (over memory cap)
KLEE: WARNING: killing 18414 states (over memory cap)
KLEE: WARNING: killing 18845 states (over memory cap)
KLEE: WARNING: killing 18828 states (over memory cap)
KLEE: WARNING: killing 19253 states (over memory cap)
KLEE: WARNING: killing 19234 states (over memory cap)
KLEE: WARNING: killing 18159 states (over memory cap)
KLEE: WARNING: killing 18133 states (over memory cap)
KLEE: WARNING: killing 19015 states (over memory cap)
KLEE: WARNING: killing 18991 states (over memory cap)
KLEE: WARNING: killing 17467 states (over memory cap)
KLEE: WARNING: killing 18641 states (over memory cap)
KLEE: WARNING: killing 19070 states (over memory cap)
KLEE: WARNING: killing 18602 states (over memory cap)
KLEE: WARNING: killing 18730 states (over memory cap)
KLEE: WARNING: killing 19157 states (over memory cap)
KLEE: WARNING: killing 19431 states (over memory cap)
KLEE: WARNING: killing 17918 states (over memory cap)
KLEE: WARNING: killing 18498 states (over memory cap)
KLEE: WARNING: killing 18918 states (over memory cap)
KLEE: WARNING: killing 18448 states (over memory cap)
KLEE: WARNING: killing 18880 states (over memory cap)
KLEE: WARNING: killing 18857 states (over memory cap)
KLEE: WARNING: killing 18400 states (over memory cap)
KLEE: WARNING: killing 18965 states (over memory cap)
KLEE: WARNING: killing 17918 states (over memory cap)
KLEE: WARNING: killing 18333 states (over memory cap)
KLEE: WARNING: killing 18021 states (over memory cap)
KLEE: WARNING: killing 18291 states (over memory cap)
KLEE: WARNING: killing 17826 states (over memory cap)
KLEE: WARNING: killing 19280 states (over memory cap)
KLEE: WARNING: killing 19409 states (over memory cap)
KLEE: WARNING: killing 19540 states (over memory cap)
KLEE: WARNING: killing 19532 states (over memory cap)
KLEE: WARNING: killing 20238 states (over memory cap)
KLEE: WARNING: killing 18911 states (over memory cap)
KLEE: WARNING: killing 18737 states (over memory cap)
KLEE: WARNING: killing 18719 states (over memory cap)
KLEE: WARNING: killing 19133 states (over memory cap)
KLEE: WARNING: killing 17800 states (over memory cap)
KLEE: WARNING: killing 18657 states (over memory cap)
KLEE: WARNING: killing 19510 states (over memory cap)
KLEE: WARNING: killing 18914 states (over memory cap)
KLEE: WARNING: killing 18746 states (over memory cap)
KLEE: WARNING: killing 19155 states (over memory cap)
KLEE: WARNING: killing 18997 states (over memory cap)
KLEE: WARNING: killing 18982 states (over memory cap)
KLEE: WARNING: killing 18963 states (over memory cap)
KLEE: WARNING: killing 18947 states (over memory cap)
KLEE: WARNING: killing 18489 states (over memory cap)
KLEE: WARNING: killing 18035 states (over memory cap)
KLEE: WARNING: killing 18300 states (over memory cap)
KLEE: WARNING: killing 19441 states (over memory cap)
KLEE: WARNING: killing 18553 states (over memory cap)
KLEE: WARNING: killing 18111 states (over memory cap)
KLEE: WARNING: killing 19092 states (over memory cap)
KLEE: WARNING: killing 19214 states (over memory cap)
KLEE: WARNING: killing 18336 states (over memory cap)
KLEE: WARNING: killing 19466 states (over memory cap)
KLEE: WARNING: killing 19147 states (over memory cap)
KLEE: WARNING: killing 18992 states (over memory cap)
KLEE: WARNING: killing 18968 states (over memory cap)
KLEE: WARNING: killing 18796 states (over memory cap)
KLEE: WARNING: killing 18929 states (over memory cap)
KLEE: WARNING: killing 19474 states (over memory cap)
KLEE: WARNING: killing 19029 states (over memory cap)
KLEE: WARNING: killing 18157 states (over memory cap)
KLEE: WARNING: killing 18557 states (over memory cap)
KLEE: WARNING: killing 18550 states (over memory cap)
KLEE: WARNING: killing 18672 states (over memory cap)
KLEE: WARNING: killing 19072 states (over memory cap)
KLEE: WARNING: killing 18340 states (over memory cap)
KLEE: WARNING: killing 18466 states (over memory cap)
KLEE: WARNING: killing 19160 states (over memory cap)
KLEE: WARNING: killing 18850 states (over memory cap)
KLEE: WARNING: killing 19114 states (over memory cap)
KLEE: WARNING: killing 19659 states (over memory cap)
KLEE: WARNING: killing 18803 states (over memory cap)
KLEE: WARNING: killing 18359 states (over memory cap)
KLEE: WARNING: killing 19464 states (over memory cap)
KLEE: WARNING: killing 18325 states (over memory cap)
KLEE: WARNING: killing 17888 states (over memory cap)
KLEE: WARNING: killing 18010 states (over memory cap)
KLEE: WARNING: killing 18263 states (over memory cap)
KLEE: WARNING: killing 18943 states (over memory cap)
KLEE: WARNING: killing 18650 states (over memory cap)
KLEE: WARNING: killing 19055 states (over memory cap)
KLEE: WARNING: killing 19035 states (over memory cap)
KLEE: WARNING: killing 18733 states (over memory cap)
KLEE: WARNING: killing 18711 states (over memory cap)
KLEE: WARNING: killing 18558 states (over memory cap)
KLEE: WARNING: killing 19100 states (over memory cap)
KLEE: WARNING: killing 19359 states (over memory cap)
KLEE: WARNING: killing 18641 states (over memory cap)
KLEE: WARNING: killing 18485 states (over memory cap)
KLEE: WARNING: killing 18460 states (over memory cap)
KLEE: WARNING: killing 18166 states (over memory cap)
KLEE: WARNING: killing 19113 states (over memory cap)
KLEE: WARNING: killing 18821 states (over memory cap)
KLEE: WARNING: killing 18933 states (over memory cap)
KLEE: WARNING: killing 19198 states (over memory cap)
KLEE: WARNING: killing 19456 states (over memory cap)
KLEE: WARNING: killing 18616 states (over memory cap)
KLEE: WARNING: killing 17772 states (over memory cap)
KLEE: WARNING: killing 18713 states (over memory cap)
KLEE: WARNING: killing 18558 states (over memory cap)
KLEE: WARNING: killing 19633 states (over memory cap)
KLEE: WARNING: killing 19211 states (over memory cap)
KLEE: WARNING: killing 18919 states (over memory cap)
KLEE: WARNING: killing 18222 states (over memory cap)
KLEE: WARNING: killing 18477 states (over memory cap)
KLEE: WARNING: killing 18457 states (over memory cap)
KLEE: WARNING: killing 18442 states (over memory cap)
KLEE: WARNING: killing 18421 states (over memory cap)
KLEE: WARNING: killing 18940 states (over memory cap)
KLEE: WARNING: killing 18796 states (over memory cap)
KLEE: WARNING: killing 19315 states (over memory cap)
KLEE: WARNING: killing 19429 states (over memory cap)
KLEE: WARNING: killing 19953 states (over memory cap)
KLEE: WARNING: killing 18998 states (over memory cap)
KLEE: WARNING: killing 19516 states (over memory cap)
KLEE: WARNING: killing 18413 states (over memory cap)
KLEE: WARNING: killing 18258 states (over memory cap)
KLEE: WARNING: killing 18240 states (over memory cap)
KLEE: WARNING: killing 19161 states (over memory cap)
KLEE: WARNING: killing 19281 states (over memory cap)
KLEE: WARNING: killing 19268 states (over memory cap)
KLEE: WARNING: killing 18442 states (over memory cap)
KLEE: WARNING: killing 18693 states (over memory cap)
KLEE: WARNING: killing 18281 states (over memory cap)
KLEE: WARNING: killing 18390 states (over memory cap)
KLEE: WARNING: killing 19049 states (over memory cap)
KLEE: WARNING: killing 19030 states (over memory cap)
KLEE: WARNING: killing 18077 states (over memory cap)
KLEE: WARNING: killing 18598 states (over memory cap)
KLEE: WARNING: killing 18444 states (over memory cap)
KLEE: WARNING: killing 18028 states (over memory cap)
KLEE: WARNING: killing 18938 states (over memory cap)
KLEE: WARNING: killing 18130 states (over memory cap)
KLEE: WARNING: killing 18907 states (over memory cap)
KLEE: WARNING: killing 19024 states (over memory cap)
KLEE: WARNING: killing 18343 states (over memory cap)
KLEE: WARNING: killing 17933 states (over memory cap)
KLEE: WARNING: killing 18571 states (over memory cap)
KLEE: WARNING: killing 19091 states (over memory cap)
KLEE: WARNING: killing 18941 states (over memory cap)
KLEE: WARNING: killing 18786 states (over memory cap)
KLEE: WARNING: killing 19307 states (over memory cap)
KLEE: WARNING: killing 19026 states (over memory cap)
KLEE: WARNING: killing 19273 states (over memory cap)
KLEE: WARNING: killing 19395 states (over memory cap)
KLEE: WARNING: killing 18707 states (over memory cap)
