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--wireless--rtlwifi--rtl8192se--rtl8192se.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.: 302 305 4176 30596
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in arch_local_save_flags
Removed infinite loop in arch_local_irq_enable
Removed infinite loop in arch_local_irq_restore
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.799270868301
Defining function rtl_pci_probe as symbolic
Removed calls to 'vfree' (function is undefined)
Removed calls to 'rtl_efuse_shadow_map_update' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'rtl_cam_reset_all_entry' (function is undefined)
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to 'rtl_get_tcb_desc' (function is undefined)
Removed calls to 'rtl_process_phyinfo' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Removed calls to 'rtl_cam_mark_invalid' (function is undefined)
Removed calls to 'rtl_cam_empty_entry' (function is undefined)
Removed calls to 'rtl_cam_del_entry' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function rtl_btc_status_false as symbolic
Defining function printk as symbolic
Defining function rtl_cam_get_free_entry as symbolic
Defining function rtl_cam_delete_one_entry as symbolic
Defining function rtl_cam_add_one_entry as symbolic
Defining function rtl_ps_enable_nic as symbolic
Defining function jiffies_to_msecs as symbolic
Defining function rtl_ps_disable_nic as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_watching as symbolic
Defining function ieee80211_find_sta as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function rtlwifi_rate_mapping as symbolic
Defining function rtl_query_rxpwrpercentage as symbolic
Defining function rtl_evm_db_to_percentage as symbolic
Defining function rtl_signal_scale_mapping as symbolic
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Defining function __phys_addr as symbolic
Defining function pci_bus_write_config_dword as symbolic
Defining function pci_bus_read_config_dword as symbolic
Removed calls to 'rtl_addr_delay' (function is undefined)
Removed calls to 'rtl_rfreg_delay' (function is undefined)
Defining function skb_put as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function efuse_read_1byte as symbolic
Defining function vzalloc as symbolic
Removed calls to 'complete' (function is undefined)
Removed calls to 'release_firmware' (function is undefined)
Defining function request_firmware_nowait as symbolic
Defining function rtl_pci_suspend as symbolic
Defining function rtl_pci_resume as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'rtl_pci_disconnect' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function ldv_shutdown_1 as symbolic
Defining function ldv_release_3 as symbolic
Defining function ldv_probe_3 as symbolic
Defining function ldv_suspend_late_2 as symbolic
Defining function ldv_restore_early_2 as symbolic
Defining function ldv_resume_early_2 as symbolic
Defining function ldv_thaw_early_2 as symbolic
Defining function ldv_resume_noirq_2 as symbolic
Defining function ldv_freeze_noirq_2 as symbolic
Defining function ldv_prepare_2 as symbolic
Defining function ldv_freeze_late_2 as symbolic
Defining function ldv_thaw_noirq_2 as symbolic
Defining function ldv_poweroff_noirq_2 as symbolic
Defining function ldv_poweroff_late_2 as symbolic
Defining function ldv_restore_noirq_2 as symbolic
Defining function ldv_suspend_noirq_2 as symbolic
Defining function ldv_complete_2 as symbolic
Defining function __pci_register_driver 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: 1.04548406601
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 395 243 2789 18938
INFO: Starting verification
KLEE: WARNING ONCE: function "rtl92s_init_sw_vars" has inline asm
KLEE: WARNING ONCE: function "rtl92se_read_eeprom_info" has inline asm
KLEE: WARNING ONCE: function "rtl92se_hw_init" has inline asm
KLEE: WARNING ONCE: function "rtl92s_phy_set_bw_mode" has inline asm
KLEE: WARNING ONCE: function "rtl92s_phy_sw_chnl" has inline asm
KLEE: WARNING ONCE: function "rtl92se_update_interrupt_mask" has inline asm
KLEE: WARNING ONCE: function "rtl92se_get_hw_reg" has inline asm
KLEE: WARNING ONCE: function "rtl92se_set_hw_reg" has inline asm
KLEE: WARNING ONCE: function "rtl92se_update_hal_rate_tbl" has inline asm
KLEE: WARNING ONCE: function "rtl92se_tx_fill_desc" has inline asm
KLEE: WARNING ONCE: function "rtl92se_tx_fill_cmddesc" has inline asm
KLEE: WARNING ONCE: function "rtl92se_gpio_radio_on_off_checking" has inline asm
KLEE: WARNING ONCE: function "rtl92s_dm_watchdog" has inline asm
KLEE: WARNING ONCE: function "rtl92s_phy_scan_operation_backup" has inline asm
KLEE: WARNING ONCE: function "rtl92s_phy_set_rf_power_state" has inline asm
KLEE: WARNING ONCE: function "rtl92se_led_control" has inline asm
KLEE: WARNING ONCE: function "rtl92se_set_desc" has inline asm
KLEE: WARNING ONCE: function "rtl92se_enable_hw_security_config" has inline asm
KLEE: WARNING ONCE: function "rtl92se_set_key" has inline asm
KLEE: WARNING ONCE: function "rtl92s_phy_query_bb_reg" has inline asm
KLEE: WARNING ONCE: function "rtl92s_phy_set_bb_reg" has inline asm
KLEE: WARNING ONCE: function "rtl92s_phy_query_rf_reg" has inline asm
KLEE: WARNING ONCE: function "rtl92s_phy_set_rf_reg" has inline asm
KLEE: WARNING ONCE: function "_rtl92s_phy_rf_serial_read" has inline asm
KLEE: WARNING ONCE: function "rtl92se_sw_led_on" has inline asm
KLEE: WARNING ONCE: function "rtl92se_sw_led_off" has inline asm
KLEE: WARNING ONCE: function "rtl92s_phy_set_fw_cmd" has inline asm
KLEE: WARNING ONCE: function "rtl92s_phy_chk_fwcmd_iodone" has inline asm
KLEE: WARNING ONCE: function "rtl92s_phy_set_txpower" has inline asm
KLEE: WARNING ONCE: function "rtl92s_phy_rf6052_set_ofdmtxpower" has inline asm
KLEE: WARNING ONCE: function "rtl92s_phy_rf6052_set_bandwidth" has inline asm
KLEE: WARNING ONCE: function "_rtl92se_set_media_status" has inline asm
KLEE: WARNING ONCE: function "rtl92s_download_fw" has inline asm
KLEE: WARNING ONCE: function "rtl92s_phy_bb_config" has inline asm
KLEE: WARNING ONCE: function "rtl92s_phy_get_hw_reg_originalvalue" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "rtl92s_phy_config_rf" has inline asm
KLEE: WARNING ONCE: function "rtl92se_fw_cb" has inline asm
KLEE: WARNING: undefined reference to function: rtl_pci_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_0c176d70-add0-4e27-8371-ef7aa92f7f21/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:14115: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:14992: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:14496: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:20730: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:14952: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:21135: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:12931: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:14485: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:14132: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:15358: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:10993: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:15245: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:9741: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:12948: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:12489: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:18407: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:21021: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:15198: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:9700: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:14594: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:9084: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:8726: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:11459: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:12829: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:20361: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:18328: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:14761: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:15788: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:15296: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:9718: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:15636: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:14165: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:12302: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:9741: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:12097: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:11080: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:14132: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:14367: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:9700: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:14485: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:18407: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hiyx2a/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--rtlwifi--rtl8192se--rtl8192se.ko-entry_point_true-unreach-call.cil.out.c:14594: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9962 states (over memory cap)
KLEE: WARNING: killing 6918 states (over memory cap)
KLEE: WARNING: killing 6737 states (over memory cap)
KLEE: WARNING: killing 7614 states (over memory cap)
KLEE: WARNING: killing 7545 states (over memory cap)
KLEE: WARNING: killing 7810 states (over memory cap)
KLEE: WARNING: killing 7853 states (over memory cap)
KLEE: WARNING: killing 8452 states (over memory cap)
KLEE: WARNING: killing 8498 states (over memory cap)
KLEE: WARNING: killing 8485 states (over memory cap)
KLEE: WARNING: killing 8531 states (over memory cap)
KLEE: WARNING: killing 8743 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 8841 states (over memory cap)
KLEE: WARNING: killing 8941 states (over memory cap)
KLEE: WARNING: killing 9209 states (over memory cap)
KLEE: WARNING: killing 8972 states (over memory cap)
KLEE: WARNING: killing 8797 states (over memory cap)
KLEE: WARNING: killing 8624 states (over memory cap)
KLEE: WARNING: killing 7734 states (over memory cap)
KLEE: WARNING: killing 8600 states (over memory cap)
KLEE: WARNING: killing 8313 states (over memory cap)
KLEE: WARNING: killing 8519 states (over memory cap)
KLEE: WARNING: killing 8891 states (over memory cap)
KLEE: WARNING: killing 8116 states (over memory cap)
KLEE: WARNING: killing 8323 states (over memory cap)
KLEE: WARNING: killing 8254 states (over memory cap)
KLEE: WARNING: killing 8297 states (over memory cap)
KLEE: WARNING: killing 8016 states (over memory cap)
KLEE: WARNING: killing 8006 states (over memory cap)
KLEE: WARNING: killing 9131 states (over memory cap)
KLEE: WARNING: killing 8849 states (over memory cap)
KLEE: WARNING: killing 8733 states (over memory cap)
KLEE: WARNING: killing 9154 states (over memory cap)
KLEE: WARNING: killing 8659 states (over memory cap)
KLEE: WARNING: killing 9569 states (over memory cap)
KLEE: WARNING: killing 9023 states (over memory cap)
KLEE: WARNING: killing 8853 states (over memory cap)
KLEE: WARNING: killing 8626 states (over memory cap)
KLEE: WARNING: killing 9739 states (over memory cap)
KLEE: WARNING: killing 9253 states (over memory cap)
KLEE: WARNING: killing 8709 states (over memory cap)
KLEE: WARNING: killing 8699 states (over memory cap)
KLEE: WARNING: killing 9914 states (over memory cap)
KLEE: WARNING: killing 8950 states (over memory cap)
KLEE: WARNING: killing 9310 states (over memory cap)
KLEE: WARNING: killing 8770 states (over memory cap)
KLEE: WARNING: killing 9080 states (over memory cap)
KLEE: WARNING: killing 9124 states (over memory cap)
KLEE: WARNING: killing 9008 states (over memory cap)
KLEE: WARNING: killing 8575 states (over memory cap)
KLEE: WARNING: killing 8618 states (over memory cap)
KLEE: WARNING: killing 8557 states (over memory cap)
KLEE: WARNING: killing 8700 states (over memory cap)
KLEE: WARNING: killing 9168 states (over memory cap)
KLEE: WARNING: killing 8528 states (over memory cap)
KLEE: WARNING: killing 8780 states (over memory cap)
KLEE: WARNING: killing 8927 states (over memory cap)
KLEE: WARNING: killing 9335 states (over memory cap)
KLEE: WARNING: killing 8911 states (over memory cap)
KLEE: WARNING: killing 8428 states (over memory cap)
KLEE: WARNING: killing 8734 states (over memory cap)
KLEE: WARNING: killing 8832 states (over memory cap)
KLEE: WARNING: killing 8404 states (over memory cap)
KLEE: WARNING: killing 8761 states (over memory cap)
KLEE: WARNING: killing 9012 states (over memory cap)
KLEE: WARNING: killing 8953 states (over memory cap)
KLEE: WARNING: killing 8682 states (over memory cap)
KLEE: WARNING: killing 9299 states (over memory cap)
KLEE: WARNING: killing 9550 states (over memory cap)
KLEE: WARNING: killing 8658 states (over memory cap)
KLEE: WARNING: killing 8914 states (over memory cap)
KLEE: WARNING: killing 8486 states (over memory cap)
KLEE: WARNING: killing 8892 states (over memory cap)
KLEE: WARNING: killing 8625 states (over memory cap)
KLEE: WARNING: killing 9188 states (over memory cap)
KLEE: WARNING: killing 9027 states (over memory cap)
KLEE: WARNING: killing 8755 states (over memory cap)
KLEE: WARNING: killing 8646 states (over memory cap)
KLEE: WARNING: killing 8325 states (over memory cap)
KLEE: WARNING: killing 8985 states (over memory cap)
KLEE: WARNING: killing 9078 states (over memory cap)
KLEE: WARNING: killing 8763 states (over memory cap)
KLEE: WARNING: killing 9322 states (over memory cap)
KLEE: WARNING: killing 9058 states (over memory cap)
KLEE: WARNING: killing 9461 states (over memory cap)
KLEE: WARNING: killing 8839 states (over memory cap)
KLEE: WARNING: killing 8527 states (over memory cap)
KLEE: WARNING: killing 9286 states (over memory cap)
KLEE: WARNING: killing 8714 states (over memory cap)
KLEE: WARNING: killing 8706 states (over memory cap)
KLEE: WARNING: killing 9307 states (over memory cap)
KLEE: WARNING: killing 9555 states (over memory cap)
KLEE: WARNING: killing 8939 states (over memory cap)
KLEE: WARNING: killing 9083 states (over memory cap)
KLEE: WARNING: killing 8970 states (over memory cap)
KLEE: WARNING: killing 8964 states (over memory cap)
KLEE: WARNING: killing 8753 states (over memory cap)
KLEE: WARNING: killing 8643 states (over memory cap)
KLEE: WARNING: killing 9038 states (over memory cap)
KLEE: WARNING: killing 9086 states (over memory cap)
KLEE: WARNING: killing 9128 states (over memory cap)
KLEE: WARNING: killing 9218 states (over memory cap)
KLEE: WARNING: killing 8808 states (over memory cap)
KLEE: WARNING: killing 9358 states (over memory cap)
KLEE: WARNING: killing 9757 states (over memory cap)
KLEE: WARNING: killing 8539 states (over memory cap)
KLEE: WARNING: killing 9636 states (over memory cap)
KLEE: WARNING: killing 8676 states (over memory cap)
KLEE: WARNING: killing 8564 states (over memory cap)
KLEE: WARNING: killing 8607 states (over memory cap)
KLEE: WARNING: killing 8900 states (over memory cap)
KLEE: WARNING: killing 8487 states (over memory cap)
KLEE: WARNING: killing 9033 states (over memory cap)
KLEE: WARNING: killing 8924 states (over memory cap)
KLEE: WARNING: killing 8711 states (over memory cap)
KLEE: WARNING: killing 9305 states (over memory cap)
KLEE: WARNING: killing 9303 states (over memory cap)
KLEE: WARNING: killing 9442 states (over memory cap)
KLEE: WARNING: killing 8688 states (over memory cap)
KLEE: WARNING: killing 8880 states (over memory cap)
KLEE: WARNING: killing 8823 states (over memory cap)
KLEE: WARNING: killing 8317 states (over memory cap)
KLEE: WARNING: killing 8110 states (over memory cap)
KLEE: WARNING: killing 8647 states (over memory cap)
KLEE: WARNING: killing 8638 states (over memory cap)
KLEE: WARNING: killing 8830 states (over memory cap)
KLEE: WARNING: killing 8525 states (over memory cap)
KLEE: WARNING: killing 9258 states (over memory cap)
KLEE: WARNING: killing 9446 states (over memory cap)
KLEE: WARNING: killing 9196 states (over memory cap)
KLEE: WARNING: killing 9389 states (over memory cap)
KLEE: WARNING: killing 9285 states (over memory cap)
KLEE: WARNING: killing 9033 states (over memory cap)
KLEE: WARNING: killing 9367 states (over memory cap)
KLEE: WARNING: killing 9411 states (over memory cap)
KLEE: WARNING: killing 8910 states (over memory cap)
KLEE: WARNING: killing 9000 states (over memory cap)
KLEE: WARNING: killing 8996 states (over memory cap)
KLEE: WARNING: killing 8499 states (over memory cap)
KLEE: WARNING: killing 8394 states (over memory cap)
KLEE: WARNING: killing 9168 states (over memory cap)
KLEE: WARNING: killing 8719 states (over memory cap)
KLEE: WARNING: killing 8911 states (over memory cap)
KLEE: WARNING: killing 9000 states (over memory cap)
KLEE: WARNING: killing 8702 states (over memory cap)
KLEE: WARNING: killing 9964 states (over memory cap)
KLEE: WARNING: killing 9083 states (over memory cap)
KLEE: WARNING: killing 9030 states (over memory cap)
KLEE: WARNING: killing 9366 states (over memory cap)
KLEE: WARNING: killing 9167 states (over memory cap)
KLEE: WARNING: killing 9108 states (over memory cap)
KLEE: WARNING: killing 8859 states (over memory cap)
KLEE: WARNING: killing 8802 states (over memory cap)
KLEE: WARNING: killing 9037 states (over memory cap)
KLEE: WARNING: killing 8785 states (over memory cap)
KLEE: WARNING: killing 9019 states (over memory cap)
KLEE: WARNING: killing 8477 states (over memory cap)
KLEE: WARNING: killing 8275 states (over memory cap)
KLEE: WARNING: killing 8508 states (over memory cap)
KLEE: WARNING: killing 8594 states (over memory cap)
KLEE: WARNING: killing 8926 states (over memory cap)
KLEE: WARNING: killing 9502 states (over memory cap)
KLEE: WARNING: killing 9063 states (over memory cap)
KLEE: WARNING: killing 8767 states (over memory cap)
KLEE: WARNING: killing 8808 states (over memory cap)
KLEE: WARNING: killing 8801 states (over memory cap)
KLEE: WARNING: killing 9520 states (over memory cap)
KLEE: WARNING: killing 8937 states (over memory cap)
KLEE: WARNING: killing 8977 states (over memory cap)
KLEE: WARNING: killing 8921 states (over memory cap)
KLEE: WARNING: killing 9155 states (over memory cap)
KLEE: WARNING: killing 9009 states (over memory cap)
KLEE: WARNING: killing 9046 states (over memory cap)
KLEE: WARNING: killing 8613 states (over memory cap)
KLEE: WARNING: killing 8554 states (over memory cap)
KLEE: WARNING: killing 8645 states (over memory cap)
KLEE: WARNING: killing 9253 states (over memory cap)
KLEE: WARNING: killing 8678 states (over memory cap)
KLEE: WARNING: killing 8763 states (over memory cap)
KLEE: WARNING: killing 8854 states (over memory cap)
KLEE: WARNING: killing 9037 states (over memory cap)
KLEE: WARNING: killing 8557 states (over memory cap)
