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--infiniband--hw--cxgb4--iw_cxgb4.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.: 621 592 5800 50833
Removed infinite loop in c4iw_register_device
Removed infinite loop in c4iw_query_gid
Removed infinite loop in c4iw_accept_cr
Removed infinite loop in c4iw_reject_cr
Removed infinite loop in _insert_handle
Removed infinite loop in send_mpa_reject
Removed infinite loop in c4iw_ep_disconnect
Removed infinite loop in c4iw_modify_qp
Removed infinite loop in __skb_put___2
Removed infinite loop in c4iw_flush_rq
Removed infinite loop in c4iw_flush_sq
Removed infinite loop in t4_swcq_produce
Removed infinite loop in t4_next_hw_cqe
Removed infinite loop in flush_completed_wrs
Removed infinite loop in build_fastreg
Removed infinite loop in c4iw_id_free
Removed infinite loop in __skb_put___1
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in _insert_handle___0
Removed infinite loop in poll_cq
Removed infinite loop in t4_sq_consume
Removed infinite loop in t4_swcq_consume
Removed infinite loop in _insert_handle___1
Removed infinite loop in __skb_put
Removed infinite loop in process_work
Removed infinite loop in peer_close
Removed infinite loop in peer_abort
Removed infinite loop in close_con_rpl
Removed infinite loop in rx_data
Removed infinite loop in terminate
Removed infinite loop in passive_ofld_conn_reply
Removed infinite loop in __skb_put___0
Removed infinite loop in accept_cr
Removed infinite loop in reject_cr
Removed infinite loop in send_mpa_req
Removed infinite loop in __skb_pull
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 1.76819109917
Removed calls to 'skb_queue_tail' (function is undefined)
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function printk as symbolic
Defining function default_llseek as symbolic
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Defining function idr_for_each as symbolic
Defining function vmalloc as symbolic
Defining function snprintf as symbolic
Defining function simple_read_from_buffer as symbolic
Removed calls to 'dev_err' (function is undefined)
Defining function cxgb4_read_tpte as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function single_release as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Removed calls to 'set_normalized_timespec' (function is undefined)
Defining function iwpm_register_pid_cb as symbolic
Defining function iwpm_add_mapping_cb as symbolic
Defining function iwpm_add_and_query_mapping_cb as symbolic
Defining function iwpm_remote_info_cb as symbolic
Defining function iwpm_mapping_error_cb as symbolic
Defining function iwpm_mapping_info_cb as symbolic
Defining function iwpm_ack_mapping_info_cb as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to 'ib_dealloc_device' (function is undefined)
Removed calls to 'gen_pool_destroy' (function is undefined)
Removed calls to 'idr_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'ib_dispatch_event' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '__list_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 schedule_timeout as symbolic
Defining function cxgb4_flush_eq_cache as symbolic
Removed calls to '__wake_up' (function is undefined)
Defining function cxgb4_sync_txq_pidx as symbolic
Defining function cxgb4_dbfifo_count as symbolic
Defining function __usecs_to_jiffies as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'ib_unregister_device' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Removed calls to 'idr_destroy' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'device_remove_file' (function is undefined)
Defining function strlcpy as symbolic
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'idr_remove' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'ib_umem_release' (function is undefined)
Removed calls to 'getnstimeofday64' (function is undefined)
Removed calls to 'cxgb4_get_tcp_stats' (function is undefined)
Removed calls to '_raw_read_lock_bh' (function is undefined)
Removed calls to '_raw_read_unlock_bh' (function is undefined)
Removed calls to 'cxgb4_l2t_release' (function is undefined)
Removed calls to 'dst_release' (function is undefined)
Removed calls to 'cxgb4_free_atid' (function is undefined)
Removed calls to 'cxgb4_free_stid' (function is undefined)
Defining function ib_register_device as symbolic
Defining function device_create_file as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function idr_find_slowpath as symbolic
Defining function cxgb4_remove_server_filter as symbolic
Defining function cxgb4_remove_server as symbolic
Removed calls to 'cxgb4_remove_tid' (function is undefined)
Defining function iwpm_remove_mapinfo as symbolic
Defining function iwpm_remove_mapping as symbolic
Defining function wait_for_completion_timeout as symbolic
Defining function cxgb4_alloc_sftid as symbolic
Defining function cxgb4_alloc_stid as symbolic
Removed calls to 'idr_preload' (function is undefined)
Defining function iwpm_register_pid as symbolic
Defining function iwpm_valid_pid as symbolic
Defining function iwpm_add_mapping as symbolic
Defining function iwpm_create_mapinfo as symbolic
Defining function cxgb4_create_server6 as symbolic
Defining function cxgb4_create_server_filter as symbolic
Defining function cxgb4_create_server as symbolic
Defining function idr_alloc as symbolic
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'skb_trim' (function is undefined)
Defining function skb_put as symbolic
Defining function cxgb4_l2t_send as symbolic
Defining function __alloc_skb as symbolic
Defining function cxgb4_ofld_send as symbolic
Defining function del_timer_sync as symbolic
Defining function queue_work_on as symbolic
Removed calls to 'dev_warn' (function is undefined)
Defining function cxgb4_alloc_atid as symbolic
Defining function iwpm_add_and_query_mapping as symbolic
Defining function cxgb4_select_ntuple as symbolic
Defining function prandom_u32 as symbolic
Defining function cxgb4_best_aligned_mtu as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Defining function ipv6_chk_addr as symbolic
Defining function cxgb4_l2t_get as symbolic
Defining function cxgb4_port_chan as symbolic
Defining function cxgb4_port_viid as symbolic
Defining function cxgb4_port_idx as symbolic
Removed calls to 'lock_release' (function is undefined)
Removed calls to 'neigh_destroy' (function is undefined)
Defining function rcu_is_watching as symbolic
Defining function vlan_dev_real_dev as symbolic
Defining function __ip_dev_find as symbolic
Defining function ip6_route_output as symbolic
Defining function lockdep_rtnl_is_held as symbolic
Defining function rcu_read_lock_held as symbolic
Defining function __ipv6_addr_type as symbolic
Defining function ip_route_output_flow as symbolic
Removed calls to 'in_dev_finish_destroy' (function is undefined)
Defining function cxgb4_read_sge_timestamp as symbolic
Defining function dma_alloc_attrs as symbolic
Removed calls to 'gen_pool_free' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function ___ratelimit as symbolic
Defining function __phys_addr as symbolic
Defining function find_next_zero_bit as symbolic
Defining function find_first_zero_bit as symbolic
Defining function gen_pool_alloc as symbolic
Defining function ib_umem_get as symbolic
Defining function __get_free_pages as symbolic
Defining function sg_next as symbolic
Defining function prepare_to_wait_event as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Removed calls to 'list_del' (function is undefined)
Defining function cxgb4_bar2_sge_qregs as symbolic
Defining function remap_pfn_range as symbolic
Defining function pgprot_writecombine as symbolic
Defining function ib_alloc_device as symbolic
Defining function ioremap_wc as symbolic
Defining function debugfs_create_dir as symbolic
Defining function debugfs_create_file_size as symbolic
Defining function gen_pool_create as symbolic
Defining function gen_pool_add_virt as symbolic
Defining function cxgb4_pktgl_to_skb as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function skb_dequeue as symbolic
Removed calls to 'tcp_parse_options' (function is undefined)
Defining function iwpm_get_remote_info as symbolic
Defining function skb_pull as symbolic
Defining function sprintf as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'debugfs_remove_recursive' (function is undefined)
Defining function ldv_release_11 as symbolic
Defining function ibnl_add_client as symbolic
Defining function iwpm_init as symbolic
Defining function ibnl_remove_client as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Defining function cxgb4_register_uld as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function cxgb4_unregister_uld as symbolic
Defining function iwpm_exit as symbolic
Defining function queue_delayed_work_on as symbolic
Linked our definitions to these undefined functions:
  memcmp
  __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: 2.26098203659
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 855 433 3130 40217
INFO: Starting verification
KLEE: WARNING ONCE: function "c4iw_uld_state_change" has inline asm
KLEE: WARNING ONCE: function "c4iw_uld_control" has inline asm
KLEE: WARNING ONCE: function "c4iw_qp_rem_ref" has inline asm
KLEE: WARNING ONCE: function "c4iw_qp_add_ref" has inline asm
KLEE: WARNING ONCE: function "c4iw_register_device" has inline asm
KLEE: WARNING ONCE: function "c4iw_query_port" has inline asm
KLEE: WARNING ONCE: function "c4iw_query_gid" has inline asm
KLEE: WARNING ONCE: function "c4iw_create_qp" has inline asm
KLEE: WARNING ONCE: function "c4iw_destroy_qp" has inline asm
KLEE: WARNING ONCE: function "c4iw_destroy_cq" has inline asm
KLEE: WARNING ONCE: function "c4iw_poll_cq" has inline asm
KLEE: WARNING ONCE: function "c4iw_reg_user_mr" has inline asm
KLEE: WARNING ONCE: function "c4iw_arm_cq" has inline asm
KLEE: WARNING ONCE: function "c4iw_post_send" has inline asm
KLEE: WARNING ONCE: function "c4iw_connect" has inline asm
KLEE: WARNING ONCE: function "c4iw_accept_cr" has inline asm
KLEE: WARNING ONCE: function "c4iw_reject_cr" has inline asm
KLEE: WARNING ONCE: function "c4iw_create_listen" has inline asm
KLEE: WARNING ONCE: function "kref_put" has inline asm
KLEE: WARNING ONCE: function "_c4iw_free_ep" has inline asm
KLEE: WARNING ONCE: function "insert_handle" has inline asm
KLEE: WARNING ONCE: function "c4iw_ep_disconnect" has inline asm
KLEE: WARNING ONCE: function "close_complete_upcall" has inline asm
KLEE: WARNING ONCE: function "start_ep_timer" has inline asm
KLEE: WARNING ONCE: function "stop_ep_timer" has inline asm
KLEE: WARNING ONCE: function "release_ep_resources" has inline asm
KLEE: WARNING ONCE: function "get_skb" has inline asm
KLEE: WARNING ONCE: function "kref_get" has inline asm
KLEE: WARNING ONCE: function "ep_timeout" has inline asm
KLEE: WARNING ONCE: function "abort_connection" has inline asm
KLEE: WARNING ONCE: function "c4iw_modify_qp" has inline asm
KLEE: WARNING ONCE: function "kref_get___0" has inline asm
KLEE: WARNING ONCE: function "__skb_put___2" has inline asm
KLEE: WARNING ONCE: function "flush_qp" has inline asm
KLEE: WARNING ONCE: function "kref_put___0" has inline asm
KLEE: WARNING ONCE: function "c4iw_flush_rq" has inline asm
KLEE: WARNING ONCE: function "c4iw_flush_sq" has inline asm
KLEE: WARNING ONCE: function "t4_swcq_produce" has inline asm
KLEE: WARNING ONCE: function "t4_next_hw_cqe" has inline asm
KLEE: WARNING ONCE: function "flush_completed_wrs" has inline asm
KLEE: WARNING ONCE: function "write_gts" has inline asm
KLEE: WARNING ONCE: function "t4_ring_rq_db___0" has inline asm
KLEE: WARNING ONCE: function "t4_ring_sq_db___0" 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 "in_dev_put" has inline asm
KLEE: WARNING ONCE: function "import_ep" has inline asm
KLEE: WARNING ONCE: function "send_connect" has inline asm
KLEE: WARNING ONCE: function "connect_reply_upcall" has inline asm
KLEE: WARNING ONCE: function "neigh_release" has inline asm
KLEE: WARNING ONCE: function "write_tpt_entry" has inline asm
KLEE: WARNING ONCE: function "insert_handle___0" has inline asm
KLEE: WARNING ONCE: function "c4iw_id_alloc" has inline asm
KLEE: WARNING ONCE: function "c4iw_id_free" has inline asm
KLEE: WARNING ONCE: function "__skb_put___1" has inline asm
KLEE: WARNING ONCE: function "c4iw_log_wr_stats" has inline asm
KLEE: WARNING ONCE: function "insert_handle___1" has inline asm
KLEE: WARNING ONCE: function "c4iw_id_table_alloc" has inline asm
KLEE: WARNING ONCE: function "__skb_put" has inline asm
KLEE: WARNING ONCE: function "c4iw_ev_handler" has inline asm
KLEE: WARNING ONCE: function "process_work" has inline asm
KLEE: WARNING ONCE: function "process_timedout_eps" has inline asm
KLEE: WARNING ONCE: function "act_open_rpl" has inline asm
KLEE: WARNING ONCE: function "peer_close" has inline asm
KLEE: WARNING ONCE: function "peer_abort" has inline asm
KLEE: WARNING ONCE: function "close_con_rpl" has inline asm
KLEE: WARNING ONCE: function "rx_data" has inline asm
KLEE: WARNING ONCE: function "rx_pkt" has inline asm
KLEE: WARNING ONCE: function "act_establish" has inline asm
KLEE: WARNING ONCE: function "pass_establish" has inline asm
KLEE: WARNING ONCE: function "pass_accept_req" has inline asm
KLEE: WARNING ONCE: function "terminate" has inline asm
KLEE: WARNING ONCE: function "deferred_fw6_msg" has inline asm
KLEE: WARNING ONCE: function "c4iw_ev_dispatch" has inline asm
KLEE: WARNING ONCE: function "send_fw_act_open_req" has inline asm
KLEE: WARNING ONCE: function "__skb_put___0" 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_c3c3150b-04ba-49a3-bcb5-ffcdb12450de/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8745 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 14371 states (over memory cap)
KLEE: WARNING: killing 13502 states (over memory cap)
KLEE: WARNING: killing 14420 states (over memory cap)
KLEE: WARNING: killing 15301 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-bzTL8z/linux-4.2-rc1.tar.xz-08_1a-drivers--infiniband--hw--cxgb4--iw_cxgb4.ko-entry_point_true-unreach-call.cil.out.c:10979: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bzTL8z/linux-4.2-rc1.tar.xz-08_1a-drivers--infiniband--hw--cxgb4--iw_cxgb4.ko-entry_point_true-unreach-call.cil.out.c:11821: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bzTL8z/linux-4.2-rc1.tar.xz-08_1a-drivers--infiniband--hw--cxgb4--iw_cxgb4.ko-entry_point_true-unreach-call.cil.out.c:11741: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bzTL8z/linux-4.2-rc1.tar.xz-08_1a-drivers--infiniband--hw--cxgb4--iw_cxgb4.ko-entry_point_true-unreach-call.cil.out.c:11900: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bzTL8z/linux-4.2-rc1.tar.xz-08_1a-drivers--infiniband--hw--cxgb4--iw_cxgb4.ko-entry_point_true-unreach-call.cil.out.c:10635: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16341 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-bzTL8z/linux-4.2-rc1.tar.xz-08_1a-drivers--infiniband--hw--cxgb4--iw_cxgb4.ko-entry_point_true-unreach-call.cil.out.c:10793: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15848 states (over memory cap)
KLEE: WARNING: killing 15363 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-bzTL8z/linux-4.2-rc1.tar.xz-08_1a-drivers--infiniband--hw--cxgb4--iw_cxgb4.ko-entry_point_true-unreach-call.cil.out.c:10918: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16439 states (over memory cap)
KLEE: WARNING: killing 17608 states (over memory cap)
KLEE: WARNING: killing 17216 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-bzTL8z/linux-4.2-rc1.tar.xz-08_1a-drivers--infiniband--hw--cxgb4--iw_cxgb4.ko-entry_point_true-unreach-call.cil.out.c:10979: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 18344 states (over memory cap)
KLEE: WARNING: killing 17747 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-bzTL8z/linux-4.2-rc1.tar.xz-08_1a-drivers--infiniband--hw--cxgb4--iw_cxgb4.ko-entry_point_true-unreach-call.cil.out.c:10635: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17855 states (over memory cap)
KLEE: WARNING: killing 16649 states (over memory cap)
KLEE: WARNING: killing 17687 states (over memory cap)
KLEE: WARNING: killing 16808 states (over memory cap)
KLEE: WARNING: killing 17640 states (over memory cap)
KLEE: WARNING: killing 16844 states (over memory cap)
KLEE: WARNING: killing 16661 states (over memory cap)
KLEE: WARNING: killing 17205 states (over memory cap)
KLEE: WARNING: killing 16368 states (over memory cap)
KLEE: WARNING: killing 16544 states (over memory cap)
KLEE: WARNING: killing 18062 states (over memory cap)
KLEE: WARNING: killing 17806 states (over memory cap)
KLEE: WARNING: killing 18393 states (over memory cap)
KLEE: WARNING: killing 17888 states (over memory cap)
KLEE: WARNING: killing 17393 states (over memory cap)
KLEE: WARNING: killing 17167 states (over memory cap)
KLEE: WARNING: killing 17185 states (over memory cap)
KLEE: WARNING: killing 17159 states (over memory cap)
KLEE: WARNING: killing 17064 states (over memory cap)
KLEE: WARNING: killing 17884 states (over memory cap)
KLEE: WARNING: killing 17672 states (over memory cap)
KLEE: WARNING: killing 16855 states (over memory cap)
KLEE: WARNING: killing 17827 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-bzTL8z/linux-4.2-rc1.tar.xz-08_1a-drivers--infiniband--hw--cxgb4--iw_cxgb4.ko-entry_point_true-unreach-call.cil.out.c:22005: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bzTL8z/linux-4.2-rc1.tar.xz-08_1a-drivers--infiniband--hw--cxgb4--iw_cxgb4.ko-entry_point_true-unreach-call.cil.out.c:21964: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17334 states (over memory cap)
KLEE: WARNING: killing 16874 states (over memory cap)
KLEE: WARNING: killing 17133 states (over memory cap)
KLEE: WARNING: killing 17873 states (over memory cap)
KLEE: WARNING: killing 17333 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-bzTL8z/linux-4.2-rc1.tar.xz-08_1a-drivers--infiniband--hw--cxgb4--iw_cxgb4.ko-entry_point_true-unreach-call.cil.out.c:21980: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17403 states (over memory cap)
KLEE: WARNING: killing 16823 states (over memory cap)
KLEE: WARNING: killing 17126 states (over memory cap)
KLEE: WARNING: killing 17895 states (over memory cap)
KLEE: WARNING: killing 17764 states (over memory cap)
KLEE: WARNING: killing 17195 states (over memory cap)
KLEE: WARNING: killing 17408 states (over memory cap)
KLEE: WARNING: killing 17279 states (over memory cap)
KLEE: WARNING: killing 18133 states (over memory cap)
KLEE: WARNING: killing 17366 states (over memory cap)
KLEE: WARNING: killing 16755 states (over memory cap)
KLEE: WARNING: killing 17328 states (over memory cap)
KLEE: WARNING: killing 16682 states (over memory cap)
KLEE: WARNING: killing 17173 states (over memory cap)
KLEE: WARNING: killing 17827 states (over memory cap)
KLEE: WARNING: killing 18086 states (over memory cap)
KLEE: WARNING: killing 17522 states (over memory cap)
KLEE: WARNING: killing 17942 states (over memory cap)
KLEE: WARNING: killing 17453 states (over memory cap)
KLEE: WARNING: killing 17163 states (over memory cap)
KLEE: WARNING: killing 17891 states (over memory cap)
KLEE: WARNING: killing 17173 states (over memory cap)
KLEE: WARNING: killing 17276 states (over memory cap)
KLEE: WARNING: killing 16912 states (over memory cap)
KLEE: WARNING: killing 16929 states (over memory cap)
KLEE: WARNING: killing 17489 states (over memory cap)
KLEE: WARNING: killing 17834 states (over memory cap)
KLEE: WARNING: killing 17507 states (over memory cap)
KLEE: WARNING: killing 18425 states (over memory cap)
KLEE: WARNING: killing 17910 states (over memory cap)
KLEE: WARNING: killing 17432 states (over memory cap)
KLEE: WARNING: killing 17802 states (over memory cap)
KLEE: WARNING: killing 16898 states (over memory cap)
KLEE: WARNING: killing 16994 states (over memory cap)
KLEE: WARNING: killing 18023 states (over memory cap)
KLEE: WARNING: killing 17164 states (over memory cap)
KLEE: WARNING: killing 17573 states (over memory cap)
KLEE: WARNING: killing 17438 states (over memory cap)
KLEE: WARNING: killing 16927 states (over memory cap)
KLEE: WARNING: killing 17726 states (over memory cap)
KLEE: WARNING: killing 17482 states (over memory cap)
KLEE: WARNING: killing 17702 states (over memory cap)
KLEE: WARNING: killing 17843 states (over memory cap)
KLEE: WARNING: killing 17170 states (over memory cap)
KLEE: WARNING: killing 16736 states (over memory cap)
KLEE: WARNING: killing 17486 states (over memory cap)
KLEE: WARNING: killing 17356 states (over memory cap)
KLEE: WARNING: killing 18221 states (over memory cap)
KLEE: WARNING: killing 17568 states (over memory cap)
KLEE: WARNING: killing 17278 states (over memory cap)
KLEE: WARNING: killing 16766 states (over memory cap)
KLEE: WARNING: killing 17436 states (over memory cap)
KLEE: WARNING: killing 17886 states (over memory cap)
KLEE: WARNING: killing 17790 states (over memory cap)
KLEE: WARNING: killing 17125 states (over memory cap)
KLEE: WARNING: killing 17947 states (over memory cap)
KLEE: WARNING: killing 17365 states (over memory cap)
KLEE: WARNING: killing 17661 states (over memory cap)
KLEE: WARNING: killing 16700 states (over memory cap)
KLEE: WARNING: killing 17549 states (over memory cap)
KLEE: WARNING: killing 18190 states (over memory cap)
KLEE: WARNING: killing 17567 states (over memory cap)
KLEE: WARNING: killing 17408 states (over memory cap)
KLEE: WARNING: killing 17921 states (over memory cap)
KLEE: WARNING: killing 17074 states (over memory cap)
KLEE: WARNING: killing 16334 states (over memory cap)
KLEE: WARNING: killing 17869 states (over memory cap)
KLEE: WARNING: killing 17395 states (over memory cap)
KLEE: WARNING: killing 17757 states (over memory cap)
KLEE: WARNING: killing 17477 states (over memory cap)
KLEE: WARNING: killing 17388 states (over memory cap)
KLEE: WARNING: killing 17524 states (over memory cap)
KLEE: WARNING: killing 16981 states (over memory cap)
KLEE: WARNING: killing 18096 states (over memory cap)
KLEE: WARNING: killing 17630 states (over memory cap)
KLEE: WARNING: killing 16943 states (over memory cap)
KLEE: WARNING: killing 18126 states (over memory cap)
KLEE: WARNING: killing 17068 states (over memory cap)
KLEE: WARNING: killing 17240 states (over memory cap)
KLEE: WARNING: killing 17709 states (over memory cap)
