./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/benchexec/results/155-concurrency-fix-locations/goblint.2024-03-01_08-09-03.files/SV-COMP24_unreach-call/chl-poker-hand-subst.wvr.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/benchexec/results/155-concurrency-fix-locations/goblint.2024-03-01_08-09-03.files/SV-COMP24_unreach-call/chl-poker-hand-subst.wvr.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] malloc wrapper: create_fresh_int_array
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: ((((((size == 4 || size == 5) || size == 13) && size != 0) && size <= 127) && size <= 13) && 4 <= size) && 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:349:1-358:1)
[Info][Witness] unassume invariant: ((((((size == 4 || size == 5) || size == 13) && size != 0) && size <= 127) && size <= 13) && 4 <= size) && 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:350:3-350:33)
[Info][Witness] unassume invariant: ((((((size == 4 || size == 5) || size == 13) && size != 0) && size <= 127) && size <= 13) && 4 <= size) && 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:351:3-351:69)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((size == 4 || size == 5) || size == 13) && size != 0) && (int )break_26 == 0) && (int )break_24 == 0) && (int )break_21 == 0) && (int )break_19 == 0) && (int )break_16 == 0) && (int )break_14 == 0) && i2_25 == 0) && i1_23 == 0) && result_22 == 0) && i2_20 == 0) && i1_18 == 0) && result_17 == 0) && i2_15 == 0) && i1_13 == 0) && result_12 == 0) && (unsigned long )last_index_of_11 == (unsigned long )((int *)0)) && i <= 13) && size <= 127) && size <= 13) && 4 <= size) && 0 <= i) && 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:12-354:17)
[Info][Witness] unassume invariant: i <= 12 && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:7-354:32)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((size == 4 || size == 5) || size == 13) && size != 0) && (int )break_26 == 0) && (int )break_24 == 0) && (int )break_21 == 0) && (int )break_19 == 0) && (int )break_16 == 0) && (int )break_14 == 0) && i2_25 == 0) && i1_23 == 0) && result_22 == 0) && i2_20 == 0) && i1_18 == 0) && result_17 == 0) && i2_15 == 0) && i1_13 == 0) && result_12 == 0) && (unsigned long )last_index_of_11 == (unsigned long )((int *)0)) && i <= 13) && size <= 127) && size <= 13) && 4 <= size) && 0 <= i) && 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:12-354:17)
[Info][Witness] unassume invariant: (int )break_14 == 0 || (int )break_14 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:328:3-328:38)
[Info][Witness] unassume invariant: (int )break_16 == 0 || (int )break_16 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:329:3-329:38)
[Info][Witness] unassume invariant: (int )break_19 == 0 || (int )break_19 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:330:3-330:38)
[Info][Witness] unassume invariant: (int )break_21 == 0 || (int )break_21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:331:3-331:38)
[Info][Witness] unassume invariant: (int )break_24 == 0 || (int )break_24 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:332:3-332:38)
[Info][Witness] unassume invariant: (int )break_26 == 0 || (int )break_26 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:333:3-333:38)
[Info][Witness] unassume invariant: i1_13 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:53:5-53:14)
[Info][Witness] unassume invariant: (int )break_14 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:54:5-54:17)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:55:5-55:28)
[Info][Witness] unassume invariant: (int )break_14 == 0 || (int )break_14 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:58:7-58:32)
[Info][Witness] unassume invariant: (int )break_14 == 0 || (int )break_14 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:61:7-61:161)
[Info][Witness] unassume invariant: (int )break_14 == 0 || (int )break_14 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:61:7-61:161)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:62:7-62:28)
[Info][Witness] unassume invariant: -2147483647 <= i1_13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:62:7-62:28)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:63:7-63:30)
[Info][Witness] unassume invariant: (int )break_14 == 0 || (int )break_14 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:66:5-66:30)
[Info][Witness] unassume invariant: (int )break_14 == 0 || (int )break_14 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:67:7-67:63)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:362:3-362:53)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:363:10-363:15)
[Info][Witness] unassume invariant: i2_15 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:83:7-83:16)
[Info][Witness] unassume invariant: (int )break_16 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:84:7-84:19)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:85:5-85:28)
[Info][Witness] unassume invariant: (int )break_16 == 0 || (int )break_16 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:87:7-87:32)
[Info][Witness] unassume invariant: (int )break_16 == 0 || (int )break_16 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:90:9-90:202)
[Info][Witness] unassume invariant: (int )break_16 == 0 || (int )break_16 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:90:9-90:202)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:91:7-91:30)
[Info][Witness] unassume invariant: (int )break_16 == 0 || (int )break_16 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:93:5-93:30)
[Info][Witness] unassume invariant: (int )break_16 == 0 || (int )break_16 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:94:7-94:63)
[Info][Witness] unassume invariant: result_12 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:112:7-112:20)
[Info][Witness] unassume invariant: result_12 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:120:7-120:28)
[Info][Witness] unassume invariant: result_12 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:128:7-128:20)
[Info][Witness] unassume invariant: i1_18 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:139:7-139:16)
[Info][Witness] unassume invariant: (int )break_19 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:140:7-140:19)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:141:5-141:28)
[Info][Witness] unassume invariant: (int )break_19 == 0 || (int )break_19 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:143:7-143:32)
[Info][Witness] unassume invariant: (int )break_19 == 0 || (int )break_19 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:146:9-146:163)
[Info][Witness] unassume invariant: (int )break_19 == 0 || (int )break_19 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:146:9-146:163)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:147:9-147:30)
[Info][Witness] unassume invariant: -2147483647 <= i1_18 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:147:9-147:30)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:148:5-148:28)
[Info][Witness] unassume invariant: (int )break_19 == 0 || (int )break_19 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:150:5-150:30)
[Info][Witness] unassume invariant: (int )break_19 == 0 || (int )break_19 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:151:7-151:63)
[Info][Witness] unassume invariant: i2_20 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:167:7-167:16)
[Info][Witness] unassume invariant: (int )break_21 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:168:7-168:19)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:169:5-169:28)
[Info][Witness] unassume invariant: (int )break_21 == 0 || (int )break_21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:171:7-171:32)
[Info][Witness] unassume invariant: (int )break_21 == 0 || (int )break_21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:174:9-174:202)
[Info][Witness] unassume invariant: (int )break_21 == 0 || (int )break_21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:174:9-174:202)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:175:5-175:28)
[Info][Witness] unassume invariant: (int )break_21 == 0 || (int )break_21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:177:5-177:30)
[Info][Witness] unassume invariant: (int )break_21 == 0 || (int )break_21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:178:7-178:63)
[Info][Witness] unassume invariant: result_17 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:196:7-196:20)
[Info][Witness] unassume invariant: result_17 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:204:7-204:28)
[Info][Witness] unassume invariant: result_17 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:212:7-212:20)
[Info][Witness] unassume invariant: i1_23 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:223:7-223:16)
[Info][Witness] unassume invariant: (int )break_24 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:224:7-224:19)
[Info][Witness] unassume invariant: (int )break_24 == 0 || (int )break_24 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:227:7-227:32)
[Info][Witness] unassume invariant: (int )break_24 == 0 || (int )break_24 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:230:9-230:163)
[Info][Witness] unassume invariant: (int )break_24 == 0 || (int )break_24 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:230:9-230:163)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:231:9-231:30)
[Info][Witness] unassume invariant: -2147483647 <= i1_23 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:231:9-231:30)
[Info][Witness] unassume invariant: (int )break_24 == 0 || (int )break_24 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:234:5-234:30)
[Info][Witness] unassume invariant: (int )break_24 == 0 || (int )break_24 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:235:7-235:63)
[Info][Witness] unassume invariant: i2_25 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:251:7-251:16)
[Info][Witness] unassume invariant: (int )break_26 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:252:7-252:19)
[Info][Witness] unassume invariant: (int )break_26 == 0 || (int )break_26 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:255:7-255:32)
[Info][Witness] unassume invariant: (int )break_26 == 0 || (int )break_26 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:258:9-258:202)
[Info][Witness] unassume invariant: (int )break_26 == 0 || (int )break_26 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:258:9-258:202)
[Info][Witness] unassume invariant: (int )break_26 == 0 || (int )break_26 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:261:5-261:30)
[Info][Witness] unassume invariant: (int )break_26 == 0 || (int )break_26 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:262:7-262:63)
[Info][Witness] unassume invariant: result_22 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:280:7-280:20)
[Info][Witness] unassume invariant: result_22 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:288:7-288:28)
[Info][Witness] unassume invariant: result_22 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:296:7-296:20)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
  on line 346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:346-346)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 266
  dead: 1
  total lines: 267
