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--mwifiex--mwifiex.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.: 1114 933 15580 100382
Removed infinite loop in mwifiex_process_uap_txpd
Removed infinite loop in mwifiex_process_sta_txpd
Removed infinite loop in wiphy_priv
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 3.57128000259
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function queue_work_on as symbolic
Removed calls to '__wake_up' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Removed calls to 'print_hex_dump' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'skb_trim' (function is undefined)
Removed calls to 'skb_queue_head' (function is undefined)
Removed calls to 'skb_queue_tail' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'cfg80211_cac_event' (function is undefined)
Removed calls to 'idr_destroy' (function is undefined)
Removed calls to 'netif_tx_wake_queue' (function is undefined)
Defining function skb_dequeue as symbolic
Defining function printk as symbolic
Removed calls to 'cfg80211_scan_done' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function del_timer as symbolic
Removed calls to 'kfree_skb' (function is undefined)
Defining function idr_for_each as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Defining function del_timer_sync as symbolic
Removed calls to 'ieee80211_amsdu_to_8023s' (function is undefined)
Defining function skb_pull as symbolic
Defining function eth_type_trans as symbolic
Defining function netif_rx as symbolic
Defining function netif_rx_ni as symbolic
Defining function skb_copy as symbolic
Defining function skb_realloc_headroom as symbolic
Removed calls to 'do_gettimeofday' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function ktime_get_with_offset as symbolic
Defining function mod_timer as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function __memmove as symbolic
Defining function cfg80211_rx_mgmt as symbolic
Defining function cancel_delayed_work_sync as symbolic
Defining function skb_put as symbolic
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Defining function schedule_timeout as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function ieee80211_frequency_to_channel as symbolic
Defining function kmemdup as symbolic
Defining function of_property_read_u8_array as symbolic
Defining function skb_push as symbolic
Defining function __netdev_alloc_skb as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to 'netif_carrier_on' (function is undefined)
Removed calls to 'cfg80211_disconnected' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to 'cfg80211_put_bss' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'lock_acquire' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_read_lock_held as symbolic
Removed calls to 'lock_release' (function is undefined)
Defining function rcu_is_watching as symbolic
Defining function cfg80211_inform_bss_width as symbolic
Defining function __ieee80211_get_channel as symbolic
Removed calls to 'cfg80211_new_sta' (function is undefined)
Removed calls to 'cfg80211_del_sta_sinfo' (function is undefined)
Removed calls to 'cfg80211_michael_mic_failure' (function is undefined)
Removed calls to 'cfg80211_cqm_rssi_notify' (function is undefined)
Removed calls to 'cfg80211_remain_on_channel_expired' (function is undefined)
Removed calls to 'cfg80211_tdls_oper_request' (function is undefined)
Removed calls to 'idr_remove' (function is undefined)
Removed calls to 'skb_complete_wifi_ack' (function is undefined)
Removed calls to 'cfg80211_mgmt_tx_status' (function is undefined)
Removed calls to 'cfg80211_radar_event' (function is undefined)
Defining function idr_find_slowpath as symbolic
Defining function cfg80211_find_ie as symbolic
Defining function vzalloc as symbolic
Defining function sprintf as symbolic
Defining function snprintf as symbolic
Removed calls to 'dev_coredumpv' (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 'schedule' (function is undefined)
Removed calls to 'up' (function is undefined)
Defining function down_interruptible as symbolic
Defining function __alloc_workqueue_key as symbolic
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'rtnl_lock' (function is undefined)
Removed calls to 'rtnl_unlock' (function is undefined)
Removed calls to 'wiphy_unregister' (function is undefined)
Removed calls to 'wiphy_free' (function is undefined)
Removed calls to 'release_firmware' (function is undefined)
Defining function request_firmware_nowait as symbolic
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Defining function alloc_netdev_mqs as symbolic
Defining function register_netdevice as symbolic
Removed calls to 'cfg80211_ch_switch_notify' (function is undefined)
Defining function debugfs_create_dir as symbolic
Defining function debugfs_create_file as symbolic
Defining function vmalloc as symbolic
Defining function wiphy_register as symbolic
Defining function wiphy_new_nm as symbolic
Defining function of_find_node_by_name as symbolic
Defining function __bitmap_weight as symbolic
Removed calls to 'idr_init' (function is undefined)
Removed calls to 'debugfs_remove_recursive' (function is undefined)
Removed calls to 'unregister_netdevice_queue' (function is undefined)
Defining function cfg80211_classify8021d as symbolic
Defining function skb_clone as symbolic
Defining function idr_alloc as symbolic
Removed calls to 'cfg80211_connect_result' (function is undefined)
Removed calls to 'cfg80211_ibss_joined' (function is undefined)
Removed calls to 'cfg80211_ready_on_channel' (function is undefined)
Removed calls to 'cfg80211_chandef_create' (function is undefined)
Defining function queue_delayed_work_on as symbolic
Defining function cfg80211_find_vendor_ie as symbolic
Defining function mwifiex_is_11h_active as symbolic
Defining function cfg80211_chandef_valid as symbolic
Defining function ieee80211_channel_to_frequency as symbolic
Defining function prandom_u32 as symbolic
Defining function cfg80211_get_bss as symbolic
Defining function ieee80211_bss_get_ie as symbolic
Defining function jiffies_to_msecs as symbolic
Defining function cfg80211_chandef_dfs_required as symbolic
Defining function device_set_wakeup_enable as symbolic
Defining function lockdep_rtnl_is_held as symbolic
Removed calls to 'free_pages' (function is undefined)
Defining function simple_open as symbolic
Defining function get_zeroed_page as symbolic
Defining function simple_read_from_buffer as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function sscanf as symbolic
Defining function _copy_from_user as symbolic
Defining function kstrtoull as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'debugfs_remove' (function is undefined)
Defining function ldv_ndo_init_21 as symbolic
Defining function ldv_ndo_uninit_21 as symbolic
Defining function ldv_release_10 as symbolic
Defining function ldv_release_15 as symbolic
Defining function ldv_release_14 as symbolic
Defining function ldv_release_20 as symbolic
Defining function ldv_bind_20 as symbolic
Defining function ldv_release_12 as symbolic
Defining function ldv_release_9 as symbolic
Defining function ldv_release_13 as symbolic
Defining function ldv_release_16 as symbolic
Defining function ldv_release_18 as symbolic
Defining function ldv_release_17 as symbolic
Defining function ldv_release_11 as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcpy
  strlen
  strncmp
  __kmalloc
  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: 3.37029290199
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 843 726 8287 55390
INFO: Starting verification
KLEE: WARNING ONCE: function "mwifiex_process_tx_queue" has inline asm
KLEE: WARNING ONCE: function "mwifiex_wmm_process_tx" has inline asm
KLEE: WARNING ONCE: function "mwifiex_shutdown_drv" has inline asm
KLEE: WARNING ONCE: function "mwifiex_recycle_cmd_node" has inline asm
KLEE: WARNING ONCE: function "mwifiex_write_data_complete" has inline asm
KLEE: WARNING ONCE: function "mwifiex_recv_packet" has inline asm
KLEE: WARNING ONCE: function "mwifiex_hist_data_set" has inline asm
KLEE: WARNING ONCE: function "mwifiex_uap_queue_bridged_pkt" has inline asm
KLEE: WARNING ONCE: function "mwifiex_wmm_add_buf_txqueue" has inline asm
KLEE: WARNING ONCE: function "mwifiex_rx_work_queue" has inline asm
KLEE: WARNING ONCE: function "mwifiex_insert_cmd_to_pending_q" has inline asm
KLEE: WARNING ONCE: function "mwifiex_11n_aggregate_pkt" has inline asm
KLEE: WARNING ONCE: function "mwifiex_send_single_packet" has inline asm
KLEE: WARNING ONCE: function "mwifiex_process_tx" has inline asm
KLEE: WARNING ONCE: function "mwifiex_process_uap_txpd" has inline asm
KLEE: WARNING ONCE: function "mwifiex_process_sta_txpd" has inline asm
KLEE: WARNING ONCE: function "mwifiex_stop_net_dev_queue" has inline asm
KLEE: WARNING ONCE: function "mwifiex_restore_tdls_packets" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "mwifiex_wmm_del_peer_ra_list" has inline asm
KLEE: WARNING ONCE: function "mwifiex_add_virtual_intf" has inline asm
KLEE: WARNING ONCE: function "mwifiex_reg_notifier" has inline asm
KLEE: WARNING ONCE: function "mwifiex_queue_tx_pkt" has inline asm
KLEE: WARNING ONCE: function "mwifiex_cfg80211_suspend" has inline asm
KLEE: WARNING ONCE: function "mwifiex_cfg80211_set_wakeup" has inline asm
KLEE: WARNING ONCE: function "mwifiex_cfg80211_set_wiphy_params" has inline asm
KLEE: WARNING ONCE: function "mwifiex_cfg80211_set_tx_power" has inline asm
KLEE: WARNING ONCE: function "mwifiex_cfg80211_set_antenna" has inline asm
KLEE: WARNING ONCE: function "mwifiex_cfg80211_set_coalesce" has inline asm
KLEE: WARNING ONCE: function "mwifiex_tdls_oper" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to function: ether_setup
KLEE: WARNING: undefined reference to function: free_netdev
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_1f714c15-3bbf-41db-b7a7-0b97c0c8be1d/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 7180 states (over memory cap)
KLEE: WARNING: killing 20295 states (over memory cap)
KLEE: WARNING: killing 19890 states (over memory cap)
KLEE: WARNING: killing 19718 states (over memory cap)
KLEE: WARNING: killing 19554 states (over memory cap)
KLEE: WARNING: killing 19812 states (over memory cap)
KLEE: WARNING: killing 20202 states (over memory cap)
KLEE: WARNING: killing 21103 states (over memory cap)
KLEE: WARNING: killing 22392 states (over memory cap)
KLEE: WARNING: killing 21590 states (over memory cap)
KLEE: WARNING: killing 20978 states (over memory cap)
KLEE: WARNING: killing 20870 states (over memory cap)
KLEE: WARNING: killing 22238 states (over memory cap)
KLEE: WARNING: killing 21292 states (over memory cap)
KLEE: WARNING: killing 20728 states (over memory cap)
KLEE: WARNING: killing 21628 states (over memory cap)
KLEE: WARNING: killing 20752 states (over memory cap)
KLEE: WARNING: killing 19809 states (over memory cap)
KLEE: WARNING: killing 21774 states (over memory cap)
KLEE: WARNING: killing 20668 states (over memory cap)
KLEE: WARNING: killing 21804 states (over memory cap)
KLEE: WARNING: killing 21131 states (over memory cap)
KLEE: WARNING: killing 20717 states (over memory cap)
KLEE: WARNING: killing 21581 states (over memory cap)
KLEE: WARNING: killing 20721 states (over memory cap)
KLEE: WARNING: killing 21728 states (over memory cap)
KLEE: WARNING: killing 20901 states (over memory cap)
KLEE: WARNING: killing 21910 states (over memory cap)
KLEE: WARNING: killing 21272 states (over memory cap)
KLEE: WARNING: killing 21139 states (over memory cap)
KLEE: WARNING: killing 20128 states (over memory cap)
KLEE: WARNING: killing 20255 states (over memory cap)
KLEE: WARNING: killing 20956 states (over memory cap)
KLEE: WARNING: killing 22185 states (over memory cap)
KLEE: WARNING: killing 20576 states (over memory cap)
KLEE: WARNING: killing 21080 states (over memory cap)
KLEE: WARNING: killing 20905 states (over memory cap)
KLEE: WARNING: killing 21713 states (over memory cap)
KLEE: WARNING: killing 20676 states (over memory cap)
KLEE: WARNING: killing 21177 states (over memory cap)
KLEE: WARNING: killing 20481 states (over memory cap)
KLEE: WARNING: killing 20862 states (over memory cap)
KLEE: WARNING: killing 21488 states (over memory cap)
KLEE: WARNING: killing 20646 states (over memory cap)
KLEE: WARNING: killing 20624 states (over memory cap)
KLEE: WARNING: killing 21278 states (over memory cap)
KLEE: WARNING: killing 20504 states (over memory cap)
KLEE: WARNING: killing 20974 states (over memory cap)
KLEE: WARNING: killing 20426 states (over memory cap)
KLEE: WARNING: killing 20970 states (over memory cap)
KLEE: WARNING: killing 21282 states (over memory cap)
KLEE: WARNING: killing 21190 states (over memory cap)
KLEE: WARNING: killing 22402 states (over memory cap)
KLEE: WARNING: killing 21078 states (over memory cap)
KLEE: WARNING: killing 21395 states (over memory cap)
KLEE: WARNING: killing 21342 states (over memory cap)
KLEE: WARNING: killing 21321 states (over memory cap)
KLEE: WARNING: killing 20555 states (over memory cap)
KLEE: WARNING: killing 21163 states (over memory cap)
KLEE: WARNING: killing 21291 states (over memory cap)
KLEE: WARNING: killing 20760 states (over memory cap)
KLEE: WARNING: killing 19966 states (over memory cap)
KLEE: WARNING: killing 21158 states (over memory cap)
KLEE: WARNING: killing 21734 states (over memory cap)
KLEE: WARNING: killing 20466 states (over memory cap)
KLEE: WARNING: killing 20996 states (over memory cap)
KLEE: WARNING: killing 20691 states (over memory cap)
KLEE: WARNING: killing 21256 states (over memory cap)
KLEE: WARNING: killing 21381 states (over memory cap)
KLEE: WARNING: killing 22362 states (over memory cap)
KLEE: WARNING: killing 20841 states (over memory cap)
KLEE: WARNING: killing 20387 states (over memory cap)
KLEE: WARNING: killing 20950 states (over memory cap)
KLEE: WARNING: killing 21917 states (over memory cap)
KLEE: WARNING: killing 20407 states (over memory cap)
KLEE: WARNING: killing 20233 states (over memory cap)
KLEE: WARNING: killing 21492 states (over memory cap)
KLEE: WARNING: killing 21404 states (over memory cap)
KLEE: WARNING: killing 20474 states (over memory cap)
KLEE: WARNING: killing 21475 states (over memory cap)
KLEE: WARNING: killing 20986 states (over memory cap)
KLEE: WARNING: killing 21229 states (over memory cap)
KLEE: WARNING: killing 20336 states (over memory cap)
KLEE: WARNING: killing 21727 states (over memory cap)
KLEE: WARNING: killing 20951 states (over memory cap)
KLEE: WARNING: killing 21478 states (over memory cap)
KLEE: WARNING: killing 21797 states (over memory cap)
KLEE: WARNING: killing 21128 states (over memory cap)
KLEE: WARNING: killing 20380 states (over memory cap)
KLEE: WARNING: killing 21516 states (over memory cap)
KLEE: WARNING: killing 21065 states (over memory cap)
KLEE: WARNING: killing 21120 states (over memory cap)
KLEE: WARNING: killing 21605 states (over memory cap)
KLEE: WARNING: killing 20873 states (over memory cap)
KLEE: WARNING: killing 20459 states (over memory cap)
KLEE: WARNING: killing 20330 states (over memory cap)
KLEE: WARNING: killing 21750 states (over memory cap)
KLEE: WARNING: killing 21229 states (over memory cap)
KLEE: WARNING: killing 20565 states (over memory cap)
KLEE: WARNING: killing 21309 states (over memory cap)
KLEE: WARNING: killing 20606 states (over memory cap)
KLEE: WARNING: killing 22014 states (over memory cap)
KLEE: WARNING: killing 20854 states (over memory cap)
KLEE: WARNING: killing 20228 states (over memory cap)
KLEE: WARNING: killing 22276 states (over memory cap)
KLEE: WARNING: killing 20972 states (over memory cap)
KLEE: WARNING: killing 21238 states (over memory cap)
KLEE: WARNING: killing 21362 states (over memory cap)
KLEE: WARNING: killing 21237 states (over memory cap)
KLEE: WARNING: killing 21010 states (over memory cap)
KLEE: WARNING: killing 21342 states (over memory cap)
klee: /var/xchalup4/symbiotic/klee/include/klee/Internal/ADT/DiscretePDF.inc:116: void klee::DiscretePDF<T>::remove(T) [with T = klee::ExecutionState*]: Assertion `0 && "remove: argument(item) not in tree"' failed.
KLEE: output directory is "/tmp/symbiotic-72flbj/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "mwifiex_process_tx_queue" has inline asm
KLEE: WARNING ONCE: function "mwifiex_wmm_process_tx" has inline asm
KLEE: WARNING ONCE: function "mwifiex_shutdown_drv" has inline asm
KLEE: WARNING ONCE: function "mwifiex_recycle_cmd_node" has inline asm
KLEE: WARNING ONCE: function "mwifiex_write_data_complete" has inline asm
KLEE: WARNING ONCE: function "mwifiex_recv_packet" has inline asm
KLEE: WARNING ONCE: function "mwifiex_hist_data_set" has inline asm
KLEE: WARNING ONCE: function "mwifiex_uap_queue_bridged_pkt" has inline asm
KLEE: WARNING ONCE: function "mwifiex_wmm_add_buf_txqueue" has inline asm
KLEE: WARNING ONCE: function "mwifiex_rx_work_queue" has inline asm
KLEE: WARNING ONCE: function "mwifiex_insert_cmd_to_pending_q" has inline asm
KLEE: WARNING ONCE: function "mwifiex_11n_aggregate_pkt" has inline asm
KLEE: WARNING ONCE: function "mwifiex_send_single_packet" has inline asm
KLEE: WARNING ONCE: function "mwifiex_process_tx" has inline asm
KLEE: WARNING ONCE: function "mwifiex_process_uap_txpd" has inline asm
KLEE: WARNING ONCE: function "mwifiex_process_sta_txpd" has inline asm
KLEE: WARNING ONCE: function "mwifiex_stop_net_dev_queue" has inline asm
KLEE: WARNING ONCE: function "mwifiex_restore_tdls_packets" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "mwifiex_wmm_del_peer_ra_list" has inline asm
KLEE: WARNING ONCE: function "mwifiex_add_virtual_intf" has inline asm
KLEE: WARNING ONCE: function "mwifiex_reg_notifier" has inline asm
KLEE: WARNING ONCE: function "mwifiex_queue_tx_pkt" has inline asm
KLEE: WARNING ONCE: function "mwifiex_cfg80211_suspend" has inline asm
KLEE: WARNING ONCE: function "mwifiex_cfg80211_set_wakeup" has inline asm
KLEE: WARNING ONCE: function "mwifiex_cfg80211_set_wiphy_params" has inline asm
KLEE: WARNING ONCE: function "mwifiex_cfg80211_set_tx_power" has inline asm
KLEE: WARNING ONCE: function "mwifiex_cfg80211_set_antenna" has inline asm
KLEE: WARNING ONCE: function "mwifiex_cfg80211_set_coalesce" has inline asm
KLEE: WARNING ONCE: function "mwifiex_tdls_oper" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to function: ether_setup
KLEE: WARNING: undefined reference to function: free_netdev
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_1f714c15-3bbf-41db-b7a7-0b97c0c8be1d/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 7180 states (over memory cap)
KLEE: WARNING: killing 20295 states (over memory cap)
KLEE: WARNING: killing 19890 states (over memory cap)
KLEE: WARNING: killing 19718 states (over memory cap)
KLEE: WARNING: killing 19554 states (over memory cap)
KLEE: WARNING: killing 19812 states (over memory cap)
KLEE: WARNING: killing 20202 states (over memory cap)
KLEE: WARNING: killing 21103 states (over memory cap)
KLEE: WARNING: killing 22392 states (over memory cap)
KLEE: WARNING: killing 21590 states (over memory cap)
KLEE: WARNING: killing 20978 states (over memory cap)
KLEE: WARNING: killing 20870 states (over memory cap)
KLEE: WARNING: killing 22238 states (over memory cap)
KLEE: WARNING: killing 21292 states (over memory cap)
KLEE: WARNING: killing 20728 states (over memory cap)
KLEE: WARNING: killing 21628 states (over memory cap)
KLEE: WARNING: killing 20752 states (over memory cap)
KLEE: WARNING: killing 19809 states (over memory cap)
KLEE: WARNING: killing 21774 states (over memory cap)
KLEE: WARNING: killing 20668 states (over memory cap)
KLEE: WARNING: killing 21804 states (over memory cap)
KLEE: WARNING: killing 21131 states (over memory cap)
KLEE: WARNING: killing 20717 states (over memory cap)
KLEE: WARNING: killing 21581 states (over memory cap)
KLEE: WARNING: killing 20721 states (over memory cap)
KLEE: WARNING: killing 21728 states (over memory cap)
KLEE: WARNING: killing 20901 states (over memory cap)
KLEE: WARNING: killing 21910 states (over memory cap)
KLEE: WARNING: killing 21272 states (over memory cap)
KLEE: WARNING: killing 21139 states (over memory cap)
KLEE: WARNING: killing 20128 states (over memory cap)
KLEE: WARNING: killing 20255 states (over memory cap)
KLEE: WARNING: killing 20956 states (over memory cap)
KLEE: WARNING: killing 22185 states (over memory cap)
KLEE: WARNING: killing 20576 states (over memory cap)
KLEE: WARNING: killing 21080 states (over memory cap)
KLEE: WARNING: killing 20905 states (over memory cap)
KLEE: WARNING: killing 21713 states (over memory cap)
KLEE: WARNING: killing 20676 states (over memory cap)
KLEE: WARNING: killing 21177 states (over memory cap)
KLEE: WARNING: killing 20481 states (over memory cap)
KLEE: WARNING: killing 20862 states (over memory cap)
KLEE: WARNING: killing 21488 states (over memory cap)
KLEE: WARNING: killing 20646 states (over memory cap)
KLEE: WARNING: killing 20624 states (over memory cap)
KLEE: WARNING: killing 21278 states (over memory cap)
KLEE: WARNING: killing 20504 states (over memory cap)
KLEE: WARNING: killing 20974 states (over memory cap)
KLEE: WARNING: killing 20426 states (over memory cap)
KLEE: WARNING: killing 20970 states (over memory cap)
KLEE: WARNING: killing 21282 states (over memory cap)
KLEE: WARNING: killing 21190 states (over memory cap)
KLEE: WARNING: killing 22402 states (over memory cap)
KLEE: WARNING: killing 21078 states (over memory cap)
KLEE: WARNING: killing 21395 states (over memory cap)
KLEE: WARNING: killing 21342 states (over memory cap)
KLEE: WARNING: killing 21321 states (over memory cap)
KLEE: WARNING: killing 20555 states (over memory cap)
KLEE: WARNING: killing 21163 states (over memory cap)
KLEE: WARNING: killing 21291 states (over memory cap)
KLEE: WARNING: killing 20760 states (over memory cap)
KLEE: WARNING: killing 19966 states (over memory cap)
KLEE: WARNING: killing 21158 states (over memory cap)
KLEE: WARNING: killing 21734 states (over memory cap)
KLEE: WARNING: killing 20466 states (over memory cap)
KLEE: WARNING: killing 20996 states (over memory cap)
KLEE: WARNING: killing 20691 states (over memory cap)
KLEE: WARNING: killing 21256 states (over memory cap)
KLEE: WARNING: killing 21381 states (over memory cap)
KLEE: WARNING: killing 22362 states (over memory cap)
KLEE: WARNING: killing 20841 states (over memory cap)
KLEE: WARNING: killing 20387 states (over memory cap)
KLEE: WARNING: killing 20950 states (over memory cap)
KLEE: WARNING: killing 21917 states (over memory cap)
KLEE: WARNING: killing 20407 states (over memory cap)
KLEE: WARNING: killing 20233 states (over memory cap)
KLEE: WARNING: killing 21492 states (over memory cap)
KLEE: WARNING: killing 21404 states (over memory cap)
KLEE: WARNING: killing 20474 states (over memory cap)
KLEE: WARNING: killing 21475 states (over memory cap)
KLEE: WARNING: killing 20986 states (over memory cap)
KLEE: WARNING: killing 21229 states (over memory cap)
KLEE: WARNING: killing 20336 states (over memory cap)
KLEE: WARNING: killing 21727 states (over memory cap)
KLEE: WARNING: killing 20951 states (over memory cap)
KLEE: WARNING: killing 21478 states (over memory cap)
KLEE: WARNING: killing 21797 states (over memory cap)
KLEE: WARNING: killing 21128 states (over memory cap)
KLEE: WARNING: killing 20380 states (over memory cap)
KLEE: WARNING: killing 21516 states (over memory cap)
KLEE: WARNING: killing 21065 states (over memory cap)
KLEE: WARNING: killing 21120 states (over memory cap)
KLEE: WARNING: killing 21605 states (over memory cap)
KLEE: WARNING: killing 20873 states (over memory cap)
KLEE: WARNING: killing 20459 states (over memory cap)
KLEE: WARNING: killing 20330 states (over memory cap)
KLEE: WARNING: killing 21750 states (over memory cap)
KLEE: WARNING: killing 21229 states (over memory cap)
KLEE: WARNING: killing 20565 states (over memory cap)
KLEE: WARNING: killing 21309 states (over memory cap)
KLEE: WARNING: killing 20606 states (over memory cap)
KLEE: WARNING: killing 22014 states (over memory cap)
KLEE: WARNING: killing 20854 states (over memory cap)
KLEE: WARNING: killing 20228 states (over memory cap)
KLEE: WARNING: killing 22276 states (over memory cap)
KLEE: WARNING: killing 20972 states (over memory cap)
KLEE: WARNING: killing 21238 states (over memory cap)
KLEE: WARNING: killing 21362 states (over memory cap)
KLEE: WARNING: killing 21237 states (over memory cap)
KLEE: WARNING: killing 21010 states (over memory cap)
KLEE: WARNING: killing 21342 states (over memory cap)
klee: /var/xchalup4/symbiotic/klee/include/klee/Internal/ADT/DiscretePDF.inc:116: void klee::DiscretePDF<T>::remove(T) [with T = klee::ExecutionState*]: Assertion `0 && "remove: argument(item) not in tree"' failed.
0  klee            0x00000000012fcca8 llvm::sys::PrintStackTrace(llvm::raw_ostream&) + 56
1  klee            0x00000000012fac7e llvm::sys::RunSignalHandlers() + 62
2  klee            0x00000000012fadcc
3  libpthread.so.0 0x00007f0704f4f390
4  libc.so.6       0x00007f0704308428 gsignal + 56
5  libc.so.6       0x00007f070430a02a abort + 362
6  libc.so.6       0x00007f0704300bd7
7  libc.so.6       0x00007f0704300c82
8  klee            0x000000000061be59 klee::DiscretePDF<klee::ExecutionState*>::remove(klee::ExecutionState*) + 73
9  klee            0x00000000006195f1 klee::WeightedRandomSearcher::update(klee::ExecutionState*, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&) + 241
10 klee            0x0000000000617416 klee::InterleavedSearcher::update(klee::ExecutionState*, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&) + 54
11 klee            0x00000000005cecfe klee::Executor::updateStates(klee::ExecutionState*) + 46
12 klee            0x00000000005da8eb klee::Executor::run(klee::ExecutionState&) + 2155
13 klee            0x00000000005daeef klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1391
14 klee            0x0000000000593c63 main + 8867
15 libc.so.6       0x00007f07042f3830 __libc_start_main + 240
16 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 811.104464054
