./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/benchexec/results/156-concurrency-fix-locations-all-locals/goblint.2024-03-01_08-44-30.files/SV-COMP24_unreach-call/chl-poker-hand-symm.wvr.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/benchexec/results/156-concurrency-fix-locations-all-locals/goblint.2024-03-01_08-44-30.files/SV-COMP24_unreach-call/chl-poker-hand-symm.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-symm.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] Enabled congruence domain.
[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-symm.wvr.c:240:1-249: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-symm.wvr.c:241:3-241: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-symm.wvr.c:242:3-242:69)
[Info][Witness] unassume invariant: (((((((((((((((((size == 4 || size == 5) || size == 13) && size != 0) && (int )break_17 == 0) && (int )break_15 == 0) && (int )break_12 == 0) && (int )break_10 == 0) && i2_16 == 0) && i1_14 == 0) && result_13 == 0) && i2_11 == 0) && i1_9 == 0) && result_8 == 0) && (unsigned long )char_at_5 == (unsigned long )((int *)0)) && size <= 127) && size <= 13) && 4 <= size) && 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:12-245:17)
[Info][Witness] unassume invariant: (((((((((((((((((size == 4 || size == 5) || size == 13) && size != 0) && (int )break_17 == 0) && (int )break_15 == 0) && (int )break_12 == 0) && (int )break_10 == 0) && i2_16 == 0) && i1_14 == 0) && result_13 == 0) && i2_11 == 0) && i1_9 == 0) && result_8 == 0) && (unsigned long )char_at_5 == (unsigned long )((int *)0)) && size <= 127) && size <= 13) && 4 <= size) && 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:12-245:17)
[Info][Witness] unassume invariant: i1_9 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:52:5-52:13)
[Info][Witness] unassume invariant: (int )break_10 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.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-symm.wvr.c:54:5-54:28)
[Info][Witness] unassume invariant: ((int )break_10 == 0 || (int )break_10 == 1) && 0 <= i1_9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:56:7-56:32)
[Info][Witness] unassume invariant: 0 <= i1_9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:57:7-57:58)
[Info][Witness] unassume invariant: 0 <= i1_9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:58:7-58:299)
[Info][Witness] unassume invariant: 0 <= i1_9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:58:7-58:299)
[Info][Witness] unassume invariant: ((int )break_10 == 0 || (int )break_10 == 1) && 0 <= i1_9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:59:7-59:157)
[Info][Witness] unassume invariant: ((int )break_10 == 0 || (int )break_10 == 1) && 0 <= i1_9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:59:7-59:157)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:60:7-60:26)
[Info][Witness] unassume invariant: 1 <= i1_9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:60:7-60:26)
[Info][Witness] unassume invariant: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:61:7-61:30)
[Info][Witness] unassume invariant: ((int )break_10 == 0 || (int )break_10 == 1) && 0 <= i1_9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:63:5-63:30)
[Info][Witness] unassume invariant: (int )break_10 == 0 || (int )break_10 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:64:5-64:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:253:3-253:53)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:254:10-254:15)
[Info][Witness] unassume invariant: i2_11 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:80:5-80:14)
[Info][Witness] unassume invariant: (int )break_12 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.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-symm.wvr.c:82:5-82:28)
[Info][Witness] unassume invariant: ((int )break_12 == 0 || (int )break_12 == 1) && i2_11 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:84:7-84:32)
[Info][Witness] unassume invariant: i2_11 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:85:7-85:59)
[Info][Witness] unassume invariant: i2_11 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:86:7-86:424)
[Info][Witness] unassume invariant: i2_11 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:86:7-86:424)
[Info][Witness] unassume invariant: (int )break_12 == 0 || (int )break_12 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:87:7-87:200)
[Info][Witness] unassume invariant: (int )break_12 == 0 || (int )break_12 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.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-symm.wvr.c:88:7-88:30)
[Info][Witness] unassume invariant: ((int )break_12 == 0 || (int )break_12 == 1) && i2_11 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:90:5-90:30)
[Info][Witness] unassume invariant: (int )break_12 == 0 || (int )break_12 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:91:5-91:59)
[Info][Witness] unassume invariant: result_8 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:109:5-109:17)
[Info][Witness] unassume invariant: result_8 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:117:5-117:25)
[Info][Witness] unassume invariant: result_8 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:125:5-125:17)
[Info][Witness] unassume invariant: i1_14 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:136:5-136:14)
[Info][Witness] unassume invariant: (int )break_15 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.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-symm.wvr.c:138:5-138:28)
[Info][Witness] unassume invariant: ((int )break_15 == 0 || (int )break_15 == 1) && 0 <= i1_14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:140:7-140:32)
[Info][Witness] unassume invariant: 0 <= i1_14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:141:7-141:59)
[Info][Witness] unassume invariant: 0 <= i1_14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:142:7-142:309)
[Info][Witness] unassume invariant: 0 <= i1_14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:142:7-142:309)
[Info][Witness] unassume invariant: ((int )break_15 == 0 || (int )break_15 == 1) && 0 <= i1_14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:143:7-143:161)
[Info][Witness] unassume invariant: ((int )break_15 == 0 || (int )break_15 == 1) && 0 <= i1_14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.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-symm.wvr.c:144:7-144:28)
[Info][Witness] unassume invariant: 1 <= i1_14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.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-symm.wvr.c:145:7-145:30)
[Info][Witness] unassume invariant: ((int )break_15 == 0 || (int )break_15 == 1) && 0 <= i1_14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:147:5-147:30)
[Info][Witness] unassume invariant: (int )break_15 == 0 || (int )break_15 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:148:5-148:59)
[Info][Witness] unassume invariant: i2_16 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:164:5-164:14)
[Info][Witness] unassume invariant: (int )break_17 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.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-symm.wvr.c:166:5-166:28)
[Info][Witness] unassume invariant: ((int )break_17 == 0 || (int )break_17 == 1) && i2_16 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:168:7-168:32)
[Info][Witness] unassume invariant: i2_16 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:169:7-169:59)
[Info][Witness] unassume invariant: i2_16 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:170:7-170:426)
[Info][Witness] unassume invariant: i2_16 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:170:7-170:426)
[Info][Witness] unassume invariant: (int )break_17 == 0 || (int )break_17 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:171:7-171:200)
[Info][Witness] unassume invariant: (int )break_17 == 0 || (int )break_17 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.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-symm.wvr.c:172:7-172:30)
[Info][Witness] unassume invariant: ((int )break_17 == 0 || (int )break_17 == 1) && i2_16 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:174:5-174:30)
[Info][Witness] unassume invariant: (int )break_17 == 0 || (int )break_17 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:175:5-175:59)
[Info][Witness] unassume invariant: result_13 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:193:5-193:18)
[Info][Witness] unassume invariant: result_13 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:201:5-201:26)
[Info][Witness] unassume invariant: result_13 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:209:5-209:18)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
  on line 237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:237-237)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 174
  dead: 1
  total lines: 175
