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--md--raid456.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.: 256 335 6304 38430
Removed infinite loop in drop_one_stripe
Removed infinite loop in do_release_stripe
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 get_free_stripe
Removed infinite loop in __get_priority_stripe
Removed infinite loop in handle_stripe
Removed infinite loop in analyse_stripe
Removed infinite loop in handle_failed_stripe
Removed infinite loop in handle_failed_sync
Removed infinite loop in handle_parity_checks6
Removed infinite loop in handle_parity_checks5
Removed infinite loop in get_active_stripe
Removed infinite loop in schedule_reconstruction
Removed infinite loop in handle_stripe_expansion
Removed infinite loop in raid_run_ops
Removed infinite loop in ops_run_io
Removed infinite loop in raid5_end_write_request
Removed infinite loop in raid5_end_read_request
Removed infinite loop in ops_run_biofill
Removed infinite loop in ops_run_compute5
Removed infinite loop in ops_run_compute6_1
Removed infinite loop in ops_run_compute6_2
Removed infinite loop in ops_run_prexor5
Removed infinite loop in ops_run_biodrain
Removed infinite loop in ops_run_check_p
Removed infinite loop in ops_run_check_pq
Removed infinite loop in ops_complete_reconstruct
Removed infinite loop in mark_target_uptodate
Removed infinite loop in ops_complete_biofill
Removed infinite loop in compute_blocknr
Removed infinite loop in raid5_compute_sector
Removed infinite loop in init_stripe
Removed infinite loop in fetch_block
Removed infinite loop in run
Removed infinite loop in add_stripe_bio
Removed infinite loop in stripe_add_to_batch_list
Removed infinite loop in arch_local_irq_enable
Removed infinite loop in is_full_stripe_write
Removed infinite loop in reshape_request
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 1.1107749939
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'kmem_cache_free' (function is undefined)
Defining function md_allow_write as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Removed calls to 'md_wakeup_thread' (function is undefined)
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Defining function _atomic_dec_and_lock as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function __cpu_to_node as symbolic
Defining function queue_work_on as symbolic
Defining function find_first_bit as symbolic
Defining function llist_add_batch as symbolic
Defining function alloc_pages_current as symbolic
Defining function kmem_cache_alloc as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'mddev_unlock' (function is undefined)
Defining function mutex_lock_interruptible_nested as symbolic
Defining function kstrtoull as symbolic
Defining function sprintf as symbolic
Removed calls to 'mddev_suspend' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'mddev_resume' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'blk_start_plug' (function is undefined)
Removed calls to 'blk_finish_plug' (function is undefined)
Removed calls to '___might_sleep' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'md_error' (function is undefined)
Removed calls to 'md_write_end' (function is undefined)
Removed calls to 'bitmap_endwrite' (function is undefined)
Removed calls to 'md_done_sync' (function is undefined)
Removed calls to '__trace_note_message' (function is undefined)
Removed calls to 'async_tx_quiesce' (function is undefined)
Removed calls to 'md_wait_for_blocked_rdev' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'md_check_recovery' (function is undefined)
Removed calls to 'bio_reset' (function is undefined)
Removed calls to 'generic_make_request' (function is undefined)
Defining function _cond_resched as symbolic
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'bio_init' (function is undefined)
Defining function rdev_set_badblocks as symbolic
Defining function rdev_clear_badblocks as symbolic
Removed calls to 'bio_endio' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_watching as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function lock_is_held as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Defining function rcu_read_lock_held as symbolic
Removed calls to 'lock_release' (function is undefined)
Defining function ___ratelimit as symbolic
Defining function bdevname as symbolic
Defining function printk as symbolic
Defining function md_is_badblock as symbolic
Defining function async_syndrome_val as symbolic
Defining function flex_array_get as symbolic
Defining function async_xor_val as symbolic
Defining function async_trigger_callback as symbolic
Defining function async_gen_syndrome as symbolic
Defining function async_memcpy as symbolic
Defining function async_xor as symbolic
Defining function async_raid6_datap_recov as symbolic
Defining function async_raid6_2data_recov as symbolic
Defining function prepare_to_wait_event as symbolic
Defining function llist_reverse_order as symbolic
Defining function __bitmap_weight as symbolic
Removed calls to 'md_flush_request' (function is undefined)
Removed calls to 'md_write_start' (function is undefined)
Removed calls to 'blk_recount_segments' (function is undefined)
Removed calls to 'bio_put' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'flush_signals' (function is undefined)
Removed calls to 'md_set_array_sectors' (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_max_write_same_sectors' (function is undefined)
Removed calls to 'disk_stack_limits' (function is undefined)
Removed calls to 'md_unregister_thread' (function is undefined)
Removed calls to 'synchronize_sched' (function is undefined)
Removed calls to 'kernfs_notify' (function is undefined)
Removed calls to 'bitmap_end_sync' (function is undefined)
Removed calls to 'bitmap_close_sync' (function is undefined)
Removed calls to 'sysfs_notify' (function is undefined)
Removed calls to 'bitmap_cond_end_sync' (function is undefined)
Removed calls to 'md_new_event' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'get_online_cpus' (function is undefined)
Removed calls to 'put_online_cpus' (function is undefined)
Defining function register_shrinker as symbolic
Removed calls to 'bitmap_unplug' (function is undefined)
Removed calls to 'dma_issue_pending_all' (function is undefined)
Defining function md_register_thread as symbolic
Removed calls to 'unregister_shrinker' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Removed calls to 'unregister_cpu_notifier' (function is undefined)
Removed calls to 'free_percpu' (function is undefined)
Removed calls to 'flex_array_free' (function is undefined)
Defining function find_next_bit as symbolic
Removed calls to '_raw_spin_lock_nested' (function is undefined)
Defining function bitmap_startwrite as symbolic
Defining function kmem_cache_create as symbolic
Defining function __alloc_percpu as symbolic
Defining function register_cpu_notifier as symbolic
Defining function flex_array_alloc as symbolic
Defining function flex_array_prealloc as symbolic
Removed calls to '_raw_spin_lock_nest_lock' (function is undefined)
Defining function revalidate_disk as symbolic
Defining function sysfs_create_link as symbolic
Removed calls to 'list_del' (function is undefined)
Defining function bitmap_resize as symbolic
Defining function bitmap_start_sync as symbolic
Defining function schedule_timeout_uninterruptible as symbolic
Defining function seq_printf as symbolic
Defining function sysfs_create_group as symbolic
Defining function autoremove_wake_function as symbolic
Defining function blk_check_plugged as symbolic
Defining function bio_clone_mddev as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Defining function ldv_stop_3 as symbolic
Defining function ldv_stop_2 as symbolic
Defining function ldv_stop_4 as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function register_md_personality as symbolic
Defining function unregister_md_personality as symbolic
Defining function queue_delayed_work_on as symbolic
Linked our definitions to these undefined functions:
  __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.46195578575
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 373 224 3123 21917
INFO: Starting verification
WARNING: this target does not support the llvm.returnaddress intrinsic.
WARNING: this target does not support the llvm.returnaddress intrinsic.
KLEE: WARNING ONCE: function "drop_one_stripe" has inline asm
KLEE: WARNING ONCE: function "grow_one_stripe" has inline asm
KLEE: WARNING ONCE: function "release_stripe" has inline asm
KLEE: WARNING ONCE: function "arch_local_save_flags" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_disable" has inline asm
KLEE: WARNING ONCE: function "do_release_stripe" has inline asm
KLEE: WARNING ONCE: function "release_inactive_stripe_list" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "raid5_wakeup_stripe_thread" has inline asm
KLEE: WARNING ONCE: function "get_free_stripe" has inline asm
KLEE: WARNING ONCE: function "release_stripe_list" has inline asm
KLEE: WARNING ONCE: function "handle_active_stripes" has inline asm
KLEE: WARNING ONCE: function "handle_stripe" has inline asm
KLEE: WARNING ONCE: function "__release_stripe" has inline asm
KLEE: WARNING ONCE: function "break_stripe_batch_list" 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 "rdev_dec_pending" has inline asm
KLEE: WARNING ONCE: function "handle_stripe_clean_event" has inline asm
KLEE: WARNING ONCE: function "schedule_reconstruction" has inline asm
KLEE: WARNING ONCE: function "get_active_stripe" has inline asm
KLEE: WARNING ONCE: function "compute_blocknr" has inline asm
KLEE: WARNING ONCE: function "raid5_compute_sector" has inline asm
KLEE: WARNING ONCE: function "ops_complete_biofill" has inline asm
KLEE: WARNING ONCE: function "ops_complete_compute" has inline asm
KLEE: WARNING ONCE: function "ops_complete_reconstruct" has inline asm
KLEE: WARNING ONCE: function "ops_complete_check" has inline asm
KLEE: WARNING ONCE: function "ops_run_check_pq" has inline asm
KLEE: WARNING ONCE: function "raid5_end_write_request" has inline asm
KLEE: WARNING ONCE: function "raid5_end_read_request" has inline asm
KLEE: WARNING ONCE: function "trace_block_bio_remap" has inline asm
KLEE: WARNING ONCE: function "trace_block_bio_complete" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held" has inline asm
KLEE: WARNING ONCE: function "mark_target_uptodate" has inline asm
KLEE: WARNING ONCE: function "read_seqcount_begin" has inline asm
KLEE: WARNING ONCE: function "make_request" has inline asm
KLEE: WARNING ONCE: function "run" has inline asm
KLEE: WARNING ONCE: function "error" has inline asm
KLEE: WARNING ONCE: function "raid5_add_disk" has inline asm
KLEE: WARNING ONCE: function "raid5_remove_disk" has inline asm
KLEE: WARNING ONCE: function "raid5_spare_active" has inline asm
KLEE: WARNING ONCE: function "sync_request" has inline asm
KLEE: WARNING ONCE: function "raid5_resize" has inline asm
KLEE: WARNING ONCE: function "raid5_check_reshape" has inline asm
KLEE: WARNING ONCE: function "raid5_start_reshape" has inline asm
KLEE: WARNING ONCE: function "raid5_finish_reshape" has inline asm
KLEE: WARNING ONCE: function "setup_conf" has inline asm
KLEE: WARNING ONCE: function "raid456_cpu_notify" has inline asm
KLEE: WARNING ONCE: function "raid5d" has inline asm
KLEE: WARNING ONCE: function "free_conf" has inline asm
KLEE: WARNING ONCE: function "add_stripe_bio" has inline asm
KLEE: WARNING ONCE: function "stripe_can_batch" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_enable" has inline asm
KLEE: WARNING ONCE: function "check_reshape" has inline asm
KLEE: WARNING ONCE: function "raid5_align_endio" has inline asm
KLEE: WARNING ONCE: function "release_stripe_plug" has inline asm
KLEE: WARNING ONCE: function "raid5_unplug" has inline asm
KLEE: WARNING: undefined reference to function: md_do_sync
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_e006d969-f0fd-43d6-9e99-3ce72538818c/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11865 states (over memory cap)
KLEE: WARNING: killing 14833 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 14091 states (over memory cap)
KLEE: WARNING: killing 13878 states (over memory cap)
KLEE: WARNING: killing 13999 states (over memory cap)
KLEE: WARNING: killing 14305 states (over memory cap)
KLEE: WARNING: killing 14728 states (over memory cap)
KLEE: WARNING: killing 15559 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-erYjNx/linux-4.2-rc1.tar.xz-08_1a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:20473: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-erYjNx/linux-4.2-rc1.tar.xz-08_1a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:20047: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-erYjNx/linux-4.2-rc1.tar.xz-08_1a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:18852: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14643 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-erYjNx/linux-4.2-rc1.tar.xz-08_1a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:19964: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-erYjNx/linux-4.2-rc1.tar.xz-08_1a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:18958: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-erYjNx/linux-4.2-rc1.tar.xz-08_1a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:16269: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-erYjNx/linux-4.2-rc1.tar.xz-08_1a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:21065: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-erYjNx/linux-4.2-rc1.tar.xz-08_1a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:20948: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-erYjNx/linux-4.2-rc1.tar.xz-08_1a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:20325: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-erYjNx/linux-4.2-rc1.tar.xz-08_1a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:19581: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15924 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-erYjNx/linux-4.2-rc1.tar.xz-08_1a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:17821: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-erYjNx/linux-4.2-rc1.tar.xz-08_1a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:20768: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15980 states (over memory cap)
KLEE: WARNING: killing 15181 states (over memory cap)
KLEE: WARNING: killing 16570 states (over memory cap)
KLEE: WARNING: killing 15292 states (over memory cap)
KLEE: WARNING: killing 14831 states (over memory cap)
KLEE: WARNING: killing 15398 states (over memory cap)
KLEE: WARNING: killing 15049 states (over memory cap)
KLEE: WARNING: killing 14620 states (over memory cap)
KLEE: WARNING: killing 14968 states (over memory cap)
KLEE: WARNING: killing 15174 states (over memory cap)
KLEE: WARNING: killing 15743 states (over memory cap)
KLEE: WARNING: killing 14664 states (over memory cap)
KLEE: WARNING: killing 15666 states (over memory cap)
KLEE: WARNING: killing 14848 states (over memory cap)
KLEE: WARNING: killing 15740 states (over memory cap)
KLEE: WARNING: killing 15578 states (over memory cap)
KLEE: WARNING: killing 15674 states (over memory cap)
KLEE: WARNING: killing 14997 states (over memory cap)
KLEE: WARNING: killing 15458 states (over memory cap)
KLEE: WARNING: killing 15257 states (over memory cap)
KLEE: WARNING: killing 15095 states (over memory cap)
KLEE: WARNING: killing 16088 states (over memory cap)
KLEE: WARNING: killing 14774 states (over memory cap)
KLEE: WARNING: killing 15550 states (over memory cap)
KLEE: WARNING: killing 15497 states (over memory cap)
KLEE: WARNING: killing 15371 states (over memory cap)
KLEE: WARNING: killing 14705 states (over memory cap)
KLEE: WARNING: killing 15090 states (over memory cap)
KLEE: WARNING: killing 15220 states (over memory cap)
KLEE: WARNING: killing 15199 states (over memory cap)
KLEE: WARNING: killing 15076 states (over memory cap)
KLEE: WARNING: killing 15598 states (over memory cap)
KLEE: WARNING: killing 15657 states (over memory cap)
KLEE: WARNING: killing 15213 states (over memory cap)
KLEE: WARNING: killing 15088 states (over memory cap)
KLEE: WARNING: killing 15468 states (over memory cap)
KLEE: WARNING: killing 15421 states (over memory cap)
KLEE: WARNING: killing 15263 states (over memory cap)
KLEE: WARNING: killing 15534 states (over memory cap)
KLEE: WARNING: killing 15088 states (over memory cap)
KLEE: WARNING: killing 15327 states (over memory cap)
KLEE: WARNING: killing 15454 states (over memory cap)
KLEE: WARNING: killing 14514 states (over memory cap)
KLEE: WARNING: killing 15491 states (over memory cap)
KLEE: WARNING: killing 15119 states (over memory cap)
KLEE: WARNING: killing 15210 states (over memory cap)
KLEE: WARNING: killing 15094 states (over memory cap)
KLEE: WARNING: killing 15644 states (over memory cap)
KLEE: WARNING: killing 15564 states (over memory cap)
KLEE: WARNING: killing 15583 states (over memory cap)
KLEE: WARNING: killing 15216 states (over memory cap)
KLEE: WARNING: killing 14952 states (over memory cap)
KLEE: WARNING: killing 15222 states (over memory cap)
KLEE: WARNING: killing 15493 states (over memory cap)
KLEE: WARNING: killing 14988 states (over memory cap)
KLEE: WARNING: killing 15675 states (over memory cap)
KLEE: WARNING: killing 15171 states (over memory cap)
KLEE: WARNING: killing 15580 states (over memory cap)
KLEE: WARNING: killing 15465 states (over memory cap)
KLEE: WARNING: killing 15416 states (over memory cap)
KLEE: WARNING: killing 15224 states (over memory cap)
KLEE: WARNING: killing 14897 states (over memory cap)
KLEE: WARNING: killing 15097 states (over memory cap)
KLEE: WARNING: killing 14909 states (over memory cap)
KLEE: WARNING: killing 15458 states (over memory cap)
KLEE: WARNING: killing 14360 states (over memory cap)
KLEE: WARNING: killing 15429 states (over memory cap)
KLEE: WARNING: killing 15416 states (over memory cap)
KLEE: WARNING: killing 15444 states (over memory cap)
KLEE: WARNING: killing 15603 states (over memory cap)
KLEE: WARNING: killing 15108 states (over memory cap)
KLEE: WARNING: killing 14923 states (over memory cap)
KLEE: WARNING: killing 15603 states (over memory cap)
KLEE: WARNING: killing 15311 states (over memory cap)
KLEE: WARNING: killing 15129 states (over memory cap)
KLEE: WARNING: killing 14841 states (over memory cap)
KLEE: WARNING: killing 15272 states (over memory cap)
KLEE: WARNING: killing 14916 states (over memory cap)
KLEE: WARNING: killing 15700 states (over memory cap)
KLEE: WARNING: killing 15547 states (over memory cap)
KLEE: WARNING: killing 14988 states (over memory cap)
KLEE: WARNING: killing 15699 states (over memory cap)
KLEE: WARNING: killing 15546 states (over memory cap)
KLEE: WARNING: killing 15709 states (over memory cap)
KLEE: WARNING: killing 14457 states (over memory cap)
KLEE: WARNING: killing 15578 states (over memory cap)
KLEE: WARNING: killing 14812 states (over memory cap)
KLEE: WARNING: killing 15070 states (over memory cap)
KLEE: WARNING: killing 15057 states (over memory cap)
KLEE: WARNING: killing 15800 states (over memory cap)
KLEE: WARNING: killing 15209 states (over memory cap)
KLEE: WARNING: killing 14778 states (over memory cap)
KLEE: WARNING: killing 15214 states (over memory cap)
KLEE: WARNING: killing 15572 states (over memory cap)
KLEE: WARNING: killing 15395 states (over memory cap)
KLEE: WARNING: killing 15005 states (over memory cap)
KLEE: WARNING: killing 15133 states (over memory cap)
KLEE: WARNING: killing 14878 states (over memory cap)
KLEE: WARNING: killing 15437 states (over memory cap)
KLEE: WARNING: killing 15697 states (over memory cap)
KLEE: WARNING: killing 15012 states (over memory cap)
KLEE: WARNING: killing 14892 states (over memory cap)
KLEE: WARNING: killing 15287 states (over memory cap)
KLEE: WARNING: killing 15143 states (over memory cap)
KLEE: WARNING: killing 15572 states (over memory cap)
KLEE: WARNING: killing 15324 states (over memory cap)
KLEE: WARNING: killing 14939 states (over memory cap)
KLEE: WARNING: killing 15501 states (over memory cap)
KLEE: WARNING: killing 14942 states (over memory cap)
KLEE: WARNING: killing 15098 states (over memory cap)
KLEE: WARNING: killing 15290 states (over memory cap)
KLEE: WARNING: killing 15175 states (over memory cap)
KLEE: WARNING: killing 14891 states (over memory cap)
KLEE: WARNING: killing 15487 states (over memory cap)
KLEE: WARNING: killing 15105 states (over memory cap)
KLEE: WARNING: killing 14623 states (over memory cap)
KLEE: WARNING: killing 15111 states (over memory cap)
KLEE: WARNING: killing 15502 states (over memory cap)
KLEE: WARNING: killing 15087 states (over memory cap)
KLEE: WARNING: killing 15378 states (over memory cap)
KLEE: WARNING: killing 15099 states (over memory cap)
KLEE: WARNING: killing 14952 states (over memory cap)
KLEE: WARNING: killing 16008 states (over memory cap)
KLEE: WARNING: killing 15330 states (over memory cap)
KLEE: WARNING: killing 14885 states (over memory cap)
KLEE: WARNING: killing 15444 states (over memory cap)
KLEE: WARNING: killing 15664 states (over memory cap)
KLEE: WARNING: killing 15290 states (over memory cap)
KLEE: WARNING: killing 15547 states (over memory cap)
KLEE: WARNING: killing 15006 states (over memory cap)
KLEE: WARNING: killing 14692 states (over memory cap)
KLEE: WARNING: killing 14814 states (over memory cap)
KLEE: WARNING: killing 15434 states (over memory cap)
KLEE: WARNING: killing 15159 states (over memory cap)
