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--md--raid456.ko-entry_point_false-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.: 257 385 6492 39116
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.3983809948
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 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 '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
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock 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.80189704895
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 374 275 3303 22418
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_47a9b7ae-8215-49c6-88fa-c5269648f6d9/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14103 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 14633 states (over memory cap)
KLEE: WARNING: killing 14453 states (over memory cap)
KLEE: WARNING: killing 13895 states (over memory cap)
KLEE: WARNING: killing 14355 states (over memory cap)
KLEE: WARNING: killing 14700 states (over memory cap)
KLEE: WARNING: killing 14634 states (over memory cap)
KLEE: WARNING: killing 16778 states (over memory cap)
KLEE: WARNING: killing 15307 states (over memory cap)
KLEE: WARNING: killing 16038 states (over memory cap)
KLEE: WARNING: killing 15680 states (over memory cap)
KLEE: WARNING: killing 15780 states (over memory cap)
KLEE: WARNING: killing 14864 states (over memory cap)
KLEE: WARNING: killing 15215 states (over memory cap)
KLEE: WARNING: killing 14643 states (over memory cap)
KLEE: WARNING: killing 15176 states (over memory cap)
KLEE: WARNING: killing 14860 states (over memory cap)
KLEE: WARNING: killing 15469 states (over memory cap)
KLEE: WARNING: killing 15486 states (over memory cap)
KLEE: WARNING: killing 15100 states (over memory cap)
KLEE: WARNING: killing 15381 states (over memory cap)
KLEE: WARNING: killing 15839 states (over memory cap)
KLEE: WARNING: killing 15233 states (over memory cap)
KLEE: WARNING: killing 15183 states (over memory cap)
KLEE: WARNING: killing 15386 states (over memory cap)
KLEE: WARNING: killing 14674 states (over memory cap)
KLEE: WARNING: killing 15526 states (over memory cap)
KLEE: WARNING: killing 15959 states (over memory cap)
KLEE: WARNING: killing 15029 states (over memory cap)
KLEE: WARNING: killing 15849 states (over memory cap)
KLEE: WARNING: killing 15288 states (over memory cap)
KLEE: WARNING: killing 15381 states (over memory cap)
KLEE: WARNING: killing 14892 states (over memory cap)
KLEE: WARNING: killing 15419 states (over memory cap)
KLEE: WARNING: killing 15222 states (over memory cap)
KLEE: WARNING: killing 14917 states (over memory cap)
KLEE: WARNING: killing 14901 states (over memory cap)
KLEE: WARNING: killing 16148 states (over memory cap)
KLEE: WARNING: killing 15591 states (over memory cap)
KLEE: WARNING: killing 15398 states (over memory cap)
KLEE: WARNING: killing 15672 states (over memory cap)
KLEE: WARNING: killing 15144 states (over memory cap)
KLEE: WARNING: killing 15528 states (over memory cap)
KLEE: WARNING: killing 15042 states (over memory cap)
KLEE: WARNING: killing 15357 states (over memory cap)
KLEE: WARNING: killing 15302 states (over memory cap)
KLEE: WARNING: killing 15250 states (over memory cap)
KLEE: WARNING: killing 14844 states (over memory cap)
KLEE: WARNING: killing 15759 states (over memory cap)
KLEE: WARNING: killing 15278 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-LH5E8_/linux-4.2-rc1.tar.xz-32_7a-drivers--md--raid456.ko-entry_point_false-unreach-call.cil.out.c:19967: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LH5E8_/linux-4.2-rc1.tar.xz-32_7a-drivers--md--raid456.ko-entry_point_false-unreach-call.cil.out.c:16189: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15766 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-LH5E8_/linux-4.2-rc1.tar.xz-32_7a-drivers--md--raid456.ko-entry_point_false-unreach-call.cil.out.c:18878: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LH5E8_/linux-4.2-rc1.tar.xz-32_7a-drivers--md--raid456.ko-entry_point_false-unreach-call.cil.out.c:20245: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LH5E8_/linux-4.2-rc1.tar.xz-32_7a-drivers--md--raid456.ko-entry_point_false-unreach-call.cil.out.c:19884: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LH5E8_/linux-4.2-rc1.tar.xz-32_7a-drivers--md--raid456.ko-entry_point_false-unreach-call.cil.out.c:18772: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LH5E8_/linux-4.2-rc1.tar.xz-32_7a-drivers--md--raid456.ko-entry_point_false-unreach-call.cil.out.c:20985: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LH5E8_/linux-4.2-rc1.tar.xz-32_7a-drivers--md--raid456.ko-entry_point_false-unreach-call.cil.out.c:19501: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LH5E8_/linux-4.2-rc1.tar.xz-32_7a-drivers--md--raid456.ko-entry_point_false-unreach-call.cil.out.c:20868: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15110 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-LH5E8_/linux-4.2-rc1.tar.xz-32_7a-drivers--md--raid456.ko-entry_point_false-unreach-call.cil.out.c:20393: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15808 states (over memory cap)
KLEE: WARNING: killing 15405 states (over memory cap)
KLEE: WARNING: killing 15564 states (over memory cap)
KLEE: WARNING: killing 14948 states (over memory cap)
KLEE: WARNING: killing 16503 states (over memory cap)
KLEE: WARNING: killing 14779 states (over memory cap)
KLEE: WARNING: killing 14908 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-LH5E8_/linux-4.2-rc1.tar.xz-32_7a-drivers--md--raid456.ko-entry_point_false-unreach-call.cil.out.c:20688: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LH5E8_/linux-4.2-rc1.tar.xz-32_7a-drivers--md--raid456.ko-entry_point_false-unreach-call.cil.out.c:17741: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15883 states (over memory cap)
KLEE: WARNING: killing 15409 states (over memory cap)
KLEE: WARNING: killing 16069 states (over memory cap)
KLEE: WARNING: killing 15456 states (over memory cap)
KLEE: WARNING: killing 15231 states (over memory cap)
KLEE: WARNING: killing 14930 states (over memory cap)
KLEE: WARNING: killing 16120 states (over memory cap)
KLEE: WARNING: killing 15649 states (over memory cap)
KLEE: WARNING: killing 14897 states (over memory cap)
KLEE: WARNING: killing 15375 states (over memory cap)
KLEE: WARNING: killing 16031 states (over memory cap)
KLEE: WARNING: killing 15987 states (over memory cap)
KLEE: WARNING: killing 15132 states (over memory cap)
KLEE: WARNING: killing 14838 states (over memory cap)
KLEE: WARNING: killing 14854 states (over memory cap)
KLEE: WARNING: killing 15473 states (over memory cap)
KLEE: WARNING: killing 15675 states (over memory cap)
KLEE: WARNING: killing 15622 states (over memory cap)
KLEE: WARNING: killing 15475 states (over memory cap)
KLEE: WARNING: killing 15603 states (over memory cap)
KLEE: WARNING: killing 15830 states (over memory cap)
KLEE: WARNING: killing 15646 states (over memory cap)
KLEE: WARNING: killing 14725 states (over memory cap)
KLEE: WARNING: killing 15232 states (over memory cap)
KLEE: WARNING: killing 15813 states (over memory cap)
KLEE: WARNING: killing 14787 states (over memory cap)
KLEE: WARNING: killing 15997 states (over memory cap)
KLEE: WARNING: killing 15286 states (over memory cap)
KLEE: WARNING: killing 15757 states (over memory cap)
KLEE: WARNING: killing 15957 states (over memory cap)
KLEE: WARNING: killing 15875 states (over memory cap)
KLEE: WARNING: killing 14995 states (over memory cap)
KLEE: WARNING: killing 15784 states (over memory cap)
KLEE: WARNING: killing 14765 states (over memory cap)
KLEE: WARNING: killing 15581 states (over memory cap)
KLEE: WARNING: killing 15086 states (over memory cap)
KLEE: WARNING: killing 15521 states (over memory cap)
KLEE: WARNING: killing 15860 states (over memory cap)
KLEE: WARNING: killing 15085 states (over memory cap)
KLEE: WARNING: killing 15696 states (over memory cap)
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_47a9b7ae-8215-49c6-88fa-c5269648f6d9/symbiotic/lib/verifier/__VERIFIER_error.c:9: ASSERTION FAIL: verifier assertion failed
KLEE: NOTE: now ignoring this error at this location
Error found.
RESULT: false(unreach-call)

 --- Error trace ---

