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-43_2a-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 340 6303 38375
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
INFO: Compilation, preparation and instrumentation time: 1.33487010002
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)
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 __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
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
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
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)
Removed calls to 'ldv_check_final_state' (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
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  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.7545671463
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 371 223 3121 21998
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_bc63f496-99ba-40c2-9312-236b60befdd5/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14123 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 14501 states (over memory cap)
KLEE: WARNING: killing 14207 states (over memory cap)
KLEE: WARNING: killing 13950 states (over memory cap)
KLEE: WARNING: killing 14218 states (over memory cap)
KLEE: WARNING: killing 15167 states (over memory cap)
KLEE: WARNING: killing 14770 states (over memory cap)
KLEE: WARNING: killing 16248 states (over memory cap)
KLEE: WARNING: killing 14695 states (over memory cap)
KLEE: WARNING: killing 15831 states (over memory cap)
KLEE: WARNING: killing 15590 states (over memory cap)
KLEE: WARNING: killing 15940 states (over memory cap)
KLEE: WARNING: killing 15666 states (over memory cap)
KLEE: WARNING: killing 16238 states (over memory cap)
KLEE: WARNING: killing 14777 states (over memory cap)
KLEE: WARNING: killing 14867 states (over memory cap)
KLEE: WARNING: killing 15179 states (over memory cap)
KLEE: WARNING: killing 15230 states (over memory cap)
KLEE: WARNING: killing 15211 states (over memory cap)
KLEE: WARNING: killing 14680 states (over memory cap)
KLEE: WARNING: killing 16174 states (over memory cap)
KLEE: WARNING: killing 15605 states (over memory cap)
KLEE: WARNING: killing 15664 states (over memory cap)
KLEE: WARNING: killing 15575 states (over memory cap)
KLEE: WARNING: killing 14899 states (over memory cap)
KLEE: WARNING: killing 15283 states (over memory cap)
KLEE: WARNING: killing 15850 states (over memory cap)
KLEE: WARNING: killing 14846 states (over memory cap)
KLEE: WARNING: killing 15489 states (over memory cap)
KLEE: WARNING: killing 15068 states (over memory cap)
KLEE: WARNING: killing 15342 states (over memory cap)
KLEE: WARNING: killing 14992 states (over memory cap)
KLEE: WARNING: killing 15781 states (over memory cap)
KLEE: WARNING: killing 15618 states (over memory cap)
KLEE: WARNING: killing 15965 states (over memory cap)
KLEE: WARNING: killing 15593 states (over memory cap)
KLEE: WARNING: killing 15613 states (over memory cap)
KLEE: WARNING: killing 14978 states (over memory cap)
KLEE: WARNING: killing 15143 states (over memory cap)
KLEE: WARNING: killing 15303 states (over memory cap)
KLEE: WARNING: killing 15145 states (over memory cap)
KLEE: WARNING: killing 14799 states (over memory cap)
KLEE: WARNING: killing 15037 states (over memory cap)
KLEE: WARNING: killing 15958 states (over memory cap)
KLEE: WARNING: killing 15301 states (over memory cap)
KLEE: WARNING: killing 15468 states (over memory cap)
KLEE: WARNING: killing 15376 states (over memory cap)
KLEE: WARNING: killing 15365 states (over memory cap)
KLEE: WARNING: killing 15210 states (over memory cap)
KLEE: WARNING: killing 14725 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-BI3i7H/linux-4.2-rc1.tar.xz-43_2a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:20006: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BI3i7H/linux-4.2-rc1.tar.xz-43_2a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:20904: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BI3i7H/linux-4.2-rc1.tar.xz-43_2a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:16231: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BI3i7H/linux-4.2-rc1.tar.xz-43_2a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:18812: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15635 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-BI3i7H/linux-4.2-rc1.tar.xz-43_2a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:21021: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BI3i7H/linux-4.2-rc1.tar.xz-43_2a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:20283: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BI3i7H/linux-4.2-rc1.tar.xz-43_2a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:20724: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BI3i7H/linux-4.2-rc1.tar.xz-43_2a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:18918: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15978 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-BI3i7H/linux-4.2-rc1.tar.xz-43_2a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:17781: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BI3i7H/linux-4.2-rc1.tar.xz-43_2a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:19924: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BI3i7H/linux-4.2-rc1.tar.xz-43_2a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:20430: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15140 states (over memory cap)
KLEE: WARNING: killing 15129 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-BI3i7H/linux-4.2-rc1.tar.xz-43_2a-drivers--md--raid456.ko-entry_point_true-unreach-call.cil.out.c:19541: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15939 states (over memory cap)
KLEE: WARNING: killing 16325 states (over memory cap)
KLEE: WARNING: killing 15208 states (over memory cap)
KLEE: WARNING: killing 15656 states (over memory cap)
KLEE: WARNING: killing 14852 states (over memory cap)
KLEE: WARNING: killing 15618 states (over memory cap)
KLEE: WARNING: killing 15500 states (over memory cap)
KLEE: WARNING: killing 15306 states (over memory cap)
KLEE: WARNING: killing 16076 states (over memory cap)
KLEE: WARNING: killing 15353 states (over memory cap)
KLEE: WARNING: killing 15590 states (over memory cap)
KLEE: WARNING: killing 15897 states (over memory cap)
KLEE: WARNING: killing 15847 states (over memory cap)
KLEE: WARNING: killing 15733 states (over memory cap)
KLEE: WARNING: killing 15115 states (over memory cap)
KLEE: WARNING: killing 14959 states (over memory cap)
KLEE: WARNING: killing 15267 states (over memory cap)
KLEE: WARNING: killing 15355 states (over memory cap)
KLEE: WARNING: killing 14741 states (over memory cap)
KLEE: WARNING: killing 15361 states (over memory cap)
KLEE: WARNING: killing 16162 states (over memory cap)
KLEE: WARNING: killing 15481 states (over memory cap)
KLEE: WARNING: killing 15327 states (over memory cap)
KLEE: WARNING: killing 15528 states (over memory cap)
KLEE: WARNING: killing 15410 states (over memory cap)
KLEE: WARNING: killing 15398 states (over memory cap)
KLEE: WARNING: killing 15732 states (over memory cap)
KLEE: WARNING: killing 15160 states (over memory cap)
KLEE: WARNING: killing 15427 states (over memory cap)
KLEE: WARNING: killing 15592 states (over memory cap)
KLEE: WARNING: killing 15124 states (over memory cap)
KLEE: WARNING: killing 15492 states (over memory cap)
KLEE: WARNING: killing 15482 states (over memory cap)
KLEE: WARNING: killing 15297 states (over memory cap)
KLEE: WARNING: killing 15808 states (over memory cap)
KLEE: WARNING: killing 15623 states (over memory cap)
KLEE: WARNING: killing 14709 states (over memory cap)
KLEE: WARNING: killing 15352 states (over memory cap)
KLEE: WARNING: killing 15930 states (over memory cap)
KLEE: WARNING: killing 15295 states (over memory cap)
KLEE: WARNING: killing 16119 states (over memory cap)
KLEE: WARNING: killing 15623 states (over memory cap)
KLEE: WARNING: killing 14885 states (over memory cap)
KLEE: WARNING: killing 15599 states (over memory cap)
KLEE: WARNING: killing 14891 states (over memory cap)
KLEE: WARNING: killing 15571 states (over memory cap)
KLEE: WARNING: killing 15731 states (over memory cap)
KLEE: WARNING: killing 15480 states (over memory cap)
KLEE: WARNING: killing 15015 states (over memory cap)
KLEE: WARNING: killing 15759 states (over memory cap)
KLEE: WARNING: killing 15290 states (over memory cap)
KLEE: WARNING: killing 15968 states (over memory cap)
KLEE: WARNING: killing 15746 states (over memory cap)
KLEE: WARNING: killing 15567 states (over memory cap)
KLEE: WARNING: killing 15520 states (over memory cap)
KLEE: WARNING: killing 15611 states (over memory cap)
KLEE: WARNING: killing 14542 states (over memory cap)
KLEE: WARNING: killing 14794 states (over memory cap)
KLEE: WARNING: killing 15568 states (over memory cap)
KLEE: WARNING: killing 15858 states (over memory cap)
KLEE: WARNING: killing 15403 states (over memory cap)
KLEE: WARNING: killing 15694 states (over memory cap)
KLEE: WARNING: killing 15684 states (over memory cap)
KLEE: WARNING: killing 15841 states (over memory cap)
KLEE: WARNING: killing 15321 states (over memory cap)
KLEE: WARNING: killing 15274 states (over memory cap)
KLEE: WARNING: killing 15665 states (over memory cap)
KLEE: WARNING: killing 14604 states (over memory cap)
KLEE: WARNING: killing 15537 states (over memory cap)
KLEE: WARNING: killing 15595 states (over memory cap)
KLEE: WARNING: killing 15981 states (over memory cap)
KLEE: WARNING: killing 16585 states (over memory cap)
KLEE: WARNING: killing 15353 states (over memory cap)
KLEE: WARNING: killing 16119 states (over memory cap)
KLEE: WARNING: killing 15433 states (over memory cap)
KLEE: WARNING: killing 15183 states (over memory cap)
KLEE: WARNING: killing 14803 states (over memory cap)
KLEE: WARNING: killing 14891 states (over memory cap)
KLEE: WARNING: killing 15451 states (over memory cap)
KLEE: WARNING: killing 15303 states (over memory cap)
KLEE: WARNING: killing 15997 states (over memory cap)
KLEE: WARNING: killing 15213 states (over memory cap)
KLEE: WARNING: killing 15940 states (over memory cap)
KLEE: WARNING: killing 15660 states (over memory cap)
KLEE: WARNING: killing 15286 states (over memory cap)
KLEE: WARNING: killing 15537 states (over memory cap)
KLEE: WARNING: killing 15359 states (over memory cap)
KLEE: WARNING: killing 15249 states (over memory cap)
KLEE: WARNING: killing 15605 states (over memory cap)
KLEE: WARNING: killing 15662 states (over memory cap)
