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--char--ipmi--ipmi_msghandler.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.: 237 207 1921 14709
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.554088115692
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'tasklet_kill' (function is undefined)
Removed calls to 'synchronize_sched' (function is undefined)
Removed calls to '__list_add_rcu' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'driver_unregister' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function mod_timer as symbolic
Defining function driver_register as symbolic
Defining function printk as symbolic
Defining function proc_mkdir as symbolic
Defining function atomic_notifier_chain_register as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Defining function rcu_is_watching as symbolic
Removed calls to '__tasklet_schedule' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Defining function kstrdup as symbolic
Defining function proc_create_data as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'tasklet_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'put_device' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Removed calls to 'remove_proc_entry' (function is undefined)
Defining function snprintf as symbolic
Defining function platform_device_register as symbolic
Defining function sysfs_create_link as symbolic
Defining function kasprintf as symbolic
Removed calls to 'sysfs_remove_link' (function is undefined)
Removed calls to 'platform_device_unregister' (function is undefined)
Defining function driver_find_device as symbolic
Defining function sprintf as symbolic
Defining function schedule_timeout as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Defining function PDE_DATA as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Defining function seq_putc as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'proc_remove' (function is undefined)
Defining function atomic_notifier_chain_unregister as symbolic
Defining function del_timer_sync as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strlen
  strncpy
  __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.626216888428
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 344 162 1122 11451
INFO: Starting verification
KLEE: WARNING ONCE: function "ipmi_smi_watcher_register" has inline asm
KLEE: WARNING ONCE: function "kref_get" has inline asm
KLEE: WARNING ONCE: function "ipmi_free_recv_msg" has inline asm
KLEE: WARNING ONCE: function "ipmi_create_user" has inline asm
KLEE: WARNING ONCE: function "ipmi_timeout" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock" has inline asm
KLEE: WARNING ONCE: function "ipmi_alloc_smi_msg" has inline asm
KLEE: WARNING ONCE: function "deliver_response" has inline asm
KLEE: WARNING ONCE: function "tasklet_schedule" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "free_smi_msg" has inline asm
KLEE: WARNING ONCE: function "ipmi_destroy_user" has inline asm
KLEE: WARNING ONCE: function "ipmi_set_gets_events" has inline asm
KLEE: WARNING ONCE: function "ipmi_register_for_cmd" has inline asm
KLEE: WARNING ONCE: function "ipmi_unregister_for_cmd" has inline asm
KLEE: WARNING ONCE: function "i_ipmi_request" has inline asm
KLEE: WARNING ONCE: function "ipmi_alloc_recv_msg" has inline asm
KLEE: WARNING ONCE: function "free_recv_msg" has inline asm
KLEE: WARNING ONCE: function "handle_new_recv_msgs" has inline asm
KLEE: WARNING ONCE: function "handle_one_recv_msg" has inline asm
KLEE: WARNING ONCE: function "ipmi_register_smi" has inline asm
KLEE: WARNING ONCE: function "ipmi_bmc_unregister" has inline asm
KLEE: WARNING ONCE: function "ipmi_unregister_smi" has inline asm
KLEE: WARNING ONCE: function "ipmi_smi_msg_received" has inline asm
KLEE: WARNING ONCE: function "ipmi_panic_request_and_wait" has inline asm
KLEE: WARNING ONCE: function "dummy_smi_done_handler" has inline asm
KLEE: WARNING ONCE: function "dummy_recv_done_handler" has inline asm
KLEE: WARNING ONCE: function "main" 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_845c5d7e-c14e-434c-ac16-f2e970f16790/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7085: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7103: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7121: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:6977: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:6995: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7013: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7067: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:9560: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7140: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7031: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16426 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 17109 states (over memory cap)
KLEE: WARNING: killing 17854 states (over memory cap)
KLEE: WARNING: killing 16170 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:3708: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16134 states (over memory cap)
KLEE: WARNING: killing 17013 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:3865: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16650 states (over memory cap)
KLEE: WARNING: killing 17074 states (over memory cap)
KLEE: WARNING: killing 16588 states (over memory cap)
KLEE: WARNING: killing 18109 states (over memory cap)
KLEE: WARNING: killing 17686 states (over memory cap)
KLEE: WARNING: killing 18700 states (over memory cap)
KLEE: WARNING: killing 19904 states (over memory cap)
KLEE: WARNING: killing 19884 states (over memory cap)
KLEE: WARNING: killing 20244 states (over memory cap)
KLEE: WARNING: killing 21445 states (over memory cap)
KLEE: WARNING: killing 20907 states (over memory cap)
KLEE: WARNING: killing 21150 states (over memory cap)
KLEE: WARNING: killing 18995 states (over memory cap)
KLEE: WARNING: killing 20259 states (over memory cap)
KLEE: WARNING: killing 19650 states (over memory cap)
KLEE: WARNING: killing 19117 states (over memory cap)
KLEE: WARNING: killing 20123 states (over memory cap)
KLEE: WARNING: killing 19266 states (over memory cap)
KLEE: WARNING: killing 19366 states (over memory cap)
KLEE: WARNING: killing 18889 states (over memory cap)
KLEE: WARNING: killing 19444 states (over memory cap)
KLEE: WARNING: killing 19986 states (over memory cap)
KLEE: WARNING: killing 20415 states (over memory cap)
KLEE: WARNING: killing 20260 states (over memory cap)
KLEE: WARNING: killing 19098 states (over memory cap)
KLEE: WARNING: killing 20656 states (over memory cap)
KLEE: WARNING: killing 19739 states (over memory cap)
KLEE: WARNING: killing 19971 states (over memory cap)
KLEE: WARNING: killing 18810 states (over memory cap)
KLEE: WARNING: killing 19986 states (over memory cap)
KLEE: WARNING: killing 19393 states (over memory cap)
KLEE: WARNING: killing 20698 states (over memory cap)
KLEE: WARNING: killing 20742 states (over memory cap)
KLEE: WARNING: killing 20470 states (over memory cap)
KLEE: WARNING: killing 20447 states (over memory cap)
KLEE: WARNING: killing 19795 states (over memory cap)
KLEE: WARNING: killing 19965 states (over memory cap)
KLEE: WARNING: killing 18622 states (over memory cap)
KLEE: WARNING: killing 20915 states (over memory cap)
KLEE: WARNING: killing 20330 states (over memory cap)
KLEE: WARNING: killing 19504 states (over memory cap)
KLEE: WARNING: killing 20791 states (over memory cap)
KLEE: WARNING: killing 20021 states (over memory cap)
KLEE: WARNING: killing 19558 states (over memory cap)
KLEE: WARNING: killing 19920 states (over memory cap)
KLEE: WARNING: killing 20327 states (over memory cap)
KLEE: WARNING: killing 21358 states (over memory cap)
KLEE: WARNING: killing 19668 states (over memory cap)
KLEE: WARNING: killing 19209 states (over memory cap)
KLEE: WARNING: killing 19065 states (over memory cap)
KLEE: WARNING: killing 20156 states (over memory cap)
KLEE: WARNING: killing 19773 states (over memory cap)
KLEE: WARNING: killing 20487 states (over memory cap)
KLEE: WARNING: killing 20841 states (over memory cap)
KLEE: WARNING: killing 19906 states (over memory cap)
KLEE: WARNING: killing 19820 states (over memory cap)
KLEE: WARNING: killing 19613 states (over memory cap)
KLEE: WARNING: killing 19966 states (over memory cap)
KLEE: WARNING: killing 20556 states (over memory cap)
KLEE: WARNING: killing 19611 states (over memory cap)
KLEE: WARNING: killing 20391 states (over memory cap)
KLEE: WARNING: killing 20128 states (over memory cap)
KLEE: WARNING: killing 20222 states (over memory cap)
KLEE: WARNING: killing 19472 states (over memory cap)
KLEE: WARNING: killing 18590 states (over memory cap)
KLEE: WARNING: killing 19184 states (over memory cap)
KLEE: WARNING: killing 20623 states (over memory cap)
KLEE: WARNING: killing 19996 states (over memory cap)
KLEE: WARNING: killing 20152 states (over memory cap)
KLEE: WARNING: killing 20329 states (over memory cap)
KLEE: WARNING: killing 20002 states (over memory cap)
KLEE: WARNING: killing 19919 states (over memory cap)
KLEE: WARNING: killing 19842 states (over memory cap)
KLEE: WARNING: killing 20316 states (over memory cap)
KLEE: WARNING: killing 21265 states (over memory cap)
KLEE: WARNING: killing 19503 states (over memory cap)
KLEE: WARNING: killing 19967 states (over memory cap)
KLEE: WARNING: killing 20853 states (over memory cap)
KLEE: WARNING: killing 19201 states (over memory cap)
KLEE: WARNING: killing 20030 states (over memory cap)
KLEE: WARNING: killing 20133 states (over memory cap)
KLEE: WARNING: killing 19519 states (over memory cap)
KLEE: WARNING: killing 19015 states (over memory cap)
KLEE: WARNING: killing 19651 states (over memory cap)
KLEE: WARNING: killing 20230 states (over memory cap)
KLEE: WARNING: killing 20813 states (over memory cap)
KLEE: WARNING: killing 20492 states (over memory cap)
KLEE: WARNING: killing 19577 states (over memory cap)
KLEE: WARNING: killing 20336 states (over memory cap)
KLEE: WARNING: killing 20512 states (over memory cap)
KLEE: WARNING: killing 20443 states (over memory cap)
KLEE: WARNING: killing 20069 states (over memory cap)
KLEE: WARNING: killing 20052 states (over memory cap)
KLEE: WARNING: killing 19192 states (over memory cap)
KLEE: WARNING: killing 20017 states (over memory cap)
KLEE: WARNING: killing 20295 states (over memory cap)
KLEE: WARNING: killing 19981 states (over memory cap)
KLEE: WARNING: killing 19725 states (over memory cap)
KLEE: WARNING: killing 19407 states (over memory cap)
KLEE: WARNING: killing 19679 states (over memory cap)
KLEE: WARNING: killing 20073 states (over memory cap)
KLEE: WARNING: killing 20182 states (over memory cap)
KLEE: WARNING: killing 20108 states (over memory cap)
KLEE: WARNING: killing 19972 states (over memory cap)
KLEE: WARNING: killing 19793 states (over memory cap)
KLEE: WARNING: killing 20659 states (over memory cap)
KLEE: WARNING: killing 19582 states (over memory cap)
KLEE: WARNING: killing 20100 states (over memory cap)
KLEE: WARNING: killing 19252 states (over memory cap)
KLEE: WARNING: killing 19702 states (over memory cap)
klee: /var/xchalup4/symbiotic/klee/include/klee/Internal/ADT/DiscretePDF.inc:116: void klee::DiscretePDF<T>::remove(T) [with T = klee::ExecutionState*]: Assertion `0 && "remove: argument(item) not in tree"' failed.
KLEE: output directory is "/tmp/symbiotic-9b3xZI/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "ipmi_smi_watcher_register" has inline asm
KLEE: WARNING ONCE: function "kref_get" has inline asm
KLEE: WARNING ONCE: function "ipmi_free_recv_msg" has inline asm
KLEE: WARNING ONCE: function "ipmi_create_user" has inline asm
KLEE: WARNING ONCE: function "ipmi_timeout" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock" has inline asm
KLEE: WARNING ONCE: function "ipmi_alloc_smi_msg" has inline asm
KLEE: WARNING ONCE: function "deliver_response" has inline asm
KLEE: WARNING ONCE: function "tasklet_schedule" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "free_smi_msg" has inline asm
KLEE: WARNING ONCE: function "ipmi_destroy_user" has inline asm
KLEE: WARNING ONCE: function "ipmi_set_gets_events" has inline asm
KLEE: WARNING ONCE: function "ipmi_register_for_cmd" has inline asm
KLEE: WARNING ONCE: function "ipmi_unregister_for_cmd" has inline asm
KLEE: WARNING ONCE: function "i_ipmi_request" has inline asm
KLEE: WARNING ONCE: function "ipmi_alloc_recv_msg" has inline asm
KLEE: WARNING ONCE: function "free_recv_msg" has inline asm
KLEE: WARNING ONCE: function "handle_new_recv_msgs" has inline asm
KLEE: WARNING ONCE: function "handle_one_recv_msg" has inline asm
KLEE: WARNING ONCE: function "ipmi_register_smi" has inline asm
KLEE: WARNING ONCE: function "ipmi_bmc_unregister" has inline asm
KLEE: WARNING ONCE: function "ipmi_unregister_smi" has inline asm
KLEE: WARNING ONCE: function "ipmi_smi_msg_received" has inline asm
KLEE: WARNING ONCE: function "ipmi_panic_request_and_wait" has inline asm
KLEE: WARNING ONCE: function "dummy_smi_done_handler" has inline asm
KLEE: WARNING ONCE: function "dummy_recv_done_handler" has inline asm
KLEE: WARNING ONCE: function "main" 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_845c5d7e-c14e-434c-ac16-f2e970f16790/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7085: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7103: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7121: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:6977: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:6995: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7013: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7067: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:9560: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7140: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7031: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16426 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 17109 states (over memory cap)
KLEE: WARNING: killing 17854 states (over memory cap)
KLEE: WARNING: killing 16170 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:3708: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16134 states (over memory cap)
KLEE: WARNING: killing 17013 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-9b3xZI/linux-4.2-rc1.tar.xz-08_1a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:3865: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16650 states (over memory cap)
KLEE: WARNING: killing 17074 states (over memory cap)
KLEE: WARNING: killing 16588 states (over memory cap)
KLEE: WARNING: killing 18109 states (over memory cap)
KLEE: WARNING: killing 17686 states (over memory cap)
KLEE: WARNING: killing 18700 states (over memory cap)
KLEE: WARNING: killing 19904 states (over memory cap)
KLEE: WARNING: killing 19884 states (over memory cap)
KLEE: WARNING: killing 20244 states (over memory cap)
KLEE: WARNING: killing 21445 states (over memory cap)
KLEE: WARNING: killing 20907 states (over memory cap)
KLEE: WARNING: killing 21150 states (over memory cap)
KLEE: WARNING: killing 18995 states (over memory cap)
KLEE: WARNING: killing 20259 states (over memory cap)
KLEE: WARNING: killing 19650 states (over memory cap)
KLEE: WARNING: killing 19117 states (over memory cap)
KLEE: WARNING: killing 20123 states (over memory cap)
KLEE: WARNING: killing 19266 states (over memory cap)
KLEE: WARNING: killing 19366 states (over memory cap)
KLEE: WARNING: killing 18889 states (over memory cap)
KLEE: WARNING: killing 19444 states (over memory cap)
KLEE: WARNING: killing 19986 states (over memory cap)
KLEE: WARNING: killing 20415 states (over memory cap)
KLEE: WARNING: killing 20260 states (over memory cap)
KLEE: WARNING: killing 19098 states (over memory cap)
KLEE: WARNING: killing 20656 states (over memory cap)
KLEE: WARNING: killing 19739 states (over memory cap)
KLEE: WARNING: killing 19971 states (over memory cap)
KLEE: WARNING: killing 18810 states (over memory cap)
KLEE: WARNING: killing 19986 states (over memory cap)
KLEE: WARNING: killing 19393 states (over memory cap)
KLEE: WARNING: killing 20698 states (over memory cap)
KLEE: WARNING: killing 20742 states (over memory cap)
KLEE: WARNING: killing 20470 states (over memory cap)
KLEE: WARNING: killing 20447 states (over memory cap)
KLEE: WARNING: killing 19795 states (over memory cap)
KLEE: WARNING: killing 19965 states (over memory cap)
KLEE: WARNING: killing 18622 states (over memory cap)
KLEE: WARNING: killing 20915 states (over memory cap)
KLEE: WARNING: killing 20330 states (over memory cap)
KLEE: WARNING: killing 19504 states (over memory cap)
KLEE: WARNING: killing 20791 states (over memory cap)
KLEE: WARNING: killing 20021 states (over memory cap)
KLEE: WARNING: killing 19558 states (over memory cap)
KLEE: WARNING: killing 19920 states (over memory cap)
KLEE: WARNING: killing 20327 states (over memory cap)
KLEE: WARNING: killing 21358 states (over memory cap)
KLEE: WARNING: killing 19668 states (over memory cap)
KLEE: WARNING: killing 19209 states (over memory cap)
KLEE: WARNING: killing 19065 states (over memory cap)
KLEE: WARNING: killing 20156 states (over memory cap)
KLEE: WARNING: killing 19773 states (over memory cap)
KLEE: WARNING: killing 20487 states (over memory cap)
KLEE: WARNING: killing 20841 states (over memory cap)
KLEE: WARNING: killing 19906 states (over memory cap)
KLEE: WARNING: killing 19820 states (over memory cap)
KLEE: WARNING: killing 19613 states (over memory cap)
KLEE: WARNING: killing 19966 states (over memory cap)
KLEE: WARNING: killing 20556 states (over memory cap)
KLEE: WARNING: killing 19611 states (over memory cap)
KLEE: WARNING: killing 20391 states (over memory cap)
KLEE: WARNING: killing 20128 states (over memory cap)
KLEE: WARNING: killing 20222 states (over memory cap)
KLEE: WARNING: killing 19472 states (over memory cap)
KLEE: WARNING: killing 18590 states (over memory cap)
KLEE: WARNING: killing 19184 states (over memory cap)
KLEE: WARNING: killing 20623 states (over memory cap)
KLEE: WARNING: killing 19996 states (over memory cap)
KLEE: WARNING: killing 20152 states (over memory cap)
KLEE: WARNING: killing 20329 states (over memory cap)
KLEE: WARNING: killing 20002 states (over memory cap)
KLEE: WARNING: killing 19919 states (over memory cap)
KLEE: WARNING: killing 19842 states (over memory cap)
KLEE: WARNING: killing 20316 states (over memory cap)
KLEE: WARNING: killing 21265 states (over memory cap)
KLEE: WARNING: killing 19503 states (over memory cap)
KLEE: WARNING: killing 19967 states (over memory cap)
KLEE: WARNING: killing 20853 states (over memory cap)
KLEE: WARNING: killing 19201 states (over memory cap)
KLEE: WARNING: killing 20030 states (over memory cap)
KLEE: WARNING: killing 20133 states (over memory cap)
KLEE: WARNING: killing 19519 states (over memory cap)
KLEE: WARNING: killing 19015 states (over memory cap)
KLEE: WARNING: killing 19651 states (over memory cap)
KLEE: WARNING: killing 20230 states (over memory cap)
KLEE: WARNING: killing 20813 states (over memory cap)
KLEE: WARNING: killing 20492 states (over memory cap)
KLEE: WARNING: killing 19577 states (over memory cap)
KLEE: WARNING: killing 20336 states (over memory cap)
KLEE: WARNING: killing 20512 states (over memory cap)
KLEE: WARNING: killing 20443 states (over memory cap)
KLEE: WARNING: killing 20069 states (over memory cap)
KLEE: WARNING: killing 20052 states (over memory cap)
KLEE: WARNING: killing 19192 states (over memory cap)
KLEE: WARNING: killing 20017 states (over memory cap)
KLEE: WARNING: killing 20295 states (over memory cap)
KLEE: WARNING: killing 19981 states (over memory cap)
KLEE: WARNING: killing 19725 states (over memory cap)
KLEE: WARNING: killing 19407 states (over memory cap)
KLEE: WARNING: killing 19679 states (over memory cap)
KLEE: WARNING: killing 20073 states (over memory cap)
KLEE: WARNING: killing 20182 states (over memory cap)
KLEE: WARNING: killing 20108 states (over memory cap)
KLEE: WARNING: killing 19972 states (over memory cap)
KLEE: WARNING: killing 19793 states (over memory cap)
KLEE: WARNING: killing 20659 states (over memory cap)
KLEE: WARNING: killing 19582 states (over memory cap)
KLEE: WARNING: killing 20100 states (over memory cap)
KLEE: WARNING: killing 19252 states (over memory cap)
KLEE: WARNING: killing 19702 states (over memory cap)
klee: /var/xchalup4/symbiotic/klee/include/klee/Internal/ADT/DiscretePDF.inc:116: void klee::DiscretePDF<T>::remove(T) [with T = klee::ExecutionState*]: Assertion `0 && "remove: argument(item) not in tree"' failed.
0  klee            0x00000000012fcca8 llvm::sys::PrintStackTrace(llvm::raw_ostream&) + 56
1  klee            0x00000000012fac7e llvm::sys::RunSignalHandlers() + 62
2  klee            0x00000000012fadcc
3  libpthread.so.0 0x00007f1709765390
4  libc.so.6       0x00007f1708b1e428 gsignal + 56
5  libc.so.6       0x00007f1708b2002a abort + 362
6  libc.so.6       0x00007f1708b16bd7
7  libc.so.6       0x00007f1708b16c82
8  klee            0x000000000061be59 klee::DiscretePDF<klee::ExecutionState*>::remove(klee::ExecutionState*) + 73
9  klee            0x00000000006195f1 klee::WeightedRandomSearcher::update(klee::ExecutionState*, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&) + 241
10 klee            0x0000000000617416 klee::InterleavedSearcher::update(klee::ExecutionState*, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&) + 54
11 klee            0x00000000005cecfe klee::Executor::updateStates(klee::ExecutionState*) + 46
12 klee            0x00000000005da8eb klee::Executor::run(klee::ExecutionState&) + 2155
13 klee            0x00000000005daeef klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1391
14 klee            0x0000000000593c63 main + 8867
15 libc.so.6       0x00007f1708b09830 __libc_start_main + 240
16 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 543.669130087
