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-32_7a-drivers--net--usb--cdc_subset.ko-entry_point_true-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.: 40 78 392 1447
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.165892839432
Defining function usbnet_probe as symbolic
Defining function usbnet_suspend as symbolic
Defining function usbnet_resume as symbolic
Defining function usb_reset_device as symbolic
Removed calls to '__ldv_usb_unlock_device' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'usbnet_disconnect' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Defining function ldv_reset_resume_1 as symbolic
Defining function usb_register_driver 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:
  __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.197112083435
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 69 91 307 1024
INFO: Starting verification
KLEE: WARNING: undefined reference to function: usbnet_disconnect
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_87988fb2-49a6-4ec9-9e8c-a78712ac56ee/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 25506 states (over memory cap)
KLEE: WARNING: killing 21288 states (over memory cap)
KLEE: WARNING: killing 21372 states (over memory cap)
KLEE: WARNING: killing 20911 states (over memory cap)
KLEE: WARNING: killing 20450 states (over memory cap)
KLEE: WARNING: killing 20723 states (over memory cap)
KLEE: WARNING: killing 21174 states (over memory cap)
KLEE: WARNING: killing 21278 states (over memory cap)
KLEE: WARNING: killing 21192 states (over memory cap)
KLEE: WARNING: killing 20926 states (over memory cap)
KLEE: WARNING: killing 21572 states (over memory cap)
KLEE: WARNING: killing 22383 states (over memory cap)
KLEE: WARNING: killing 22136 states (over memory cap)
KLEE: WARNING: killing 22237 states (over memory cap)
KLEE: WARNING: killing 23049 states (over memory cap)
KLEE: WARNING: killing 22632 states (over memory cap)
KLEE: WARNING: killing 23080 states (over memory cap)
KLEE: WARNING: killing 23367 states (over memory cap)
KLEE: WARNING: killing 22767 states (over memory cap)
KLEE: WARNING: killing 22709 states (over memory cap)
KLEE: WARNING: killing 23341 states (over memory cap)
KLEE: WARNING: killing 22750 states (over memory cap)
KLEE: WARNING: killing 23211 states (over memory cap)
KLEE: WARNING: killing 22810 states (over memory cap)
KLEE: WARNING: killing 22059 states (over memory cap)
KLEE: WARNING: killing 23362 states (over memory cap)
KLEE: WARNING: killing 22951 states (over memory cap)
KLEE: WARNING: killing 22717 states (over memory cap)
KLEE: WARNING: killing 22828 states (over memory cap)
KLEE: WARNING: killing 22256 states (over memory cap)
KLEE: WARNING: killing 22529 states (over memory cap)
KLEE: WARNING: killing 22635 states (over memory cap)
KLEE: WARNING: killing 21891 states (over memory cap)
KLEE: WARNING: killing 22843 states (over memory cap)
KLEE: WARNING: killing 22282 states (over memory cap)
KLEE: WARNING: killing 22395 states (over memory cap)
KLEE: WARNING: killing 22495 states (over memory cap)
KLEE: WARNING: killing 22266 states (over memory cap)
KLEE: WARNING: killing 22207 states (over memory cap)
KLEE: WARNING: killing 22821 states (over memory cap)
KLEE: WARNING: killing 22921 states (over memory cap)
KLEE: WARNING: killing 23197 states (over memory cap)
KLEE: WARNING: killing 22150 states (over memory cap)
KLEE: WARNING: killing 22251 states (over memory cap)
KLEE: WARNING: killing 21869 states (over memory cap)
KLEE: WARNING: killing 22622 states (over memory cap)
KLEE: WARNING: killing 22407 states (over memory cap)
KLEE: WARNING: killing 22834 states (over memory cap)
KLEE: WARNING: killing 22615 states (over memory cap)
KLEE: WARNING: killing 22567 states (over memory cap)
KLEE: WARNING: killing 22502 states (over memory cap)
KLEE: WARNING: killing 22612 states (over memory cap)
KLEE: WARNING: killing 22400 states (over memory cap)
KLEE: WARNING: killing 22178 states (over memory cap)
KLEE: WARNING: killing 22125 states (over memory cap)
KLEE: WARNING: killing 22398 states (over memory cap)
KLEE: WARNING: killing 22337 states (over memory cap)
KLEE: WARNING: killing 22123 states (over memory cap)
KLEE: WARNING: killing 22870 states (over memory cap)
KLEE: WARNING: killing 22656 states (over memory cap)
KLEE: WARNING: killing 22132 states (over memory cap)
KLEE: WARNING: killing 22404 states (over memory cap)
KLEE: WARNING: killing 22516 states (over memory cap)
KLEE: WARNING: killing 22456 states (over memory cap)
KLEE: WARNING: killing 22411 states (over memory cap)
KLEE: WARNING: killing 21907 states (over memory cap)
KLEE: WARNING: killing 22322 states (over memory cap)
KLEE: WARNING: killing 22575 states (over memory cap)
KLEE: WARNING: killing 22999 states (over memory cap)
KLEE: WARNING: killing 22794 states (over memory cap)
KLEE: WARNING: killing 22123 states (over memory cap)
KLEE: WARNING: killing 22229 states (over memory cap)
KLEE: WARNING: killing 22341 states (over memory cap)
KLEE: WARNING: killing 22127 states (over memory cap)
KLEE: WARNING: killing 22540 states (over memory cap)
KLEE: WARNING: killing 22045 states (over memory cap)
KLEE: WARNING: killing 22757 states (over memory cap)
KLEE: WARNING: killing 22259 states (over memory cap)
KLEE: WARNING: killing 22065 states (over memory cap)
KLEE: WARNING: killing 23076 states (over memory cap)
KLEE: WARNING: killing 22439 states (over memory cap)
KLEE: WARNING: killing 22081 states (over memory cap)
KLEE: WARNING: killing 22796 states (over memory cap)
KLEE: WARNING: killing 22454 states (over memory cap)
KLEE: WARNING: killing 21954 states (over memory cap)
KLEE: WARNING: killing 21765 states (over memory cap)
KLEE: WARNING: killing 21715 states (over memory cap)
KLEE: WARNING: killing 22420 states (over memory cap)
KLEE: WARNING: killing 21627 states (over memory cap)
KLEE: WARNING: killing 22028 states (over memory cap)
KLEE: WARNING: killing 22875 states (over memory cap)
KLEE: WARNING: killing 22087 states (over memory cap)
KLEE: WARNING: killing 22644 states (over memory cap)
KLEE: WARNING: killing 22755 states (over memory cap)
KLEE: WARNING: killing 22862 states (over memory cap)
KLEE: WARNING: killing 22977 states (over memory cap)
KLEE: WARNING: killing 22051 states (over memory cap)
KLEE: WARNING: killing 22589 states (over memory cap)
KLEE: WARNING: killing 22408 states (over memory cap)
KLEE: WARNING: killing 22951 states (over memory cap)
KLEE: WARNING: killing 21895 states (over memory cap)
KLEE: WARNING: killing 22422 states (over memory cap)
KLEE: WARNING: killing 21947 states (over memory cap)
KLEE: WARNING: killing 22486 states (over memory cap)
KLEE: WARNING: killing 22150 states (over memory cap)
KLEE: WARNING: killing 22403 states (over memory cap)
KLEE: WARNING: killing 22655 states (over memory cap)
KLEE: WARNING: killing 22607 states (over memory cap)
KLEE: WARNING: killing 21418 states (over memory cap)
KLEE: WARNING: killing 21948 states (over memory cap)
KLEE: WARNING: killing 21911 states (over memory cap)
KLEE: WARNING: killing 21861 states (over memory cap)
KLEE: WARNING: killing 22250 states (over memory cap)
KLEE: WARNING: killing 21782 states (over memory cap)
KLEE: WARNING: killing 21591 states (over memory cap)
KLEE: WARNING: killing 22414 states (over memory cap)
KLEE: WARNING: killing 22647 states (over memory cap)
KLEE: WARNING: killing 22188 states (over memory cap)
KLEE: WARNING: killing 22150 states (over memory cap)
KLEE: WARNING: killing 22816 states (over memory cap)
KLEE: WARNING: killing 22644 states (over memory cap)
KLEE: WARNING: killing 22464 states (over memory cap)
KLEE: WARNING: killing 22001 states (over memory cap)
KLEE: WARNING: killing 22235 states (over memory cap)
KLEE: WARNING: killing 22760 states (over memory cap)
KLEE: WARNING: killing 22300 states (over memory cap)
KLEE: WARNING: killing 22123 states (over memory cap)
KLEE: WARNING: killing 22499 states (over memory cap)
KLEE: WARNING: killing 22880 states (over memory cap)
KLEE: WARNING: killing 22566 states (over memory cap)
KLEE: WARNING: killing 22384 states (over memory cap)
KLEE: WARNING: killing 22492 states (over memory cap)
KLEE: WARNING: killing 22039 states (over memory cap)
KLEE: WARNING: killing 22262 states (over memory cap)
KLEE: WARNING: killing 22083 states (over memory cap)
KLEE: WARNING: killing 22318 states (over memory cap)
