bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful.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.: 193 482 3558 24738
Removed infinite loop in ttm_mem_unregister_shrink
Removed infinite loop in ttm_bo_add_to_lru
Removed infinite loop in ttm_bo_ref_bug
Removed infinite loop in ttm_bo_release_list
Removed infinite loop in ttm_tt_unbind
Removed infinite loop in ttm_tt_swapin
Removed infinite loop in ttm_get_kobj
Removed infinite loop in arch_local_save_flags
Removed infinite loop in ttm_tt_swapout
Removed infinite loop in ttm_mem_evict_first
Removed infinite loop in ttm_bo_evict
Removed infinite loop in ttm_bo_move_buffer
Removed infinite loop in ttm_bo_validate
Removed infinite loop in ttm_bo_check_placement
Removed infinite loop in ttm_bo_vm_insert_rb
Removed infinite loop in ttm_bo_init_mm
Removed infinite loop in ttm_bo_device_release
Removed infinite loop in ttm_bo_kmap
Removed infinite loop in ttm_bo_kmap_ttm
Removed infinite loop in ttm_bo_kunmap
Removed infinite loop in ttm_ref_object_add
Removed infinite loop in ttm_read_trylock
Removed infinite loop in ttm_vt_lock_remove
INFO: Compilation, preparation and instrumentation time: 0.904083013535
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'drm_mm_takedown' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'drm_mm_put_block' (function is undefined)
Removed calls to 'drm_mm_debug_table' (function is undefined)
Defining function drm_mm_pre_get as symbolic
Defining function drm_mm_get_block_range_generic as symbolic
Defining function drm_mm_search_free_in_range_generic as symbolic
Defining function drm_mm_clean as symbolic
Defining function drm_mm_init as symbolic
Removed calls to 'agp_free_memory' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Defining function agp_unbind_memory as symbolic
Defining function agp_allocate_memory as symbolic
Defining function agp_bind_memory as symbolic
Defining function printk as symbolic
Defining function sscanf as symbolic
Defining function queue_work as symbolic
Defining function snprintf as symbolic
Removed calls to '__free_pages' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function vm_get_page_prot as symbolic
Defining function vm_insert_mixed as symbolic
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function pgprot_writecombine as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'unmap_mapping_range' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Defining function mutex_lock_interruptible as symbolic
Removed calls to 'fput' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function autoremove_wake_function as symbolic
Removed calls to '_raw_write_lock' (function is undefined)
Removed calls to 'rb_erase' (function is undefined)
Removed calls to '_raw_write_unlock' (function is undefined)
Defining function schedule_delayed_work as symbolic
Defining function __vmalloc as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'clear_page' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Removed calls to 'copy_page' (function is undefined)
Defining function shmem_read_mapping_page_gfp as symbolic
Defining function capable as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function set_pages_array_wb as symbolic
Removed calls to 'list_del' (function is undefined)
Defining function set_pages_array_uc as symbolic
Defining function set_pages_array_wc as symbolic
Defining function alloc_pages_current as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'kobject_put' (function is undefined)
Removed calls to 'si_meminfo' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function kobject_init_and_add as symbolic
Removed calls to 'register_shrinker' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'kobject_del' (function is undefined)
Removed calls to 'unregister_shrinker' (function is undefined)
Defining function devres_destroy as symbolic
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Removed calls to 'drm_clflush_pages' (function is undefined)
Defining function set_pages_wb as symbolic
Defining function set_memory_wc as symbolic
Defining function set_pages_uc as symbolic
Removed calls to 'mark_page_accessed' (function is undefined)
Defining function shmem_file_setup as symbolic
Defining function set_page_dirty as symbolic
Defining function mutex_trylock as symbolic
Defining function cancel_delayed_work_sync as symbolic
Removed calls to 'iowrite32' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Defining function ioread32 as symbolic
Defining function ioremap_wc as symbolic
Defining function ioremap_nocache as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'rb_insert_color' (function is undefined)
Defining function drm_mm_get_block_generic as symbolic
Defining function drm_mm_search_free_generic as symbolic
Removed calls to '__rwlock_init' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Defining function vmap as symbolic
Removed calls to 'vunmap' (function is undefined)
Removed calls to '_raw_read_lock' (function is undefined)
Removed calls to '_raw_read_unlock' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Removed calls to 'drm_class_device_unregister' (function is undefined)
Defining function dev_set_name as symbolic
Defining function drm_class_device_register as symbolic
Defining function drm_ht_just_insert_please as symbolic
Defining function drm_ht_remove_item as symbolic
Defining function drm_ht_find_item as symbolic
Defining function drm_ht_insert_item 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 debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_cpu_idle as symbolic
Removed calls to 'drm_ht_remove' (function is undefined)
Defining function drm_ht_create as symbolic
Defining function send_sig as symbolic
Defining function seq_printf as symbolic
Removed calls to 'devres_add' (function is undefined)
Removed calls to 'devres_free' (function is undefined)
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Defining function __phys_addr as symbolic
Defining function __devres_alloc as symbolic
Defining function dev_driver_string as symbolic
Defining function __kmalloc_node as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_long_named
  __VERIFIER_nondet_pointer_named
