bin/symbiotic --witness witness.graphml --no-slice --no-prepare --32 --prp=../sv-benchmarks/c/ReachSafety.prp ../sv-benchmarks/c/eca-rers2012/Problem08_label05_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.: 23 83 302860 972467
INFO: Compilation, preparation and instrumentation time: 31.8782801628
Linked our definitions to these undefined functions:
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 40.1453278065
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 29 86 72128 473605
INFO: Starting verification
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 82 states (over memory cap)
KLEE: WARNING: killing 77 states (over memory cap)
KLEE: WARNING: killing 75 states (over memory cap)
KLEE: WARNING: killing 69 states (over memory cap)
KLEE: WARNING: killing 64 states (over memory cap)
KLEE: WARNING: killing 62 states (over memory cap)
KLEE: WARNING: killing 59 states (over memory cap)
KLEE: WARNING: killing 54 states (over memory cap)
KLEE: WARNING: killing 51 states (over memory cap)
KLEE: WARNING: killing 49 states (over memory cap)
KLEE: WARNING: killing 44 states (over memory cap)
KLEE: WARNING: killing 42 states (over memory cap)
KLEE: WARNING: killing 39 states (over memory cap)
KLEE: WARNING: killing 35 states (over memory cap)
KLEE: WARNING: killing 33 states (over memory cap)
KLEE: WARNING: killing 30 states (over memory cap)
KLEE: WARNING: killing 39 states (over memory cap)
KLEE: WARNING: killing 35 states (over memory cap)
KLEE: WARNING: killing 32 states (over memory cap)
KLEE: WARNING: killing 30 states (over memory cap)
KLEE: WARNING: killing 49 states (over memory cap)
KLEE: WARNING: killing 46 states (over memory cap)
KLEE: WARNING: killing 43 states (over memory cap)
KLEE: WARNING: killing 40 states (over memory cap)
KLEE: WARNING: killing 37 states (over memory cap)
KLEE: WARNING: killing 41 states (over memory cap)
KLEE: WARNING: killing 35 states (over memory cap)
KLEE: WARNING: killing 33 states (over memory cap)
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_617afb87-f563-4d80-8ff1-5c5ff0007233/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_617afb87-f563-4d80-8ff1-5c5ff0007233/symbiotic/lib/verifier/__VERIFIER_error.c
Line: 9
assembly.ll line: 48
Stack: 
	#000000048 in __VERIFIER_error () at /tmp/vcloud-vcloud-master/worker/working_dir_617afb87-f563-4d80-8ff1-5c5ff0007233/symbiotic/lib/verifier/__VERIFIER_error.c:9
	#100617556 in calculate_output82 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:171423
	#200615944 in calculate_output81 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:171013
	#300608100 in calculate_output80 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:168870
	#400600414 in calculate_output79 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:166788
	#500592869 in calculate_output78 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:164660
	#600585228 in calculate_output77 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:162597
	#700577444 in calculate_output76 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:160379
	#800569675 in calculate_output75 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:158185
	#900561993 in calculate_output74 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:156134
	#1000554375 in calculate_output73 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:153932
	#1100546584 in calculate_output72 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:151811
	#1200539052 in calculate_output71 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:149689
	#1300531524 in calculate_output70 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:147539
	#1400524001 in calculate_output69 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:145398
	#1500516420 in calculate_output68 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:143245
	#1600508862 in calculate_output67 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:141142
	#1700501213 in calculate_output66 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:139071
	#1800493647 in calculate_output65 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:136946
	#1900486021 in calculate_output64 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:134798
	#2000478632 in calculate_output63 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:132720
	#2100470919 in calculate_output62 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:130676
	#2200463217 in calculate_output61 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:128564
	#2300455812 in calculate_output60 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:126499
	#2400448528 in calculate_output59 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:124400
	#2500440868 in calculate_output58 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:122268
	#2600433396 in calculate_output57 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:120193
	#2700425883 in calculate_output56 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:118156
	#2800418123 in calculate_output55 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:116092
	#2900410140 in calculate_output54 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:113939
	#3000402339 in calculate_output53 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:111759
	#3100394781 in calculate_output52 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:109796
	#3200387315 in calculate_output51 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:107739
	#3300379654 in calculate_output50 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:105588
	#3400372078 in calculate_output49 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:103502
	#3500364530 in calculate_output48 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:101436
	#3600356677 in calculate_output47 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:99297
	#3700349109 in calculate_output46 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:97130
	#3800341721 in calculate_output45 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:95165
	#3900334239 in calculate_output44 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:93118
	#4000326844 in calculate_output43 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:91008
	#4100319339 in calculate_output42 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:88955
	#4200311607 in calculate_output41 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:86759
	#4300303917 in calculate_output40 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:84608
	#4400296201 in calculate_output39 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:82409
	#4500288276 in calculate_output38 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:80146
	#4600280627 in calculate_output37 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:77993
	#4700273120 in calculate_output36 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:75919
	#4800265514 in calculate_output35 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:73780
	#4900257897 in calculate_output34 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:71662
	#5000250267 in calculate_output33 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:69586
	#5100242563 in calculate_output32 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:67483
	#5200234792 in calculate_output31 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:65465
	#5300227114 in calculate_output30 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:63416
	#5400219544 in calculate_output29 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:61295
	#5500211701 in calculate_output28 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:59206
	#5600204037 in calculate_output27 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:57051
	#5700196520 in calculate_output26 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:54837
	#5800188949 in calculate_output25 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:52743
	#5900181596 in calculate_output24 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:50698
	#6000174221 in calculate_output23 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:48617
	#6100166786 in calculate_output22 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:46489
	#6200159273 in calculate_output21 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:44407
	#6300151523 in calculate_output20 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:42202
	#6400144166 in calculate_output19 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:40110
	#6500136496 in calculate_output18 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:37977
	#6600128856 in calculate_output17 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:35839
	#6700121185 in calculate_output16 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:33791
	#6800113487 in calculate_output15 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:31708
	#6900105972 in calculate_output14 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:29552
	#7000098053 in calculate_output13 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:27377
	#7100090436 in calculate_output12 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:25314
	#7200082981 in calculate_output11 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:23255
	#7300075558 in calculate_output10 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:21277
	#7400068157 in calculate_output9 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:19174
	#7500060659 in calculate_output8 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:17053
	#7600053178 in calculate_output7 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:14999
	#7700045618 in calculate_output6 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:12890
	#7800038010 in calculate_output5 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:10779
	#7900030578 in calculate_output4 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:8689
	#8000022939 in calculate_output3 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:6664
	#8100015273 in calculate_output2 () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:4460
	#8200007638 in calculate_output () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:2340
	#8300617990 in main () at /tmp/symbiotic-_3EsQ6/Problem08_label05_false-unreach-call.c:171577

 --- ----------- ---
Generating witness: /tmp/vcloud-vcloud-master/worker/working_dir_617afb87-f563-4d80-8ff1-5c5ff0007233/symbiotic/witness.graphml
 -- ---- --
Symbolic objects:
nondet := len 4 bytes, |4 times 0x0|
main:input:171573 := len 4 bytes, |0x1|3 times 0x0|
main:input:171573:1 := len 4 bytes, |0x1|3 times 0x0|
main:input:171573:2 := len 4 bytes, |0x2|3 times 0x0|
main:input:171573:3 := len 4 bytes, |0x2|3 times 0x0|
main:input:171573:4 := len 4 bytes, |0x4|3 times 0x0|
main:input:171573:5 := len 4 bytes, |0x6|3 times 0x0|
main:input:171573:6 := len 4 bytes, |0x1|3 times 0x0|
main:input:171573:7 := len 4 bytes, |0x3|3 times 0x0|
 -- ---- --
INFO: Total time elapsed: 787.302356005