Error: ASSERTION FAIL: verifier assertion failed
File: /tmp/vcloud-vcloud-master/worker/working_dir_47a9b7ae-8215-49c6-88fa-c5269648f6d9/symbiotic/lib/verifier/__VERIFIER_error.c
Line: 9
assembly.ll line: 857
Stack: 
	#000000857 in __VERIFIER_error () at /tmp/vcloud-vcloud-master/worker/working_dir_47a9b7ae-8215-49c6-88fa-c5269648f6d9/symbiotic/lib/verifier/__VERIFIER_error.c:9
	#100002152 in ldv_error () at /tmp/symbiotic-LH5E8_/linux-4.2-rc1.tar.xz-32_7a-drivers--md--raid456.ko-entry_point_false-unreach-call.cil.out.c:23238
	#200002133 in ldv_mutex_lock_interruptible_reconfig_mutex_of_mddev (=0) at /tmp/symbiotic-LH5E8_/linux-4.2-rc1.tar.xz-32_7a-drivers--md--raid456.ko-entry_point_false-unreach-call.cil.out.c:23805
	#300002217 in raid5_store_preread_threshold (=2319080864, =57233072, =0) at /tmp/symbiotic-LH5E8_/linux-4.2-rc1.tar.xz-32_7a-drivers--md--raid456.ko-entry_point_false-unreach-call.cil.out.c:23085
	#400024018 in main () at /tmp/symbiotic-LH5E8_/linux-4.2-rc1.tar.xz-32_7a-drivers--md--raid456.ko-entry_point_false-unreach-call.cil.out.c:22412

 --- ----------- ---