[Warning][Deadcode][CWE-571] condition 'i2_11 <= 12' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:91:5-91:59)
[Warning][Deadcode][CWE-571] condition 'i2_16 <= 12' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:169:7-169:59)
[Warning][Deadcode][CWE-571] condition 'i2_16 <= 12' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:175:5-175:59)
[Warning][Deadcode][CWE-571] condition 'i2_11 <= 12' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:85:7-85:59)
[Success][Witness] invariant confirmed: 1 <= i1_14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:145:7)
[Success][Witness] invariant confirmed: 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:242:3)
[Success][Witness] invariant confirmed: 4 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:242:3)
[Success][Witness] invariant confirmed: size <= 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:242:3)
[Success][Witness] invariant confirmed: size <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:242:3)
[Success][Witness] invariant confirmed: size != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:242:3)
[Success][Witness] invariant confirmed: (size == 4 || size == 5) || size == 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:242:3)
[Success][Witness] invariant confirmed: break_15 == (_Bool)0 || break_15 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:149:5)
[Success][Witness] invariant confirmed: result_8 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:118:5)
[Success][Witness] invariant confirmed: 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:241:3)
[Success][Witness] invariant confirmed: 4 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:241:3)
[Success][Witness] invariant confirmed: size <= 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:241:3)
[Success][Witness] invariant confirmed: size <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:241:3)
[Success][Witness] invariant confirmed: size != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:241:3)
[Success][Witness] invariant confirmed: (size == 4 || size == 5) || size == 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:241:3)
[Success][Witness] invariant confirmed: 0 <= i1_9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:57:7)
[Success][Witness] invariant confirmed: break_10 == (_Bool)0 || break_10 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:57:7)
[Success][Witness] invariant confirmed: break_17 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:166:5)
[Success][Witness] invariant confirmed: 0 <= i1_14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:144:7)
[Success][Witness] invariant confirmed: break_15 == (_Bool)0 || break_15 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:144:7)
[Success][Witness] invariant confirmed: 0 <= i1_14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:143:7)
[Success][Witness] invariant confirmed: 0 <= i1_9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:58:7)
[Success][Witness] invariant confirmed: break_17 == (_Bool)0 || break_17 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:172:7)
[Success][Witness] invariant confirmed: break_15 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:138:5)
[Success][Witness] invariant confirmed: break_17 == (_Bool)0 || break_17 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:176:5)
[Success][Witness] invariant confirmed: 0 <= i1_14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:148:5)
[Success][Witness] invariant confirmed: break_15 == (_Bool)0 || break_15 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:148:5)
[Success][Witness] invariant confirmed: 0 <= i1_14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:141:7)
[Success][Witness] invariant confirmed: break_15 == (_Bool)0 || break_15 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:141:7)
[Success][Witness] invariant confirmed: i2_16 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:170:7)
[Success][Witness] invariant confirmed: result_8 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:110:5)
[Success][Witness] invariant confirmed: i2_11 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:81:5)
[Success][Witness] invariant confirmed: 1 <= i1_9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:61:7)
[Success][Witness] invariant confirmed: break_12 == (_Bool)0 || break_12 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:88:7)
[Success][Witness] invariant confirmed: result_13 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:210:5)
[Success][Witness] invariant confirmed: i2_16 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:171:7)
[Success][Witness] invariant confirmed: 0 <= i1_9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:60:7)
[Success][Witness] invariant confirmed: break_10 == (_Bool)0 || break_10 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:60:7)
[Success][Witness] invariant confirmed: i2_16 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:165:5)
[Success][Witness] invariant confirmed: 0 <= i1_14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:142:7)
[Success][Witness] invariant confirmed: i1_14 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:137:5)
[Success][Witness] invariant confirmed: i2_11 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:91:5)
[Success][Witness] invariant confirmed: break_12 == (_Bool)0 || break_12 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:91:5)
[Success][Witness] invariant confirmed: break_10 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:54:5)
[Success][Witness] invariant confirmed: break_10 == (_Bool)0 || break_10 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:65:5)
[Success][Witness] invariant confirmed: i2_16 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:169:7)
[Success][Witness] invariant confirmed: break_17 == (_Bool)0 || break_17 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:169:7)
[Success][Witness] invariant confirmed: i1_9 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:53:5)
[Success][Witness] invariant confirmed: i2_11 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:87:7)
[Success][Witness] invariant confirmed: i2_16 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:175:5)
[Success][Witness] invariant confirmed: break_17 == (_Bool)0 || break_17 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:175:5)
[Success][Witness] invariant confirmed: result_13 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:194:5)
[Success][Witness] invariant confirmed: 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:244:3)
[Success][Witness] invariant confirmed: 4 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:244:3)
[Success][Witness] invariant confirmed: size <= 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:244:3)
[Success][Witness] invariant confirmed: size <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:244:3)
[Success][Witness] invariant confirmed: size != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:244:3)
[Success][Witness] invariant confirmed: (size == 4 || size == 5) || size == 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:244:3)
[Success][Witness] invariant confirmed: break_12 == (_Bool)0 || break_12 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:92:5)
[Success][Witness] invariant confirmed: 0 <= i1_9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:59:7)
[Success][Witness] invariant confirmed: i2_11 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:86:7)
[Success][Witness] invariant confirmed: 0 <= i1_9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:64:5)
[Success][Witness] invariant confirmed: break_10 == (_Bool)0 || break_10 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:64:5)
[Success][Witness] invariant confirmed: break_12 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:82:5)
[Success][Witness] invariant confirmed: i2_11 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:85:7)
[Success][Witness] invariant confirmed: break_12 == (_Bool)0 || break_12 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:85:7)
[Success][Witness] invariant confirmed: result_13 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:202:5)
[Success][Witness] invariant confirmed: result_8 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:126:5)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:139:5)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:55:5)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:83:5)
[Success][Witness] invariant confirmed: 0 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: 4 <= size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: size <= 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: size <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: char_at_5 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: result_8 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: i1_9 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: i2_11 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: result_13 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: i1_14 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: i2_16 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: break_10 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: break_12 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: break_15 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: break_17 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: size != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: (size == 4 || size == 5) || size == 13 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:245:3)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c:167:5)
[Info][Witness] witness validation summary:
  confirmed: 89
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 89
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 19
  vulnerable: 0
  unsafe: 0
  total memory locations: 19
