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--crypto--qat--qat_common--intel_qat.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.: 327 625 3908 28638
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in sg_page
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.938812017441
Removed calls to '__init_rwsem' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Defining function debugfs_create_file as symbolic
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Removed calls to 'debugfs_remove' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function strlcpy as symbolic
Defining function snprintf as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function printk as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function request_firmware as symbolic
Removed calls to 'release_firmware' (function is undefined)
Defining function kstrtoull as symbolic
Defining function kmemdup as symbolic
Defining function __memmove as symbolic
Defining function debugfs_create_dir as symbolic
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Defining function kstrtouint as symbolic
Defining function __kmalloc_node as symbolic
Removed calls to '_dev_info' (function is undefined)
Defining function crypto_register_algs as symbolic
Removed calls to 'msleep' (function is undefined)
Defining function crypto_unregister_algs as symbolic
Removed calls to 'dma_free_attrs' (function is undefined)
Defining function pci_enable_pcie_error_reporting as symbolic
Defining function pci_disable_pcie_error_reporting as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function seq_release as symbolic
Defining function seq_open as symbolic
Defining function seq_printf as symbolic
Defining function seq_list_next as symbolic
Defining function seq_list_start as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Defining function mutex_lock_interruptible as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Defining function pci_cleanup_aer_uncorrect_error_status as symbolic
Removed calls to 'pci_restore_state' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function wait_for_completion_timeout as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function queue_work_on as symbolic
Defining function pci_wait_for_pending_transaction as symbolic
Defining function pci_save_state as symbolic
Defining function pci_bus_write_config_word as symbolic
Defining function pci_bus_read_config_word as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'crypto_destroy_tfm' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function sg_nents as symbolic
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Defining function sg_next as symbolic
Defining function __phys_addr as symbolic
Defining function dma_alloc_attrs as symbolic
Defining function try_module_get as symbolic
Defining function crypto_alloc_shash as symbolic
Defining function crypto_authenc_extractkeys as symbolic
Removed calls to 'memzero_explicit' (function is undefined)
Defining function crypto_shash_digest as symbolic
Defining function crypto_shash_update as symbolic
Defining function seq_puts as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Defining function mutex_trylock as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'crypto_put_default_rng' (function is undefined)
Removed calls to 'mutex_destroy' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'cdev_init' (function is undefined)
Removed calls to 'cdev_del' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Removed calls to 'unregister_chrdev_region' (function is undefined)
Defining function ldv_open_7 as symbolic
Defining function ldv_release_7 as symbolic
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'device_destroy' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function alloc_chrdev_region as symbolic
Defining function __class_create as symbolic
Defining function cdev_add as symbolic
Defining function device_create as symbolic
Defining function crypto_get_default_rng as symbolic
Defining function ldv_suspend_6 as symbolic
Defining function ldv_release_6 as symbolic
Defining function ldv_probe_6 as symbolic
Linked our definitions to these undefined functions:
  strcmp
  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.0839600563
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 419 523 2564 17709
INFO: Starting verification
KLEE: WARNING ONCE: function "adf_dev_init" has inline asm
KLEE: WARNING ONCE: function "adf_init_etr_data" has inline asm
KLEE: WARNING ONCE: function "adf_ae_init" has inline asm
KLEE: WARNING ONCE: function "qat_uclo_map_uof_obj" has inline asm
KLEE: WARNING ONCE: function "qat_uclo_wr_all_uimage" has inline asm
KLEE: WARNING ONCE: function "qat_hal_wr_umem" has inline asm
KLEE: WARNING ONCE: function "qat_hal_rd_ae_csr" has inline asm
KLEE: WARNING ONCE: function "qat_hal_wr_ae_csr" has inline asm
KLEE: WARNING ONCE: function "qat_hal_init_gpr" has inline asm
KLEE: WARNING ONCE: function "qat_hal_init_rd_xfer" has inline asm
KLEE: WARNING ONCE: function "qat_hal_init_wr_xfer" has inline asm
KLEE: WARNING ONCE: function "qat_hal_init_nn" has inline asm
KLEE: WARNING ONCE: function "qat_hal_clr_reset" has inline asm
KLEE: WARNING ONCE: function "adf_dev_start" has inline asm
KLEE: WARNING ONCE: function "qat_algs_register" has inline asm
KLEE: WARNING ONCE: function "adf_dev_stop" has inline asm
KLEE: WARNING ONCE: function "qat_algs_unregister" has inline asm
KLEE: WARNING ONCE: function "adf_dev_shutdown" has inline asm
KLEE: WARNING ONCE: function "adf_cfg_del_all" has inline asm
KLEE: WARNING ONCE: function "adf_response_handler" has inline asm
KLEE: WARNING ONCE: function "adf_ctl_ioctl" has inline asm
KLEE: WARNING ONCE: function "adf_slot_reset" has inline asm
KLEE: WARNING ONCE: function "adf_device_reset_worker" has inline asm
KLEE: WARNING ONCE: function "qat_alg_aead_setkey" has inline asm
KLEE: WARNING ONCE: function "qat_alg_ablkcipher_setkey" has inline asm
KLEE: WARNING ONCE: function "qat_crypto_put_instance" has inline asm
KLEE: WARNING ONCE: function "adf_send_message" has inline asm
KLEE: WARNING ONCE: function "dma_unmap_single_attrs" has inline asm
KLEE: WARNING ONCE: function "dma_map_single_attrs" has inline asm
KLEE: WARNING ONCE: function "sg_virt" has inline asm
KLEE: WARNING ONCE: function "qat_crypto_get_instance_node" has inline asm
KLEE: WARNING ONCE: function "adf_dev_get" has inline asm
KLEE: WARNING ONCE: function "adf_ring_show" has inline asm
KLEE: WARNING ONCE: function "adf_bank_show" has inline asm
KLEE: WARNING ONCE: function "qat_hal_reset" has inline asm
KLEE: WARNING ONCE: function "adf_dev_put" has inline asm
KLEE: WARNING ONCE: function "adf_create_ring" has inline asm
KLEE: WARNING ONCE: function "adf_remove_ring" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_2faad5bf-fb12-4149-ae0a-f62a081fd1d9/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING: killing 13141 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 15297 states (over memory cap)
KLEE: WARNING: killing 15337 states (over memory cap)
KLEE: WARNING: killing 15224 states (over memory cap)
KLEE: WARNING: killing 14412 states (over memory cap)
KLEE: WARNING: killing 14688 states (over memory cap)
KLEE: WARNING: killing 14268 states (over memory cap)
KLEE: WARNING: killing 14156 states (over memory cap)
KLEE: WARNING: killing 14276 states (over memory cap)
KLEE: WARNING: killing 14634 states (over memory cap)
KLEE: WARNING: killing 15224 states (over memory cap)
KLEE: WARNING: killing 15587 states (over memory cap)
KLEE: WARNING: killing 15639 states (over memory cap)
KLEE: WARNING: killing 16303 states (over memory cap)
KLEE: WARNING: killing 15972 states (over memory cap)
KLEE: WARNING: killing 15570 states (over memory cap)
KLEE: WARNING: killing 16162 states (over memory cap)
KLEE: WARNING: killing 16679 states (over memory cap)
KLEE: WARNING: killing 15897 states (over memory cap)
KLEE: WARNING: killing 16327 states (over memory cap)
KLEE: WARNING: killing 16008 states (over memory cap)
KLEE: WARNING: killing 16221 states (over memory cap)
KLEE: WARNING: killing 15893 states (over memory cap)
KLEE: WARNING: killing 15492 states (over memory cap)
KLEE: WARNING: killing 15241 states (over memory cap)
KLEE: WARNING: killing 16354 states (over memory cap)
KLEE: WARNING: killing 15128 states (over memory cap)
KLEE: WARNING: killing 15862 states (over memory cap)
KLEE: WARNING: killing 15696 states (over memory cap)
KLEE: WARNING: killing 15370 states (over memory cap)
KLEE: WARNING: killing 15276 states (over memory cap)
KLEE: WARNING: killing 15480 states (over memory cap)
KLEE: WARNING: killing 15908 states (over memory cap)
KLEE: WARNING: killing 15144 states (over memory cap)
KLEE: WARNING: killing 15946 states (over memory cap)
KLEE: WARNING: killing 15334 states (over memory cap)
KLEE: WARNING: killing 15765 states (over memory cap)
KLEE: WARNING: killing 15515 states (over memory cap)
KLEE: WARNING: killing 15651 states (over memory cap)
KLEE: WARNING: killing 15557 states (over memory cap)
KLEE: WARNING: killing 15609 states (over memory cap)
KLEE: WARNING: killing 15894 states (over memory cap)
KLEE: WARNING: killing 15724 states (over memory cap)
KLEE: WARNING: killing 15931 states (over memory cap)
KLEE: WARNING: killing 16360 states (over memory cap)
KLEE: WARNING: killing 15015 states (over memory cap)
KLEE: WARNING: killing 16028 states (over memory cap)
KLEE: WARNING: killing 15942 states (over memory cap)
KLEE: WARNING: killing 16150 states (over memory cap)
KLEE: WARNING: killing 15835 states (over memory cap)
KLEE: WARNING: killing 15376 states (over memory cap)
KLEE: WARNING: killing 15067 states (over memory cap)
KLEE: WARNING: killing 15414 states (over memory cap)
KLEE: WARNING: killing 15467 states (over memory cap)
KLEE: WARNING: killing 15382 states (over memory cap)
KLEE: WARNING: killing 15438 states (over memory cap)
KLEE: WARNING: killing 15709 states (over memory cap)
KLEE: WARNING: killing 15403 states (over memory cap)
KLEE: WARNING: killing 16261 states (over memory cap)
KLEE: WARNING: killing 15515 states (over memory cap)
KLEE: WARNING: killing 15140 states (over memory cap)
KLEE: WARNING: killing 15634 states (over memory cap)
KLEE: WARNING: killing 16201 states (over memory cap)
KLEE: WARNING: killing 15746 states (over memory cap)
KLEE: WARNING: killing 15508 states (over memory cap)
KLEE: WARNING: killing 15420 states (over memory cap)
KLEE: WARNING: killing 16128 states (over memory cap)
KLEE: WARNING: killing 16113 states (over memory cap)
KLEE: WARNING: killing 15594 states (over memory cap)
KLEE: WARNING: killing 15725 states (over memory cap)
KLEE: WARNING: killing 15781 states (over memory cap)
KLEE: WARNING: killing 15047 states (over memory cap)
KLEE: WARNING: killing 15037 states (over memory cap)
KLEE: WARNING: killing 15589 states (over memory cap)
KLEE: WARNING: killing 15725 states (over memory cap)
KLEE: WARNING: killing 16140 states (over memory cap)
KLEE: WARNING: killing 15546 states (over memory cap)
KLEE: WARNING: killing 15392 states (over memory cap)
KLEE: WARNING: killing 15801 states (over memory cap)
KLEE: WARNING: killing 15786 states (over memory cap)
KLEE: WARNING: killing 15557 states (over memory cap)
KLEE: WARNING: killing 15892 states (over memory cap)
KLEE: WARNING: killing 15743 states (over memory cap)
KLEE: WARNING: killing 15870 states (over memory cap)
KLEE: WARNING: killing 15711 states (over memory cap)
KLEE: WARNING: killing 15057 states (over memory cap)
KLEE: WARNING: killing 15468 states (over memory cap)
KLEE: WARNING: killing 16237 states (over memory cap)
KLEE: WARNING: killing 15230 states (over memory cap)
KLEE: WARNING: killing 15563 states (over memory cap)
KLEE: WARNING: killing 16189 states (over memory cap)
KLEE: WARNING: killing 15395 states (over memory cap)
KLEE: WARNING: killing 15522 states (over memory cap)
KLEE: WARNING: killing 16075 states (over memory cap)
KLEE: WARNING: killing 15071 states (over memory cap)
KLEE: WARNING: killing 15905 states (over memory cap)
KLEE: WARNING: killing 15608 states (over memory cap)
KLEE: WARNING: killing 15380 states (over memory cap)
KLEE: WARNING: killing 15436 states (over memory cap)
KLEE: WARNING: killing 15774 states (over memory cap)
KLEE: WARNING: killing 15967 states (over memory cap)
KLEE: WARNING: killing 15743 states (over memory cap)
KLEE: WARNING: killing 15376 states (over memory cap)
KLEE: WARNING: killing 16130 states (over memory cap)
KLEE: WARNING: killing 15914 states (over memory cap)
KLEE: WARNING: killing 15128 states (over memory cap)
KLEE: WARNING: killing 15462 states (over memory cap)
KLEE: WARNING: killing 15449 states (over memory cap)
KLEE: WARNING: killing 15778 states (over memory cap)
KLEE: WARNING: killing 15275 states (over memory cap)
KLEE: WARNING: killing 15675 states (over memory cap)
KLEE: WARNING: killing 15526 states (over memory cap)
KLEE: WARNING: killing 15990 states (over memory cap)
KLEE: WARNING: killing 15701 states (over memory cap)
KLEE: WARNING: killing 15275 states (over memory cap)
KLEE: WARNING: killing 15878 states (over memory cap)
KLEE: WARNING: killing 16357 states (over memory cap)
KLEE: WARNING: killing 15790 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-SXIGxw/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "adf_dev_init" has inline asm
KLEE: WARNING ONCE: function "adf_init_etr_data" has inline asm
KLEE: WARNING ONCE: function "adf_ae_init" has inline asm
KLEE: WARNING ONCE: function "qat_uclo_map_uof_obj" has inline asm
KLEE: WARNING ONCE: function "qat_uclo_wr_all_uimage" has inline asm
KLEE: WARNING ONCE: function "qat_hal_wr_umem" has inline asm
KLEE: WARNING ONCE: function "qat_hal_rd_ae_csr" has inline asm
KLEE: WARNING ONCE: function "qat_hal_wr_ae_csr" has inline asm
KLEE: WARNING ONCE: function "qat_hal_init_gpr" has inline asm
KLEE: WARNING ONCE: function "qat_hal_init_rd_xfer" has inline asm
KLEE: WARNING ONCE: function "qat_hal_init_wr_xfer" has inline asm
KLEE: WARNING ONCE: function "qat_hal_init_nn" has inline asm
KLEE: WARNING ONCE: function "qat_hal_clr_reset" has inline asm
KLEE: WARNING ONCE: function "adf_dev_start" has inline asm
KLEE: WARNING ONCE: function "qat_algs_register" has inline asm
KLEE: WARNING ONCE: function "adf_dev_stop" has inline asm
KLEE: WARNING ONCE: function "qat_algs_unregister" has inline asm
KLEE: WARNING ONCE: function "adf_dev_shutdown" has inline asm
KLEE: WARNING ONCE: function "adf_cfg_del_all" has inline asm
KLEE: WARNING ONCE: function "adf_response_handler" has inline asm
KLEE: WARNING ONCE: function "adf_ctl_ioctl" has inline asm
KLEE: WARNING ONCE: function "adf_slot_reset" has inline asm
KLEE: WARNING ONCE: function "adf_device_reset_worker" has inline asm
KLEE: WARNING ONCE: function "qat_alg_aead_setkey" has inline asm
KLEE: WARNING ONCE: function "qat_alg_ablkcipher_setkey" has inline asm
KLEE: WARNING ONCE: function "qat_crypto_put_instance" has inline asm
KLEE: WARNING ONCE: function "adf_send_message" has inline asm
KLEE: WARNING ONCE: function "dma_unmap_single_attrs" has inline asm
KLEE: WARNING ONCE: function "dma_map_single_attrs" has inline asm
KLEE: WARNING ONCE: function "sg_virt" has inline asm
KLEE: WARNING ONCE: function "qat_crypto_get_instance_node" has inline asm
KLEE: WARNING ONCE: function "adf_dev_get" has inline asm
KLEE: WARNING ONCE: function "adf_ring_show" has inline asm
KLEE: WARNING ONCE: function "adf_bank_show" has inline asm
KLEE: WARNING ONCE: function "qat_hal_reset" has inline asm
KLEE: WARNING ONCE: function "adf_dev_put" has inline asm
KLEE: WARNING ONCE: function "adf_create_ring" has inline asm
KLEE: WARNING ONCE: function "adf_remove_ring" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_2faad5bf-fb12-4149-ae0a-f62a081fd1d9/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING: killing 13141 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 15297 states (over memory cap)
KLEE: WARNING: killing 15337 states (over memory cap)
KLEE: WARNING: killing 15224 states (over memory cap)
KLEE: WARNING: killing 14412 states (over memory cap)
KLEE: WARNING: killing 14688 states (over memory cap)
KLEE: WARNING: killing 14268 states (over memory cap)
KLEE: WARNING: killing 14156 states (over memory cap)
KLEE: WARNING: killing 14276 states (over memory cap)
KLEE: WARNING: killing 14634 states (over memory cap)
KLEE: WARNING: killing 15224 states (over memory cap)
KLEE: WARNING: killing 15587 states (over memory cap)
KLEE: WARNING: killing 15639 states (over memory cap)
KLEE: WARNING: killing 16303 states (over memory cap)
KLEE: WARNING: killing 15972 states (over memory cap)
KLEE: WARNING: killing 15570 states (over memory cap)
KLEE: WARNING: killing 16162 states (over memory cap)
KLEE: WARNING: killing 16679 states (over memory cap)
KLEE: WARNING: killing 15897 states (over memory cap)
KLEE: WARNING: killing 16327 states (over memory cap)
KLEE: WARNING: killing 16008 states (over memory cap)
KLEE: WARNING: killing 16221 states (over memory cap)
KLEE: WARNING: killing 15893 states (over memory cap)
KLEE: WARNING: killing 15492 states (over memory cap)
KLEE: WARNING: killing 15241 states (over memory cap)
KLEE: WARNING: killing 16354 states (over memory cap)
KLEE: WARNING: killing 15128 states (over memory cap)
KLEE: WARNING: killing 15862 states (over memory cap)
KLEE: WARNING: killing 15696 states (over memory cap)
KLEE: WARNING: killing 15370 states (over memory cap)
KLEE: WARNING: killing 15276 states (over memory cap)
KLEE: WARNING: killing 15480 states (over memory cap)
KLEE: WARNING: killing 15908 states (over memory cap)
KLEE: WARNING: killing 15144 states (over memory cap)
KLEE: WARNING: killing 15946 states (over memory cap)
KLEE: WARNING: killing 15334 states (over memory cap)
KLEE: WARNING: killing 15765 states (over memory cap)
KLEE: WARNING: killing 15515 states (over memory cap)
KLEE: WARNING: killing 15651 states (over memory cap)
KLEE: WARNING: killing 15557 states (over memory cap)
KLEE: WARNING: killing 15609 states (over memory cap)
KLEE: WARNING: killing 15894 states (over memory cap)
KLEE: WARNING: killing 15724 states (over memory cap)
KLEE: WARNING: killing 15931 states (over memory cap)
KLEE: WARNING: killing 16360 states (over memory cap)
KLEE: WARNING: killing 15015 states (over memory cap)
KLEE: WARNING: killing 16028 states (over memory cap)
KLEE: WARNING: killing 15942 states (over memory cap)
KLEE: WARNING: killing 16150 states (over memory cap)
KLEE: WARNING: killing 15835 states (over memory cap)
KLEE: WARNING: killing 15376 states (over memory cap)
KLEE: WARNING: killing 15067 states (over memory cap)
KLEE: WARNING: killing 15414 states (over memory cap)
KLEE: WARNING: killing 15467 states (over memory cap)
KLEE: WARNING: killing 15382 states (over memory cap)
KLEE: WARNING: killing 15438 states (over memory cap)
KLEE: WARNING: killing 15709 states (over memory cap)
KLEE: WARNING: killing 15403 states (over memory cap)
KLEE: WARNING: killing 16261 states (over memory cap)
KLEE: WARNING: killing 15515 states (over memory cap)
KLEE: WARNING: killing 15140 states (over memory cap)
KLEE: WARNING: killing 15634 states (over memory cap)
KLEE: WARNING: killing 16201 states (over memory cap)
KLEE: WARNING: killing 15746 states (over memory cap)
KLEE: WARNING: killing 15508 states (over memory cap)
KLEE: WARNING: killing 15420 states (over memory cap)
KLEE: WARNING: killing 16128 states (over memory cap)
KLEE: WARNING: killing 16113 states (over memory cap)
KLEE: WARNING: killing 15594 states (over memory cap)
KLEE: WARNING: killing 15725 states (over memory cap)
KLEE: WARNING: killing 15781 states (over memory cap)
KLEE: WARNING: killing 15047 states (over memory cap)
KLEE: WARNING: killing 15037 states (over memory cap)
KLEE: WARNING: killing 15589 states (over memory cap)
KLEE: WARNING: killing 15725 states (over memory cap)
KLEE: WARNING: killing 16140 states (over memory cap)
KLEE: WARNING: killing 15546 states (over memory cap)
KLEE: WARNING: killing 15392 states (over memory cap)
KLEE: WARNING: killing 15801 states (over memory cap)
KLEE: WARNING: killing 15786 states (over memory cap)
KLEE: WARNING: killing 15557 states (over memory cap)
KLEE: WARNING: killing 15892 states (over memory cap)
KLEE: WARNING: killing 15743 states (over memory cap)
KLEE: WARNING: killing 15870 states (over memory cap)
KLEE: WARNING: killing 15711 states (over memory cap)
KLEE: WARNING: killing 15057 states (over memory cap)
KLEE: WARNING: killing 15468 states (over memory cap)
KLEE: WARNING: killing 16237 states (over memory cap)
KLEE: WARNING: killing 15230 states (over memory cap)
KLEE: WARNING: killing 15563 states (over memory cap)
KLEE: WARNING: killing 16189 states (over memory cap)
KLEE: WARNING: killing 15395 states (over memory cap)
KLEE: WARNING: killing 15522 states (over memory cap)
KLEE: WARNING: killing 16075 states (over memory cap)
KLEE: WARNING: killing 15071 states (over memory cap)
KLEE: WARNING: killing 15905 states (over memory cap)
KLEE: WARNING: killing 15608 states (over memory cap)
KLEE: WARNING: killing 15380 states (over memory cap)
KLEE: WARNING: killing 15436 states (over memory cap)
KLEE: WARNING: killing 15774 states (over memory cap)
KLEE: WARNING: killing 15967 states (over memory cap)
KLEE: WARNING: killing 15743 states (over memory cap)
KLEE: WARNING: killing 15376 states (over memory cap)
KLEE: WARNING: killing 16130 states (over memory cap)
KLEE: WARNING: killing 15914 states (over memory cap)
KLEE: WARNING: killing 15128 states (over memory cap)
KLEE: WARNING: killing 15462 states (over memory cap)
KLEE: WARNING: killing 15449 states (over memory cap)
KLEE: WARNING: killing 15778 states (over memory cap)
KLEE: WARNING: killing 15275 states (over memory cap)
KLEE: WARNING: killing 15675 states (over memory cap)
KLEE: WARNING: killing 15526 states (over memory cap)
KLEE: WARNING: killing 15990 states (over memory cap)
KLEE: WARNING: killing 15701 states (over memory cap)
KLEE: WARNING: killing 15275 states (over memory cap)
KLEE: WARNING: killing 15878 states (over memory cap)
KLEE: WARNING: killing 16357 states (over memory cap)
KLEE: WARNING: killing 15790 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 0x00007f66613bd390
4  libc.so.6       0x00007f6660776428 gsignal + 56
5  libc.so.6       0x00007f666077802a abort + 362
6  libc.so.6       0x00007f666076ebd7
7  libc.so.6       0x00007f666076ec82
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       0x00007f6660761830 __libc_start_main + 240
16 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 445.543237925
