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--net--wireless--rtlwifi--btcoexist--btcoexist.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.: 256 177 2739 15827
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.494955778122
Defining function printk as symbolic
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
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.492701053619
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 341 118 1336 6596
INFO: Starting verification
KLEE: WARNING ONCE: function "rtl_btc_init_hal_vars" has inline asm
KLEE: WARNING ONCE: function "ex_btc8723b2ant_display_coex_info" has inline asm
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_5f6825ba-576f-42ba-9b9f-ff761d05295f/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8Owjey/linux-4.2-rc1.tar.xz-08_1a-drivers--net--wireless--rtlwifi--btcoexist--btcoexist.ko-entry_point_true-unreach-call.cil.out.c:12770: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9135 states (over memory cap)
KLEE: WARNING: killing 8444 states (over memory cap)
KLEE: WARNING: killing 8922 states (over memory cap)
KLEE: WARNING: killing 8832 states (over memory cap)
KLEE: WARNING: killing 9424 states (over memory cap)
KLEE: WARNING: killing 9548 states (over memory cap)
KLEE: WARNING: killing 9195 states (over memory cap)
KLEE: WARNING: killing 10104 states (over memory cap)
KLEE: WARNING: killing 10294 states (over memory cap)
KLEE: WARNING: killing 10605 states (over memory cap)
KLEE: WARNING: killing 10168 states (over memory cap)
KLEE: WARNING: killing 10170 states (over memory cap)
KLEE: WARNING: killing 10813 states (over memory cap)
KLEE: WARNING: killing 10552 states (over memory cap)
KLEE: WARNING: killing 11000 states (over memory cap)
KLEE: WARNING: killing 10811 states (over memory cap)
KLEE: WARNING: killing 11181 states (over memory cap)
KLEE: WARNING: killing 11341 states (over memory cap)
KLEE: WARNING: killing 11673 states (over memory cap)
KLEE: WARNING: killing 12289 states (over memory cap)
KLEE: WARNING: killing 12428 states (over memory cap)
KLEE: WARNING: killing 13277 states (over memory cap)
KLEE: WARNING: killing 13726 states (over memory cap)
KLEE: WARNING: killing 13381 states (over memory cap)
KLEE: WARNING: killing 13226 states (over memory cap)
KLEE: WARNING: killing 13376 states (over memory cap)
KLEE: WARNING: killing 13241 states (over memory cap)
KLEE: WARNING: killing 13666 states (over memory cap)
KLEE: WARNING: killing 14345 states (over memory cap)
KLEE: WARNING: killing 13501 states (over memory cap)
KLEE: WARNING: killing 13926 states (over memory cap)
KLEE: WARNING: killing 13862 states (over memory cap)
KLEE: WARNING: killing 14396 states (over memory cap)
KLEE: WARNING: killing 14300 states (over memory cap)
KLEE: WARNING: killing 14114 states (over memory cap)
KLEE: WARNING: killing 10542 states (over memory cap)
KLEE: WARNING: killing 14222 states (over memory cap)
KLEE: WARNING: killing 14926 states (over memory cap)
KLEE: WARNING: killing 14833 states (over memory cap)
KLEE: WARNING: killing 14740 states (over memory cap)
KLEE: WARNING: killing 14629 states (over memory cap)
KLEE: WARNING: killing 14446 states (over memory cap)
KLEE: WARNING: killing 10325 states (over memory cap)
KLEE: WARNING: killing 10315 states (over memory cap)
KLEE: WARNING: killing 14260 states (over memory cap)
KLEE: WARNING: killing 14453 states (over memory cap)
KLEE: WARNING: killing 14546 states (over memory cap)
KLEE: WARNING: killing 10272 states (over memory cap)
KLEE: WARNING: killing 14380 states (over memory cap)
KLEE: WARNING: killing 10142 states (over memory cap)
KLEE: WARNING: killing 14450 states (over memory cap)
KLEE: WARNING: killing 10294 states (over memory cap)
KLEE: WARNING: killing 13886 states (over memory cap)
KLEE: WARNING: killing 10462 states (over memory cap)
KLEE: WARNING: killing 10440 states (over memory cap)
KLEE: WARNING: killing 10306 states (over memory cap)
KLEE: WARNING: killing 14009 states (over memory cap)
KLEE: WARNING: killing 10504 states (over memory cap)
KLEE: WARNING: killing 10102 states (over memory cap)
KLEE: WARNING: killing 13588 states (over memory cap)
KLEE: WARNING: killing 10385 states (over memory cap)
KLEE: WARNING: killing 14226 states (over memory cap)
KLEE: WARNING: killing 14525 states (over memory cap)
KLEE: WARNING: killing 10420 states (over memory cap)
KLEE: WARNING: killing 14174 states (over memory cap)
KLEE: WARNING: killing 10129 states (over memory cap)
KLEE: WARNING: killing 10215 states (over memory cap)
KLEE: WARNING: killing 10210 states (over memory cap)
KLEE: WARNING: killing 10505 states (over memory cap)
KLEE: WARNING: killing 10488 states (over memory cap)
KLEE: WARNING: killing 10284 states (over memory cap)
KLEE: WARNING: killing 10183 states (over memory cap)
KLEE: WARNING: killing 10346 states (over memory cap)
KLEE: WARNING: killing 10422 states (over memory cap)
KLEE: WARNING: killing 10222 states (over memory cap)
KLEE: WARNING: killing 10415 states (over memory cap)
KLEE: WARNING: killing 9819 states (over memory cap)
KLEE: WARNING: killing 10183 states (over memory cap)
KLEE: WARNING: killing 9768 states (over memory cap)
KLEE: WARNING: killing 13738 states (over memory cap)
KLEE: WARNING: killing 10519 states (over memory cap)
KLEE: WARNING: killing 10301 states (over memory cap)
KLEE: WARNING: killing 13592 states (over memory cap)
KLEE: WARNING: killing 10756 states (over memory cap)
KLEE: WARNING: killing 10337 states (over memory cap)
KLEE: WARNING: killing 9932 states (over memory cap)
KLEE: WARNING: killing 13974 states (over memory cap)
KLEE: WARNING: killing 10496 states (over memory cap)
KLEE: WARNING: killing 10201 states (over memory cap)
KLEE: WARNING: killing 9996 states (over memory cap)
KLEE: WARNING: killing 10161 states (over memory cap)
KLEE: WARNING: killing 9860 states (over memory cap)
KLEE: WARNING: killing 9749 states (over memory cap)
KLEE: WARNING: killing 9743 states (over memory cap)
KLEE: WARNING: killing 10204 states (over memory cap)
KLEE: WARNING: killing 10016 states (over memory cap)
KLEE: WARNING: killing 9827 states (over memory cap)
KLEE: WARNING: killing 9838 states (over memory cap)
KLEE: WARNING: killing 9736 states (over memory cap)
KLEE: WARNING: killing 9894 states (over memory cap)
KLEE: WARNING: killing 10632 states (over memory cap)
KLEE: WARNING: killing 9861 states (over memory cap)
KLEE: WARNING: killing 9854 states (over memory cap)
KLEE: WARNING: killing 9649 states (over memory cap)
KLEE: WARNING: killing 10018 states (over memory cap)
KLEE: WARNING: killing 10077 states (over memory cap)
KLEE: WARNING: killing 10171 states (over memory cap)
KLEE: WARNING: killing 9681 states (over memory cap)
KLEE: WARNING: killing 9490 states (over memory cap)
KLEE: WARNING: killing 10702 states (over memory cap)
KLEE: WARNING: killing 10388 states (over memory cap)
KLEE: WARNING: killing 10078 states (over memory cap)
KLEE: WARNING: killing 10068 states (over memory cap)
KLEE: WARNING: killing 9967 states (over memory cap)
KLEE: WARNING: killing 10049 states (over memory cap)
KLEE: WARNING: killing 9480 states (over memory cap)
KLEE: WARNING: killing 9930 states (over memory cap)
KLEE: WARNING: killing 9540 states (over memory cap)
KLEE: WARNING: killing 10004 states (over memory cap)
KLEE: WARNING: killing 10815 states (over memory cap)
KLEE: WARNING: killing 10249 states (over memory cap)
KLEE: WARNING: killing 9847 states (over memory cap)
