bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.14/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-ethernet-qlogic-qlge-qlge_true-unreach-call.cil.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.: 445 643 5448 32038
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.19262218475
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '__napi_schedule' (function is undefined)
Defining function netdev_printk as symbolic
Defining function netdev_err as symbolic
Defining function queue_delayed_work_on as symbolic
Defining function netdev_info as symbolic
Removed calls to '__ldv_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function netdev_crit as symbolic
Defining function netdev_alert as symbolic
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function __pci_register_driver as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'netif_napi_del' (function is undefined)
Removed calls to 'netif_napi_add' (function is undefined)
Defining function dev_close as symbolic
Removed calls to 'netif_carrier_on' (function is undefined)
Defining function usecs_to_jiffies as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function find_first_bit as symbolic
Defining function find_next_bit as symbolic
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Removed calls to 'dump_page' (function is undefined)
Removed calls to 'debug_dma_sync_single_for_device' (function is undefined)
Defining function __get_page_tail as symbolic
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Defining function alloc_pages_current as symbolic
Defining function __phys_addr as symbolic
Defining function __netdev_alloc_skb as symbolic
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Removed calls to 'napi_complete' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Defining function skb_put as symbolic
Defining function eth_type_trans as symbolic
Defining function napi_gro_receive as symbolic
Defining function netif_receive_skb as symbolic
Removed calls to 'debug_dma_sync_single_for_cpu' (function is undefined)
Defining function napi_get_frags as symbolic
Defining function napi_gro_frags as symbolic
Defining function __pskb_pull_tail as symbolic
Defining function netpoll_trap as symbolic
Defining function netdev_warn as symbolic
Defining function cancel_delayed_work_sync as symbolic
Defining function pskb_expand_head as symbolic
Defining function csum_ipv6_magic as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function printk as symbolic
Defining function skb_pad as symbolic
Defining function eth_validate_addr as symbolic
Removed calls to 'netif_device_detach' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Defining function dev_err as symbolic
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'pci_disable_msix' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Defining function del_timer_sync as symbolic
Removed calls to 'netif_device_attach' (function is undefined)
Defining function mod_timer as symbolic
Defining function request_threaded_irq as symbolic
Defining function sprintf as symbolic
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Defining function pci_enable_msix as symbolic
Defining function pci_enable_msi_block as symbolic
Defining function __bitmap_weight as symbolic
Removed calls to 'pci_restore_state' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Defining function pci_enable_device as symbolic
Defining function ethtool_op_get_link as symbolic
Defining function msleep_interruptible as symbolic
Defining function strlcpy as symbolic
Defining function snprintf as symbolic
Removed calls to '__raw_spin_lock_init' (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 '__init_waitqueue_head' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Defining function pci_set_power_state as symbolic
Defining function __pci_enable_wake as symbolic
Defining function pci_save_state as symbolic
Defining function pci_choose_state as symbolic
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to 'pci_release_regions' (function is undefined)
Defining function netif_get_num_default_rss_queues as symbolic
Defining function register_netdev as symbolic
Defining function ldv_pre_register_netdev as symbolic
Defining function pcie_set_readrq as symbolic
Defining function pci_request_regions as symbolic
Defining function ioremap_nocache as symbolic
Defining function __alloc_workqueue_key as symbolic
Removed calls to 'rtnl_lock' (function is undefined)
Removed calls to 'rtnl_unlock' (function is undefined)
Defining function _dev_info as symbolic
Defining function wait_for_completion_timeout as symbolic
Defining function dma_supported as symbolic
Defining function dma_set_mask as symbolic
Defining function alloc_etherdev_mqs as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_switch_to_interrupt_context' (function is undefined)
Removed calls to 'ldv_switch_to_process_context' (function is undefined)
Removed calls to 'ldv_pre_probe' (function is undefined)
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  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: 1.38462495804
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 531 478 2791 19091
INFO: Starting verification
KLEE: WARNING ONCE: function "qlge_isr" has inline asm
KLEE: WARNING ONCE: function "ql_disable_completion_interrupt" has inline asm
KLEE: WARNING ONCE: function "ql_queue_asic_error" has inline asm
KLEE: WARNING ONCE: function "ql_enable_completion_interrupt" has inline asm
KLEE: WARNING ONCE: function "ql_set_mac_addr" has inline asm
KLEE: WARNING ONCE: function "ql_set_mac_addr_reg" has inline asm
KLEE: WARNING ONCE: function "ql_wait_reg_rdy" has inline asm
KLEE: WARNING ONCE: function "ql_sem_trylock" has inline asm
KLEE: WARNING ONCE: function "qlge_change_mtu" has inline asm
KLEE: WARNING ONCE: function "ql_adapter_down" has inline asm
KLEE: WARNING ONCE: function "ql_adapter_up" has inline asm
KLEE: WARNING ONCE: function "ql_write_cfg" has inline asm
KLEE: WARNING ONCE: function "ql_cam_route_initialize" has inline asm
KLEE: WARNING ONCE: function "ql_update_buffer_queues" has inline asm
KLEE: WARNING ONCE: function "qlge_set_multicast_list" has inline asm
KLEE: WARNING ONCE: function "ql_adapter_reset" has inline asm
KLEE: WARNING ONCE: function "ql_clear_routing_entries" has inline asm
KLEE: WARNING ONCE: function "ql_wait_fifo_empty" has inline asm
KLEE: WARNING ONCE: function "ql_mailbox_command" has inline asm
KLEE: WARNING ONCE: function "ql_write_mpi_reg" has inline asm
KLEE: WARNING ONCE: function "ql_mpi_handler" has inline asm
KLEE: WARNING ONCE: function "ql_get_mb_sts" has inline asm
KLEE: WARNING ONCE: function "ql_read_mpi_reg" has inline asm
KLEE: WARNING ONCE: function "ql_set_routing_reg" has inline asm
KLEE: WARNING ONCE: function "pci_map_single" has inline asm
KLEE: WARNING ONCE: function "dma_map_page" has inline asm
KLEE: WARNING ONCE: function "ql_wait_cfg" has inline asm
KLEE: WARNING ONCE: function "pci_unmap_single" has inline asm
KLEE: WARNING ONCE: function "pci_unmap_page" has inline asm
KLEE: WARNING ONCE: function "qlge_set_features" has inline asm
KLEE: WARNING ONCE: function "qlge_set_mac_address" has inline asm
KLEE: WARNING ONCE: function "qlge_send" has inline asm
KLEE: WARNING ONCE: function "netif_tx_stop_queue" has inline asm
KLEE: WARNING ONCE: function "qlge_vlan_rx_add_vid" has inline asm
KLEE: WARNING ONCE: function "qlge_vlan_rx_kill_vid" has inline asm
KLEE: WARNING ONCE: function "qlge_io_error_detected" has inline asm
KLEE: WARNING ONCE: function "ql_eeh_close" has inline asm
KLEE: WARNING ONCE: function "ql_free_irq" has inline asm
KLEE: WARNING ONCE: function "pci_free_consistent" has inline asm
KLEE: WARNING ONCE: function "qlge_open" has inline asm
KLEE: WARNING ONCE: function "qlge_io_slot_reset" has inline asm
KLEE: WARNING ONCE: function "ql_get_8000_flash_params" has inline asm
KLEE: WARNING ONCE: function "ql_read_flash_word" has inline asm
KLEE: WARNING ONCE: function "ql_get_8012_flash_params" has inline asm
KLEE: WARNING ONCE: function "ql_8012_port_initialize" has inline asm
KLEE: WARNING ONCE: function "ql_read_xgmac_reg" has inline asm
KLEE: WARNING ONCE: function "ql_write_xgmac_reg" has inline asm
KLEE: WARNING ONCE: function "ql_self_test" has inline asm
KLEE: WARNING ONCE: function "ql_get_ethtool_stats" has inline asm
KLEE: WARNING ONCE: function "ql_clean_inbound_rx_ring" has inline asm
KLEE: WARNING ONCE: function "ql_check_lb_frame" has inline asm
KLEE: WARNING ONCE: function "ql_get_dump" has inline asm
KLEE: WARNING ONCE: function "ql_core_dump" has inline asm
KLEE: WARNING ONCE: function "ql_get_cam_entries" has inline asm
KLEE: WARNING ONCE: function "ql_get_routing_entries" has inline asm
KLEE: WARNING ONCE: function "ql_get_ets_regs" has inline asm
KLEE: WARNING ONCE: function "ql_get_routing_reg" has inline asm
KLEE: WARNING ONCE: function "ql_get_mac_addr_reg" has inline asm
KLEE: WARNING ONCE: function "ql_pause_mpi_risc" has inline asm
KLEE: WARNING ONCE: function "ql_read_serdes_reg" has inline asm
KLEE: WARNING ONCE: function "ql_get_probe" has inline asm
KLEE: WARNING ONCE: function "ql_hard_reset_mpi_risc" has inline asm
KLEE: WARNING ONCE: function "qlge_probe" has inline asm
KLEE: WARNING ONCE: function "qlge_close" has inline asm
KLEE: WARNING ONCE: function "ql_asic_reset_work" has inline asm
KLEE: WARNING ONCE: function "ql_mpi_reset_work" has inline asm
KLEE: WARNING ONCE: function "ql_mpi_work" has inline asm
KLEE: WARNING ONCE: function "ql_mpi_port_cfg_work" has inline asm
KLEE: WARNING ONCE: function "ql_mpi_idc_work" has inline asm
KLEE: WARNING ONCE: function "ql_timer" has inline asm
KLEE: WARNING ONCE: function "ql_sem_unlock" has inline asm
KLEE: WARNING ONCE: function "ql_own_firmware" has inline asm
KLEE: WARNING ONCE: function "ql_unpause_mpi_risc" has inline asm
KLEE: WARNING ONCE: function "ldv_dummy_resourceless_instance_callback_1_31" has inline asm
KLEE: WARNING ONCE: function "ldv_net_dummy_resourceless_instance_1" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_0d311831-efc2-4db6-9918-6300f430b0d9/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 16287 states (over memory cap)
KLEE: WARNING: killing 17279 states (over memory cap)
KLEE: WARNING: killing 17980 states (over memory cap)
KLEE: WARNING: killing 9674 states (over memory cap)
KLEE: WARNING: killing 18370 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-VfYcVt/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-ethernet-qlogic-qlge-qlge_true-unreach-call.cil.c:8695: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17922 states (over memory cap)
KLEE: WARNING: killing 16995 states (over memory cap)
KLEE: WARNING: killing 17986 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-VfYcVt/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-ethernet-qlogic-qlge-qlge_true-unreach-call.cil.c:8707: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17921 states (over memory cap)
KLEE: WARNING: killing 9584 states (over memory cap)
KLEE: WARNING: killing 18209 states (over memory cap)
KLEE: WARNING: killing 10290 states (over memory cap)
KLEE: WARNING: killing 9622 states (over memory cap)
KLEE: WARNING: killing 9420 states (over memory cap)
KLEE: WARNING: killing 9780 states (over memory cap)
KLEE: WARNING: killing 10324 states (over memory cap)
KLEE: WARNING: killing 9937 states (over memory cap)
KLEE: WARNING: killing 9647 states (over memory cap)
KLEE: WARNING: killing 10006 states (over memory cap)
KLEE: WARNING: killing 10179 states (over memory cap)
KLEE: WARNING: killing 10070 states (over memory cap)
KLEE: WARNING: killing 9506 states (over memory cap)
KLEE: WARNING: killing 9861 states (over memory cap)
KLEE: WARNING: killing 9480 states (over memory cap)
KLEE: WARNING: killing 9745 states (over memory cap)
KLEE: WARNING: killing 9362 states (over memory cap)
KLEE: WARNING: killing 9908 states (over memory cap)
KLEE: WARNING: killing 9525 states (over memory cap)
KLEE: WARNING: killing 9325 states (over memory cap)
KLEE: WARNING: killing 9773 states (over memory cap)
KLEE: WARNING: killing 9577 states (over memory cap)
KLEE: WARNING: killing 9385 states (over memory cap)
KLEE: WARNING: killing 9560 states (over memory cap)
KLEE: WARNING: killing 9731 states (over memory cap)
KLEE: WARNING: killing 9537 states (over memory cap)
KLEE: WARNING: killing 9526 states (over memory cap)
KLEE: WARNING: killing 9330 states (over memory cap)
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9230 states (over memory cap)
KLEE: WARNING: killing 9125 states (over memory cap)
KLEE: WARNING: killing 9659 states (over memory cap)
KLEE: WARNING: killing 9465 states (over memory cap)
KLEE: WARNING: killing 9182 states (over memory cap)
KLEE: WARNING: killing 9349 states (over memory cap)
KLEE: WARNING: killing 9065 states (over memory cap)
KLEE: WARNING: killing 9414 states (over memory cap)
KLEE: WARNING: killing 9586 states (over memory cap)
KLEE: WARNING: killing 9754 states (over memory cap)
KLEE: WARNING: killing 9203 states (over memory cap)
KLEE: WARNING: killing 9912 states (over memory cap)
KLEE: WARNING: killing 9185 states (over memory cap)
KLEE: WARNING: killing 9444 states (over memory cap)
KLEE: WARNING: killing 9077 states (over memory cap)
KLEE: WARNING: killing 9783 states (over memory cap)
KLEE: WARNING: killing 9324 states (over memory cap)
KLEE: WARNING: killing 9494 states (over memory cap)
KLEE: WARNING: killing 9391 states (over memory cap)
KLEE: WARNING: killing 9561 states (over memory cap)
KLEE: WARNING: killing 9281 states (over memory cap)
KLEE: WARNING: killing 9006 states (over memory cap)
KLEE: WARNING: killing 9352 states (over memory cap)
KLEE: WARNING: killing 9522 states (over memory cap)
KLEE: WARNING: killing 9688 states (over memory cap)
KLEE: WARNING: killing 9149 states (over memory cap)
KLEE: WARNING: killing 9402 states (over memory cap)
KLEE: WARNING: killing 9217 states (over memory cap)
KLEE: WARNING: killing 9646 states (over memory cap)
KLEE: WARNING: killing 9463 states (over memory cap)
KLEE: WARNING: killing 9986 states (over memory cap)
KLEE: WARNING: killing 9186 states (over memory cap)
KLEE: WARNING: killing 9348 states (over memory cap)
KLEE: WARNING: killing 9342 states (over memory cap)
KLEE: WARNING: killing 9333 states (over memory cap)
KLEE: WARNING: killing 9407 states (over memory cap)
KLEE: WARNING: killing 9397 states (over memory cap)
KLEE: WARNING: killing 9654 states (over memory cap)
KLEE: WARNING: killing 9469 states (over memory cap)
KLEE: WARNING: killing 9632 states (over memory cap)
KLEE: WARNING: killing 9539 states (over memory cap)
KLEE: WARNING: killing 9179 states (over memory cap)
KLEE: WARNING: killing 9342 states (over memory cap)
KLEE: WARNING: killing 9683 states (over memory cap)
KLEE: WARNING: killing 9587 states (over memory cap)
KLEE: WARNING: killing 9315 states (over memory cap)
KLEE: WARNING: killing 8871 states (over memory cap)
KLEE: WARNING: killing 9033 states (over memory cap)
KLEE: WARNING: killing 9284 states (over memory cap)
KLEE: WARNING: killing 9361 states (over memory cap)
KLEE: WARNING: killing 9265 states (over memory cap)
KLEE: WARNING: killing 9516 states (over memory cap)
KLEE: WARNING: killing 9680 states (over memory cap)
KLEE: WARNING: killing 8895 states (over memory cap)
KLEE: WARNING: killing 9659 states (over memory cap)
KLEE: WARNING: killing 9740 states (over memory cap)
KLEE: WARNING: killing 9391 states (over memory cap)
KLEE: WARNING: killing 9723 states (over memory cap)
KLEE: WARNING: killing 9372 states (over memory cap)
KLEE: WARNING: killing 9102 states (over memory cap)
KLEE: WARNING: killing 8921 states (over memory cap)
KLEE: WARNING: killing 9167 states (over memory cap)
KLEE: WARNING: killing 9160 states (over memory cap)
KLEE: WARNING: killing 9321 states (over memory cap)
KLEE: WARNING: killing 9397 states (over memory cap)
KLEE: WARNING: killing 9474 states (over memory cap)
KLEE: WARNING: killing 9383 states (over memory cap)
KLEE: WARNING: killing 9289 states (over memory cap)
KLEE: WARNING: killing 9367 states (over memory cap)
KLEE: WARNING: killing 9529 states (over memory cap)
KLEE: WARNING: killing 9517 states (over memory cap)
KLEE: WARNING: killing 9340 states (over memory cap)
KLEE: WARNING: killing 9592 states (over memory cap)
KLEE: WARNING: killing 8989 states (over memory cap)
KLEE: WARNING: killing 9909 states (over memory cap)
KLEE: WARNING: killing 9563 states (over memory cap)
KLEE: WARNING: killing 9638 states (over memory cap)
KLEE: WARNING: killing 9374 states (over memory cap)
KLEE: WARNING: killing 9366 states (over memory cap)
KLEE: WARNING: killing 9273 states (over memory cap)
KLEE: WARNING: killing 9267 states (over memory cap)
KLEE: WARNING: killing 9677 states (over memory cap)
KLEE: WARNING: killing 9419 states (over memory cap)
KLEE: WARNING: killing 9414 states (over memory cap)
KLEE: WARNING: killing 9405 states (over memory cap)
KLEE: WARNING: killing 9561 states (over memory cap)
KLEE: WARNING: killing 8798 states (over memory cap)
KLEE: WARNING: killing 9795 states (over memory cap)
KLEE: WARNING: killing 9451 states (over memory cap)
KLEE: WARNING: killing 9523 states (over memory cap)
KLEE: WARNING: killing 9519 states (over memory cap)
KLEE: WARNING: killing 9426 states (over memory cap)
KLEE: WARNING: killing 9584 states (over memory cap)
KLEE: WARNING: killing 9325 states (over memory cap)
KLEE: WARNING: killing 9565 states (over memory cap)
KLEE: WARNING: killing 9474 states (over memory cap)
KLEE: WARNING: killing 9137 states (over memory cap)
KLEE: WARNING: killing 9544 states (over memory cap)
KLEE: WARNING: killing 9455 states (over memory cap)
KLEE: WARNING: killing 9441 states (over memory cap)
KLEE: WARNING: killing 9519 states (over memory cap)
KLEE: WARNING: killing 9427 states (over memory cap)
KLEE: WARNING: killing 9254 states (over memory cap)
KLEE: WARNING: killing 8995 states (over memory cap)
KLEE: WARNING: killing 8578 states (over memory cap)
KLEE: WARNING: killing 9474 states (over memory cap)
KLEE: WARNING: killing 9220 states (over memory cap)
KLEE: WARNING: killing 9379 states (over memory cap)
KLEE: WARNING: killing 9448 states (over memory cap)
KLEE: WARNING: killing 9034 states (over memory cap)
KLEE: WARNING: killing 9593 states (over memory cap)
KLEE: WARNING: killing 9586 states (over memory cap)
KLEE: WARNING: killing 9495 states (over memory cap)
KLEE: WARNING: killing 9573 states (over memory cap)
KLEE: WARNING: killing 9562 states (over memory cap)
KLEE: WARNING: killing 9635 states (over memory cap)
KLEE: WARNING: killing 9302 states (over memory cap)
KLEE: WARNING: killing 9451 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-VfYcVt/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-ethernet-qlogic-qlge-qlge_true-unreach-call.cil.c:6887: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9442 states (over memory cap)
KLEE: WARNING: killing 9518 states (over memory cap)
KLEE: WARNING: killing 9674 states (over memory cap)
KLEE: WARNING: killing 9422 states (over memory cap)
KLEE: WARNING: killing 9497 states (over memory cap)
KLEE: WARNING: killing 9246 states (over memory cap)
KLEE: WARNING: killing 9313 states (over memory cap)
KLEE: WARNING: killing 9225 states (over memory cap)
KLEE: WARNING: killing 9946 states (over memory cap)
KLEE: WARNING: killing 9453 states (over memory cap)
KLEE: WARNING: killing 9282 states (over memory cap)
KLEE: WARNING: killing 9035 states (over memory cap)
KLEE: WARNING: killing 9344 states (over memory cap)
KLEE: WARNING: killing 9259 states (over memory cap)
KLEE: WARNING: killing 9246 states (over memory cap)
KLEE: WARNING: killing 9480 states (over memory cap)
KLEE: WARNING: killing 9472 states (over memory cap)
KLEE: WARNING: killing 9626 states (over memory cap)
KLEE: WARNING: killing 9058 states (over memory cap)
KLEE: WARNING: killing 9529 states (over memory cap)
KLEE: WARNING: killing 9359 states (over memory cap)
KLEE: WARNING: killing 9435 states (over memory cap)
KLEE: WARNING: killing 9746 states (over memory cap)
KLEE: WARNING: killing 9340 states (over memory cap)
KLEE: WARNING: killing 9333 states (over memory cap)
KLEE: WARNING: killing 9483 states (over memory cap)
KLEE: WARNING: killing 9314 states (over memory cap)
KLEE: WARNING: killing 9229 states (over memory cap)
KLEE: WARNING: killing 9222 states (over memory cap)
KLEE: WARNING: killing 9208 states (over memory cap)
