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--mthca--ib_mthca.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.: 368 610 5768 50971
Removed infinite loop in mthca_cmd_wait
Removed infinite loop in sg_page
Removed infinite loop in dma_unmap_sg_attrs
Removed infinite loop in dma_unmap_page
Removed infinite loop in mthca_multicast_attach
Removed infinite loop in mthca_multicast_detach
Removed infinite loop in mthca_process_mad
Removed infinite loop in dma_sync_single_for_cpu
Removed infinite loop in dma_sync_single_for_device
Removed infinite loop in mthca_fmr_alloc
Removed infinite loop in mthca_alloc_icm
Removed infinite loop in mthca_alloc_icm_coherent
Removed infinite loop in dma_map_sg_attrs
Removed infinite loop in sg_assign_page
Removed infinite loop in sg_set_buf
Removed infinite loop in mthca_arbel_write_mtt_seg
Removed infinite loop in dma_map_page
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 1.47818493843
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'ib_unregister_device' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'pci_disable_msix' (function is undefined)
Removed calls to 'ib_dealloc_device' (function is undefined)
Removed calls to 'pci_release_regions' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'dma_pool_destroy' (function is undefined)
Removed calls to 'down' (function is undefined)
Removed calls to 'up' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'dev_printk' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Defining function wait_for_completion_timeout as symbolic
Removed calls to 'debug_dma_unmap_sg' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Removed calls to 'dev_warn' (function is undefined)
Defining function find_first_bit as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'free_irq' (function is undefined)
Defining function printk as symbolic
Removed calls to 'dma_pool_free' (function is undefined)
Defining function dma_pool_alloc as symbolic
Removed calls to 'free_pages' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function ib_unregister_mad_agent as symbolic
Defining function ib_destroy_ah as symbolic
Removed calls to 'dev_err' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Defining function pci_enable_device as symbolic
Defining function pci_request_regions as symbolic
Defining function ib_alloc_device as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to 'pci_dev_put' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'ib_free_send_mad' (function is undefined)
Defining function ib_register_mad_agent as symbolic
Defining function ib_query_port as symbolic
Defining function strlcpy as symbolic
Removed calls to 'ib_umem_release' (function is undefined)
Removed calls to 'ib_dispatch_event' (function is undefined)
Defining function ib_register_device as symbolic
Defining function device_create_file as symbolic
Removed calls to 'add_timer' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function round_jiffies as symbolic
Defining function mod_timer as symbolic
Defining function queue_work_on as symbolic
Defining function ioremap_nocache as symbolic
Removed calls to 'ib_ud_header_init' (function is undefined)
Defining function ib_get_cached_pkey as symbolic
Defining function ib_ud_header_pack as symbolic
Defining function ib_get_cached_gid as symbolic
Defining function ib_create_ah as symbolic
Defining function ib_create_send_mad as symbolic
Defining function ib_post_send_mad as symbolic
Defining function find_next_zero_bit as symbolic
Defining function find_first_zero_bit as symbolic
Removed calls to 'debug_dma_sync_single_for_cpu' (function is undefined)
Removed calls to 'debug_dma_sync_single_for_device' (function is undefined)
Removed calls to 'sg_init_table' (function is undefined)
Removed calls to 'debug_dma_map_sg' (function is undefined)
Defining function sg_next as symbolic
Defining function alloc_pages_current as symbolic
Defining function dma_alloc_attrs as symbolic
Defining function __virt_addr_valid as symbolic
Defining function __phys_addr as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function ib_umem_get as symbolic
Defining function __get_free_pages as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function _copy_from_user as symbolic
Removed calls to 'synchronize_irq' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Removed calls to 'clear_page' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function get_zeroed_page as symbolic
Defining function get_user_pages as symbolic
Removed calls to '_raw_spin_lock_nested' (function is undefined)
Defining function mult_to_ib_rate as symbolic
Defining function ib_modify_qp_is_ok as symbolic
Defining function ib_rate_to_mult as symbolic
Defining function remap_pfn_range as symbolic
Defining function mutex_lock_interruptible_nested as symbolic
Defining function dma_pool_create as symbolic
Defining function __msecs_to_jiffies as symbolic
Removed calls to 'lockdep_init_map' (function is undefined)
Defining function snprintf as symbolic
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function request_threaded_irq as symbolic
Defining function pci_enable_msix_range as symbolic
Removed calls to '_dev_info' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Defining function pci_find_capability as symbolic
Defining function pci_get_device as symbolic
Defining function pcie_capability_write_word as symbolic
Defining function pci_bus_write_config_dword as symbolic
Defining function pci_bus_read_config_dword as symbolic
Defining function dma_supported as symbolic
Defining function dma_set_mask as symbolic
Defining function sprintf as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Defining function ldv_shutdown_7 as symbolic
Removed calls to '__init_work' (function is undefined)
Defining function __pci_register_driver as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
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: 1.4976439476
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 346 466 3202 28563
INFO: Starting verification
KLEE: WARNING ONCE: function "mthca_free" has inline asm
KLEE: WARNING ONCE: function "mthca_free_icm" has inline asm
KLEE: WARNING ONCE: function "pci_unmap_sg" has inline asm
KLEE: WARNING ONCE: function "sg_page" has inline asm
KLEE: WARNING ONCE: function "mthca_buddy_free" has inline asm
KLEE: WARNING ONCE: function "mthca_cmd_wait" has inline asm
KLEE: WARNING ONCE: function "mthca_cmd_poll" has inline asm
KLEE: WARNING ONCE: function "mthca_cmd_post" has inline asm
KLEE: WARNING ONCE: function "mthca_reset" has inline asm
KLEE: WARNING ONCE: function "mthca_alloc_icm" has inline asm
KLEE: WARNING ONCE: function "mthca_map_cmd" has inline asm
KLEE: WARNING ONCE: function "mthca_make_profile" has inline asm
KLEE: WARNING ONCE: function "mthca_query_device" has inline asm
KLEE: WARNING ONCE: function "mthca_arbel_post_srq_recv" has inline asm
KLEE: WARNING ONCE: function "mthca_tavor_post_srq_recv" has inline asm
KLEE: WARNING ONCE: function "mthca_modify_qp" has inline asm
KLEE: WARNING ONCE: function "mthca_resize_cq" has inline asm
KLEE: WARNING ONCE: function "mthca_poll_cq" has inline asm
KLEE: WARNING ONCE: function "mthca_reg_phys_mr" has inline asm
KLEE: WARNING ONCE: function "mthca_reg_user_mr" has inline asm
KLEE: WARNING ONCE: function "mthca_unmap_fmr" has inline asm
KLEE: WARNING ONCE: function "mthca_arbel_map_phys_fmr" has inline asm
KLEE: WARNING ONCE: function "mthca_tavor_map_phys_fmr" has inline asm
KLEE: WARNING ONCE: function "mthca_multicast_attach" has inline asm
KLEE: WARNING ONCE: function "mthca_multicast_detach" has inline asm
KLEE: WARNING ONCE: function "mthca_process_mad" has inline asm
KLEE: WARNING ONCE: function "mthca_tavor_arm_cq" has inline asm
KLEE: WARNING ONCE: function "mthca_arbel_arm_cq" has inline asm
KLEE: WARNING ONCE: function "mthca_tavor_post_send" has inline asm
KLEE: WARNING ONCE: function "mthca_arbel_post_send" has inline asm
KLEE: WARNING ONCE: function "mthca_tavor_post_receive" has inline asm
KLEE: WARNING ONCE: function "mthca_arbel_post_receive" has inline asm
KLEE: WARNING ONCE: function "poll_catas" has inline asm
KLEE: WARNING ONCE: function "mthca_alloc" has inline asm
KLEE: WARNING ONCE: function "mthca_fmr_alloc" has inline asm
KLEE: WARNING ONCE: function "mthca_buddy_alloc" has inline asm
KLEE: WARNING ONCE: function "mthca_write_mtt" has inline asm
KLEE: WARNING ONCE: function "update_cons_index" has inline asm
KLEE: WARNING ONCE: function "mthca_free_db" has inline asm
KLEE: WARNING ONCE: function "mthca_buf_alloc" has inline asm
KLEE: WARNING ONCE: function "mthca_map_user_db" has inline asm
KLEE: WARNING ONCE: function "mthca_init_cq" has inline asm
KLEE: WARNING ONCE: function "mthca_alloc_db" has inline asm
KLEE: WARNING ONCE: function "sg_set_page" has inline asm
KLEE: WARNING ONCE: function "pci_map_sg" has inline asm
KLEE: WARNING ONCE: function "mthca_free_qp" has inline asm
KLEE: WARNING ONCE: function "mthca_cq_clean" has inline asm
KLEE: WARNING ONCE: function "mthca_alloc_sqp" has inline asm
KLEE: WARNING ONCE: function "mthca_set_qp_size" has inline asm
KLEE: WARNING ONCE: function "mthca_alloc_srq" has inline asm
KLEE: WARNING ONCE: function "mthca_alloc_init" has inline asm
KLEE: WARNING ONCE: function "mthca_init_mr_table" has inline asm
KLEE: WARNING ONCE: function "mthca_init_eq_table" has inline asm
KLEE: WARNING ONCE: function "mthca_create_eq" has inline asm
KLEE: WARNING ONCE: function "mthca_arbel_msi_x_interrupt" has inline asm
KLEE: WARNING ONCE: function "mthca_tavor_msi_x_interrupt" has inline asm
KLEE: WARNING ONCE: function "mthca_arbel_interrupt" has inline asm
KLEE: WARNING ONCE: function "mthca_tavor_interrupt" has inline asm
KLEE: WARNING ONCE: function "mthca_eq_int" has inline asm
KLEE: WARNING ONCE: function "mthca_buddy_init" has inline asm
KLEE: WARNING ONCE: function "mthca_max_srq_sge" has inline asm
KLEE: WARNING ONCE: function "mthca_tavor_fmr_unmap" has inline asm
KLEE: WARNING ONCE: function "__mthca_check_profile_val" 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_ffcc42bd-e6e7-4e14-a678-ee973fb14181/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-tW2ax6/linux-4.2-rc1.tar.xz-08_1a-drivers--infiniband--hw--mthca--ib_mthca.ko-entry_point_true-unreach-call.cil.out.c:4781: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 6969 states (over memory cap)
KLEE: WARNING: killing 12029 states (over memory cap)
KLEE: WARNING: killing 11603 states (over memory cap)
KLEE: WARNING: killing 11570 states (over memory cap)
KLEE: WARNING: killing 11863 states (over memory cap)
KLEE: WARNING: killing 12029 states (over memory cap)
KLEE: WARNING: killing 11552 states (over memory cap)
KLEE: WARNING: killing 11071 states (over memory cap)
KLEE: WARNING: killing 12078 states (over memory cap)
KLEE: WARNING: killing 11216 states (over memory cap)
KLEE: WARNING: killing 12213 states (over memory cap)
KLEE: WARNING: killing 12259 states (over memory cap)
KLEE: WARNING: killing 12744 states (over memory cap)
KLEE: WARNING: killing 12792 states (over memory cap)
KLEE: WARNING: killing 12515 states (over memory cap)
KLEE: WARNING: killing 13005 states (over memory cap)
KLEE: WARNING: killing 12479 states (over memory cap)
KLEE: WARNING: killing 12397 states (over memory cap)
KLEE: WARNING: killing 12699 states (over memory cap)
KLEE: WARNING: killing 12678 states (over memory cap)
KLEE: WARNING: killing 12283 states (over memory cap)
KLEE: WARNING: killing 12519 states (over memory cap)
KLEE: WARNING: killing 12375 states (over memory cap)
KLEE: WARNING: killing 12294 states (over memory cap)
KLEE: WARNING: killing 11833 states (over memory cap)
KLEE: WARNING: killing 12195 states (over memory cap)
KLEE: WARNING: killing 12365 states (over memory cap)
KLEE: WARNING: killing 11973 states (over memory cap)
KLEE: WARNING: killing 11955 states (over memory cap)
KLEE: WARNING: killing 12436 states (over memory cap)
KLEE: WARNING: killing 12166 states (over memory cap)
KLEE: WARNING: killing 12336 states (over memory cap)
KLEE: WARNING: killing 12507 states (over memory cap)
KLEE: WARNING: killing 11929 states (over memory cap)
KLEE: WARNING: killing 12472 states (over memory cap)
KLEE: WARNING: killing 12021 states (over memory cap)
KLEE: WARNING: killing 12631 states (over memory cap)
KLEE: WARNING: killing 11932 states (over memory cap)
KLEE: WARNING: killing 12470 states (over memory cap)
KLEE: WARNING: killing 12087 states (over memory cap)
KLEE: WARNING: killing 12009 states (over memory cap)
KLEE: WARNING: killing 12179 states (over memory cap)
KLEE: WARNING: killing 12159 states (over memory cap)
KLEE: WARNING: killing 12390 states (over memory cap)
KLEE: WARNING: killing 12193 states (over memory cap)
KLEE: WARNING: killing 12482 states (over memory cap)
KLEE: WARNING: killing 12348 states (over memory cap)
KLEE: WARNING: killing 12577 states (over memory cap)
KLEE: WARNING: killing 12383 states (over memory cap)
KLEE: WARNING: killing 12246 states (over memory cap)
KLEE: WARNING: killing 12168 states (over memory cap)
KLEE: WARNING: killing 11728 states (over memory cap)
KLEE: WARNING: killing 12013 states (over memory cap)
KLEE: WARNING: killing 12726 states (over memory cap)
KLEE: WARNING: killing 12658 states (over memory cap)
KLEE: WARNING: killing 12162 states (over memory cap)
KLEE: WARNING: killing 12450 states (over memory cap)
KLEE: WARNING: killing 11826 states (over memory cap)
KLEE: WARNING: killing 12297 states (over memory cap)
KLEE: WARNING: killing 12042 states (over memory cap)
KLEE: WARNING: killing 12628 states (over memory cap)
KLEE: WARNING: killing 12560 states (over memory cap)
KLEE: WARNING: killing 12251 states (over memory cap)
KLEE: WARNING: killing 12113 states (over memory cap)
KLEE: WARNING: killing 12579 states (over memory cap)
KLEE: WARNING: killing 12210 states (over memory cap)
KLEE: WARNING: killing 12254 states (over memory cap)
KLEE: WARNING: killing 11761 states (over memory cap)
KLEE: WARNING: killing 12105 states (over memory cap)
KLEE: WARNING: killing 12273 states (over memory cap)
KLEE: WARNING: killing 12317 states (over memory cap)
KLEE: WARNING: killing 12126 states (over memory cap)
KLEE: WARNING: killing 11995 states (over memory cap)
KLEE: WARNING: killing 11801 states (over memory cap)
KLEE: WARNING: killing 12445 states (over memory cap)
KLEE: WARNING: killing 12727 states (over memory cap)
KLEE: WARNING: killing 12126 states (over memory cap)
KLEE: WARNING: killing 12647 states (over memory cap)
KLEE: WARNING: killing 11749 states (over memory cap)
KLEE: WARNING: killing 12205 states (over memory cap)
KLEE: WARNING: killing 12315 states (over memory cap)
KLEE: WARNING: killing 12593 states (over memory cap)
KLEE: WARNING: killing 12114 states (over memory cap)
KLEE: WARNING: killing 12279 states (over memory cap)
KLEE: WARNING: killing 11971 states (over memory cap)
KLEE: WARNING: killing 12607 states (over memory cap)
KLEE: WARNING: killing 12127 states (over memory cap)
KLEE: WARNING: killing 12638 states (over memory cap)
KLEE: WARNING: killing 12220 states (over memory cap)
KLEE: WARNING: killing 12091 states (over memory cap)
KLEE: WARNING: killing 11905 states (over memory cap)
KLEE: WARNING: killing 12416 states (over memory cap)
KLEE: WARNING: killing 11880 states (over memory cap)
KLEE: WARNING: killing 12042 states (over memory cap)
KLEE: WARNING: killing 12493 states (over memory cap)
KLEE: WARNING: killing 12539 states (over memory cap)
KLEE: WARNING: killing 12239 states (over memory cap)
KLEE: WARNING: killing 12347 states (over memory cap)
KLEE: WARNING: killing 11927 states (over memory cap)
KLEE: WARNING: killing 12605 states (over memory cap)
KLEE: WARNING: killing 12480 states (over memory cap)
KLEE: WARNING: killing 12242 states (over memory cap)
KLEE: WARNING: killing 12169 states (over memory cap)
KLEE: WARNING: killing 12161 states (over memory cap)
KLEE: WARNING: killing 12437 states (over memory cap)
KLEE: WARNING: killing 12423 states (over memory cap)
KLEE: WARNING: killing 11777 states (over memory cap)
KLEE: WARNING: killing 12226 states (over memory cap)
KLEE: WARNING: killing 12220 states (over memory cap)
KLEE: WARNING: killing 12030 states (over memory cap)
KLEE: WARNING: killing 12481 states (over memory cap)
KLEE: WARNING: killing 11841 states (over memory cap)
KLEE: WARNING: killing 12175 states (over memory cap)
KLEE: WARNING: killing 12102 states (over memory cap)
KLEE: WARNING: killing 12609 states (over memory cap)
KLEE: WARNING: killing 12600 states (over memory cap)
KLEE: WARNING: killing 12017 states (over memory cap)
KLEE: WARNING: killing 12010 states (over memory cap)
KLEE: WARNING: killing 11998 states (over memory cap)
KLEE: WARNING: killing 12153 states (over memory cap)
KLEE: WARNING: killing 12252 states (over memory cap)
KLEE: WARNING: killing 12412 states (over memory cap)
KLEE: WARNING: killing 12347 states (over memory cap)
KLEE: WARNING: killing 12166 states (over memory cap)
KLEE: WARNING: killing 12267 states (over memory cap)
KLEE: WARNING: killing 12536 states (over memory cap)
KLEE: WARNING: killing 12130 states (over memory cap)
KLEE: WARNING: killing 12230 states (over memory cap)
KLEE: WARNING: killing 12560 states (over memory cap)
KLEE: WARNING: killing 12273 states (over memory cap)
KLEE: WARNING: killing 11979 states (over memory cap)
KLEE: WARNING: killing 12243 states (over memory cap)
KLEE: WARNING: killing 12232 states (over memory cap)
KLEE: WARNING: killing 12387 states (over memory cap)
KLEE: WARNING: killing 12323 states (over memory cap)
KLEE: WARNING: killing 12874 states (over memory cap)
KLEE: WARNING: killing 11847 states (over memory cap)
KLEE: WARNING: killing 12064 states (over memory cap)
KLEE: WARNING: killing 11995 states (over memory cap)
KLEE: WARNING: killing 12041 states (over memory cap)
KLEE: WARNING: killing 11860 states (over memory cap)
KLEE: WARNING: killing 12577 states (over memory cap)
KLEE: WARNING: killing 12064 states (over memory cap)
KLEE: WARNING: killing 12269 states (over memory cap)
KLEE: WARNING: killing 12260 states (over memory cap)
KLEE: WARNING: killing 12469 states (over memory cap)
KLEE: WARNING: killing 12236 states (over memory cap)
KLEE: WARNING: killing 12056 states (over memory cap)
KLEE: WARNING: killing 12433 states (over memory cap)
KLEE: WARNING: killing 12537 states (over memory cap)
KLEE: WARNING: killing 11970 states (over memory cap)
KLEE: WARNING: killing 12235 states (over memory cap)
KLEE: WARNING: killing 12334 states (over memory cap)
KLEE: WARNING: killing 12381 states (over memory cap)
KLEE: WARNING: killing 12370 states (over memory cap)
KLEE: WARNING: killing 12305 states (over memory cap)
KLEE: WARNING: killing 11517 states (over memory cap)
KLEE: WARNING: killing 12607 states (over memory cap)
KLEE: WARNING: killing 12209 states (over memory cap)
KLEE: WARNING: killing 12471 states (over memory cap)
KLEE: WARNING: killing 11970 states (over memory cap)
KLEE: WARNING: killing 12286 states (over memory cap)
KLEE: WARNING: killing 12443 states (over memory cap)
KLEE: WARNING: killing 12316 states (over memory cap)
KLEE: WARNING: killing 12093 states (over memory cap)
KLEE: WARNING: killing 12024 states (over memory cap)
KLEE: WARNING: killing 12231 states (over memory cap)
KLEE: WARNING: killing 12278 states (over memory cap)
KLEE: WARNING: killing 12106 states (over memory cap)
KLEE: WARNING: killing 12475 states (over memory cap)
KLEE: WARNING: killing 12244 states (over memory cap)
KLEE: WARNING: killing 12347 states (over memory cap)
KLEE: WARNING: killing 12448 states (over memory cap)
KLEE: WARNING: killing 12542 states (over memory cap)
KLEE: WARNING: killing 11937 states (over memory cap)
KLEE: WARNING: killing 12250 states (over memory cap)
KLEE: WARNING: killing 12242 states (over memory cap)
KLEE: WARNING: killing 12178 states (over memory cap)
