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/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--arcnet--arc-rawmode.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.: 19 43 198 1079
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.203953027725
Defining function printk as symbolic
Defining function skb_push as symbolic
Defining function skb_put as symbolic
Defining function skb_pull as symbolic
Removed calls to 'arcnet_unregister_proto' (function is undefined)
Linked our definitions to these undefined functions:
  __memcpy
  __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
  __VERIFIER_nondet_ushort_named
INFO: After-slicing optimizations and preparation time: 0.233538150787
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 59 48 131 693
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_219473cf-b02b-4ff5-8186-c9f66fdde643/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 9604 states (over memory cap)
KLEE: WARNING: killing 9300 states (over memory cap)
KLEE: WARNING: killing 9458 states (over memory cap)
KLEE: WARNING: killing 8805 states (over memory cap)
KLEE: WARNING: killing 8197 states (over memory cap)
KLEE: WARNING: killing 8201 states (over memory cap)
KLEE: WARNING: killing 7834 states (over memory cap)
KLEE: WARNING: killing 7741 states (over memory cap)
KLEE: WARNING: killing 7046 states (over memory cap)
KLEE: WARNING: killing 7078 states (over memory cap)
KLEE: WARNING: killing 7047 states (over memory cap)
KLEE: WARNING: killing 6764 states (over memory cap)
KLEE: WARNING: killing 6493 states (over memory cap)
KLEE: WARNING: killing 6147 states (over memory cap)
KLEE: WARNING: killing 5997 states (over memory cap)
KLEE: WARNING: killing 5916 states (over memory cap)
KLEE: WARNING: killing 6016 states (over memory cap)
KLEE: WARNING: killing 5891 states (over memory cap)
KLEE: WARNING: killing 5481 states (over memory cap)
KLEE: WARNING: killing 5503 states (over memory cap)
KLEE: WARNING: killing 5534 states (over memory cap)
KLEE: WARNING: killing 5572 states (over memory cap)
KLEE: WARNING: killing 5670 states (over memory cap)
KLEE: WARNING: killing 5223 states (over memory cap)
KLEE: WARNING: killing 5285 states (over memory cap)
KLEE: WARNING: killing 5410 states (over memory cap)
KLEE: WARNING: killing 5448 states (over memory cap)
KLEE: WARNING: killing 5480 states (over memory cap)
