bin/symbiotic --witness witness.graphml --no-slice --no-prepare --32 --prp=../sv-benchmarks/c/ReachSafety.prp ../sv-benchmarks/c/reducercommutativity/rangesum60_false-unreach-call.i


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 0 3 23 141
INFO: Compilation, preparation and instrumentation time: 0.0479209423065
Linked our definitions to these undefined functions:
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_nondet_int
INFO: After-slicing optimizations and preparation time: 0.0713839530945
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 7 6 49 218
INFO: Starting verification
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_b31b88ac-96a7-4429-9982-3eebf225e515/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_b31b88ac-96a7-4429-9982-3eebf225e515/symbiotic/lib/verifier/__VERIFIER_error.c
Line: 9
assembly.ll line: 26
Stack: 
	#000000026 in __VERIFIER_error () at /tmp/vcloud-vcloud-master/worker/working_dir_b31b88ac-96a7-4429-9982-3eebf225e515/symbiotic/lib/verifier/__VERIFIER_error.c:9
	#100000320 in main () at /tmp/symbiotic-N6Of1N/rangesum60_false-unreach-call.i:50

 --- ----------- ---
Generating witness: /tmp/vcloud-vcloud-master/worker/working_dir_b31b88ac-96a7-4429-9982-3eebf225e515/symbiotic/witness.graphml
 -- ---- --
Symbolic objects:
nondet := len 4 bytes, |4 times 0x0|
nondet:1 := len 240 bytes, |240 times 0x0|
nondet-int := len 4 bytes, |4 times 0x0|
nondet-int:1 := len 4 bytes, |3 times 0x0|0xc|
nondet-int:2 := len 4 bytes, |4 times 0x0|
nondet-int:3 := len 4 bytes, |4 times 0x0|
nondet-int:4 := len 4 bytes, |4 times 0x0|
nondet-int:5 := len 4 bytes, |4 times 0x0|
nondet-int:6 := len 4 bytes, |4 times 0x0|
nondet-int:7 := len 4 bytes, |4 times 0x0|
nondet-int:8 := len 4 bytes, |4 times 0x0|
nondet-int:9 := len 4 bytes, |4 times 0x0|
nondet-int:10 := len 4 bytes, |4 times 0x0|
nondet-int:11 := len 4 bytes, |4 times 0x0|
nondet-int:12 := len 4 bytes, |4 times 0x0|
nondet-int:13 := len 4 bytes, |4 times 0x0|
nondet-int:14 := len 4 bytes, |4 times 0x0|
nondet-int:15 := len 4 bytes, |4 times 0x0|
nondet-int:16 := len 4 bytes, |4 times 0x0|
nondet-int:17 := len 4 bytes, |4 times 0x0|
nondet-int:18 := len 4 bytes, |4 times 0x0|
nondet-int:19 := len 4 bytes, |4 times 0x0|
nondet-int:20 := len 4 bytes, |4 times 0x0|
nondet-int:21 := len 4 bytes, |4 times 0x0|
nondet-int:22 := len 4 bytes, |4 times 0x0|
nondet-int:23 := len 4 bytes, |4 times 0x0|
nondet-int:24 := len 4 bytes, |4 times 0x0|
nondet-int:25 := len 4 bytes, |4 times 0x0|
nondet-int:26 := len 4 bytes, |4 times 0x0|
nondet-int:27 := len 4 bytes, |4 times 0x0|
nondet-int:28 := len 4 bytes, |4 times 0x0|
nondet-int:29 := len 4 bytes, |4 times 0x0|
nondet-int:30 := len 4 bytes, |4 times 0x0|
nondet-int:31 := len 4 bytes, |3 times 0x0|0x68|
nondet-int:32 := len 4 bytes, |3 times 0x0|0x44|
nondet-int:33 := len 4 bytes, |3 times 0x0|0xc|
nondet-int:34 := len 4 bytes, |3 times 0x0|0x18|
nondet-int:35 := len 4 bytes, |3 times 0x0|0x84|
nondet-int:36 := len 4 bytes, |2 times 0x0|0x80|0x83|
nondet-int:37 := len 4 bytes, |2 times 0x0|0x80|0x81|
nondet-int:38 := len 4 bytes, |2 times 0x0|0xc0|0xc1|
nondet-int:39 := len 4 bytes, |2 times 0x0|0x40|0xf7|
nondet-int:40 := len 4 bytes, |3 times 0x0|0xe8|
nondet-int:41 := len 4 bytes, |3 times 0x0|0x7c|
nondet-int:42 := len 4 bytes, |3 times 0x0|0xfc|
nondet-int:43 := len 4 bytes, |3 times 0x0|0x20|
nondet-int:44 := len 4 bytes, |3 times 0x0|0xdc|
nondet-int:45 := len 4 bytes, |3 times 0x0|0xe4|
nondet-int:46 := len 4 bytes, |3 times 0x0|0x50|
nondet-int:47 := len 4 bytes, |3 times 0x0|0x70|
nondet-int:48 := len 4 bytes, |3 times 0x0|0xc0|
nondet-int:49 := len 4 bytes, |3 times 0x0|0x80|
nondet-int:50 := len 4 bytes, |3 times 0x0|0x10|
nondet-int:51 := len 4 bytes, |3 times 0x0|0xf0|
nondet-int:52 := len 4 bytes, |3 times 0x0|0x60|
nondet-int:53 := len 4 bytes, |3 times 0x0|0xa0|
nondet-int:54 := len 4 bytes, |3 times 0x0|0x91|
nondet-int:55 := len 4 bytes, |3 times 0x0|0xfb|
nondet-int:56 := len 4 bytes, |3 times 0x0|0xf4|
nondet-int:57 := len 4 bytes, |3 times 0x0|0x60|
nondet-int:58 := len 4 bytes, |3 times 0x0|0xe0|
nondet-int:59 := len 4 bytes, |3 times 0x0|0x5f|
 -- ---- --
INFO: Total time elapsed: 0.861494064331
