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--lm78.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.: 210 139 1076 6217
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.243494987488
Removed calls to '__dynamic_dev_dbg' (function is undefined)
Defining function sprintf as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function i2c_smbus_read_byte_data as symbolic
Defining function i2c_smbus_write_byte_data as symbolic
Defining function kstrtoull as symbolic
Defining function kstrtoll as symbolic
Removed calls to 'dev_err' (function is undefined)
Defining function vid_from_reg as symbolic
Removed calls to '__mutex_init' (function is undefined)
Defining function strlcpy as symbolic
Defining function devm_hwmon_device_register_with_groups as symbolic
Defining function devm_kmalloc as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'i2c_del_driver' (function is undefined)
Defining function ldv_release_1 as symbolic
Defining function i2c_register_driver as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  __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.353932142258
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 289 135 653 4962
INFO: Starting verification
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_70e3bb95-fb61-43ed-be5b-993a3d25a8e3/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 41996 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 38478 states (over memory cap)
KLEE: WARNING: killing 40288 states (over memory cap)
KLEE: WARNING: killing 40732 states (over memory cap)
KLEE: WARNING: killing 42139 states (over memory cap)
KLEE: WARNING: killing 44153 states (over memory cap)
KLEE: WARNING: killing 45242 states (over memory cap)
KLEE: WARNING: killing 46368 states (over memory cap)
KLEE: WARNING: killing 44933 states (over memory cap)
KLEE: WARNING: killing 44213 states (over memory cap)
KLEE: WARNING: killing 42890 states (over memory cap)
KLEE: WARNING: killing 42733 states (over memory cap)
KLEE: WARNING: killing 43140 states (over memory cap)
KLEE: WARNING: killing 43472 states (over memory cap)
KLEE: WARNING: killing 44426 states (over memory cap)
KLEE: WARNING: killing 43767 states (over memory cap)
KLEE: WARNING: killing 43704 states (over memory cap)
KLEE: WARNING: killing 46389 states (over memory cap)
KLEE: WARNING: killing 41889 states (over memory cap)
KLEE: WARNING: killing 44632 states (over memory cap)
KLEE: WARNING: killing 45034 states (over memory cap)
KLEE: WARNING: killing 43947 states (over memory cap)
KLEE: WARNING: killing 42489 states (over memory cap)
KLEE: WARNING: killing 44755 states (over memory cap)
KLEE: WARNING: killing 43752 states (over memory cap)
KLEE: WARNING: killing 42577 states (over memory cap)
KLEE: WARNING: killing 46798 states (over memory cap)
KLEE: WARNING: killing 41460 states (over memory cap)
KLEE: WARNING: killing 43613 states (over memory cap)
KLEE: WARNING: killing 43060 states (over memory cap)
KLEE: WARNING: killing 41970 states (over memory cap)
KLEE: WARNING: killing 45370 states (over memory cap)
KLEE: WARNING: killing 44246 states (over memory cap)
KLEE: WARNING: killing 44306 states (over memory cap)
KLEE: WARNING: killing 44378 states (over memory cap)
KLEE: WARNING: killing 42139 states (over memory cap)
KLEE: WARNING: killing 44380 states (over memory cap)
KLEE: WARNING: killing 44065 states (over memory cap)
KLEE: WARNING: killing 42988 states (over memory cap)
KLEE: WARNING: killing 44288 states (over memory cap)
KLEE: WARNING: killing 44417 states (over memory cap)
KLEE: WARNING: killing 45145 states (over memory cap)
KLEE: WARNING: killing 44279 states (over memory cap)
KLEE: WARNING: killing 41565 states (over memory cap)
KLEE: WARNING: killing 45028 states (over memory cap)
KLEE: WARNING: killing 41564 states (over memory cap)
KLEE: WARNING: killing 44782 states (over memory cap)
KLEE: WARNING: killing 44579 states (over memory cap)
KLEE: WARNING: killing 45311 states (over memory cap)
KLEE: WARNING: killing 46164 states (over memory cap)
KLEE: WARNING: killing 40684 states (over memory cap)
KLEE: WARNING: killing 46044 states (over memory cap)
KLEE: WARNING: killing 42277 states (over memory cap)
KLEE: WARNING: killing 45552 states (over memory cap)
KLEE: WARNING: killing 43527 states (over memory cap)
KLEE: WARNING: killing 43954 states (over memory cap)
KLEE: WARNING: killing 43187 states (over memory cap)
KLEE: WARNING: killing 42965 states (over memory cap)
KLEE: WARNING: killing 45894 states (over memory cap)
KLEE: WARNING: killing 42303 states (over memory cap)
KLEE: WARNING: killing 44417 states (over memory cap)
KLEE: WARNING: killing 44681 states (over memory cap)
KLEE: WARNING: killing 43428 states (over memory cap)
KLEE: WARNING: killing 43235 states (over memory cap)
KLEE: WARNING: killing 44864 states (over memory cap)
KLEE: WARNING: killing 43553 states (over memory cap)
KLEE: WARNING: killing 43660 states (over memory cap)
KLEE: WARNING: killing 42870 states (over memory cap)
KLEE: WARNING: killing 44545 states (over memory cap)
KLEE: WARNING: killing 44673 states (over memory cap)
KLEE: WARNING: killing 44606 states (over memory cap)
KLEE: WARNING: killing 44376 states (over memory cap)
KLEE: WARNING: killing 43521 states (over memory cap)
KLEE: WARNING: killing 45242 states (over memory cap)
KLEE: WARNING: killing 44976 states (over memory cap)
KLEE: WARNING: killing 43486 states (over memory cap)
KLEE: WARNING: killing 44005 states (over memory cap)
KLEE: WARNING: killing 41526 states (over memory cap)
KLEE: WARNING: killing 44537 states (over memory cap)
KLEE: WARNING: killing 45508 states (over memory cap)
KLEE: WARNING: killing 45931 states (over memory cap)
KLEE: WARNING: killing 42706 states (over memory cap)
KLEE: WARNING: killing 45072 states (over memory cap)
KLEE: WARNING: killing 39552 states (over memory cap)
KLEE: WARNING: killing 43969 states (over memory cap)
KLEE: WARNING: killing 44314 states (over memory cap)
KLEE: WARNING: killing 46449 states (over memory cap)
KLEE: WARNING: killing 43019 states (over memory cap)
KLEE: WARNING: killing 43622 states (over memory cap)