INFO: After-slicing optimizations and preparation time: 0.98538517952
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 355 389 2242 13782
INFO: Starting verification
KLEE: WARNING ONCE: function "ttm_bo_global_kobj_release" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_vm_open" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_vm_fault" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_reserve" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_wait" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_add_to_lru" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_wait_unreserved" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_unref" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_cleanup_refs_or_queue" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_release_list" has inline asm
KLEE: WARNING ONCE: function "kref_sub" has inline asm
KLEE: WARNING ONCE: function "ttm_tt_unbind" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_ref_bug" has inline asm
KLEE: WARNING ONCE: function "ttm_tt_swapin" has inline asm
KLEE: WARNING ONCE: function "copy_highpage" has inline asm
KLEE: WARNING ONCE: function "__ttm_dma_free_page" has inline asm
KLEE: WARNING ONCE: function "ttm_dma_pool_mm_shrink" has inline asm
KLEE: WARNING ONCE: function "ttm_pool_mm_shrink" has inline asm
KLEE: WARNING ONCE: function "ttm_tt_swapout" has inline asm
KLEE: WARNING ONCE: function "ttm_mem_evict_first" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_cleanup_refs_and_unlock" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_move_memcpy" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_move_buffer" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_validate" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_check_placement" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_init" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_init_mm" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_swapout" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_device_release" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_delayed_delete" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_synccpu_write_grab" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_synccpu_write_release" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_kmap" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_kunmap" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_move_accel_cleanup" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_mmap" has inline asm
KLEE: WARNING ONCE: function "ttm_fbdev_mmap" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_io" has inline asm
KLEE: WARNING ONCE: function "ldv_main6_sequence_infinite_withcheck_stateful" has inline asm
KLEE: WARNING ONCE: function "ttm_base_object_init" has inline asm
KLEE: WARNING ONCE: function "ttm_ref_object_add" has inline asm
KLEE: WARNING ONCE: function "ttm_base_object_unref" has inline asm
KLEE: WARNING ONCE: function "ttm_base_object_lookup" has inline asm
KLEE: WARNING ONCE: function "ttm_ref_object_base_unref" has inline asm
KLEE: WARNING ONCE: function "ttm_object_file_unref" has inline asm
KLEE: WARNING ONCE: function "ttm_read_lock" has inline asm
KLEE: WARNING ONCE: function "__ttm_read_lock" has inline asm
KLEE: WARNING ONCE: function "ttm_read_trylock" has inline asm
KLEE: WARNING ONCE: function "__ttm_read_trylock" has inline asm
KLEE: WARNING ONCE: function "ttm_write_lock" has inline asm
KLEE: WARNING ONCE: function "__ttm_write_lock" has inline asm
KLEE: WARNING ONCE: function "ttm_vt_lock" has inline asm
KLEE: WARNING ONCE: function "ttm_vt_lock_remove" has inline asm
KLEE: WARNING ONCE: function "ttm_suspend_lock" has inline asm
KLEE: WARNING ONCE: function "ttm_eu_list_ref_sub" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/symbiotic-wLPF1b/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:10444: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 9576 bytes on read, may be slow and/or crash: MO80[9576] allocated at global:
KLEE: ERROR: /tmp/symbiotic-wLPF1b/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:10444: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wLPF1b/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:10446: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wLPF1b/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:10446: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wLPF1b/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:10449: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
klee: /var/xchalup4/symbiotic/klee/lib/Core/SpecialFunctionHandler.cpp:250: std::__cxx11::string klee::SpecialFunctionHandler::readStringAtAddress(klee::ExecutionState&, klee::ref<klee::Expr>): Assertion `isa<ConstantExpr>(cur) && "hit symbolic char while reading concrete string"' failed.
KLEE: output directory is "/tmp/symbiotic-wLPF1b/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "ttm_bo_global_kobj_release" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_vm_open" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_vm_fault" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_reserve" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_wait" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_add_to_lru" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_wait_unreserved" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_unref" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_cleanup_refs_or_queue" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_release_list" has inline asm
KLEE: WARNING ONCE: function "kref_sub" has inline asm
KLEE: WARNING ONCE: function "ttm_tt_unbind" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_ref_bug" has inline asm
KLEE: WARNING ONCE: function "ttm_tt_swapin" has inline asm
KLEE: WARNING ONCE: function "copy_highpage" has inline asm
KLEE: WARNING ONCE: function "__ttm_dma_free_page" has inline asm
KLEE: WARNING ONCE: function "ttm_dma_pool_mm_shrink" has inline asm
KLEE: WARNING ONCE: function "ttm_pool_mm_shrink" has inline asm
KLEE: WARNING ONCE: function "ttm_tt_swapout" has inline asm
KLEE: WARNING ONCE: function "ttm_mem_evict_first" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_cleanup_refs_and_unlock" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_move_memcpy" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_move_buffer" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_validate" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_check_placement" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_init" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_init_mm" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_swapout" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_device_release" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_delayed_delete" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_synccpu_write_grab" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_synccpu_write_release" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_kmap" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_kunmap" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_move_accel_cleanup" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_mmap" has inline asm
KLEE: WARNING ONCE: function "ttm_fbdev_mmap" has inline asm
KLEE: WARNING ONCE: function "ttm_bo_io" has inline asm
KLEE: WARNING ONCE: function "ldv_main6_sequence_infinite_withcheck_stateful" has inline asm
KLEE: WARNING ONCE: function "ttm_base_object_init" has inline asm
KLEE: WARNING ONCE: function "ttm_ref_object_add" has inline asm
KLEE: WARNING ONCE: function "ttm_base_object_unref" has inline asm
KLEE: WARNING ONCE: function "ttm_base_object_lookup" has inline asm
KLEE: WARNING ONCE: function "ttm_ref_object_base_unref" has inline asm
KLEE: WARNING ONCE: function "ttm_object_file_unref" has inline asm
KLEE: WARNING ONCE: function "ttm_read_lock" has inline asm
KLEE: WARNING ONCE: function "__ttm_read_lock" has inline asm
KLEE: WARNING ONCE: function "ttm_read_trylock" has inline asm
KLEE: WARNING ONCE: function "__ttm_read_trylock" has inline asm
KLEE: WARNING ONCE: function "ttm_write_lock" has inline asm
KLEE: WARNING ONCE: function "__ttm_write_lock" has inline asm
KLEE: WARNING ONCE: function "ttm_vt_lock" has inline asm
KLEE: WARNING ONCE: function "ttm_vt_lock_remove" has inline asm
KLEE: WARNING ONCE: function "ttm_suspend_lock" has inline asm
KLEE: WARNING ONCE: function "ttm_eu_list_ref_sub" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/symbiotic-wLPF1b/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:10444: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 9576 bytes on read, may be slow and/or crash: MO80[9576] allocated at global:
KLEE: ERROR: /tmp/symbiotic-wLPF1b/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:10444: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wLPF1b/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:10446: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wLPF1b/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:10446: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wLPF1b/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c:10449: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
klee: /var/xchalup4/symbiotic/klee/lib/Core/SpecialFunctionHandler.cpp:250: std::__cxx11::string klee::SpecialFunctionHandler::readStringAtAddress(klee::ExecutionState&, klee::ref<klee::Expr>): Assertion `isa<ConstantExpr>(cur) && "hit symbolic char while reading concrete string"' 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 0x00007f4c62a38390
4  libc.so.6       0x00007f4c61df1428 gsignal + 56
5  libc.so.6       0x00007f4c61df302a abort + 362
6  libc.so.6       0x00007f4c61de9bd7
7  libc.so.6       0x00007f4c61de9c82
8  klee            0x00000000005f7297 klee::SpecialFunctionHandler::readStringAtAddress[abi:cxx11](klee::ExecutionState&, klee::ref<klee::Expr>) + 1607
9  klee            0x00000000005f8ba7 klee::SpecialFunctionHandler::handleMakeSymbolic(klee::ExecutionState&, klee::KInstruction*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 183
10 klee            0x00000000005f6b9f klee::SpecialFunctionHandler::handle(klee::ExecutionState&, llvm::Function*, klee::KInstruction*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 143
11 klee            0x00000000005cdfa3 klee::Executor::callExternalFunction(klee::ExecutionState&, klee::KInstruction*, llvm::Function*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 83
12 klee            0x00000000005d3229 klee::Executor::executeCall(klee::ExecutionState&, klee::KInstruction*, llvm::Function*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 1321
13 klee            0x00000000005d8788 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 14952
14 klee            0x00000000005da8c5 klee::Executor::run(klee::ExecutionState&) + 2117
15 klee            0x00000000005daeef klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1391
16 klee            0x0000000000593c63 main + 8867
17 libc.so.6       0x00007f4c61ddc830 __libc_start_main + 240
18 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 420.531742096
