bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--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.: 319 456 3372 26462
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: 1.02266383171
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_nested' (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
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
Defining function mutex_lock_interruptible_nested 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
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 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)
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)
Removed calls to 'ldv_check_final_state' (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 dma_alloc_attrs as symbolic
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
Defining function ldv_some_page 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.19121694565
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 415 355 1983 16058
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_27421e69-60fb-4841-ade8-9b9c3b85e23d/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 14995 states (over memory cap)
KLEE: WARNING: killing 16037 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 14618 states (over memory cap)
KLEE: WARNING: killing 14500 states (over memory cap)
KLEE: WARNING: killing 14009 states (over memory cap)
KLEE: WARNING: killing 13439 states (over memory cap)
KLEE: WARNING: killing 13565 states (over memory cap)
KLEE: WARNING: killing 14673 states (over memory cap)
KLEE: WARNING: killing 14795 states (over memory cap)
KLEE: WARNING: killing 14759 states (over memory cap)
KLEE: WARNING: killing 15417 states (over memory cap)
KLEE: WARNING: killing 15470 states (over memory cap)
KLEE: WARNING: killing 15668 states (over memory cap)
KLEE: WARNING: killing 16556 states (over memory cap)
KLEE: WARNING: killing 16006 states (over memory cap)
KLEE: WARNING: killing 16068 states (over memory cap)
KLEE: WARNING: killing 16270 states (over memory cap)
KLEE: WARNING: killing 16179 states (over memory cap)
KLEE: WARNING: killing 15929 states (over memory cap)
KLEE: WARNING: killing 15834 states (over memory cap)
KLEE: WARNING: killing 15887 states (over memory cap)
KLEE: WARNING: killing 15867 states (over memory cap)
KLEE: WARNING: killing 15845 states (over memory cap)
KLEE: WARNING: killing 15755 states (over memory cap)
KLEE: WARNING: killing 16324 states (over memory cap)
KLEE: WARNING: killing 15569 states (over memory cap)
KLEE: WARNING: killing 16215 states (over memory cap)
KLEE: WARNING: killing 15526 states (over memory cap)
KLEE: WARNING: killing 15882 states (over memory cap)
KLEE: WARNING: killing 15050 states (over memory cap)
KLEE: WARNING: killing 15318 states (over memory cap)
KLEE: WARNING: killing 15005 states (over memory cap)
KLEE: WARNING: killing 15649 states (over memory cap)
KLEE: WARNING: killing 15629 states (over memory cap)
KLEE: WARNING: killing 15465 states (over memory cap)
KLEE: WARNING: killing 15883 states (over memory cap)
KLEE: WARNING: killing 15938 states (over memory cap)
KLEE: WARNING: killing 15699 states (over memory cap)
KLEE: WARNING: killing 16126 states (over memory cap)
KLEE: WARNING: killing 15524 states (over memory cap)
KLEE: WARNING: killing 15359 states (over memory cap)
KLEE: WARNING: killing 15925 states (over memory cap)
KLEE: WARNING: killing 15690 states (over memory cap)
KLEE: WARNING: killing 16107 states (over memory cap)
KLEE: WARNING: killing 15653 states (over memory cap)
KLEE: WARNING: killing 15492 states (over memory cap)
KLEE: WARNING: killing 15394 states (over memory cap)
KLEE: WARNING: killing 16107 states (over memory cap)
KLEE: WARNING: killing 15508 states (over memory cap)
KLEE: WARNING: killing 15499 states (over memory cap)
KLEE: WARNING: killing 15699 states (over memory cap)
KLEE: WARNING: killing 15602 states (over memory cap)
KLEE: WARNING: killing 15659 states (over memory cap)
KLEE: WARNING: killing 15787 states (over memory cap)
KLEE: WARNING: killing 15631 states (over memory cap)
KLEE: WARNING: killing 16692 states (over memory cap)
KLEE: WARNING: killing 15598 states (over memory cap)
KLEE: WARNING: killing 15514 states (over memory cap)
KLEE: WARNING: killing 15136 states (over memory cap)
KLEE: WARNING: killing 15765 states (over memory cap)
KLEE: WARNING: killing 15826 states (over memory cap)
KLEE: WARNING: killing 15237 states (over memory cap)
KLEE: WARNING: killing 15359 states (over memory cap)
KLEE: WARNING: killing 15196 states (over memory cap)
KLEE: WARNING: killing 15251 states (over memory cap)
KLEE: WARNING: killing 15735 states (over memory cap)
KLEE: WARNING: killing 15716 states (over memory cap)
KLEE: WARNING: killing 16276 states (over memory cap)
KLEE: WARNING: killing 15339 states (over memory cap)
KLEE: WARNING: killing 15392 states (over memory cap)
KLEE: WARNING: killing 15943 states (over memory cap)
KLEE: WARNING: killing 16078 states (over memory cap)
KLEE: WARNING: killing 15285 states (over memory cap)
KLEE: WARNING: killing 15262 states (over memory cap)
KLEE: WARNING: killing 15674 states (over memory cap)
KLEE: WARNING: killing 15095 states (over memory cap)
KLEE: WARNING: killing 15992 states (over memory cap)
KLEE: WARNING: killing 15346 states (over memory cap)
KLEE: WARNING: killing 15961 states (over memory cap)
KLEE: WARNING: killing 16308 states (over memory cap)
KLEE: WARNING: killing 16014 states (over memory cap)
KLEE: WARNING: killing 15366 states (over memory cap)
KLEE: WARNING: killing 15142 states (over memory cap)
KLEE: WARNING: killing 15052 states (over memory cap)
KLEE: WARNING: killing 15320 states (over memory cap)
KLEE: WARNING: killing 15366 states (over memory cap)
KLEE: WARNING: killing 15637 states (over memory cap)
KLEE: WARNING: killing 15336 states (over memory cap)
KLEE: WARNING: killing 15318 states (over memory cap)
KLEE: WARNING: killing 15234 states (over memory cap)
KLEE: WARNING: killing 15714 states (over memory cap)
KLEE: WARNING: killing 15620 states (over memory cap)
KLEE: WARNING: killing 15755 states (over memory cap)
KLEE: WARNING: killing 16086 states (over memory cap)
KLEE: WARNING: killing 15867 states (over memory cap)
KLEE: WARNING: killing 14957 states (over memory cap)
KLEE: WARNING: killing 16049 states (over memory cap)
KLEE: WARNING: killing 15970 states (over memory cap)
KLEE: WARNING: killing 15191 states (over memory cap)
KLEE: WARNING: killing 15447 states (over memory cap)
KLEE: WARNING: killing 15222 states (over memory cap)
KLEE: WARNING: killing 16036 states (over memory cap)
KLEE: WARNING: killing 16507 states (over memory cap)
KLEE: WARNING: killing 15388 states (over memory cap)
KLEE: WARNING: killing 15307 states (over memory cap)
KLEE: WARNING: killing 15503 states (over memory cap)
KLEE: WARNING: killing 15345 states (over memory cap)
KLEE: WARNING: killing 15886 states (over memory cap)
KLEE: WARNING: killing 15530 states (over memory cap)
KLEE: WARNING: killing 15304 states (over memory cap)
KLEE: WARNING: killing 15839 states (over memory cap)
KLEE: WARNING: killing 15560 states (over memory cap)
KLEE: WARNING: killing 15407 states (over memory cap)
KLEE: WARNING: killing 15116 states (over memory cap)
KLEE: WARNING: killing 15105 states (over memory cap)
KLEE: WARNING: killing 15633 states (over memory cap)
KLEE: WARNING: killing 15820 states (over memory cap)
KLEE: WARNING: killing 15602 states (over memory cap)
KLEE: WARNING: killing 15381 states (over memory cap)
KLEE: WARNING: killing 15781 states (over memory cap)
KLEE: WARNING: killing 15693 states (over memory cap)
KLEE: WARNING: killing 16088 states (over memory cap)
KLEE: WARNING: killing 15735 states (over memory cap)
KLEE: WARNING: killing 15315 states (over memory cap)
KLEE: WARNING: killing 15977 states (over memory cap)
KLEE: WARNING: killing 15620 states (over memory cap)
KLEE: WARNING: killing 15537 states (over memory cap)
KLEE: WARNING: killing 15191 states (over memory cap)
KLEE: WARNING: killing 15983 states (over memory cap)
KLEE: WARNING: killing 15504 states (over memory cap)
KLEE: WARNING: killing 15088 states (over memory cap)
KLEE: WARNING: killing 15943 states (over memory cap)
KLEE: WARNING: killing 15863 states (over memory cap)
KLEE: WARNING: killing 15718 states (over memory cap)
KLEE: WARNING: killing 16175 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-ZWFzMO/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_27421e69-60fb-4841-ade8-9b9c3b85e23d/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 14995 states (over memory cap)
KLEE: WARNING: killing 16037 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 14618 states (over memory cap)
KLEE: WARNING: killing 14500 states (over memory cap)
KLEE: WARNING: killing 14009 states (over memory cap)
KLEE: WARNING: killing 13439 states (over memory cap)
KLEE: WARNING: killing 13565 states (over memory cap)
KLEE: WARNING: killing 14673 states (over memory cap)
KLEE: WARNING: killing 14795 states (over memory cap)
KLEE: WARNING: killing 14759 states (over memory cap)
KLEE: WARNING: killing 15417 states (over memory cap)
KLEE: WARNING: killing 15470 states (over memory cap)
KLEE: WARNING: killing 15668 states (over memory cap)
KLEE: WARNING: killing 16556 states (over memory cap)
KLEE: WARNING: killing 16006 states (over memory cap)
KLEE: WARNING: killing 16068 states (over memory cap)
KLEE: WARNING: killing 16270 states (over memory cap)
KLEE: WARNING: killing 16179 states (over memory cap)
KLEE: WARNING: killing 15929 states (over memory cap)
KLEE: WARNING: killing 15834 states (over memory cap)
KLEE: WARNING: killing 15887 states (over memory cap)
KLEE: WARNING: killing 15867 states (over memory cap)
KLEE: WARNING: killing 15845 states (over memory cap)
KLEE: WARNING: killing 15755 states (over memory cap)
KLEE: WARNING: killing 16324 states (over memory cap)
KLEE: WARNING: killing 15569 states (over memory cap)
KLEE: WARNING: killing 16215 states (over memory cap)
KLEE: WARNING: killing 15526 states (over memory cap)
KLEE: WARNING: killing 15882 states (over memory cap)
KLEE: WARNING: killing 15050 states (over memory cap)
KLEE: WARNING: killing 15318 states (over memory cap)
KLEE: WARNING: killing 15005 states (over memory cap)
KLEE: WARNING: killing 15649 states (over memory cap)
KLEE: WARNING: killing 15629 states (over memory cap)
KLEE: WARNING: killing 15465 states (over memory cap)
KLEE: WARNING: killing 15883 states (over memory cap)
KLEE: WARNING: killing 15938 states (over memory cap)
KLEE: WARNING: killing 15699 states (over memory cap)
KLEE: WARNING: killing 16126 states (over memory cap)
KLEE: WARNING: killing 15524 states (over memory cap)
KLEE: WARNING: killing 15359 states (over memory cap)
KLEE: WARNING: killing 15925 states (over memory cap)
KLEE: WARNING: killing 15690 states (over memory cap)
KLEE: WARNING: killing 16107 states (over memory cap)
KLEE: WARNING: killing 15653 states (over memory cap)
KLEE: WARNING: killing 15492 states (over memory cap)
KLEE: WARNING: killing 15394 states (over memory cap)
KLEE: WARNING: killing 16107 states (over memory cap)
KLEE: WARNING: killing 15508 states (over memory cap)
KLEE: WARNING: killing 15499 states (over memory cap)
KLEE: WARNING: killing 15699 states (over memory cap)
KLEE: WARNING: killing 15602 states (over memory cap)
KLEE: WARNING: killing 15659 states (over memory cap)
KLEE: WARNING: killing 15787 states (over memory cap)
KLEE: WARNING: killing 15631 states (over memory cap)
KLEE: WARNING: killing 16692 states (over memory cap)
KLEE: WARNING: killing 15598 states (over memory cap)
KLEE: WARNING: killing 15514 states (over memory cap)
KLEE: WARNING: killing 15136 states (over memory cap)
KLEE: WARNING: killing 15765 states (over memory cap)
KLEE: WARNING: killing 15826 states (over memory cap)
KLEE: WARNING: killing 15237 states (over memory cap)
KLEE: WARNING: killing 15359 states (over memory cap)
KLEE: WARNING: killing 15196 states (over memory cap)
KLEE: WARNING: killing 15251 states (over memory cap)
KLEE: WARNING: killing 15735 states (over memory cap)
KLEE: WARNING: killing 15716 states (over memory cap)
KLEE: WARNING: killing 16276 states (over memory cap)
KLEE: WARNING: killing 15339 states (over memory cap)
KLEE: WARNING: killing 15392 states (over memory cap)
KLEE: WARNING: killing 15943 states (over memory cap)
KLEE: WARNING: killing 16078 states (over memory cap)
KLEE: WARNING: killing 15285 states (over memory cap)
KLEE: WARNING: killing 15262 states (over memory cap)
KLEE: WARNING: killing 15674 states (over memory cap)
KLEE: WARNING: killing 15095 states (over memory cap)
KLEE: WARNING: killing 15992 states (over memory cap)
KLEE: WARNING: killing 15346 states (over memory cap)
KLEE: WARNING: killing 15961 states (over memory cap)
KLEE: WARNING: killing 16308 states (over memory cap)
KLEE: WARNING: killing 16014 states (over memory cap)
KLEE: WARNING: killing 15366 states (over memory cap)
KLEE: WARNING: killing 15142 states (over memory cap)
KLEE: WARNING: killing 15052 states (over memory cap)
KLEE: WARNING: killing 15320 states (over memory cap)
KLEE: WARNING: killing 15366 states (over memory cap)
KLEE: WARNING: killing 15637 states (over memory cap)
KLEE: WARNING: killing 15336 states (over memory cap)
KLEE: WARNING: killing 15318 states (over memory cap)
KLEE: WARNING: killing 15234 states (over memory cap)
KLEE: WARNING: killing 15714 states (over memory cap)
KLEE: WARNING: killing 15620 states (over memory cap)
KLEE: WARNING: killing 15755 states (over memory cap)
KLEE: WARNING: killing 16086 states (over memory cap)
KLEE: WARNING: killing 15867 states (over memory cap)
KLEE: WARNING: killing 14957 states (over memory cap)
KLEE: WARNING: killing 16049 states (over memory cap)
KLEE: WARNING: killing 15970 states (over memory cap)
KLEE: WARNING: killing 15191 states (over memory cap)
KLEE: WARNING: killing 15447 states (over memory cap)
KLEE: WARNING: killing 15222 states (over memory cap)
KLEE: WARNING: killing 16036 states (over memory cap)
KLEE: WARNING: killing 16507 states (over memory cap)
KLEE: WARNING: killing 15388 states (over memory cap)
KLEE: WARNING: killing 15307 states (over memory cap)
KLEE: WARNING: killing 15503 states (over memory cap)
KLEE: WARNING: killing 15345 states (over memory cap)
KLEE: WARNING: killing 15886 states (over memory cap)
KLEE: WARNING: killing 15530 states (over memory cap)
KLEE: WARNING: killing 15304 states (over memory cap)
KLEE: WARNING: killing 15839 states (over memory cap)
KLEE: WARNING: killing 15560 states (over memory cap)
KLEE: WARNING: killing 15407 states (over memory cap)
KLEE: WARNING: killing 15116 states (over memory cap)
KLEE: WARNING: killing 15105 states (over memory cap)
KLEE: WARNING: killing 15633 states (over memory cap)
KLEE: WARNING: killing 15820 states (over memory cap)
KLEE: WARNING: killing 15602 states (over memory cap)
KLEE: WARNING: killing 15381 states (over memory cap)
KLEE: WARNING: killing 15781 states (over memory cap)
KLEE: WARNING: killing 15693 states (over memory cap)
KLEE: WARNING: killing 16088 states (over memory cap)
KLEE: WARNING: killing 15735 states (over memory cap)
KLEE: WARNING: killing 15315 states (over memory cap)
KLEE: WARNING: killing 15977 states (over memory cap)
KLEE: WARNING: killing 15620 states (over memory cap)
KLEE: WARNING: killing 15537 states (over memory cap)
KLEE: WARNING: killing 15191 states (over memory cap)
KLEE: WARNING: killing 15983 states (over memory cap)
KLEE: WARNING: killing 15504 states (over memory cap)
KLEE: WARNING: killing 15088 states (over memory cap)
KLEE: WARNING: killing 15943 states (over memory cap)
KLEE: WARNING: killing 15863 states (over memory cap)
KLEE: WARNING: killing 15718 states (over memory cap)
KLEE: WARNING: killing 16175 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 0x00007f8b4fb47390
4  libc.so.6       0x00007f8b4ef00428 gsignal + 56
5  libc.so.6       0x00007f8b4ef0202a abort + 362
6  libc.so.6       0x00007f8b4eef8bd7
7  libc.so.6       0x00007f8b4eef8c82
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       0x00007f8b4eeeb830 __libc_start_main + 240
16 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 670.805582047
