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-32_7a-drivers--block--rbd.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.: 464 356 3403 21173
Removed infinite loop in rbd_release
Removed infinite loop in rbd_queue_workfn
Removed infinite loop in rbd_img_request_fill
Removed infinite loop in rbd_img_request_put
Removed infinite loop in rbd_img_request_destroy
Removed infinite loop in rbd_img_obj_request_del
Removed infinite loop in rbd_dev_remove_parent
Removed infinite loop in rbd_obj_request_put
Removed infinite loop in rbd_obj_request_destroy
Removed infinite loop in img_obj_request_simple
Removed infinite loop in rbd_img_obj_parent_read_full
Removed infinite loop in rbd_img_obj_exists_submit
Removed infinite loop in rbd_obj_request_create
Removed infinite loop in rbd_osd_req_create
Removed infinite loop in rbd_img_obj_exists_callback
Removed infinite loop in rbd_osd_req_format_read
Removed infinite loop in rbd_osd_req_callback
Removed infinite loop in rbd_img_parent_read
Removed infinite loop in rbd_img_obj_request_read_callback
Removed infinite loop in zero_pages
Removed infinite loop in arch_local_irq_restore
Removed infinite loop in arch_local_save_flags
Removed infinite loop in arch_local_irq_disable
Removed infinite loop in rbd_parent_request_create
Removed infinite loop in rbd_img_parent_read_callback
Removed infinite loop in rbd_img_obj_parent_read_full_callback
Removed infinite loop in rbd_osd_req_create_copyup
Removed infinite loop in rbd_img_obj_copyup_callback
Removed infinite loop in rbd_img_obj_callback
Removed infinite loop in rbd_img_obj_end_request
Removed infinite loop in rbd_osd_req_format_write
Removed infinite loop in rbd_segment_length
Removed infinite loop in rbd_img_obj_request_add
Removed infinite loop in rbd_dev_header_unwatch_sync
Removed infinite loop in rbd_snap_size
Removed infinite loop in rbd_snap_features
Removed infinite loop in rbd_obj_method_sync
Removed infinite loop in rbd_merge_bvec
Removed infinite loop in rbd_dev_header_name
Removed infinite loop in rbd_dev_header_watch_sync
Removed infinite loop in rbd_dev_header_info
Removed infinite loop in rbd_spec_fill_snap_id
Removed infinite loop in rbd_spec_fill_names
Removed infinite loop in rbd_dev_image_name
Removed infinite loop in rbd_snap_name
Removed infinite loop in _rbd_dev_v1_snap_name
Removed infinite loop in ceph_encode_string
Removed infinite loop in rbd_obj_read_sync
Removed infinite loop in ldv_stop
Removed infinite loop in rbd_slab_init
Removed infinite loop in rbd_slab_exit
INFO: Compilation, preparation and instrumentation time: 0.836400032043
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'put_device' (function is undefined)
Removed calls to '__might_fault' (function is undefined)
Removed calls to 'set_disk_ro' (function is undefined)
Defining function printk as symbolic
Defining function get_device as symbolic
Defining function blk_mq_map_queue as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'blk_mq_start_request' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to 'ceph_put_snap_context' (function is undefined)
Removed calls to 'blk_mq_end_request' (function is undefined)
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Defining function ceph_get_snap_context as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'kmem_cache_free' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'bio_advance' (function is undefined)
Removed calls to 'bio_put' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'ceph_destroy_client' (function is undefined)
Removed calls to 'ceph_osdc_put_request' (function is undefined)
Removed calls to 'ceph_release_page_vector' (function is undefined)
Removed calls to 'osd_req_op_init' (function is undefined)
Removed calls to 'osd_req_op_raw_data_in_pages' (function is undefined)
Defining function ceph_alloc_page_vector as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'ceph_osdc_build_request' (function is undefined)
Removed calls to 'complete_all' (function is undefined)
Defining function ceph_osdc_alloc_request as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function kmem_cache_alloc as symbolic
Removed calls to 'osd_req_op_cls_init' (function is undefined)
Removed calls to 'osd_req_op_cls_request_data_pages' (function is undefined)
Removed calls to 'osd_req_op_alloc_hint_init' (function is undefined)
Removed calls to 'osd_req_op_extent_init' (function is undefined)
Removed calls to 'osd_req_op_extent_osd_data_bio' (function is undefined)
Removed calls to 'osd_req_op_extent_osd_data_pages' (function is undefined)
Removed calls to '__blk_mq_end_request' (function is undefined)
Defining function blk_update_request as symbolic
Defining function current_kernel_time as symbolic
Defining function ceph_osdc_start_request as symbolic
Defining function bio_clone_bioset as symbolic
Defining function snprintf as symbolic
Defining function queue_work_on as symbolic
Removed calls to 'ceph_destroy_options' (function is undefined)
Removed calls to 'ceph_monc_request_next_osdmap' (function is undefined)
Removed calls to 'put_disk' (function is undefined)
Removed calls to 'blk_queue_max_hw_sectors' (function is undefined)
Removed calls to 'blk_queue_max_segments' (function is undefined)
Removed calls to 'blk_queue_max_segment_size' (function is undefined)
Removed calls to 'blk_queue_io_min' (function is undefined)
Removed calls to 'blk_queue_io_opt' (function is undefined)
Removed calls to 'blk_queue_merge_bvec' (function is undefined)
Removed calls to 'blk_mq_free_tag_set' (function is undefined)
Removed calls to 'unregister_blkdev' (function is undefined)
Removed calls to 'add_disk' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Defining function try_module_get as symbolic
Removed calls to '__init_rwsem' (function is undefined)
Removed calls to 'ceph_osdc_cancel_event' (function is undefined)
Removed calls to 'ceph_osdc_cancel_request' (function is undefined)
Removed calls to 'osd_req_op_watch_init' (function is undefined)
Removed calls to 'ceph_osdc_set_request_linger' (function is undefined)
Defining function wait_for_completion_interruptible_timeout as symbolic
Defining function sprintf as symbolic
Defining function register_blkdev as symbolic
Removed calls to 'del_gendisk' (function is undefined)
Removed calls to 'blk_cleanup_queue' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'ida_simple_remove' (function is undefined)
Defining function dev_set_name as symbolic
Defining function device_register as symbolic
Removed calls to 'osd_req_op_cls_request_data_pagelist' (function is undefined)
Removed calls to 'osd_req_op_cls_response_data_pages' (function is undefined)
Removed calls to 'ceph_copy_from_page_vector' (function is undefined)
Defining function ceph_pagelist_append as symbolic
Defining function bsearch as symbolic
Defining function alloc_disk as symbolic
Defining function blk_mq_alloc_tag_set as symbolic
Defining function blk_mq_init_queue as symbolic
Defining function ida_simple_get as symbolic
Defining function ceph_pg_pool_name_by_id as symbolic
Defining function kstrdup as symbolic
Defining function ceph_create_snap_context as symbolic
Defining function strnlen as symbolic
Defining function ceph_osdc_create_event as symbolic
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Defining function revalidate_disk as symbolic
Defining function ceph_pg_poolid_by_name as symbolic
Defining function ceph_monc_do_get_version as symbolic
Defining function ceph_monc_wait_osdmap as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function ceph_create_client as symbolic
Defining function ceph_open_session as symbolic
Defining function ceph_compare_options as symbolic
Defining function kmemdup as symbolic
Defining function ceph_parse_options as symbolic
Defining function match_token as symbolic
Defining function match_int as symbolic
Removed calls to 'ceph_osdc_flush_notifies' (function is undefined)
Removed calls to 'device_unregister' (function is undefined)
Defining function kstrtoull as symbolic
Defining function ceph_client_id as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ida_destroy' (function is undefined)
Removed calls to 'bus_unregister' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Defining function ldv_probe_17 as symbolic
Defining function ldv_probe_2 as symbolic
Defining function libceph_compatible as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function bus_register as symbolic
Defining function kmem_cache_create as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strcspn
  strlen
  strspn
  __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: 0.798480033875
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 502 235 1703 10935
INFO: Starting verification
KLEE: WARNING ONCE: function "rbd_release" has inline asm
KLEE: WARNING ONCE: function "rbd_ioctl" has inline asm
KLEE: WARNING ONCE: function "rbd_queue_workfn" has inline asm
KLEE: WARNING ONCE: function "rbd_img_request_create" has inline asm
KLEE: WARNING ONCE: function "rbd_img_request_fill" has inline asm
KLEE: WARNING ONCE: function "rbd_img_request_put" has inline asm
KLEE: WARNING ONCE: function "rbd_obj_request_put" has inline asm
KLEE: WARNING ONCE: function "rbd_img_request_destroy" has inline asm
KLEE: WARNING ONCE: function "rbd_img_obj_request_del" has inline asm
KLEE: WARNING ONCE: function "rbd_dev_parent_put" has inline asm
KLEE: WARNING ONCE: function "rbd_dev_unparent" has inline asm
KLEE: WARNING ONCE: function "rbd_dev_destroy" has inline asm
KLEE: WARNING ONCE: function "rbd_img_obj_request_submit" has inline asm
KLEE: WARNING ONCE: function "rbd_parent_request_create" has inline asm
KLEE: WARNING ONCE: function "rbd_img_obj_parent_read_full_callback" has inline asm
KLEE: WARNING ONCE: function "obj_request_done_set" has inline asm
KLEE: WARNING ONCE: function "rbd_obj_request_create" has inline asm
KLEE: WARNING ONCE: function "kref_get" has inline asm
KLEE: WARNING ONCE: function "rbd_osd_req_create" has inline asm
KLEE: WARNING ONCE: function "rbd_img_obj_exists_callback" has inline asm
KLEE: WARNING ONCE: function "rbd_osd_req_format_read" has inline asm
KLEE: WARNING ONCE: function "rbd_osd_req_callback" has inline asm
KLEE: WARNING ONCE: function "rbd_img_parent_read_callback" has inline asm
KLEE: WARNING ONCE: function "rbd_img_obj_request_read_callback" has inline asm
KLEE: WARNING ONCE: function "zero_pages" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "rbd_img_obj_request_fill" has inline asm
KLEE: WARNING ONCE: function "rbd_img_obj_copyup_callback" has inline asm
KLEE: WARNING ONCE: function "rbd_img_obj_callback" has inline asm
KLEE: WARNING ONCE: function "rbd_osd_req_format_write" has inline asm
KLEE: WARNING ONCE: function "do_rbd_add" has inline asm
KLEE: WARNING ONCE: function "rbd_dev_image_probe" has inline asm
KLEE: WARNING ONCE: function "rbd_dev_device_release" has inline asm
KLEE: WARNING ONCE: function "rbd_dev_header_unwatch_sync" has inline asm
KLEE: WARNING ONCE: function "rbd_obj_method_sync" has inline asm
KLEE: WARNING ONCE: function "rbd_dev_header_info" has inline asm
KLEE: WARNING ONCE: function "rbd_dev_v2_parent_info" has inline asm
KLEE: WARNING ONCE: function "rbd_dev_refresh" has inline asm
KLEE: WARNING ONCE: function "do_rbd_remove" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "rbd_slab_exit" 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_e630b85b-b7f0-4813-8577-abfc3af73931/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-HSThha/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rbd.ko-entry_point_true-unreach-call.cil.out.c:12345: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-HSThha/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rbd.ko-entry_point_true-unreach-call.cil.out.c:12505: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-HSThha/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rbd.ko-entry_point_true-unreach-call.cil.out.c:12359: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-HSThha/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rbd.ko-entry_point_true-unreach-call.cil.out.c:12200: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-HSThha/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rbd.ko-entry_point_true-unreach-call.cil.out.c:12438: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-HSThha/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rbd.ko-entry_point_true-unreach-call.cil.out.c:12394: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-HSThha/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rbd.ko-entry_point_true-unreach-call.cil.out.c:12453: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-HSThha/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rbd.ko-entry_point_true-unreach-call.cil.out.c:12473: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-HSThha/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rbd.ko-entry_point_true-unreach-call.cil.out.c:12409: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-HSThha/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rbd.ko-entry_point_true-unreach-call.cil.out.c:12374: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-HSThha/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rbd.ko-entry_point_true-unreach-call.cil.out.c:6553: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-HSThha/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rbd.ko-entry_point_true-unreach-call.cil.out.c:12487: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-HSThha/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rbd.ko-entry_point_true-unreach-call.cil.out.c:12424: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 24257 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 25704 states (over memory cap)
KLEE: WARNING: killing 23270 states (over memory cap)
KLEE: WARNING: killing 24345 states (over memory cap)
KLEE: WARNING: killing 23609 states (over memory cap)
KLEE: WARNING: killing 23950 states (over memory cap)
KLEE: WARNING: killing 24236 states (over memory cap)
KLEE: WARNING: killing 24247 states (over memory cap)
KLEE: WARNING: killing 24864 states (over memory cap)
KLEE: WARNING: killing 25276 states (over memory cap)
KLEE: WARNING: killing 28518 states (over memory cap)
KLEE: WARNING: killing 27538 states (over memory cap)
KLEE: WARNING: killing 28180 states (over memory cap)
KLEE: WARNING: killing 27870 states (over memory cap)
KLEE: WARNING: killing 27624 states (over memory cap)
KLEE: WARNING: killing 24882 states (over memory cap)
KLEE: WARNING: killing 24736 states (over memory cap)
KLEE: WARNING: killing 25363 states (over memory cap)
KLEE: WARNING: killing 24885 states (over memory cap)
KLEE: WARNING: killing 26783 states (over memory cap)
KLEE: WARNING: killing 25494 states (over memory cap)
KLEE: WARNING: killing 24585 states (over memory cap)
KLEE: WARNING: killing 25205 states (over memory cap)
KLEE: WARNING: killing 25838 states (over memory cap)
KLEE: WARNING: killing 26528 states (over memory cap)
KLEE: WARNING: killing 27209 states (over memory cap)
KLEE: WARNING: killing 26918 states (over memory cap)
KLEE: WARNING: killing 26065 states (over memory cap)
KLEE: WARNING: killing 26089 states (over memory cap)
KLEE: WARNING: killing 25088 states (over memory cap)
KLEE: WARNING: killing 26091 states (over memory cap)
KLEE: WARNING: killing 26553 states (over memory cap)
KLEE: WARNING: killing 25280 states (over memory cap)
KLEE: WARNING: killing 25639 states (over memory cap)
KLEE: WARNING: killing 25596 states (over memory cap)
KLEE: WARNING: killing 25138 states (over memory cap)
KLEE: WARNING: killing 25274 states (over memory cap)
KLEE: WARNING: killing 25252 states (over memory cap)
KLEE: WARNING: killing 26513 states (over memory cap)
KLEE: WARNING: killing 26814 states (over memory cap)
KLEE: WARNING: killing 26956 states (over memory cap)
KLEE: WARNING: killing 26115 states (over memory cap)
KLEE: WARNING: killing 25124 states (over memory cap)
KLEE: WARNING: killing 26489 states (over memory cap)
KLEE: WARNING: killing 26247 states (over memory cap)
KLEE: WARNING: killing 26917 states (over memory cap)
KLEE: WARNING: killing 24751 states (over memory cap)
KLEE: WARNING: killing 26001 states (over memory cap)
KLEE: WARNING: killing 25497 states (over memory cap)
KLEE: WARNING: killing 25354 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-HSThha/linux-4.2-rc1.tar.xz-32_7a-drivers--block--rbd.ko-entry_point_true-unreach-call.cil.out.c:11698: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25594 states (over memory cap)
KLEE: WARNING: killing 27920 states (over memory cap)
KLEE: WARNING: killing 26719 states (over memory cap)
KLEE: WARNING: killing 25200 states (over memory cap)
KLEE: WARNING: killing 27632 states (over memory cap)
KLEE: WARNING: killing 25528 states (over memory cap)
KLEE: WARNING: killing 26403 states (over memory cap)
KLEE: WARNING: killing 25425 states (over memory cap)
KLEE: WARNING: killing 25181 states (over memory cap)
KLEE: WARNING: killing 25954 states (over memory cap)
KLEE: WARNING: killing 26561 states (over memory cap)
KLEE: WARNING: killing 25793 states (over memory cap)
KLEE: WARNING: killing 24982 states (over memory cap)
KLEE: WARNING: killing 26579 states (over memory cap)
KLEE: WARNING: killing 25195 states (over memory cap)
KLEE: WARNING: killing 26960 states (over memory cap)
KLEE: WARNING: killing 24780 states (over memory cap)
KLEE: WARNING: killing 25080 states (over memory cap)
KLEE: WARNING: killing 26101 states (over memory cap)
KLEE: WARNING: killing 25712 states (over memory cap)
KLEE: WARNING: killing 26788 states (over memory cap)
KLEE: WARNING: killing 25248 states (over memory cap)
KLEE: WARNING: killing 26842 states (over memory cap)
KLEE: WARNING: killing 25451 states (over memory cap)
KLEE: WARNING: killing 25965 states (over memory cap)
KLEE: WARNING: killing 26722 states (over memory cap)
KLEE: WARNING: killing 25810 states (over memory cap)
KLEE: WARNING: killing 25685 states (over memory cap)
KLEE: WARNING: killing 26595 states (over memory cap)
KLEE: WARNING: killing 25892 states (over memory cap)
KLEE: WARNING: killing 26764 states (over memory cap)
KLEE: WARNING: killing 24499 states (over memory cap)
KLEE: WARNING: killing 26134 states (over memory cap)
KLEE: WARNING: killing 26365 states (over memory cap)
KLEE: WARNING: killing 25887 states (over memory cap)
KLEE: WARNING: killing 25294 states (over memory cap)
KLEE: WARNING: killing 25739 states (over memory cap)
KLEE: WARNING: killing 25654 states (over memory cap)
KLEE: WARNING: killing 26716 states (over memory cap)
KLEE: WARNING: killing 25974 states (over memory cap)
KLEE: WARNING: killing 26878 states (over memory cap)
KLEE: WARNING: killing 24907 states (over memory cap)
KLEE: WARNING: killing 26017 states (over memory cap)
KLEE: WARNING: killing 25685 states (over memory cap)
KLEE: WARNING: killing 25567 states (over memory cap)
KLEE: WARNING: killing 26216 states (over memory cap)
KLEE: WARNING: killing 26138 states (over memory cap)
KLEE: WARNING: killing 25867 states (over memory cap)
KLEE: WARNING: killing 26611 states (over memory cap)
KLEE: WARNING: killing 25616 states (over memory cap)
KLEE: WARNING: killing 26515 states (over memory cap)
KLEE: WARNING: killing 27009 states (over memory cap)
KLEE: WARNING: killing 26076 states (over memory cap)
KLEE: WARNING: killing 23749 states (over memory cap)
KLEE: WARNING: killing 26634 states (over memory cap)
KLEE: WARNING: killing 26057 states (over memory cap)
KLEE: WARNING: killing 26289 states (over memory cap)
KLEE: WARNING: killing 25507 states (over memory cap)
KLEE: WARNING: killing 25482 states (over memory cap)
KLEE: WARNING: killing 25970 states (over memory cap)
KLEE: WARNING: killing 26867 states (over memory cap)
KLEE: WARNING: killing 26128 states (over memory cap)
KLEE: WARNING: killing 26978 states (over memory cap)
KLEE: WARNING: killing 25189 states (over memory cap)
KLEE: WARNING: killing 25562 states (over memory cap)
KLEE: WARNING: killing 25740 states (over memory cap)
KLEE: WARNING: killing 25766 states (over memory cap)
KLEE: WARNING: killing 26258 states (over memory cap)
KLEE: WARNING: killing 25931 states (over memory cap)
KLEE: WARNING: killing 26317 states (over memory cap)
KLEE: WARNING: killing 26032 states (over memory cap)
KLEE: WARNING: killing 26117 states (over memory cap)
KLEE: WARNING: killing 25693 states (over memory cap)
KLEE: WARNING: killing 26179 states (over memory cap)
KLEE: WARNING: killing 25501 states (over memory cap)
KLEE: WARNING: killing 26437 states (over memory cap)
