bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--usb--dvb-usb--dvb-usb-cxusb.ko-entry_point_false-unreach-call.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.: 159 104 1140 6870
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.443158149719
Removed calls to '__symbol_put' (function is undefined)
Defining function printk as symbolic
Defining function dvb_usb_generic_write as symbolic
Defining function dvb_usb_generic_rw as symbolic
Defining function __symbol_get as symbolic
Defining function __request_module as symbolic
Defining function usb_set_interface as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_lock_interruptible_nested as symbolic
Removed calls to 'vfree' (function is undefined)
Defining function vmalloc as symbolic
Defining function usb_cypress_load_firmware as symbolic
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Defining function dib0070_wbd_offset as symbolic
Defining function usb_clear_halt as symbolic
Defining function usb_bulk_msg as symbolic
Removed calls to 'i2c_unregister_device' (function is undefined)
Defining function strlcpy as symbolic
Defining function i2c_new_device as symbolic
Removed calls to 'dvb_usb_device_exit' (function is undefined)
Defining function dvb_usb_device_init as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Defining function usb_register_driver as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  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.415405035019
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 260 118 672 4624
INFO: Starting verification
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_6de5284a-37e9-4b72-b788-eaf80405c872/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 19067 states (over memory cap)
KLEE: WARNING: killing 21007 states (over memory cap)
KLEE: WARNING: killing 21621 states (over memory cap)
KLEE: WARNING: killing 21629 states (over memory cap)
KLEE: WARNING: killing 22243 states (over memory cap)
KLEE: WARNING: killing 21398 states (over memory cap)
KLEE: WARNING: killing 20887 states (over memory cap)
KLEE: WARNING: killing 21907 states (over memory cap)
KLEE: WARNING: killing 21663 states (over memory cap)
KLEE: WARNING: killing 22345 states (over memory cap)
KLEE: WARNING: killing 23957 states (over memory cap)
KLEE: WARNING: killing 23666 states (over memory cap)
KLEE: WARNING: killing 24751 states (over memory cap)
KLEE: WARNING: killing 24597 states (over memory cap)
KLEE: WARNING: killing 25359 states (over memory cap)
KLEE: WARNING: killing 25132 states (over memory cap)
KLEE: WARNING: killing 24512 states (over memory cap)
KLEE: WARNING: killing 23307 states (over memory cap)
KLEE: WARNING: killing 24266 states (over memory cap)
KLEE: WARNING: killing 23132 states (over memory cap)
KLEE: WARNING: killing 24336 states (over memory cap)
KLEE: WARNING: killing 22876 states (over memory cap)
KLEE: WARNING: killing 23043 states (over memory cap)
KLEE: WARNING: killing 23343 states (over memory cap)
KLEE: WARNING: killing 22533 states (over memory cap)
KLEE: WARNING: killing 23413 states (over memory cap)
KLEE: WARNING: killing 22862 states (over memory cap)
KLEE: WARNING: killing 23867 states (over memory cap)
KLEE: WARNING: killing 23396 states (over memory cap)
KLEE: WARNING: killing 21501 states (over memory cap)
KLEE: WARNING: killing 23528 states (over memory cap)
KLEE: WARNING: killing 23630 states (over memory cap)
KLEE: WARNING: killing 23284 states (over memory cap)
KLEE: WARNING: killing 24419 states (over memory cap)
KLEE: WARNING: killing 24213 states (over memory cap)
KLEE: WARNING: killing 23808 states (over memory cap)
KLEE: WARNING: killing 23269 states (over memory cap)
KLEE: WARNING: killing 24460 states (over memory cap)
KLEE: WARNING: killing 23165 states (over memory cap)
KLEE: WARNING: killing 23137 states (over memory cap)
KLEE: WARNING: killing 23757 states (over memory cap)
KLEE: WARNING: killing 22906 states (over memory cap)
KLEE: WARNING: killing 23135 states (over memory cap)
KLEE: WARNING: killing 22726 states (over memory cap)
KLEE: WARNING: killing 23337 states (over memory cap)
KLEE: WARNING: killing 23183 states (over memory cap)
KLEE: WARNING: killing 22779 states (over memory cap)
KLEE: WARNING: killing 24729 states (over memory cap)
KLEE: WARNING: killing 23558 states (over memory cap)
KLEE: WARNING: killing 23982 states (over memory cap)
KLEE: WARNING: killing 23959 states (over memory cap)
KLEE: WARNING: killing 22546 states (over memory cap)
KLEE: WARNING: killing 23273 states (over memory cap)
KLEE: WARNING: killing 23567 states (over memory cap)
KLEE: WARNING: killing 24810 states (over memory cap)
KLEE: WARNING: killing 23842 states (over memory cap)
KLEE: WARNING: killing 22180 states (over memory cap)
KLEE: WARNING: killing 24034 states (over memory cap)
KLEE: WARNING: killing 22823 states (over memory cap)
KLEE: WARNING: killing 24115 states (over memory cap)
KLEE: WARNING: killing 24222 states (over memory cap)
KLEE: WARNING: killing 22952 states (over memory cap)
KLEE: WARNING: killing 23305 states (over memory cap)
KLEE: WARNING: killing 23037 states (over memory cap)
KLEE: WARNING: killing 23946 states (over memory cap)
KLEE: WARNING: killing 23487 states (over memory cap)
KLEE: WARNING: killing 22778 states (over memory cap)
KLEE: WARNING: killing 24119 states (over memory cap)
KLEE: WARNING: killing 22611 states (over memory cap)
KLEE: WARNING: killing 22765 states (over memory cap)
KLEE: WARNING: killing 23241 states (over memory cap)
KLEE: WARNING: killing 23835 states (over memory cap)
KLEE: WARNING: killing 23820 states (over memory cap)
KLEE: WARNING: killing 23733 states (over memory cap)
KLEE: WARNING: killing 23844 states (over memory cap)
KLEE: WARNING: killing 23081 states (over memory cap)
KLEE: WARNING: killing 23490 states (over memory cap)
KLEE: WARNING: killing 24455 states (over memory cap)
KLEE: WARNING: killing 23198 states (over memory cap)
KLEE: WARNING: killing 23802 states (over memory cap)
KLEE: WARNING: killing 23965 states (over memory cap)
KLEE: WARNING: killing 23578 states (over memory cap)
KLEE: WARNING: killing 24163 states (over memory cap)
KLEE: WARNING: killing 22307 states (over memory cap)
KLEE: WARNING: killing 22959 states (over memory cap)
KLEE: WARNING: killing 23178 states (over memory cap)
KLEE: WARNING: killing 23710 states (over memory cap)
KLEE: WARNING: killing 23205 states (over memory cap)
KLEE: WARNING: killing 22691 states (over memory cap)
KLEE: WARNING: killing 24628 states (over memory cap)
KLEE: WARNING: killing 23077 states (over memory cap)
KLEE: WARNING: killing 24762 states (over memory cap)
KLEE: WARNING: killing 23343 states (over memory cap)
KLEE: WARNING: killing 22538 states (over memory cap)
KLEE: WARNING: killing 24096 states (over memory cap)
KLEE: WARNING: killing 23777 states (over memory cap)
KLEE: WARNING: killing 21876 states (over memory cap)
KLEE: WARNING: killing 24952 states (over memory cap)
KLEE: WARNING: killing 22435 states (over memory cap)
KLEE: WARNING: killing 23261 states (over memory cap)
KLEE: WARNING: killing 24099 states (over memory cap)
KLEE: WARNING: killing 23665 states (over memory cap)
KLEE: WARNING: killing 22431 states (over memory cap)
KLEE: WARNING: killing 23616 states (over memory cap)
KLEE: WARNING: killing 23602 states (over memory cap)
KLEE: WARNING: killing 23274 states (over memory cap)
KLEE: WARNING: killing 23257 states (over memory cap)
KLEE: WARNING: killing 23004 states (over memory cap)
KLEE: WARNING: killing 22913 states (over memory cap)
KLEE: WARNING: killing 23261 states (over memory cap)
KLEE: WARNING: killing 23426 states (over memory cap)
KLEE: WARNING: killing 22858 states (over memory cap)
KLEE: WARNING: killing 22361 states (over memory cap)
KLEE: WARNING: killing 23780 states (over memory cap)
KLEE: WARNING: killing 24721 states (over memory cap)
KLEE: WARNING: killing 24652 states (over memory cap)
KLEE: WARNING: killing 22719 states (over memory cap)
KLEE: WARNING: killing 23776 states (over memory cap)
KLEE: WARNING: killing 23098 states (over memory cap)
KLEE: WARNING: killing 23619 states (over memory cap)
KLEE: WARNING: killing 22878 states (over memory cap)
KLEE: WARNING: killing 23512 states (over memory cap)
KLEE: WARNING: killing 23500 states (over memory cap)
KLEE: WARNING: killing 23061 states (over memory cap)
KLEE: WARNING: killing 23041 states (over memory cap)
KLEE: WARNING: killing 22845 states (over memory cap)
KLEE: WARNING: killing 23965 states (over memory cap)
KLEE: WARNING: killing 24477 states (over memory cap)
KLEE: WARNING: killing 23988 states (over memory cap)
KLEE: WARNING: killing 22952 states (over memory cap)
KLEE: WARNING: killing 23709 states (over memory cap)
KLEE: WARNING: killing 24044 states (over memory cap)
KLEE: WARNING: killing 23913 states (over memory cap)
KLEE: WARNING: killing 22827 states (over memory cap)
KLEE: WARNING: killing 23515 states (over memory cap)
KLEE: WARNING: killing 23207 states (over memory cap)
KLEE: WARNING: killing 22714 states (over memory cap)
KLEE: WARNING: killing 23460 states (over memory cap)
KLEE: WARNING: killing 23796 states (over memory cap)
KLEE: WARNING: killing 22775 states (over memory cap)
KLEE: WARNING: killing 23694 states (over memory cap)
KLEE: WARNING: killing 23502 states (over memory cap)
KLEE: WARNING: killing 24717 states (over memory cap)
KLEE: WARNING: killing 23762 states (over memory cap)
KLEE: WARNING: killing 23866 states (over memory cap)
KLEE: WARNING: killing 23143 states (over memory cap)
KLEE: WARNING: killing 24111 states (over memory cap)
KLEE: WARNING: killing 23862 states (over memory cap)
KLEE: WARNING: killing 23486 states (over memory cap)
KLEE: WARNING: killing 23184 states (over memory cap)
KLEE: WARNING: killing 22986 states (over memory cap)
KLEE: WARNING: killing 22032 states (over memory cap)
KLEE: WARNING: killing 24046 states (over memory cap)
KLEE: WARNING: killing 23864 states (over memory cap)
KLEE: WARNING: killing 23082 states (over memory cap)
KLEE: WARNING: killing 23641 states (over memory cap)
KLEE: WARNING: killing 24151 states (over memory cap)
KLEE: WARNING: killing 23612 states (over memory cap)
KLEE: WARNING: killing 24232 states (over memory cap)
