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--iwlegacy--iwl3945.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.: 653 483 4503 35261
Removed infinite loop in dma_unmap_page
Removed infinite loop in il3945_tx_queue_reclaim
Removed infinite loop in il3945_rx_handle
Removed infinite loop in dma_map_page
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in il3945_rate_scale_init
Removed infinite loop in il3945_get_rate_idx_by_rssi
Removed infinite loop in il3945_hw_get_beacon_cmd
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.17897987366
Removed calls to 'dev_err' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to 'il_wr_prph' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Removed calls to 'il_clear_ucode_stations' (function is undefined)
Removed calls to 'il_restore_stations' (function is undefined)
Removed calls to 'il_set_rxon_hwcrypto' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'dev_warn' (function is undefined)
Defining function il_send_cmd as symbolic
Defining function scnprintf as symbolic
Defining function simple_read_from_buffer as symbolic
Removed calls to 'pci_disable_link_state' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'il_free_channel_map' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'il_setup_scan_deferred_work' (function is undefined)
Removed calls to 'tasklet_init' (function is undefined)
Removed calls to 'il_setup_rx_scan_handlers' (function is undefined)
Removed calls to 'il_power_initialize' (function is undefined)
Removed calls to 'il_leds_init' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'sysfs_remove_group' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Removed calls to 'il_free_geos' (function is undefined)
Removed calls to 'il_eeprom_free' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'pci_release_regions' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'ieee80211_free_hw' (function is undefined)
Removed calls to 'il_dbgfs_unregister' (function is undefined)
Removed calls to 'il_leds_exit' (function is undefined)
Removed calls to 'ieee80211_unregister_hw' (function is undefined)
Removed calls to 'il_apm_stop' (function is undefined)
Removed calls to 'synchronize_irq' (function is undefined)
Removed calls to 'tasklet_kill' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'il_cancel_scan_deferred_work' (function is undefined)
Removed calls to 'il_cmd_queue_free' (function is undefined)
Removed calls to 'il_tx_queue_free' (function is undefined)
Removed calls to 'il_free_txq_mem' (function is undefined)
Defining function queue_delayed_work_on as symbolic
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function cancel_delayed_work_sync as symbolic
Removed calls to 'il_dealloc_bcast_stations' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'ieee80211_stop_queues' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_il_apm_stop' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function cancel_delayed_work as symbolic
Defining function il_scan_cancel_timeout as symbolic
Defining function _il_poll_bit as symbolic
Defining function del_timer_sync as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_request_regions as symbolic
Defining function pci_ioremap_bar as symbolic
Defining function il_eeprom_init as symbolic
Defining function il_isr as symbolic
Defining function sysfs_create_group as symbolic
Defining function il_set_rxon_channel as symbolic
Defining function il_dbgfs_register as symbolic
Defining function ieee80211_register_hw as symbolic
Removed calls to 'wiphy_rfkill_set_hw_state' (function is undefined)
Removed calls to 'ieee80211_tx_status_irqsafe' (function is undefined)
Removed calls to 'skb_add_rx_frag' (function is undefined)
Removed calls to 'il_update_stats' (function is undefined)
Removed calls to 'ieee80211_rx' (function is undefined)
Defining function ieee80211_channel_to_frequency as symbolic
Defining function il_set_decrypted_flag as symbolic
Defining function skb_put as symbolic
Removed calls to 'ieee80211_wake_queue' (function is undefined)
Defining function il_queue_space as symbolic
Removed calls to 'ieee80211_stop_queue' (function is undefined)
Defining function il_scan_cancel as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function il_read_targ_mem as symbolic
Defining function __alloc_workqueue_key as symbolic
Removed calls to 'ieee80211_restart_hw' (function is undefined)
Removed calls to 'il_setup_watchdog' (function is undefined)
Removed calls to 'ieee80211_wake_queues' (function is undefined)
Removed calls to 'il_connection_init_rx_config' (function is undefined)
Removed calls to 'il_send_bt_config' (function is undefined)
Removed calls to 'il_irq_handle_error' (function is undefined)
Removed calls to 'il_rx_queue_update_write_ptr' (function is undefined)
Removed calls to 'il_txq_update_write_ptr' (function is undefined)
Removed calls to 'il_tx_cmd_complete' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function _il_grab_nic_access as symbolic
Defining function il_get_cmd_string as symbolic
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Defining function il_rx_queue_space as symbolic
Defining function queue_work_on as symbolic
Defining function net_ratelimit as symbolic
Defining function round_jiffies_relative as symbolic
Defining function il_rd_prph as symbolic
Defining function il_power_update_mode as symbolic
Removed calls to 'il_set_bit' (function is undefined)
Removed calls to 'il_clear_bit' (function is undefined)
Defining function il_rx_queue_alloc as symbolic
Defining function il_alloc_txq_mem as symbolic
Defining function il_tx_queue_init as symbolic
Defining function il_prep_station as symbolic
Defining function request_threaded_irq as symbolic
Defining function pci_enable_msi_range as symbolic
Defining function il_init_channel_map as symbolic
Defining function il_init_geos as symbolic
Defining function dma_alloc_attrs as symbolic
Defining function pci_bus_write_config_byte as symbolic
Defining function dma_supported as symbolic
Defining function dma_set_mask as symbolic
Defining function ieee80211_alloc_hw_nm as symbolic
Removed calls to 'il_tx_cmd_protection' (function is undefined)
Removed calls to 'print_hex_dump' (function is undefined)
Removed calls to 'release_firmware' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function il_mac_add_interface as symbolic
Defining function il_mac_change_interface as symbolic
Defining function il_mac_config as symbolic
Defining function il_mac_hw_scan as symbolic
Defining function il_mac_sta_remove as symbolic
Defining function il_mac_conf_tx as symbolic
Defining function il_mac_tx_last_beacon as symbolic
Defining function il_add_station_common as symbolic
Defining function jiffies_to_msecs as symbolic
Defining function mod_timer as symbolic
Defining function il_send_add_sta as symbolic
Defining function il_get_free_ucode_key_idx as symbolic
Defining function prepare_to_wait_event as symbolic
Defining function schedule_timeout as symbolic
Defining function sprintf as symbolic
Defining function request_firmware as symbolic
Defining function snprintf as symbolic
Defining function ieee80211_hdrlen as symbolic
Defining function __phys_addr as symbolic
Defining function sscanf as symbolic
Defining function strnlen as symbolic
Defining function simple_strtoul as symbolic
Defining function strlcpy as symbolic
Defining function il_usecs_to_beacons as symbolic
Defining function il_add_beacon_time as symbolic
Defining function il_send_cmd_sync as symbolic
Defining function hex_dump_to_buffer as symbolic
Defining function kstrtoull as symbolic
Removed calls to 'debugfs_remove' (function is undefined)
Defining function debugfs_create_file as symbolic
Defining function rate_control_send_low as symbolic
Defining function default_llseek as symbolic
Defining function simple_open as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Defining function il_remove_station as symbolic
Defining function ieee80211_find_sta as symbolic
Removed calls to 'lock_release' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_watching as symbolic
Defining function il_send_rxon_timing as symbolic
Defining function il_get_lowest_plcp as symbolic
Defining function il_send_cmd_pdu as symbolic
Defining function lock_is_held as symbolic
Defining function il_fill_probe_req as symbolic
Defining function il_get_active_dwell_time as symbolic
Defining function il_get_passive_dwell_time as symbolic
Defining function il_get_channel_info as symbolic
Defining function il_check_rxon_cmd as symbolic
Defining function il_full_rxon_required as symbolic
Defining function il_set_tx_power as symbolic
Defining function il_apm_init as symbolic
Removed calls to 'il_bg_watchdog' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'ieee80211_rate_control_unregister' (function is undefined)
Removed calls to 'il_mac_reset_tsf' (function is undefined)
Removed calls to 'il_mac_flush' (function is undefined)
Removed calls to 'il_mac_bss_info_changed' (function is undefined)
Removed calls to 'il_mac_remove_interface' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_shutdown_14 as symbolic
Defining function ldv_release_10 as symbolic
Defining function ldv_probe_10 as symbolic
Defining function ldv_release_12 as symbolic
Defining function printk as symbolic
Defining function __pci_register_driver as symbolic
Defining function ieee80211_rate_control_register as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strlen
  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: 1.19491100311
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 481 411 2530 19361
INFO: Starting verification
KLEE: WARNING ONCE: function "il3945_hw_tx_queue_init" has inline asm
KLEE: WARNING ONCE: function "il3945_load_bsm" has inline asm
KLEE: WARNING ONCE: function "il3945_apm_init" has inline asm
KLEE: WARNING ONCE: function "il3945_send_tx_power" has inline asm
KLEE: WARNING ONCE: function "il3945_eeprom_acquire_semaphore" has inline asm
KLEE: WARNING ONCE: function "il3945_send_rxon_assoc" has inline asm
KLEE: WARNING ONCE: function "il3945_commit_rxon" has inline asm
KLEE: WARNING ONCE: function "il3945_request_scan" has inline asm
KLEE: WARNING ONCE: function "il3945_post_associate" has inline asm
KLEE: WARNING ONCE: function "il3945_manage_ibss_station" has inline asm
KLEE: WARNING ONCE: function "il3945_pci_probe" has inline asm
KLEE: WARNING ONCE: function "il3945_pci_remove" has inline asm
KLEE: WARNING ONCE: function "il3945_is_temp_calib_needed" has inline asm
KLEE: WARNING ONCE: function "il3945_hw_reg_txpower_get_temperature" has inline asm
KLEE: WARNING ONCE: function "__il3945_down" has inline asm
KLEE: WARNING ONCE: function "il3945_hw_txq_ctx_stop" has inline asm
KLEE: WARNING ONCE: function "il3945_hw_rxq_stop" has inline asm
KLEE: WARNING ONCE: function "il3945_txpower_set_from_eeprom" has inline asm
KLEE: WARNING ONCE: function "il3945_bg_restart" has inline asm
KLEE: WARNING ONCE: function "il3945_bg_init_alive_start" has inline asm
KLEE: WARNING ONCE: function "il3945_bg_alive_start" has inline asm
KLEE: WARNING ONCE: function "il3945_rfkill_poll" has inline asm
KLEE: WARNING ONCE: function "il3945_hdl_alive" has inline asm
KLEE: WARNING ONCE: function "il3945_hdl_add_sta" has inline asm
KLEE: WARNING ONCE: function "il3945_hdl_beacon" has inline asm
KLEE: WARNING ONCE: function "il3945_hdl_c_stats" has inline asm
KLEE: WARNING ONCE: function "il3945_hdl_stats" has inline asm
KLEE: WARNING ONCE: function "il3945_hdl_card_state" has inline asm
KLEE: WARNING ONCE: function "il3945_hdl_tx" has inline asm
KLEE: WARNING ONCE: function "il3945_hdl_rx" has inline asm
KLEE: WARNING ONCE: function "_il_wake_queue" has inline asm
KLEE: WARNING ONCE: function "_il_stop_queue" has inline asm
KLEE: WARNING ONCE: function "il3945_disable_events" has inline asm
KLEE: WARNING ONCE: function "il3945_verify_ucode" has inline asm
KLEE: WARNING ONCE: function "il3945_verify_inst_sparse" has inline asm
KLEE: WARNING ONCE: function "il_wr" has inline asm
KLEE: WARNING ONCE: function "il3945_rx_allocate" has inline asm
KLEE: WARNING ONCE: function "__il3945_up" has inline asm
KLEE: WARNING ONCE: function "il3945_hw_nic_init" has inline asm
KLEE: WARNING ONCE: function "il_wr___0" has inline asm
KLEE: WARNING ONCE: function "il3945_mac_tx" has inline asm
KLEE: WARNING ONCE: function "il3945_mac_start" has inline asm
KLEE: WARNING ONCE: function "il3945_mac_stop" has inline asm
KLEE: WARNING ONCE: function "il3945_configure_filter" has inline asm
KLEE: WARNING ONCE: function "il3945_mac_set_key" has inline asm
KLEE: WARNING ONCE: function "il3945_mac_sta_add" has inline asm
KLEE: WARNING ONCE: function "il3945_rs_rate_init" has inline asm
KLEE: WARNING ONCE: function "il3945_bg_rate_scale_flush" has inline asm
KLEE: WARNING ONCE: function "il3945_hw_build_tx_cmd_rate" has inline asm
KLEE: WARNING ONCE: function "il3945_store_antenna" has inline asm
KLEE: WARNING ONCE: function "il3945_store_flags" has inline asm
KLEE: WARNING ONCE: function "il3945_store_filter_flags" has inline asm
KLEE: WARNING ONCE: function "il3945_store_measurement" has inline asm
KLEE: WARNING ONCE: function "il3945_show_temperature" has inline asm
KLEE: WARNING ONCE: function "il3945_hw_reg_set_txpower" has inline asm
KLEE: WARNING ONCE: function "il3945_rs_alloc_sta" has inline asm
KLEE: WARNING ONCE: function "il3945_rs_tx_status" has inline asm
KLEE: WARNING ONCE: function "il3945_rs_get_rate" has inline asm
KLEE: WARNING ONCE: function "il3945_collect_tx_data" has inline asm
KLEE: WARNING ONCE: function "il3945_rate_scale_init" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "il3945_hw_get_beacon_cmd" has inline asm
KLEE: WARNING ONCE: function "il3945_init_hw_rate_table" has inline asm
KLEE: WARNING ONCE: function "il3945_hw_get_temperature" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_13" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to function: il_bg_watchdog
KLEE: WARNING: undefined reference to function: il_hdl_csa
KLEE: WARNING: undefined reference to function: il_hdl_error
KLEE: WARNING: undefined reference to function: il_hdl_pm_debug_stats
KLEE: WARNING: undefined reference to function: il_hdl_pm_sleep
KLEE: WARNING: undefined reference to function: il_hdl_spectrum_measurement
KLEE: WARNING: undefined reference to function: il_mac_bss_info_changed
KLEE: WARNING: undefined reference to function: il_mac_flush
KLEE: WARNING: undefined reference to function: il_mac_remove_interface
KLEE: WARNING: undefined reference to function: il_mac_reset_tsf
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_c83a1627-aa74-4a1c-821d-8a0871411254/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 25303 states (over memory cap)
KLEE: WARNING: killing 22842 states (over memory cap)
KLEE: WARNING: killing 22183 states (over memory cap)
KLEE: WARNING: killing 22719 states (over memory cap)
KLEE: WARNING: killing 22801 states (over memory cap)
KLEE: WARNING: killing 21943 states (over memory cap)
KLEE: WARNING: killing 23392 states (over memory cap)
KLEE: WARNING: killing 23359 states (over memory cap)
KLEE: WARNING: killing 24316 states (over memory cap)
KLEE: WARNING: killing 25731 states (over memory cap)
KLEE: WARNING: killing 25800 states (over memory cap)
KLEE: WARNING: killing 24962 states (over memory cap)
KLEE: WARNING: killing 25112 states (over memory cap)
KLEE: WARNING: killing 24672 states (over memory cap)
KLEE: WARNING: killing 25546 states (over memory cap)
KLEE: WARNING: killing 24218 states (over memory cap)
KLEE: WARNING: killing 23326 states (over memory cap)
KLEE: WARNING: killing 24055 states (over memory cap)
KLEE: WARNING: killing 24298 states (over memory cap)
KLEE: WARNING: killing 25118 states (over memory cap)
KLEE: WARNING: killing 24695 states (over memory cap)
KLEE: WARNING: killing 23685 states (over memory cap)
KLEE: WARNING: killing 24186 states (over memory cap)
KLEE: WARNING: killing 23857 states (over memory cap)
KLEE: WARNING: killing 26326 states (over memory cap)
KLEE: WARNING: killing 24734 states (over memory cap)
KLEE: WARNING: killing 24889 states (over memory cap)
KLEE: WARNING: killing 24827 states (over memory cap)
KLEE: WARNING: killing 23999 states (over memory cap)
KLEE: WARNING: killing 24370 states (over memory cap)
KLEE: WARNING: killing 24565 states (over memory cap)
KLEE: WARNING: killing 24017 states (over memory cap)
KLEE: WARNING: killing 23986 states (over memory cap)
KLEE: WARNING: killing 25199 states (over memory cap)
KLEE: WARNING: killing 24334 states (over memory cap)
KLEE: WARNING: killing 24133 states (over memory cap)
KLEE: WARNING: killing 24643 states (over memory cap)
KLEE: WARNING: killing 25361 states (over memory cap)
KLEE: WARNING: killing 24548 states (over memory cap)
KLEE: WARNING: killing 24693 states (over memory cap)
KLEE: WARNING: killing 23392 states (over memory cap)
KLEE: WARNING: killing 24781 states (over memory cap)
KLEE: WARNING: killing 23130 states (over memory cap)
KLEE: WARNING: killing 23671 states (over memory cap)
KLEE: WARNING: killing 26009 states (over memory cap)
KLEE: WARNING: killing 23630 states (over memory cap)
KLEE: WARNING: killing 24042 states (over memory cap)
KLEE: WARNING: killing 25056 states (over memory cap)
KLEE: WARNING: killing 24768 states (over memory cap)
KLEE: WARNING: killing 25227 states (over memory cap)
KLEE: WARNING: killing 23766 states (over memory cap)
KLEE: WARNING: killing 23171 states (over memory cap)
KLEE: WARNING: killing 24103 states (over memory cap)
KLEE: WARNING: killing 24159 states (over memory cap)
KLEE: WARNING: killing 24219 states (over memory cap)
KLEE: WARNING: killing 23774 states (over memory cap)
KLEE: WARNING: killing 25172 states (over memory cap)
KLEE: WARNING: killing 24244 states (over memory cap)
KLEE: WARNING: killing 24524 states (over memory cap)
KLEE: WARNING: killing 24624 states (over memory cap)
KLEE: WARNING: killing 25592 states (over memory cap)
KLEE: WARNING: killing 23931 states (over memory cap)
KLEE: WARNING: killing 23946 states (over memory cap)
KLEE: WARNING: killing 25174 states (over memory cap)
KLEE: WARNING: killing 23830 states (over memory cap)
KLEE: WARNING: killing 25359 states (over memory cap)
KLEE: WARNING: killing 24053 states (over memory cap)
KLEE: WARNING: killing 23591 states (over memory cap)
KLEE: WARNING: killing 25712 states (over memory cap)
KLEE: WARNING: killing 23930 states (over memory cap)
KLEE: WARNING: killing 24630 states (over memory cap)
KLEE: WARNING: killing 25043 states (over memory cap)
KLEE: WARNING: killing 24382 states (over memory cap)
KLEE: WARNING: killing 23384 states (over memory cap)
KLEE: WARNING: killing 24135 states (over memory cap)
KLEE: WARNING: killing 23633 states (over memory cap)
KLEE: WARNING: killing 23818 states (over memory cap)
KLEE: WARNING: killing 24600 states (over memory cap)
KLEE: WARNING: killing 24715 states (over memory cap)
KLEE: WARNING: killing 24700 states (over memory cap)
KLEE: WARNING: killing 24126 states (over memory cap)
KLEE: WARNING: killing 24957 states (over memory cap)
KLEE: WARNING: killing 25065 states (over memory cap)
KLEE: WARNING: killing 23989 states (over memory cap)
KLEE: WARNING: killing 23887 states (over memory cap)
KLEE: WARNING: killing 25098 states (over memory cap)
KLEE: WARNING: killing 23933 states (over memory cap)
KLEE: WARNING: killing 24963 states (over memory cap)
KLEE: WARNING: killing 23847 states (over memory cap)
KLEE: WARNING: killing 24669 states (over memory cap)
KLEE: WARNING: killing 25620 states (over memory cap)
KLEE: WARNING: killing 24340 states (over memory cap)
KLEE: WARNING: killing 24236 states (over memory cap)
KLEE: WARNING: killing 23465 states (over memory cap)
KLEE: WARNING: killing 24401 states (over memory cap)
KLEE: WARNING: killing 24847 states (over memory cap)
KLEE: WARNING: killing 23824 states (over memory cap)
KLEE: WARNING: killing 24595 states (over memory cap)
KLEE: WARNING: killing 24995 states (over memory cap)
KLEE: WARNING: killing 25021 states (over memory cap)
KLEE: WARNING: killing 24126 states (over memory cap)
KLEE: WARNING: killing 25230 states (over memory cap)
KLEE: WARNING: killing 23669 states (over memory cap)
KLEE: WARNING: killing 24394 states (over memory cap)
KLEE: WARNING: killing 23377 states (over memory cap)
KLEE: WARNING: killing 24438 states (over memory cap)
KLEE: WARNING: killing 23802 states (over memory cap)
KLEE: WARNING: killing 24235 states (over memory cap)
KLEE: WARNING: killing 24502 states (over memory cap)
KLEE: WARNING: killing 24275 states (over memory cap)
KLEE: WARNING: killing 24423 states (over memory cap)
KLEE: WARNING: killing 24859 states (over memory cap)
KLEE: WARNING: killing 24840 states (over memory cap)
KLEE: WARNING: killing 24566 states (over memory cap)
KLEE: WARNING: killing 24621 states (over memory cap)
KLEE: WARNING: killing 24562 states (over memory cap)
KLEE: WARNING: killing 24369 states (over memory cap)
KLEE: WARNING: killing 23277 states (over memory cap)
KLEE: WARNING: killing 24075 states (over memory cap)
KLEE: WARNING: killing 23969 states (over memory cap)
KLEE: WARNING: killing 25183 states (over memory cap)
