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--hwmon--applesmc.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.: 141 169 1119 5551
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.291472911835
Defining function queue_work_on as symbolic
Defining function printk as symbolic
Defining function snprintf as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to '__udelay' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function kstrtoull as symbolic
Defining function sprintf as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'hwmon_device_unregister' (function is undefined)
Removed calls to 'platform_device_unregister' (function is undefined)
Removed calls to 'platform_driver_unregister' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to 'input_set_abs_params' (function is undefined)
Removed calls to 'input_free_polled_device' (function is undefined)
Defining function ldv_remove_4 as symbolic
Defining function ldv_suspend_late_5 as symbolic
Defining function ldv_restore_early_5 as symbolic
Defining function ldv_resume_early_5 as symbolic
Defining function ldv_resume_noirq_5 as symbolic
Defining function ldv_prepare_5 as symbolic
Defining function ldv_poweroff_5 as symbolic
Defining function ldv_poweroff_noirq_5 as symbolic
Defining function ldv_poweroff_late_5 as symbolic
Defining function ldv_restore_noirq_5 as symbolic
Defining function ldv_suspend_5 as symbolic
Defining function ldv_suspend_noirq_5 as symbolic
Defining function ldv_complete_5 as symbolic
Defining function dmi_check_system as symbolic
Defining function __request_region as symbolic
Defining function hwmon_device_register as symbolic
Removed calls to 'led_classdev_unregister' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'input_unregister_polled_device' (function is undefined)
Removed calls to 'sysfs_remove_file_ns' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function led_classdev_register as symbolic
Defining function input_allocate_polled_device as symbolic
Removed calls to 'input_event' (function is undefined)
Defining function input_register_polled_device as symbolic
Defining function sysfs_create_file_ns as symbolic
Defining function platform_device_register_full as symbolic
Defining function __platform_driver_register as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  strcmp
  __kmalloc
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.32473897934
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 211 174 759 3492
INFO: Starting verification
KLEE: WARNING ONCE: function "read_smc" has inline asm
KLEE: WARNING ONCE: function "send_byte" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_2751e767-8ab6-4831-aac9-6eea723e4cbd/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 ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 17009 states (over memory cap)
KLEE: WARNING: killing 17518 states (over memory cap)
KLEE: WARNING: killing 17246 states (over memory cap)
KLEE: WARNING: killing 17668 states (over memory cap)
KLEE: WARNING: killing 17889 states (over memory cap)
KLEE: WARNING: killing 17915 states (over memory cap)
KLEE: WARNING: killing 18332 states (over memory cap)
KLEE: WARNING: killing 18661 states (over memory cap)
KLEE: WARNING: killing 10214 states (over memory cap)
KLEE: WARNING: killing 18482 states (over memory cap)
KLEE: WARNING: killing 10266 states (over memory cap)
KLEE: WARNING: killing 18880 states (over memory cap)
KLEE: WARNING: killing 10510 states (over memory cap)
KLEE: WARNING: killing 9726 states (over memory cap)
KLEE: WARNING: killing 9617 states (over memory cap)
KLEE: WARNING: killing 18952 states (over memory cap)
KLEE: WARNING: killing 9963 states (over memory cap)
KLEE: WARNING: killing 9663 states (over memory cap)
KLEE: WARNING: killing 10125 states (over memory cap)
KLEE: WARNING: killing 9926 states (over memory cap)
KLEE: WARNING: killing 9910 states (over memory cap)
KLEE: WARNING: killing 18883 states (over memory cap)
KLEE: WARNING: killing 10064 states (over memory cap)
KLEE: WARNING: killing 9575 states (over memory cap)
KLEE: WARNING: killing 9468 states (over memory cap)
KLEE: WARNING: killing 9551 states (over memory cap)
KLEE: WARNING: killing 9628 states (over memory cap)
KLEE: WARNING: killing 9616 states (over memory cap)
KLEE: WARNING: killing 9698 states (over memory cap)
KLEE: WARNING: killing 9406 states (over memory cap)
KLEE: WARNING: killing 18538 states (over memory cap)
KLEE: WARNING: killing 10207 states (over memory cap)
KLEE: WARNING: killing 9451 states (over memory cap)
KLEE: WARNING: killing 18251 states (over memory cap)
KLEE: WARNING: killing 9785 states (over memory cap)
KLEE: WARNING: killing 18649 states (over memory cap)
KLEE: WARNING: killing 9744 states (over memory cap)
KLEE: WARNING: killing 9364 states (over memory cap)
KLEE: WARNING: killing 9349 states (over memory cap)
KLEE: WARNING: killing 9616 states (over memory cap)
KLEE: WARNING: killing 9507 states (over memory cap)
KLEE: WARNING: killing 9866 states (over memory cap)
KLEE: WARNING: killing 9394 states (over memory cap)
KLEE: WARNING: killing 9477 states (over memory cap)
KLEE: WARNING: killing 9648 states (over memory cap)
KLEE: WARNING: killing 9547 states (over memory cap)
KLEE: WARNING: killing 9808 states (over memory cap)
KLEE: WARNING: killing 9252 states (over memory cap)
KLEE: WARNING: killing 9784 states (over memory cap)
KLEE: WARNING: killing 9503 states (over memory cap)
KLEE: WARNING: killing 9490 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-bSYbl2/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "read_smc" has inline asm
KLEE: WARNING ONCE: function "send_byte" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_2751e767-8ab6-4831-aac9-6eea723e4cbd/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 ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 17009 states (over memory cap)
KLEE: WARNING: killing 17518 states (over memory cap)
KLEE: WARNING: killing 17246 states (over memory cap)
KLEE: WARNING: killing 17668 states (over memory cap)
KLEE: WARNING: killing 17889 states (over memory cap)
KLEE: WARNING: killing 17915 states (over memory cap)
KLEE: WARNING: killing 18332 states (over memory cap)
KLEE: WARNING: killing 18661 states (over memory cap)
KLEE: WARNING: killing 10214 states (over memory cap)
KLEE: WARNING: killing 18482 states (over memory cap)
KLEE: WARNING: killing 10266 states (over memory cap)
KLEE: WARNING: killing 18880 states (over memory cap)
KLEE: WARNING: killing 10510 states (over memory cap)
KLEE: WARNING: killing 9726 states (over memory cap)
KLEE: WARNING: killing 9617 states (over memory cap)
KLEE: WARNING: killing 18952 states (over memory cap)
KLEE: WARNING: killing 9963 states (over memory cap)
KLEE: WARNING: killing 9663 states (over memory cap)
KLEE: WARNING: killing 10125 states (over memory cap)
KLEE: WARNING: killing 9926 states (over memory cap)
KLEE: WARNING: killing 9910 states (over memory cap)
KLEE: WARNING: killing 18883 states (over memory cap)
KLEE: WARNING: killing 10064 states (over memory cap)
KLEE: WARNING: killing 9575 states (over memory cap)
KLEE: WARNING: killing 9468 states (over memory cap)
KLEE: WARNING: killing 9551 states (over memory cap)
KLEE: WARNING: killing 9628 states (over memory cap)
KLEE: WARNING: killing 9616 states (over memory cap)
KLEE: WARNING: killing 9698 states (over memory cap)
KLEE: WARNING: killing 9406 states (over memory cap)
KLEE: WARNING: killing 18538 states (over memory cap)
KLEE: WARNING: killing 10207 states (over memory cap)
KLEE: WARNING: killing 9451 states (over memory cap)
KLEE: WARNING: killing 18251 states (over memory cap)
KLEE: WARNING: killing 9785 states (over memory cap)
KLEE: WARNING: killing 18649 states (over memory cap)
KLEE: WARNING: killing 9744 states (over memory cap)
KLEE: WARNING: killing 9364 states (over memory cap)
KLEE: WARNING: killing 9349 states (over memory cap)
KLEE: WARNING: killing 9616 states (over memory cap)
KLEE: WARNING: killing 9507 states (over memory cap)
KLEE: WARNING: killing 9866 states (over memory cap)
KLEE: WARNING: killing 9394 states (over memory cap)
KLEE: WARNING: killing 9477 states (over memory cap)
KLEE: WARNING: killing 9648 states (over memory cap)
KLEE: WARNING: killing 9547 states (over memory cap)
KLEE: WARNING: killing 9808 states (over memory cap)
KLEE: WARNING: killing 9252 states (over memory cap)
KLEE: WARNING: killing 9784 states (over memory cap)
KLEE: WARNING: killing 9503 states (over memory cap)
KLEE: WARNING: killing 9490 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 0x00007f380231a390
4  libc.so.6       0x00007f38016d3428 gsignal + 56
5  libc.so.6       0x00007f38016d502a abort + 362
6  libc.so.6       0x00007f38016cbbd7
7  libc.so.6       0x00007f38016cbc82
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       0x00007f38016be830 __libc_start_main + 240
16 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 202.354620934
