bin/symbiotic --witness witness.graphml --no-slice --no-prepare --32 --prp=../sv-benchmarks/c/ReachSafety.prp ../sv-benchmarks/c/ntdrivers/cdaudio_true-unreach-call.i.cil.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.: 47 87 1901 13278
INFO: Compilation, preparation and instrumentation time: 0.373483896255
Defining function IoOpenDeviceRegistryKey as symbolic
Defining function MmLockPagableDataSection as symbolic
Defining function RtlWriteRegistryValue as symbolic
Defining function InterlockedIncrement as symbolic
Defining function InterlockedDecrement as symbolic
Linked our definitions to these undefined functions:
  memcmp
  __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.268552064896
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 120 99 548 4130
INFO: Starting verification
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
RESULT: unknown
INFO: Total time elapsed: 0.914628982544