[Success][Witness] invariant confirmed: result_22 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:297:5)
[Success][Witness] invariant confirmed: break_16 == (_Bool)0 || break_16 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:330:3)
[Success][Witness] invariant confirmed: break_24 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:225:5)
[Success][Witness] invariant confirmed: break_26 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:253:5)
[Success][Witness] invariant confirmed: result_12 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:129:5)
[Success][Witness] invariant confirmed: break_16 == (_Bool)0 || break_16 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:95:7)
[Success][Witness] invariant confirmed: 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:350:3)
[Success][Witness] invariant confirmed: 4 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:350:3)
[Success][Witness] invariant confirmed: size <= 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:350:3)
[Success][Witness] invariant confirmed: size <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:350:3)
[Success][Witness] invariant confirmed: size != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:350:3)
[Success][Witness] invariant confirmed: (size == 4 || size == 5) || size == 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:350:3)
[Success][Witness] invariant confirmed: break_19 == (_Bool)0 || break_19 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:151:7)
[Success][Witness] invariant confirmed: break_19 == (_Bool)0 || break_19 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:331:3)
[Success][Witness] invariant confirmed: break_16 == (_Bool)0 || break_16 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:94:7)
[Success][Witness] invariant confirmed: break_16 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:85:5)
[Success][Witness] invariant confirmed: result_12 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:113:5)
[Success][Witness] invariant confirmed: break_24 == (_Bool)0 || break_24 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:333:3)
[Success][Witness] invariant confirmed: -2147483647 <= i1_23 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:232:5)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:355:5)
[Success][Witness] invariant confirmed: i <= 12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:355:5)
[Success][Witness] invariant confirmed: break_21 == (_Bool)0 || break_21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:178:7)
[Success][Witness] invariant confirmed: result_22 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:281:5)
[Success][Witness] invariant confirmed: break_14 == (_Bool)0 || break_14 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:62:7)
[Success][Witness] invariant confirmed: break_26 == (_Bool)0 || break_26 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:259:5)
[Success][Witness] invariant confirmed: break_14 == (_Bool)0 || break_14 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:329:3)
[Success][Witness] invariant confirmed: i1_23 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:224:7)
[Success][Witness] invariant confirmed: break_24 == (_Bool)0 || break_24 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:235:7)
[Success][Witness] invariant confirmed: break_21 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:169:5)
[Success][Witness] invariant confirmed: break_21 == (_Bool)0 || break_21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:179:7)
[Success][Witness] invariant confirmed: -2147483647 <= i1_13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:63:7)
[Success][Witness] invariant confirmed: break_24 == (_Bool)0 || break_24 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:236:7)
[Success][Witness] invariant confirmed: break_26 == (_Bool)0 || break_26 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:256:9)
[Success][Witness] invariant confirmed: result_22 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:289:5)
[Success][Witness] invariant confirmed: i2_25 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:252:7)
[Success][Witness] invariant confirmed: break_26 == (_Bool)0 || break_26 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:336:3)
[Success][Witness] invariant confirmed: i2_15 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:84:7)
[Success][Witness] invariant confirmed: result_17 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:205:5)
[Success][Witness] invariant confirmed: break_26 == (_Bool)0 || break_26 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:262:7)
[Success][Witness] invariant confirmed: i1_18 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:140:7)
[Success][Witness] invariant confirmed: break_24 == (_Bool)0 || break_24 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:231:9)
[Success][Witness] invariant confirmed: break_14 == (_Bool)0 || break_14 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:67:7)
[Success][Witness] invariant confirmed: break_19 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:141:5)
[Success][Witness] invariant confirmed: result_17 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:213:5)
[Success][Witness] invariant confirmed: break_16 == (_Bool)0 || break_16 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:91:7)
[Success][Witness] invariant confirmed: i1_13 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:54:5)
[Success][Witness] invariant confirmed: break_19 == (_Bool)0 || break_19 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:147:9)
[Success][Witness] invariant confirmed: break_21 == (_Bool)0 || break_21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:332:3)
[Success][Witness] invariant confirmed: result_12 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:121:5)
[Success][Witness] invariant confirmed: break_14 == (_Bool)0 || break_14 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:59:7)
[Success][Witness] invariant confirmed: 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:353:3)
[Success][Witness] invariant confirmed: 4 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:353:3)
[Success][Witness] invariant confirmed: size <= 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:353:3)
[Success][Witness] invariant confirmed: size <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:353:3)
[Success][Witness] invariant confirmed: size != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:353:3)
[Success][Witness] invariant confirmed: (size == 4 || size == 5) || size == 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:353:3)
[Success][Witness] invariant confirmed: break_19 == (_Bool)0 || break_19 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:144:9)
[Success][Witness] invariant confirmed: break_21 == (_Bool)0 || break_21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:175:5)
[Success][Witness] invariant confirmed: i2_20 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:168:7)
[Success][Witness] invariant confirmed: break_26 == (_Bool)0 || break_26 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:263:7)
[Success][Witness] invariant confirmed: 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:351:3)
[Success][Witness] invariant confirmed: 4 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:351:3)
[Success][Witness] invariant confirmed: size <= 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:351:3)
[Success][Witness] invariant confirmed: size <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:351:3)
[Success][Witness] invariant confirmed: size != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:351:3)
[Success][Witness] invariant confirmed: (size == 4 || size == 5) || size == 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:351:3)
[Success][Witness] invariant confirmed: break_14 == (_Bool)0 || break_14 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:68:7)
[Success][Witness] invariant confirmed: break_14 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:55:5)
[Success][Witness] invariant confirmed: break_19 == (_Bool)0 || break_19 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:152:7)
[Success][Witness] invariant confirmed: break_24 == (_Bool)0 || break_24 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:228:9)
[Success][Witness] invariant confirmed: break_16 == (_Bool)0 || break_16 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:88:9)
[Success][Witness] invariant confirmed: break_21 == (_Bool)0 || break_21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:172:9)
[Success][Witness] invariant confirmed: -2147483647 <= i1_18 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:148:5)
[Success][Witness] invariant confirmed: result_17 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:197:5)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:142:5)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:170:5)
[Success][Witness] invariant confirmed: 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: 4 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: size <= 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: size <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: i <= 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: last_index_of_11 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: result_12 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: i1_13 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: i2_15 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: result_17 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: i1_18 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: i2_20 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: result_22 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: i1_23 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: i2_25 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: break_14 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: break_16 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: break_19 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: break_21 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: break_24 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: break_26 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: size != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: (size == 4 || size == 5) || size == 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:354:3)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:86:5)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c:57:5)
[Info][Witness] witness validation summary:
  confirmed: 102
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 102
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 39
  vulnerable: 0
  unsafe: 0
  total memory locations: 39
