./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-trans.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-trans.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-trans.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-trans.wvr.c:346:1-355: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-trans.wvr.c:347:3-347: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-trans.wvr.c:348:3-348: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-trans.wvr.c:351:12-351:17)
[Info][Witness] unassume invariant: i <= 12 && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:7-351: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-trans.wvr.c:351:12-351:17)
[Info][Witness] unassume invariant: (int )break_14 == 0 || (int )break_14 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:325:3-325:38)
[Info][Witness] unassume invariant: (int )break_16 == 0 || (int )break_16 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:326:3-326:38)
[Info][Witness] unassume invariant: (int )break_19 == 0 || (int )break_19 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:327:3-327:38)
[Info][Witness] unassume invariant: (int )break_21 == 0 || (int )break_21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:328:3-328:38)
[Info][Witness] unassume invariant: (int )break_24 == 0 || (int )break_24 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:329:3-329:38)
[Info][Witness] unassume invariant: (int )break_26 == 0 || (int )break_26 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:330:3-330:38)
[Info][Witness] unassume invariant: i1_13 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:52:5-52:14)
[Info][Witness] unassume invariant: (int )break_14 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:53:5-53:17)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:54:5-54:28)
[Info][Witness] unassume invariant: (int )break_14 == 0 || (int )break_14 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:56:7-56:32)
[Info][Witness] unassume invariant: (int )break_14 == 0 || (int )break_14 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:59:7-59:161)
[Info][Witness] unassume invariant: (int )break_14 == 0 || (int )break_14 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:59:7-59:161)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:60:7-60:28)
[Info][Witness] unassume invariant: -2147483647 <= i1_13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:60:7-60:28)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:61:7-61:30)
[Info][Witness] unassume invariant: (int )break_14 == 0 || (int )break_14 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:63:5-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-trans.wvr.c:64:5-64:59)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:359:3-359:53)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:360:10-360:15)
[Info][Witness] unassume invariant: i2_15 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:80:5-80:14)
[Info][Witness] unassume invariant: (int )break_16 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:81:5-81:17)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:82:5-82:28)
[Info][Witness] unassume invariant: (int )break_16 == 0 || (int )break_16 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:84:7-84:32)
[Info][Witness] unassume invariant: (int )break_16 == 0 || (int )break_16 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:87:7-87:200)
[Info][Witness] unassume invariant: (int )break_16 == 0 || (int )break_16 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:87:7-87:200)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:88:7-88:30)
[Info][Witness] unassume invariant: (int )break_16 == 0 || (int )break_16 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:90:5-90:30)
[Info][Witness] unassume invariant: (int )break_16 == 0 || (int )break_16 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:91:5-91:59)
[Info][Witness] unassume invariant: result_12 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:109:5-109:18)
[Info][Witness] unassume invariant: result_12 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:117:5-117:26)
[Info][Witness] unassume invariant: result_12 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:125:5-125:18)
[Info][Witness] unassume invariant: i1_18 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:136:5-136:14)
[Info][Witness] unassume invariant: (int )break_19 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:137:5-137:17)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:138:5-138:28)
[Info][Witness] unassume invariant: (int )break_19 == 0 || (int )break_19 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:140:7-140:32)
[Info][Witness] unassume invariant: (int )break_19 == 0 || (int )break_19 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:143:7-143:161)
[Info][Witness] unassume invariant: (int )break_19 == 0 || (int )break_19 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:143:7-143:161)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:144:7-144:28)
[Info][Witness] unassume invariant: -2147483647 <= i1_18 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:144:7-144:28)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:145:7-145:30)
[Info][Witness] unassume invariant: (int )break_19 == 0 || (int )break_19 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:147:5-147:30)
[Info][Witness] unassume invariant: (int )break_19 == 0 || (int )break_19 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:148:5-148:59)
[Info][Witness] unassume invariant: i2_20 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:164:5-164:14)
[Info][Witness] unassume invariant: (int )break_21 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:165:5-165:17)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:166:5-166:28)
[Info][Witness] unassume invariant: (int )break_21 == 0 || (int )break_21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:168:7-168:32)
[Info][Witness] unassume invariant: (int )break_21 == 0 || (int )break_21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:171:7-171:200)
[Info][Witness] unassume invariant: (int )break_21 == 0 || (int )break_21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:171:7-171:200)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:172:7-172:30)
[Info][Witness] unassume invariant: (int )break_21 == 0 || (int )break_21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:174:5-174:30)
[Info][Witness] unassume invariant: (int )break_21 == 0 || (int )break_21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:175:5-175:59)
[Info][Witness] unassume invariant: result_17 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:193:5-193:18)
[Info][Witness] unassume invariant: result_17 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:201:5-201:26)
[Info][Witness] unassume invariant: result_17 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:209:5-209:18)
[Info][Witness] unassume invariant: i1_23 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:220:5-220:14)
[Info][Witness] unassume invariant: (int )break_24 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:221:5-221:17)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:222:5-222:28)
[Info][Witness] unassume invariant: (int )break_24 == 0 || (int )break_24 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:224:7-224:32)
[Info][Witness] unassume invariant: (int )break_24 == 0 || (int )break_24 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:227:7-227:161)
[Info][Witness] unassume invariant: (int )break_24 == 0 || (int )break_24 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:227:7-227:161)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:228:7-228:28)
[Info][Witness] unassume invariant: -2147483647 <= i1_23 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:228:7-228:28)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:229:7-229:30)
[Info][Witness] unassume invariant: (int )break_24 == 0 || (int )break_24 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:231:5-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-trans.wvr.c:232:5-232:59)
[Info][Witness] unassume invariant: i2_25 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:248:5-248:14)
[Info][Witness] unassume invariant: (int )break_26 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:249:5-249:17)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:250:5-250:28)
[Info][Witness] unassume invariant: (int )break_26 == 0 || (int )break_26 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:252:7-252:32)
[Info][Witness] unassume invariant: (int )break_26 == 0 || (int )break_26 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:255:7-255:200)
[Info][Witness] unassume invariant: (int )break_26 == 0 || (int )break_26 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:255:7-255:200)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:256:7-256:30)
[Info][Witness] unassume invariant: (int )break_26 == 0 || (int )break_26 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:258:5-258:30)
[Info][Witness] unassume invariant: (int )break_26 == 0 || (int )break_26 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:259:5-259:59)
[Info][Witness] unassume invariant: result_22 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:277:5-277:18)
[Info][Witness] unassume invariant: result_22 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:285:5-285:26)
[Info][Witness] unassume invariant: result_22 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:293:5-293:18)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
  on line 343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:343-343)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 266
  dead: 1
  total lines: 267
