bin/symbiotic --witness witness.graphml --no-slice --no-prepare --32 --prp=../sv-benchmarks/c/ReachSafety.prp ../sv-benchmarks/c/eca-rers2012/Problem05_label15_false-unreach-call.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.: 14 9 21437 65454
INFO: Compilation, preparation and instrumentation time: 1.71781206131
Linked our definitions to these undefined functions:
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 1.99945497513
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 20 12 5347 27598
INFO: Starting verification
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 1016 states (over memory cap)
KLEE: WARNING: killing 956 states (over memory cap)
KLEE: WARNING: killing 890 states (over memory cap)
KLEE: WARNING: killing 818 states (over memory cap)
KLEE: WARNING: killing 762 states (over memory cap)
KLEE: WARNING: killing 708 states (over memory cap)
KLEE: WARNING: killing 619 states (over memory cap)
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_ee340fa5-954d-4437-9eb9-3d41e67a034f/symbiotic/lib/verifier/__VERIFIER_error.c:9: ASSERTION FAIL: verifier assertion failed
KLEE: NOTE: now ignoring this error at this location
Error found.
RESULT: false(unreach-call)

 --- Error trace ---

Error: ASSERTION FAIL: verifier assertion failed
File: /tmp/vcloud-vcloud-master/worker/working_dir_ee340fa5-954d-4437-9eb9-3d41e67a034f/symbiotic/lib/verifier/__VERIFIER_error.c
Line: 9
assembly.ll line: 39
Stack: 
	#000000039 in __VERIFIER_error () at /tmp/vcloud-vcloud-master/worker/working_dir_ee340fa5-954d-4437-9eb9-3d41e67a034f/symbiotic/lib/verifier/__VERIFIER_error.c:9
	#100037878 in calculate_output8 () at /tmp/symbiotic-2X8ba2/Problem05_label15_false-unreach-call.c:10994
	#200035687 in calculate_output7 () at /tmp/symbiotic-2X8ba2/Problem05_label15_false-unreach-call.c:10421
	#300030512 in calculate_output6 () at /tmp/symbiotic-2X8ba2/Problem05_label15_false-unreach-call.c:8903
	#400025536 in calculate_output5 () at /tmp/symbiotic-2X8ba2/Problem05_label15_false-unreach-call.c:7450
	#500020357 in calculate_output4 () at /tmp/symbiotic-2X8ba2/Problem05_label15_false-unreach-call.c:6016
	#600015212 in calculate_output3 () at /tmp/symbiotic-2X8ba2/Problem05_label15_false-unreach-call.c:4462
	#700010140 in calculate_output2 () at /tmp/symbiotic-2X8ba2/Problem05_label15_false-unreach-call.c:3014
	#800005063 in calculate_output () at /tmp/symbiotic-2X8ba2/Problem05_label15_false-unreach-call.c:1524
	#900038338 in main () at /tmp/symbiotic-2X8ba2/Problem05_label15_false-unreach-call.c:11139

 --- ----------- ---
Generating witness: /tmp/vcloud-vcloud-master/worker/working_dir_ee340fa5-954d-4437-9eb9-3d41e67a034f/symbiotic/witness.graphml
 -- ---- --
Symbolic objects:
nondet := len 4 bytes, |4 times 0x0|
main:input:11135 := len 4 bytes, |0x5|3 times 0x0|
main:input:11135:1 := len 4 bytes, |0x5|3 times 0x0|
main:input:11135:2 := len 4 bytes, |0x4|3 times 0x0|
main:input:11135:3 := len 4 bytes, |0x6|3 times 0x0|
main:input:11135:4 := len 4 bytes, |0x5|3 times 0x0|
main:input:11135:5 := len 4 bytes, |0x2|3 times 0x0|
main:input:11135:6 := len 4 bytes, |0x2|3 times 0x0|
main:input:11135:7 := len 4 bytes, |0x4|3 times 0x0|
 -- ---- --
INFO: Total time elapsed: 464.786427975