Generating witness: /tmp/vcloud-vcloud-master/worker/working_dir_47a9b7ae-8215-49c6-88fa-c5269648f6d9/symbiotic/witness.graphml
 -- ---- --
Symbolic objects:
nondet := len 8 bytes, |8 times 0x1|
nondet:1 := len 8 bytes, |8 times 0x0|
nondet:2 := len 8 bytes, |8 times 0x0|
nondet:3 := len 8 bytes, |8 times 0x0|
nondet:4 := len 8 bytes, |8 times 0x0|
nondet:5 := len 8 bytes, |8 times 0x0|
nondet:6 := len 8 bytes, |8 times 0x0|
nondet:7 := len 8 bytes, |8 times 0x0|
nondet:8 := len 8 bytes, |8 times 0x0|
nondet:9 := len 8 bytes, |8 times 0x0|
nondet:10 := len 1 bytes, |0x0|
nondet:11 := len 8 bytes, |8 times 0x0|
nondet:12 := len 4 bytes, |4 times 0x0|
nondet:13 := len 2 bytes, |2 times 0x0|
nondet:14 := len 8 bytes, |8 times 0x0|
nondet:15 := len 8 bytes, |8 times 0x0|
nondet:16 := len 8 bytes, |8 times 0x0|
nondet:17 := len 8 bytes, |8 times 0x0|
nondet:18 := len 8 bytes, |8 times 0x0|
nondet:19 := len 8 bytes, |8 times 0x0|
nondet:20 := len 8 bytes, |8 times 0x0|
nondet:21 := len 8 bytes, |8 times 0x0|
nondet:22 := len 4 bytes, |4 times 0x0|
nondet:23 := len 8 bytes, |8 times 0x0|
nondet:24 := len 8 bytes, |8 times 0x0|
nondet:25 := len 672 bytes, |672 times 0x0|
nondet:26 := len 24 bytes, |24 times 0x0|
nondet:27 := len 16 bytes, |16 times 0x0|
nondet:28 := len 8 bytes, |8 times 0x0|
nondet:29 := len 8 bytes, |8 times 0x0|
nondet:30 := len 8 bytes, |8 times 0x0|
nondet:31 := len 96 bytes, |96 times 0x0|
nondet:32 := len 1 bytes, |0x0|
nondet:33 := len 8 bytes, |8 times 0x0|
nondet:34 := len 8 bytes, |8 times 0x0|
nondet:35 := len 8 bytes, |8 times 0x0|
nondet:36 := len 8 bytes, |8 times 0x0|
nondet:37 := len 40 bytes, |40 times 0x0|
nondet:38 := len 40 bytes, |40 times 0x0|
nondet:39 := len 8 bytes, |8 times 0x0|
nondet:40 := len 8 bytes, |8 times 0x0|
nondet:41 := len 8 bytes, |8 times 0x0|
nondet:42 := len 8 bytes, |8 times 0x0|
nondet:43 := len 8 bytes, |8 times 0x0|
nondet:44 := len 112 bytes, |112 times 0x0|
nondet:45 := len 8 bytes, |8 times 0x0|
nondet:46 := len 8 bytes, |8 times 0x0|
nondet:47 := len 48 bytes, |48 times 0x0|
nondet:48 := len 8 bytes, |8 times 0x0|
nondet:49 := len 8 bytes, |8 times 0x0|
nondet:50 := len 8 bytes, |8 times 0x0|
nondet:51 := len 40 bytes, |40 times 0x0|
nondet:52 := len 8 bytes, |8 times 0x0|
nondet:53 := len 8 bytes, |8 times 0x0|
nondet:54 := len 8 bytes, |8 times 0x0|
nondet:55 := len 8 bytes, |8 times 0x0|
nondet:56 := len 8 bytes, |8 times 0x0|
nondet:57 := len 8 bytes, |8 times 0x0|
nondet:58 := len 1 bytes, |0x0|
nondet:59 := len 16 bytes, |16 times 0x0|
nondet:60 := len 8 bytes, |8 times 0x0|
nondet:61 := len 8 bytes, |8 times 0x0|
nondet:62 := len 8 bytes, |8 times 0x0|
nondet:63 := len 4 bytes, |4 times 0x0|
extern-global:current_task := len 11712 bytes, |11712 times 0x0|
extern-global:__tracepoint_block_unplug := len 40 bytes, |40 times 0x0|
extern-global:jiffies := len 8 bytes, |8 times 0x0|
extern-global:cpu_present_mask := len 1024 bytes, |1024 times 0x0|
extern-global:cpu_possible_mask := len 1024 bytes, |1024 times 0x0|
extern-global:__this_module := len 1128 bytes, |1128 times 0x0|
extern-global:raid6_call := len 40 bytes, |40 times 0x0|
extern-global:node_states := len 640 bytes, |640 times 0x0|
extern-global:__per_cpu_offset := len 65536 bytes, |65536 times 0x0|
extern-global:cpu_number := len 4 bytes, |4 times 0x0|
extern-global:rcu_lock_map := len 48 bytes, |48 times 0x0|
extern-global:__tracepoint_block_bio_remap := len 40 bytes, |40 times 0x0|
extern-global:rcu_sched_lock_map := len 48 bytes, |48 times 0x0|
extern-global:debug_locks := len 4 bytes, |4 times 0x0|
extern-global:__preempt_count := len 4 bytes, |4 times 0x0|
extern-global:__tracepoint_block_bio_complete := len 40 bytes, |40 times 0x0|
extern-global:nr_cpu_ids := len 4 bytes, |4 times 0x0|
extern-global:cpu_online_mask := len 1024 bytes, |1024 times 0x0|
extern-global:pv_irq_ops := len 56 bytes, |56 times 0x0|
calloc0 := len 1 bytes, |0x0|
calloc0:1 := len 2096 bytes, |2096 times 0x0|
calloc0:2 := len 4 bytes, |4 times 0x0|
calloc0:3 := len 1 bytes, |0x0|
calloc0:4 := len 136 bytes, |136 times 0x0|
calloc0:5 := len 832 bytes, |832 times 0x0|
calloc0:6 := len 256 bytes, |256 times 0x0|
calloc0:7 := len 1 bytes, |0x0|
calloc0:8 := len 1 bytes, |0x0|
calloc0:9 := len 1 bytes, |0x0|
calloc0:10 := len 1 bytes, |0x0|
calloc0:11 := len 1 bytes, |0x0|
calloc0:12 := len 832 bytes, |832 times 0x0|
calloc0:13 := len 4 bytes, |4 times 0x0|
calloc0:14 := len 256 bytes, |256 times 0x0|
calloc0:15 := len 136 bytes, |136 times 0x0|
calloc0:16 := len 1 bytes, |0x0|
calloc0:17 := len 1 bytes, |0x0|
calloc0:18 := len 136 bytes, |136 times 0x0|
calloc0:19 := len 832 bytes, |832 times 0x0|
calloc0:20 := len 4 bytes, |4 times 0x0|
calloc0:21 := len 256 bytes, |256 times 0x0|
calloc0:22 := len 1 bytes, |0x0|
calloc0:23 := len 1 bytes, |0x0|
calloc0:24 := len 1 bytes, |0x0|
calloc0:25 := len 1 bytes, |0x0|
calloc0:26 := len 1 bytes, |0x0|
main:tmp___32:21622 := len 4 bytes, |0x8|3 times 0x0|
main:tmp___40:22797 := len 4 bytes, |0x1|3 times 0x0|
calloc0:27 := len 2096 bytes, |2096 times 0x0|
calloc0:28 := len 2096 bytes, |2096 times 0x0|
calloc0:29 := len 2096 bytes, |2096 times 0x0|
calloc0:30 := len 2096 bytes, |2096 times 0x0|
calloc0:31 := len 2096 bytes, |2096 times 0x0|
main:tmp___32:21622:1 := len 4 bytes, |0x6|3 times 0x0|
invoke_work_1:tmp:21313 := len 4 bytes, |0x1|3 times 0x0|
main:tmp___32:21622:2 := len 4 bytes, |0x2|3 times 0x0|
main:tmp___35:21999 := len 4 bytes, |4 times 0x0|
ldv_undef_int:tmp:5530 := len 4 bytes, |4 times 0x1|
main:tmp___32:21622:3 := len 4 bytes, |0x1|3 times 0x0|
main:tmp___34:21646 := len 4 bytes, |0x12|3 times 0x0|
main:tmp___32:21622:4 := len 4 bytes, |0x4|3 times 0x0|
main:tmp___32:21622:5 := len 4 bytes, |0x5|3 times 0x0|
main:tmp___38:22408 := len 4 bytes, |4 times 0x0|
 -- ---- --
INFO: Total time elapsed: 520.286355019
