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-43_2a-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 207 2763 16350
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.658249855042
Defining function printk as symbolic
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_some_page 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.655725955963
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 345 149 1422 7104
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_7d4d4881-c270-4d3c-86b6-5c9b4be2508b/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-1Tzyo0/linux-4.2-rc1.tar.xz-43_2a-drivers--net--wireless--rtlwifi--btcoexist--btcoexist.ko-entry_point_true-unreach-call.cil.out.c:12909: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8633 states (over memory cap)
KLEE: WARNING: killing 8488 states (over memory cap)
KLEE: WARNING: killing 8310 states (over memory cap)
KLEE: WARNING: killing 9019 states (over memory cap)
KLEE: WARNING: killing 9851 states (over memory cap)
KLEE: WARNING: killing 9687 states (over memory cap)
KLEE: WARNING: killing 9678 states (over memory cap)
KLEE: WARNING: killing 9903 states (over memory cap)
KLEE: WARNING: killing 9686 states (over memory cap)
KLEE: WARNING: killing 10430 states (over memory cap)
KLEE: WARNING: killing 9387 states (over memory cap)
KLEE: WARNING: killing 9830 states (over memory cap)
KLEE: WARNING: killing 10463 states (over memory cap)
KLEE: WARNING: killing 10878 states (over memory cap)
KLEE: WARNING: killing 10218 states (over memory cap)
KLEE: WARNING: killing 11877 states (over memory cap)
KLEE: WARNING: killing 11504 states (over memory cap)
KLEE: WARNING: killing 11939 states (over memory cap)
KLEE: WARNING: killing 11921 states (over memory cap)
KLEE: WARNING: killing 12573 states (over memory cap)
KLEE: WARNING: killing 12144 states (over memory cap)
KLEE: WARNING: killing 12024 states (over memory cap)
KLEE: WARNING: killing 12344 states (over memory cap)
KLEE: WARNING: killing 12701 states (over memory cap)
KLEE: WARNING: killing 12458 states (over memory cap)
KLEE: WARNING: killing 12700 states (over memory cap)
KLEE: WARNING: killing 13216 states (over memory cap)
KLEE: WARNING: killing 13438 states (over memory cap)
KLEE: WARNING: killing 13065 states (over memory cap)
KLEE: WARNING: killing 13758 states (over memory cap)
KLEE: WARNING: killing 13638 states (over memory cap)
KLEE: WARNING: killing 13925 states (over memory cap)
KLEE: WARNING: killing 13628 states (over memory cap)
KLEE: WARNING: killing 13415 states (over memory cap)
KLEE: WARNING: killing 13307 states (over memory cap)
KLEE: WARNING: killing 12901 states (over memory cap)
KLEE: WARNING: killing 9938 states (over memory cap)
KLEE: WARNING: killing 13492 states (over memory cap)
KLEE: WARNING: killing 14061 states (over memory cap)
KLEE: WARNING: killing 13748 states (over memory cap)
KLEE: WARNING: killing 13456 states (over memory cap)
KLEE: WARNING: killing 13924 states (over memory cap)
KLEE: WARNING: killing 13417 states (over memory cap)
KLEE: WARNING: killing 13576 states (over memory cap)
KLEE: WARNING: killing 13834 states (over memory cap)
KLEE: WARNING: killing 9730 states (over memory cap)
KLEE: WARNING: killing 12821 states (over memory cap)
KLEE: WARNING: killing 9811 states (over memory cap)
KLEE: WARNING: killing 13358 states (over memory cap)
KLEE: WARNING: killing 9674 states (over memory cap)
KLEE: WARNING: killing 13693 states (over memory cap)
KLEE: WARNING: killing 13765 states (over memory cap)
KLEE: WARNING: killing 10180 states (over memory cap)
KLEE: WARNING: killing 14060 states (over memory cap)
KLEE: WARNING: killing 10143 states (over memory cap)
KLEE: WARNING: killing 13548 states (over memory cap)
KLEE: WARNING: killing 9901 states (over memory cap)
KLEE: WARNING: killing 13761 states (over memory cap)
KLEE: WARNING: killing 10293 states (over memory cap)
KLEE: WARNING: killing 9428 states (over memory cap)
KLEE: WARNING: killing 9498 states (over memory cap)
KLEE: WARNING: killing 9859 states (over memory cap)
KLEE: WARNING: killing 9385 states (over memory cap)
KLEE: WARNING: killing 9567 states (over memory cap)
KLEE: WARNING: killing 13546 states (over memory cap)
KLEE: WARNING: killing 9793 states (over memory cap)
KLEE: WARNING: killing 13785 states (over memory cap)
KLEE: WARNING: killing 13499 states (over memory cap)
KLEE: WARNING: killing 9877 states (over memory cap)
KLEE: WARNING: killing 9580 states (over memory cap)
KLEE: WARNING: killing 9391 states (over memory cap)
KLEE: WARNING: killing 13581 states (over memory cap)
KLEE: WARNING: killing 9943 states (over memory cap)
KLEE: WARNING: killing 9841 states (over memory cap)
KLEE: WARNING: killing 13405 states (over memory cap)
KLEE: WARNING: killing 10043 states (over memory cap)
KLEE: WARNING: killing 9748 states (over memory cap)
KLEE: WARNING: killing 9485 states (over memory cap)
KLEE: WARNING: killing 13500 states (over memory cap)
KLEE: WARNING: killing 10076 states (over memory cap)
KLEE: WARNING: killing 9533 states (over memory cap)
KLEE: WARNING: killing 9619 states (over memory cap)
KLEE: WARNING: killing 9870 states (over memory cap)
KLEE: WARNING: killing 9570 states (over memory cap)
KLEE: WARNING: killing 13371 states (over memory cap)
KLEE: WARNING: killing 9472 states (over memory cap)
KLEE: WARNING: killing 9563 states (over memory cap)
KLEE: WARNING: killing 9271 states (over memory cap)
KLEE: WARNING: killing 13413 states (over memory cap)
KLEE: WARNING: killing 9237 states (over memory cap)
KLEE: WARNING: killing 9822 states (over memory cap)
KLEE: WARNING: killing 9193 states (over memory cap)
KLEE: WARNING: killing 9685 states (over memory cap)
KLEE: WARNING: killing 9596 states (over memory cap)
KLEE: WARNING: killing 9589 states (over memory cap)
KLEE: WARNING: killing 9846 states (over memory cap)
KLEE: WARNING: killing 9628 states (over memory cap)
KLEE: WARNING: killing 9515 states (over memory cap)
KLEE: WARNING: killing 9238 states (over memory cap)
KLEE: WARNING: killing 9758 states (over memory cap)
KLEE: WARNING: killing 9649 states (over memory cap)
KLEE: WARNING: killing 9903 states (over memory cap)
KLEE: WARNING: killing 9902 states (over memory cap)
KLEE: WARNING: killing 9873 states (over memory cap)
KLEE: WARNING: killing 9517 states (over memory cap)
KLEE: WARNING: killing 9511 states (over memory cap)
KLEE: WARNING: killing 8974 states (over memory cap)
KLEE: WARNING: killing 9301 states (over memory cap)