[Success][Witness] invariant confirmed: break_24 == (_Bool)0 || break_24 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:233:5)
[Success][Witness] invariant confirmed: break_26 == (_Bool)0 || break_26 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:260:5)
[Success][Witness] invariant confirmed: result_12 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:118:5)
[Success][Witness] invariant confirmed: 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:348:3)
[Success][Witness] invariant confirmed: 4 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:348:3)
[Success][Witness] invariant confirmed: size <= 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:348:3)
[Success][Witness] invariant confirmed: size <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:348:3)
[Success][Witness] invariant confirmed: size != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:348:3)
[Success][Witness] invariant confirmed: (size == 4 || size == 5) || size == 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:348:3)
[Success][Witness] invariant confirmed: break_16 == (_Bool)0 || break_16 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:88:7)
[Success][Witness] invariant confirmed: -2147483647 <= i1_23 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:229:7)
[Success][Witness] invariant confirmed: break_16 == (_Bool)0 || break_16 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:327:3)
[Success][Witness] invariant confirmed: result_22 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:278:5)
[Success][Witness] invariant confirmed: result_17 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:202:5)
[Success][Witness] invariant confirmed: break_21 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:166:5)
[Success][Witness] invariant confirmed: i2_25 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:249:5)
[Success][Witness] invariant confirmed: break_14 == (_Bool)0 || break_14 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:64:5)
[Success][Witness] invariant confirmed: i1_18 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:137:5)
[Success][Witness] invariant confirmed: i2_20 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:165:5)
[Success][Witness] invariant confirmed: result_12 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:126:5)
[Success][Witness] invariant confirmed: i2_15 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:81:5)
[Success][Witness] invariant confirmed: -2147483647 <= i1_13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:61:7)
[Success][Witness] invariant confirmed: break_19 == (_Bool)0 || break_19 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:149:5)
[Success][Witness] invariant confirmed: i1_13 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:53:5)
[Success][Witness] invariant confirmed: break_16 == (_Bool)0 || break_16 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:92:5)
[Success][Witness] invariant confirmed: break_16 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:82:5)
[Success][Witness] invariant confirmed: break_26 == (_Bool)0 || break_26 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:256:7)
[Success][Witness] invariant confirmed: break_14 == (_Bool)0 || break_14 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:60:7)
[Success][Witness] invariant confirmed: result_22 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:294:5)
[Success][Witness] invariant confirmed: break_26 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:250:5)
[Success][Witness] invariant confirmed: result_17 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:194:5)
[Success][Witness] invariant confirmed: break_19 == (_Bool)0 || break_19 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:144:7)
[Success][Witness] invariant confirmed: break_26 == (_Bool)0 || break_26 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:253:7)
[Success][Witness] invariant confirmed: break_24 == (_Bool)0 || break_24 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:225:7)
[Success][Witness] invariant confirmed: break_21 == (_Bool)0 || break_21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:329:3)
[Success][Witness] invariant confirmed: break_24 == (_Bool)0 || break_24 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:228:7)
[Success][Witness] invariant confirmed: 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:350:3)
[Success][Witness] invariant confirmed: 4 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:350:3)
[Success][Witness] invariant confirmed: size <= 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:350:3)
[Success][Witness] invariant confirmed: size <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:350:3)
[Success][Witness] invariant confirmed: size != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.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-trans.wvr.c:350:3)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:352:5)
[Success][Witness] invariant confirmed: i <= 12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:352:5)
[Success][Witness] invariant confirmed: break_24 == (_Bool)0 || break_24 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:330:3)
[Success][Witness] invariant confirmed: break_26 == (_Bool)0 || break_26 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:333:3)
[Success][Witness] invariant confirmed: break_19 == (_Bool)0 || break_19 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:328:3)
[Success][Witness] invariant confirmed: break_21 == (_Bool)0 || break_21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:175:5)
[Success][Witness] invariant confirmed: result_17 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:210:5)
[Success][Witness] invariant confirmed: break_14 == (_Bool)0 || break_14 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:326:3)
[Success][Witness] invariant confirmed: result_22 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:286:5)
[Success][Witness] invariant confirmed: break_16 == (_Bool)0 || break_16 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:85:7)
[Success][Witness] invariant confirmed: result_12 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:110:5)
[Success][Witness] invariant confirmed: break_24 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:222:5)
[Success][Witness] invariant confirmed: break_21 == (_Bool)0 || break_21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:172:7)
[Success][Witness] invariant confirmed: break_19 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:138:5)
[Success][Witness] invariant confirmed: i1_23 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:221:5)
[Success][Witness] invariant confirmed: break_21 == (_Bool)0 || break_21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:176:5)
[Success][Witness] invariant confirmed: break_21 == (_Bool)0 || break_21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:169:7)
[Success][Witness] invariant confirmed: -2147483647 <= i1_18 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:145:7)
[Success][Witness] invariant confirmed: break_14 == (_Bool)0 || break_14 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:65:5)
[Success][Witness] invariant confirmed: break_14 == (_Bool)0 || break_14 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:57:7)
[Success][Witness] invariant confirmed: break_19 == (_Bool)0 || break_19 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:148:5)
[Success][Witness] invariant confirmed: break_19 == (_Bool)0 || break_19 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:141:7)
[Success][Witness] invariant confirmed: break_24 == (_Bool)0 || break_24 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:232:5)
[Success][Witness] invariant confirmed: 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:347:3)
[Success][Witness] invariant confirmed: 4 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:347:3)
[Success][Witness] invariant confirmed: size <= 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:347:3)
[Success][Witness] invariant confirmed: size <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:347:3)
[Success][Witness] invariant confirmed: size != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:347:3)
[Success][Witness] invariant confirmed: (size == 4 || size == 5) || size == 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:347:3)
[Success][Witness] invariant confirmed: break_14 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:54:5)
[Success][Witness] invariant confirmed: break_16 == (_Bool)0 || break_16 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:91:5)
[Success][Witness] invariant confirmed: break_26 == (_Bool)0 || break_26 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:259:5)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:223:5)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:167:5)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:83:5)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:55:5)
[Success][Witness] invariant confirmed: 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: 4 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: size <= 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: size <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: i <= 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: last_index_of_11 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: result_12 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: i1_13 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: i2_15 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: result_17 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: i1_18 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: i2_20 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: result_22 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: i1_23 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: i2_25 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: break_14 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: break_16 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: break_19 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: break_21 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: break_24 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: break_26 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: size != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.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-trans.wvr.c:351:3)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:251:5)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-trans.wvr.c:139:5)
[Info][Witness] witness validation summary:
  confirmed: 104
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 104
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 39
  vulnerable: 0
  unsafe: 0
  total memory locations: 39
