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--staging--lustre--lnet--selftest--lnet_selftest.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.: 717 456 6990 52544
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.65824389458
Removed calls to 'lbug_with_loc' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Defining function libcfs_debug_msg as symbolic
Defining function vmalloc as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Defining function get_seconds as symbolic
Removed calls to '__copy_to_user_overflow' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function _copy_to_user as symbolic
Removed calls to '__list_add' (function is undefined)
Defining function libcfs_id2str as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Defining function schedule_timeout as symbolic
Defining function libcfs_nid2str as symbolic
Removed calls to 'cfs_wi_schedule' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function lnet_cpt_of_nid as symbolic
Removed calls to 'schedule' (function is undefined)
Removed calls to 'cfs_wi_exit' (function is undefined)
Defining function LNetMDUnlink as symbolic
Defining function LNetMDBind as symbolic
Defining function LNetPut as symbolic
Defining function LNetGet as symbolic
Defining function LNetMEAttach as symbolic
Defining function LNetMDAttach as symbolic
Defining function LNetMEUnlink as symbolic
Defining function alloc_pages_current as symbolic
Defining function LNetGetId as symbolic
Defining function _copy_from_user as symbolic
Removed calls to '__mutex_init' (function is undefined)
Defining function libcfs_register_ioctl as symbolic
Defining function cfs_percpt_number as symbolic
Removed calls to 'cfs_percpt_free' (function is undefined)
Defining function cfs_wi_deschedule as symbolic
Defining function cfs_percpt_alloc as symbolic
Defining function cfs_cpt_number as symbolic
Defining function cfs_cpt_spread_node as symbolic
Defining function __kmalloc_node as symbolic
Defining function libcfs_deregister_ioctl as symbolic
Defining function mutex_trylock as symbolic
Defining function strlcpy as symbolic
Defining function vmalloc_node as symbolic
Defining function __alloc_pages_nodemask as symbolic
Removed calls to 'lnet_counters_get' (function is undefined)
Defining function current_kernel_time as symbolic
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function cfs_block_allsigs as symbolic
Defining function LNetNIInit as symbolic
Defining function LNetEQAlloc as symbolic
Defining function LNetSetLazyPortal as symbolic
Defining function LNetClearLazyPortal as symbolic
Defining function LNetEQFree as symbolic
Defining function LNetNIFini as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'cfs_wi_sched_destroy' (function is undefined)
Defining function cfs_wi_sched_create as symbolic
Defining function cfs_cpt_weight as symbolic
Linked our definitions to these undefined functions:
  strcpy
  strlen
  strncmp
  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: 1.92722392082
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 840 366 3983 40260
INFO: Starting verification
KLEE: WARNING ONCE: function "lstcon_ioctl_entry" has inline asm
KLEE: WARNING ONCE: function "lstcon_session_info" has inline asm
KLEE: WARNING ONCE: function "lstcon_group_info" has inline asm
KLEE: WARNING ONCE: function "lstcon_batch_add" has inline asm
KLEE: WARNING ONCE: function "lstcon_batch_info" has inline asm
KLEE: WARNING ONCE: function "lstcon_test_add" has inline asm
KLEE: WARNING ONCE: function "lstcon_group_alloc" has inline asm
KLEE: WARNING ONCE: function "lstcon_group_put" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_trans_destroy" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_put" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_post" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_trans_prep" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_prep" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_init" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_done" has inline asm
KLEE: WARNING ONCE: function "srpc_create_client_rpc" has inline asm
KLEE: WARNING ONCE: function "lstcon_ndlink_release" has inline asm
KLEE: WARNING ONCE: function "lstcon_node_put" has inline asm
KLEE: WARNING ONCE: function "lstcon_ndlink_find" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_cleanup_wait" has inline asm
KLEE: WARNING ONCE: function "lstcon_batch_destroy" has inline asm
KLEE: WARNING ONCE: function "lstcon_console_init" has inline asm
KLEE: WARNING ONCE: function "srpc_add_service" has inline asm
KLEE: WARNING ONCE: function "srpc_service_add_buffers" has inline asm
KLEE: WARNING ONCE: function "srpc_wait_service_shutdown" has inline asm
KLEE: WARNING ONCE: function "srpc_service_fini" has inline asm
KLEE: WARNING ONCE: function "srpc_add_buffer" has inline asm
KLEE: WARNING ONCE: function "srpc_service_post_buffer" has inline asm
KLEE: WARNING ONCE: function "lstcon_console_fini" has inline asm
KLEE: WARNING ONCE: function "sfw_make_session" has inline asm
KLEE: WARNING ONCE: function "sfw_deactivate_session" has inline asm
KLEE: WARNING ONCE: function "sfw_destroy_session" has inline asm
KLEE: WARNING ONCE: function "sfw_destroy_test_instance" has inline asm
KLEE: WARNING ONCE: function "sfw_test_rpc_done" has inline asm
KLEE: WARNING ONCE: function "sfw_test_unit_done" has inline asm
KLEE: WARNING ONCE: function "srpc_free_bulk" has inline asm
KLEE: WARNING ONCE: function "srpc_alloc_bulk" has inline asm
KLEE: WARNING ONCE: function "brw_client_done_rpc" has inline asm
KLEE: WARNING ONCE: function "sfw_register_test" has inline asm
KLEE: WARNING ONCE: function "ping_client_done_rpc" has inline asm
KLEE: WARNING ONCE: function "sfw_handle_server_rpc" has inline asm
KLEE: WARNING ONCE: function "sfw_shutdown" has inline asm
KLEE: WARNING ONCE: function "srpc_wait_service_shutdown___0" has inline asm
KLEE: WARNING ONCE: function "sfw_add_test" has inline asm
KLEE: WARNING ONCE: function "stt_shutdown" has inline asm
KLEE: WARNING ONCE: function "srpc_server_rpc_done" has inline asm
KLEE: WARNING ONCE: function "srpc_startup" has inline asm
KLEE: WARNING ONCE: function "srpc_lnet_ev_handler" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "lnet_selftest_fini" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_fa682495-43dd-48aa-936f-30f0f942275c/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-0lz1xF/linux-4.2-rc1.tar.xz-32_7a-drivers--staging--lustre--lnet--selftest--lnet_selftest.ko-entry_point_true-unreach-call.cil.out.c:21629: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 5422 states (over memory cap)
KLEE: WARNING: killing 6231 states (over memory cap)
KLEE: WARNING: killing 6404 states (over memory cap)
KLEE: WARNING: killing 6574 states (over memory cap)
KLEE: WARNING: killing 6698 states (over memory cap)
KLEE: WARNING: killing 4648 states (over memory cap)
KLEE: WARNING: killing 6658 states (over memory cap)
KLEE: WARNING: killing 4850 states (over memory cap)
KLEE: WARNING: killing 4653 states (over memory cap)
KLEE: WARNING: killing 4911 states (over memory cap)
KLEE: WARNING: killing 4853 states (over memory cap)
KLEE: WARNING: killing 4930 states (over memory cap)
KLEE: WARNING: killing 4777 states (over memory cap)
KLEE: WARNING: killing 4807 states (over memory cap)
KLEE: WARNING: killing 4885 states (over memory cap)
KLEE: WARNING: killing 4736 states (over memory cap)
KLEE: WARNING: killing 4810 states (over memory cap)
KLEE: WARNING: killing 4706 states (over memory cap)
KLEE: WARNING: killing 4779 states (over memory cap)
KLEE: WARNING: killing 4633 states (over memory cap)
KLEE: WARNING: killing 4707 states (over memory cap)
KLEE: WARNING: killing 4741 states (over memory cap)
KLEE: WARNING: killing 4730 states (over memory cap)
KLEE: WARNING: killing 4629 states (over memory cap)
KLEE: WARNING: killing 4578 states (over memory cap)
KLEE: WARNING: killing 4698 states (over memory cap)
KLEE: WARNING: killing 4731 states (over memory cap)
KLEE: WARNING: killing 4677 states (over memory cap)
KLEE: WARNING: killing 4579 states (over memory cap)
KLEE: WARNING: killing 4524 states (over memory cap)
KLEE: WARNING: killing 4732 states (over memory cap)
KLEE: WARNING: killing 4638 states (over memory cap)
KLEE: WARNING: killing 6302 states (over memory cap)
KLEE: WARNING: killing 4652 states (over memory cap)
KLEE: WARNING: killing 4772 states (over memory cap)
KLEE: WARNING: killing 4636 states (over memory cap)
KLEE: WARNING: killing 4624 states (over memory cap)
KLEE: WARNING: killing 4529 states (over memory cap)
KLEE: WARNING: killing 4650 states (over memory cap)
KLEE: WARNING: killing 4640 states (over memory cap)
KLEE: WARNING: killing 4418 states (over memory cap)
KLEE: WARNING: killing 4496 states (over memory cap)
KLEE: WARNING: killing 4614 states (over memory cap)
KLEE: WARNING: killing 4479 states (over memory cap)
KLEE: WARNING: killing 4343 states (over memory cap)
KLEE: WARNING: killing 4546 states (over memory cap)
KLEE: WARNING: killing 4449 states (over memory cap)
KLEE: WARNING: killing 4443 states (over memory cap)
KLEE: WARNING: killing 4522 states (over memory cap)
KLEE: WARNING: killing 4431 states (over memory cap)
KLEE: WARNING: killing 4592 states (over memory cap)
KLEE: WARNING: killing 4418 states (over memory cap)
KLEE: WARNING: killing 4579 states (over memory cap)
KLEE: WARNING: killing 4612 states (over memory cap)
KLEE: WARNING: killing 4523 states (over memory cap)
KLEE: WARNING: killing 4391 states (over memory cap)
KLEE: WARNING: killing 4299 states (over memory cap)
KLEE: WARNING: killing 4373 states (over memory cap)
KLEE: WARNING: killing 4449 states (over memory cap)
KLEE: WARNING: killing 4729 states (over memory cap)
KLEE: WARNING: killing 4686 states (over memory cap)
KLEE: WARNING: killing 4477 states (over memory cap)
KLEE: WARNING: killing 4553 states (over memory cap)
KLEE: WARNING: killing 4421 states (over memory cap)
KLEE: WARNING: killing 4247 states (over memory cap)
KLEE: WARNING: killing 4441 states (over memory cap)
KLEE: WARNING: killing 4517 states (over memory cap)
KLEE: WARNING: killing 4469 states (over memory cap)
KLEE: WARNING: killing 4666 states (over memory cap)
KLEE: WARNING: killing 4538 states (over memory cap)
KLEE: WARNING: killing 4450 states (over memory cap)
KLEE: WARNING: killing 4447 states (over memory cap)
KLEE: WARNING: killing 4558 states (over memory cap)
KLEE: WARNING: killing 4430 states (over memory cap)
KLEE: WARNING: killing 4584 states (over memory cap)
KLEE: WARNING: killing 4576 states (over memory cap)
KLEE: WARNING: killing 4612 states (over memory cap)
KLEE: WARNING: killing 4365 states (over memory cap)
KLEE: WARNING: killing 4360 states (over memory cap)
KLEE: WARNING: killing 4469 states (over memory cap)
KLEE: WARNING: killing 4465 states (over memory cap)
KLEE: WARNING: killing 4614 states (over memory cap)
KLEE: WARNING: killing 4606 states (over memory cap)
KLEE: WARNING: killing 4639 states (over memory cap)
KLEE: WARNING: killing 4433 states (over memory cap)
KLEE: WARNING: killing 4508 states (over memory cap)
KLEE: WARNING: killing 4542 states (over memory cap)
KLEE: WARNING: killing 4535 states (over memory cap)
KLEE: WARNING: killing 4409 states (over memory cap)
KLEE: WARNING: killing 4598 states (over memory cap)
KLEE: WARNING: killing 4512 states (over memory cap)
KLEE: WARNING: killing 4469 states (over memory cap)
KLEE: WARNING: killing 4423 states (over memory cap)
KLEE: WARNING: killing 4494 states (over memory cap)
KLEE: WARNING: killing 4529 states (over memory cap)
KLEE: WARNING: killing 4645 states (over memory cap)
KLEE: WARNING: killing 4440 states (over memory cap)
KLEE: WARNING: killing 4355 states (over memory cap)
KLEE: WARNING: killing 4505 states (over memory cap)
KLEE: WARNING: killing 4576 states (over memory cap)
KLEE: WARNING: killing 4413 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-0lz1xF/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "lstcon_ioctl_entry" has inline asm
KLEE: WARNING ONCE: function "lstcon_session_info" has inline asm
KLEE: WARNING ONCE: function "lstcon_group_info" has inline asm
KLEE: WARNING ONCE: function "lstcon_batch_add" has inline asm
KLEE: WARNING ONCE: function "lstcon_batch_info" has inline asm
KLEE: WARNING ONCE: function "lstcon_test_add" has inline asm
KLEE: WARNING ONCE: function "lstcon_group_alloc" has inline asm
KLEE: WARNING ONCE: function "lstcon_group_put" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_trans_destroy" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_put" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_post" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_trans_prep" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_prep" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_init" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_done" has inline asm
KLEE: WARNING ONCE: function "srpc_create_client_rpc" has inline asm
KLEE: WARNING ONCE: function "lstcon_ndlink_release" has inline asm
KLEE: WARNING ONCE: function "lstcon_node_put" has inline asm
KLEE: WARNING ONCE: function "lstcon_ndlink_find" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_cleanup_wait" has inline asm
KLEE: WARNING ONCE: function "lstcon_batch_destroy" has inline asm
KLEE: WARNING ONCE: function "lstcon_console_init" has inline asm
KLEE: WARNING ONCE: function "srpc_add_service" has inline asm
KLEE: WARNING ONCE: function "srpc_service_add_buffers" has inline asm
KLEE: WARNING ONCE: function "srpc_wait_service_shutdown" has inline asm
KLEE: WARNING ONCE: function "srpc_service_fini" has inline asm
KLEE: WARNING ONCE: function "srpc_add_buffer" has inline asm
KLEE: WARNING ONCE: function "srpc_service_post_buffer" has inline asm
KLEE: WARNING ONCE: function "lstcon_console_fini" has inline asm
KLEE: WARNING ONCE: function "sfw_make_session" has inline asm
KLEE: WARNING ONCE: function "sfw_deactivate_session" has inline asm
KLEE: WARNING ONCE: function "sfw_destroy_session" has inline asm
KLEE: WARNING ONCE: function "sfw_destroy_test_instance" has inline asm
KLEE: WARNING ONCE: function "sfw_test_rpc_done" has inline asm
KLEE: WARNING ONCE: function "sfw_test_unit_done" has inline asm
KLEE: WARNING ONCE: function "srpc_free_bulk" has inline asm
KLEE: WARNING ONCE: function "srpc_alloc_bulk" has inline asm
KLEE: WARNING ONCE: function "brw_client_done_rpc" has inline asm
KLEE: WARNING ONCE: function "sfw_register_test" has inline asm
KLEE: WARNING ONCE: function "ping_client_done_rpc" has inline asm
KLEE: WARNING ONCE: function "sfw_handle_server_rpc" has inline asm
KLEE: WARNING ONCE: function "sfw_shutdown" has inline asm
KLEE: WARNING ONCE: function "srpc_wait_service_shutdown___0" has inline asm
KLEE: WARNING ONCE: function "sfw_add_test" has inline asm
KLEE: WARNING ONCE: function "stt_shutdown" has inline asm
KLEE: WARNING ONCE: function "srpc_server_rpc_done" has inline asm
KLEE: WARNING ONCE: function "srpc_startup" has inline asm
KLEE: WARNING ONCE: function "srpc_lnet_ev_handler" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "lnet_selftest_fini" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_fa682495-43dd-48aa-936f-30f0f942275c/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-0lz1xF/linux-4.2-rc1.tar.xz-32_7a-drivers--staging--lustre--lnet--selftest--lnet_selftest.ko-entry_point_true-unreach-call.cil.out.c:21629: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 5422 states (over memory cap)
KLEE: WARNING: killing 6231 states (over memory cap)
KLEE: WARNING: killing 6404 states (over memory cap)
KLEE: WARNING: killing 6574 states (over memory cap)
KLEE: WARNING: killing 6698 states (over memory cap)
KLEE: WARNING: killing 4648 states (over memory cap)
KLEE: WARNING: killing 6658 states (over memory cap)
KLEE: WARNING: killing 4850 states (over memory cap)
KLEE: WARNING: killing 4653 states (over memory cap)
KLEE: WARNING: killing 4911 states (over memory cap)
KLEE: WARNING: killing 4853 states (over memory cap)
KLEE: WARNING: killing 4930 states (over memory cap)
KLEE: WARNING: killing 4777 states (over memory cap)
KLEE: WARNING: killing 4807 states (over memory cap)
KLEE: WARNING: killing 4885 states (over memory cap)
KLEE: WARNING: killing 4736 states (over memory cap)
KLEE: WARNING: killing 4810 states (over memory cap)
KLEE: WARNING: killing 4706 states (over memory cap)
KLEE: WARNING: killing 4779 states (over memory cap)
KLEE: WARNING: killing 4633 states (over memory cap)
KLEE: WARNING: killing 4707 states (over memory cap)
KLEE: WARNING: killing 4741 states (over memory cap)
KLEE: WARNING: killing 4730 states (over memory cap)
KLEE: WARNING: killing 4629 states (over memory cap)
KLEE: WARNING: killing 4578 states (over memory cap)
KLEE: WARNING: killing 4698 states (over memory cap)
KLEE: WARNING: killing 4731 states (over memory cap)
KLEE: WARNING: killing 4677 states (over memory cap)
KLEE: WARNING: killing 4579 states (over memory cap)
KLEE: WARNING: killing 4524 states (over memory cap)
KLEE: WARNING: killing 4732 states (over memory cap)
KLEE: WARNING: killing 4638 states (over memory cap)
KLEE: WARNING: killing 6302 states (over memory cap)
KLEE: WARNING: killing 4652 states (over memory cap)
KLEE: WARNING: killing 4772 states (over memory cap)
KLEE: WARNING: killing 4636 states (over memory cap)
KLEE: WARNING: killing 4624 states (over memory cap)
KLEE: WARNING: killing 4529 states (over memory cap)
KLEE: WARNING: killing 4650 states (over memory cap)
KLEE: WARNING: killing 4640 states (over memory cap)
KLEE: WARNING: killing 4418 states (over memory cap)
KLEE: WARNING: killing 4496 states (over memory cap)
KLEE: WARNING: killing 4614 states (over memory cap)
KLEE: WARNING: killing 4479 states (over memory cap)
KLEE: WARNING: killing 4343 states (over memory cap)
KLEE: WARNING: killing 4546 states (over memory cap)
KLEE: WARNING: killing 4449 states (over memory cap)
KLEE: WARNING: killing 4443 states (over memory cap)
KLEE: WARNING: killing 4522 states (over memory cap)
KLEE: WARNING: killing 4431 states (over memory cap)
KLEE: WARNING: killing 4592 states (over memory cap)
KLEE: WARNING: killing 4418 states (over memory cap)
KLEE: WARNING: killing 4579 states (over memory cap)
KLEE: WARNING: killing 4612 states (over memory cap)
KLEE: WARNING: killing 4523 states (over memory cap)
KLEE: WARNING: killing 4391 states (over memory cap)
KLEE: WARNING: killing 4299 states (over memory cap)
KLEE: WARNING: killing 4373 states (over memory cap)
KLEE: WARNING: killing 4449 states (over memory cap)
KLEE: WARNING: killing 4729 states (over memory cap)
KLEE: WARNING: killing 4686 states (over memory cap)
KLEE: WARNING: killing 4477 states (over memory cap)
KLEE: WARNING: killing 4553 states (over memory cap)
KLEE: WARNING: killing 4421 states (over memory cap)
KLEE: WARNING: killing 4247 states (over memory cap)
KLEE: WARNING: killing 4441 states (over memory cap)
KLEE: WARNING: killing 4517 states (over memory cap)
KLEE: WARNING: killing 4469 states (over memory cap)
KLEE: WARNING: killing 4666 states (over memory cap)
KLEE: WARNING: killing 4538 states (over memory cap)
KLEE: WARNING: killing 4450 states (over memory cap)
KLEE: WARNING: killing 4447 states (over memory cap)
KLEE: WARNING: killing 4558 states (over memory cap)
KLEE: WARNING: killing 4430 states (over memory cap)
KLEE: WARNING: killing 4584 states (over memory cap)
KLEE: WARNING: killing 4576 states (over memory cap)
KLEE: WARNING: killing 4612 states (over memory cap)
KLEE: WARNING: killing 4365 states (over memory cap)
KLEE: WARNING: killing 4360 states (over memory cap)
KLEE: WARNING: killing 4469 states (over memory cap)
KLEE: WARNING: killing 4465 states (over memory cap)
KLEE: WARNING: killing 4614 states (over memory cap)
KLEE: WARNING: killing 4606 states (over memory cap)
KLEE: WARNING: killing 4639 states (over memory cap)
KLEE: WARNING: killing 4433 states (over memory cap)
KLEE: WARNING: killing 4508 states (over memory cap)
KLEE: WARNING: killing 4542 states (over memory cap)
KLEE: WARNING: killing 4535 states (over memory cap)
KLEE: WARNING: killing 4409 states (over memory cap)
KLEE: WARNING: killing 4598 states (over memory cap)
KLEE: WARNING: killing 4512 states (over memory cap)
KLEE: WARNING: killing 4469 states (over memory cap)
KLEE: WARNING: killing 4423 states (over memory cap)
KLEE: WARNING: killing 4494 states (over memory cap)
KLEE: WARNING: killing 4529 states (over memory cap)
KLEE: WARNING: killing 4645 states (over memory cap)
KLEE: WARNING: killing 4440 states (over memory cap)
KLEE: WARNING: killing 4355 states (over memory cap)
KLEE: WARNING: killing 4505 states (over memory cap)
KLEE: WARNING: killing 4576 states (over memory cap)
KLEE: WARNING: killing 4413 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 0x00007f285f336390
4  libc.so.6       0x00007f285e6ef428 gsignal + 56
5  libc.so.6       0x00007f285e6f102a abort + 362
6  libc.so.6       0x00007f285e6e7bd7
7  libc.so.6       0x00007f285e6e7c82
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       0x00007f285e6da830 __libc_start_main + 240
16 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 887.835705996
