bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-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.: 126 99 785 4257
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.240854978561
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 '__const_udelay' (function is undefined)
Removed calls to '__udelay' (function is undefined)
Defining function queue_work_on as symbolic
Defining function snprintf as symbolic
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)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_suspend_late_4 as symbolic
Defining function ldv_restore_early_4 as symbolic
Defining function ldv_resume_early_4 as symbolic
Defining function ldv_resume_noirq_4 as symbolic
Defining function ldv_prepare_4 as symbolic
Defining function ldv_poweroff_4 as symbolic
Defining function ldv_poweroff_noirq_4 as symbolic
Defining function ldv_poweroff_late_4 as symbolic
Defining function ldv_restore_noirq_4 as symbolic
Defining function ldv_suspend_4 as symbolic
Defining function ldv_suspend_noirq_4 as symbolic
Defining function ldv_complete_4 as symbolic
Defining function ldv_release_3 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 platform_device_register_full as symbolic
Defining function __platform_driver_register as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strcmp
  __kmalloc
  __memcpy
  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.251280069351
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 200 104 463 2409
INFO: Starting verification
KLEE: WARNING ONCE: function "send_byte" has inline asm
KLEE: WARNING ONCE: function "read_smc" has inline asm
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_b8bcb3a9-c511-483d-a1df-b246bcff0b4b/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 12443 states (over memory cap)
KLEE: WARNING: killing 17179 states (over memory cap)
KLEE: WARNING: killing 17754 states (over memory cap)
KLEE: WARNING: killing 16928 states (over memory cap)
KLEE: WARNING: killing 16850 states (over memory cap)
KLEE: WARNING: killing 17243 states (over memory cap)
KLEE: WARNING: killing 17369 states (over memory cap)
KLEE: WARNING: killing 17949 states (over memory cap)
KLEE: WARNING: killing 9400 states (over memory cap)
KLEE: WARNING: killing 9296 states (over memory cap)
KLEE: WARNING: killing 9190 states (over memory cap)
KLEE: WARNING: killing 9176 states (over memory cap)
KLEE: WARNING: killing 9165 states (over memory cap)
KLEE: WARNING: killing 9425 states (over memory cap)
KLEE: WARNING: killing 9143 states (over memory cap)
KLEE: WARNING: killing 9220 states (over memory cap)
KLEE: WARNING: killing 17800 states (over memory cap)
KLEE: WARNING: killing 9364 states (over memory cap)
KLEE: WARNING: killing 17367 states (over memory cap)
KLEE: WARNING: killing 17769 states (over memory cap)
KLEE: WARNING: killing 9115 states (over memory cap)
KLEE: WARNING: killing 9012 states (over memory cap)
KLEE: WARNING: killing 8997 states (over memory cap)
KLEE: WARNING: killing 17278 states (over memory cap)
KLEE: WARNING: killing 8958 states (over memory cap)
KLEE: WARNING: killing 17120 states (over memory cap)
KLEE: WARNING: killing 9274 states (over memory cap)
KLEE: WARNING: killing 16778 states (over memory cap)
KLEE: WARNING: killing 9324 states (over memory cap)
KLEE: WARNING: killing 9138 states (over memory cap)
KLEE: WARNING: killing 8949 states (over memory cap)
KLEE: WARNING: killing 17295 states (over memory cap)
KLEE: WARNING: killing 9093 states (over memory cap)
KLEE: WARNING: killing 8910 states (over memory cap)
KLEE: WARNING: killing 9070 states (over memory cap)
KLEE: WARNING: killing 9063 states (over memory cap)
KLEE: WARNING: killing 8791 states (over memory cap)
KLEE: WARNING: killing 8781 states (over memory cap)
KLEE: WARNING: killing 8856 states (over memory cap)
KLEE: WARNING: killing 17117 states (over memory cap)
KLEE: WARNING: killing 9345 states (over memory cap)
KLEE: WARNING: killing 8813 states (over memory cap)
KLEE: WARNING: killing 8718 states (over memory cap)
KLEE: WARNING: killing 8793 states (over memory cap)
KLEE: WARNING: killing 8783 states (over memory cap)
KLEE: WARNING: killing 17064 states (over memory cap)
KLEE: WARNING: killing 9354 states (over memory cap)
KLEE: WARNING: killing 16919 states (over memory cap)
KLEE: WARNING: killing 9409 states (over memory cap)
KLEE: WARNING: killing 8878 states (over memory cap)
KLEE: WARNING: killing 16841 states (over memory cap)
KLEE: WARNING: killing 9448 states (over memory cap)
KLEE: WARNING: killing 8754 states (over memory cap)
KLEE: WARNING: killing 8742 states (over memory cap)
KLEE: WARNING: killing 8733 states (over memory cap)
KLEE: WARNING: killing 8641 states (over memory cap)
KLEE: WARNING: killing 8799 states (over memory cap)
KLEE: WARNING: killing 8789 states (over memory cap)
KLEE: WARNING: killing 8952 states (over memory cap)
KLEE: WARNING: killing 8605 states (over memory cap)
KLEE: WARNING: killing 8934 states (over memory cap)
KLEE: WARNING: killing 8925 states (over memory cap)
KLEE: WARNING: killing 8830 states (over memory cap)
KLEE: WARNING: killing 8990 states (over memory cap)
KLEE: WARNING: killing 8897 states (over memory cap)
KLEE: WARNING: killing 8803 states (over memory cap)
KLEE: WARNING: killing 8625 states (over memory cap)
KLEE: WARNING: killing 8699 states (over memory cap)
KLEE: WARNING: killing 8522 states (over memory cap)
KLEE: WARNING: killing 8595 states (over memory cap)
KLEE: WARNING: killing 8672 states (over memory cap)
KLEE: WARNING: killing 8745 states (over memory cap)
KLEE: WARNING: killing 8906 states (over memory cap)
KLEE: WARNING: killing 9152 states (over memory cap)
KLEE: WARNING: killing 8890 states (over memory cap)
KLEE: WARNING: killing 8797 states (over memory cap)
KLEE: WARNING: killing 8704 states (over memory cap)
KLEE: WARNING: killing 9115 states (over memory cap)
KLEE: WARNING: killing 8939 states (over memory cap)
KLEE: WARNING: killing 8681 states (over memory cap)
KLEE: WARNING: killing 8755 states (over memory cap)
KLEE: WARNING: killing 9076 states (over memory cap)
KLEE: WARNING: killing 8901 states (over memory cap)
KLEE: WARNING: killing 8564 states (over memory cap)
KLEE: WARNING: killing 8634 states (over memory cap)
KLEE: WARNING: killing 8955 states (over memory cap)
KLEE: WARNING: killing 8870 states (over memory cap)
KLEE: WARNING: killing 8694 states (over memory cap)
KLEE: WARNING: killing 8600 states (over memory cap)
KLEE: WARNING: killing 8673 states (over memory cap)
KLEE: WARNING: killing 9239 states (over memory cap)
KLEE: WARNING: killing 8985 states (over memory cap)
KLEE: WARNING: killing 8561 states (over memory cap)
KLEE: WARNING: killing 8716 states (over memory cap)
KLEE: WARNING: killing 8791 states (over memory cap)
KLEE: WARNING: killing 8861 states (over memory cap)
KLEE: WARNING: killing 9098 states (over memory cap)
KLEE: WARNING: killing 8600 states (over memory cap)
KLEE: WARNING: killing 8834 states (over memory cap)
KLEE: WARNING: killing 8666 states (over memory cap)
KLEE: WARNING: killing 8817 states (over memory cap)
KLEE: WARNING: killing 8811 states (over memory cap)
KLEE: WARNING: killing 8636 states (over memory cap)
KLEE: WARNING: killing 9280 states (over memory cap)
KLEE: WARNING: killing 8949 states (over memory cap)
KLEE: WARNING: killing 8451 states (over memory cap)
KLEE: WARNING: killing 8521 states (over memory cap)
KLEE: WARNING: killing 8591 states (over memory cap)
KLEE: WARNING: killing 8985 states (over memory cap)
KLEE: WARNING: killing 8655 states (over memory cap)
KLEE: WARNING: killing 8725 states (over memory cap)
KLEE: WARNING: killing 8800 states (over memory cap)
KLEE: WARNING: killing 9032 states (over memory cap)
KLEE: WARNING: killing 8943 states (over memory cap)
KLEE: WARNING: killing 9175 states (over memory cap)
KLEE: WARNING: killing 9006 states (over memory cap)
KLEE: WARNING: killing 8996 states (over memory cap)
KLEE: WARNING: killing 8910 states (over memory cap)
KLEE: WARNING: killing 8340 states (over memory cap)
KLEE: WARNING: killing 8811 states (over memory cap)
KLEE: WARNING: killing 9122 states (over memory cap)
KLEE: WARNING: killing 8634 states (over memory cap)
KLEE: WARNING: killing 8706 states (over memory cap)
KLEE: WARNING: killing 8537 states (over memory cap)
KLEE: WARNING: killing 8925 states (over memory cap)
KLEE: WARNING: killing 8837 states (over memory cap)
KLEE: WARNING: killing 8827 states (over memory cap)
KLEE: WARNING: killing 8898 states (over memory cap)
KLEE: WARNING: killing 8810 states (over memory cap)
KLEE: WARNING: killing 8568 states (over memory cap)
KLEE: WARNING: killing 8796 states (over memory cap)
KLEE: WARNING: killing 8787 states (over memory cap)
KLEE: WARNING: killing 9016 states (over memory cap)
KLEE: WARNING: killing 9006 states (over memory cap)
KLEE: WARNING: killing 8523 states (over memory cap)
KLEE: WARNING: killing 8437 states (over memory cap)
KLEE: WARNING: killing 8817 states (over memory cap)
KLEE: WARNING: killing 8813 states (over memory cap)
KLEE: WARNING: killing 9041 states (over memory cap)
KLEE: WARNING: killing 9032 states (over memory cap)
KLEE: WARNING: killing 8870 states (over memory cap)
KLEE: WARNING: killing 8858 states (over memory cap)
KLEE: WARNING: killing 8928 states (over memory cap)
KLEE: WARNING: killing 8607 states (over memory cap)
KLEE: WARNING: killing 8595 states (over memory cap)
KLEE: WARNING: killing 9054 states (over memory cap)
KLEE: WARNING: killing 8654 states (over memory cap)
KLEE: WARNING: killing 8649 states (over memory cap)
KLEE: WARNING: killing 8951 states (over memory cap)
KLEE: WARNING: killing 8862 states (over memory cap)
KLEE: WARNING: killing 8857 states (over memory cap)
KLEE: WARNING: killing 8769 states (over memory cap)
KLEE: WARNING: killing 8914 states (over memory cap)
KLEE: WARNING: killing 8523 states (over memory cap)
KLEE: WARNING: killing 8897 states (over memory cap)
KLEE: WARNING: killing 8814 states (over memory cap)
KLEE: WARNING: killing 8805 states (over memory cap)
KLEE: WARNING: killing 9109 states (over memory cap)
KLEE: WARNING: killing 8792 states (over memory cap)
KLEE: WARNING: killing 8785 states (over memory cap)
KLEE: WARNING: killing 9082 states (over memory cap)
KLEE: WARNING: killing 8686 states (over memory cap)
KLEE: WARNING: killing 8756 states (over memory cap)
KLEE: WARNING: killing 8905 states (over memory cap)
KLEE: WARNING: killing 8895 states (over memory cap)
KLEE: WARNING: killing 8350 states (over memory cap)
KLEE: WARNING: killing 8724 states (over memory cap)
KLEE: WARNING: killing 8639 states (over memory cap)
KLEE: WARNING: killing 8936 states (over memory cap)
KLEE: WARNING: killing 8700 states (over memory cap)
KLEE: WARNING: killing 8844 states (over memory cap)
KLEE: WARNING: killing 8837 states (over memory cap)
KLEE: WARNING: killing 8449 states (over memory cap)
KLEE: WARNING: killing 9199 states (over memory cap)
KLEE: WARNING: killing 8737 states (over memory cap)
KLEE: WARNING: killing 8505 states (over memory cap)
KLEE: WARNING: killing 9105 states (over memory cap)
KLEE: WARNING: killing 9100 states (over memory cap)
KLEE: WARNING: killing 8710 states (over memory cap)
KLEE: WARNING: killing 8705 states (over memory cap)
KLEE: WARNING: killing 8774 states (over memory cap)
KLEE: WARNING: killing 8917 states (over memory cap)
KLEE: WARNING: killing 8679 states (over memory cap)
KLEE: WARNING: killing 8372 states (over memory cap)
KLEE: WARNING: killing 8589 states (over memory cap)
KLEE: WARNING: killing 8884 states (over memory cap)
KLEE: WARNING: killing 8726 states (over memory cap)
KLEE: WARNING: killing 8868 states (over memory cap)
KLEE: WARNING: killing 8638 states (over memory cap)
KLEE: WARNING: killing 8781 states (over memory cap)
KLEE: WARNING: killing 8698 states (over memory cap)
KLEE: WARNING: killing 8692 states (over memory cap)
KLEE: WARNING: killing 8531 states (over memory cap)
KLEE: WARNING: killing 8676 states (over memory cap)
KLEE: WARNING: killing 8967 states (over memory cap)
KLEE: WARNING: killing 8887 states (over memory cap)
KLEE: WARNING: killing 8655 states (over memory cap)
KLEE: WARNING: killing 9095 states (over memory cap)
KLEE: WARNING: killing 8638 states (over memory cap)
KLEE: WARNING: killing 8778 states (over memory cap)
KLEE: WARNING: killing 8997 states (over memory cap)
KLEE: WARNING: killing 8769 states (over memory cap)
KLEE: WARNING: killing 8835 states (over memory cap)
KLEE: WARNING: killing 8978 states (over memory cap)
KLEE: WARNING: killing 9047 states (over memory cap)
KLEE: WARNING: killing 8447 states (over memory cap)
KLEE: WARNING: killing 8591 states (over memory cap)
KLEE: WARNING: killing 9026 states (over memory cap)
KLEE: WARNING: killing 8867 states (over memory cap)
