./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/parallel-barrier.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/parallel-barrier.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/parallel-barrier.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] Enabled octagon domain for:
[Info] __VERIFIER_atomic_begin, __VERIFIER_atomic_end, i, key, count, a, tmp, count, i, j, i___0, j___0, k, size, r, top, t1, t4, tmp, tmp___0, t5, t6, tmp, tmp, tmp, t2, t3, tmp, tmp, tmp
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: (int )f1_2 == 0 || (int )f1_2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:178:3-178:34)
[Info][Witness] unassume invariant: (int )f2_3 == 0 || (int )f2_3 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:179:3-179:34)
[Info][Witness] unassume invariant: (int )f1_8 == 0 || (int )f1_8 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:184:3-184:34)
[Info][Witness] unassume invariant: (int )f2_9 == 0 || (int )f2_9 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:185:3-185:34)
[Info][Witness] unassume invariant: y_7 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:187:3-187:36)
[Info][Witness] unassume invariant: ((int )f2_3 == 0 || (int )f2_3 == 1) && ((int )f1_2 == 0 || (int )f1_2 == 1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:96:1-107:1)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:51:3-51:19)
[Info][Witness] unassume invariant: -2147483647 <= x_0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:51:3-51:19)
[Info][Witness] unassume invariant: (int )f1_2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:55:3-55:11)
[Info][Witness] unassume invariant: ((int )f2_3 == 0 || (int )f2_3 == 1) && ((int )f1_2 == 0 || (int )f1_2 == 1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:57:3-57:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:65:3-65:19)
[Info][Witness] unassume invariant: -2147483647 <= y_1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:65:3-65:19)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:76:3-76:19)
[Info][Witness] unassume invariant: -2147483647 <= y_1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:76:3-76:19)
[Info][Witness] unassume invariant: (int )f2_3 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:80:3-80:11)
[Info][Witness] unassume invariant: ((int )f2_3 == 0 || (int )f2_3 == 1) && ((int )f1_2 == 0 || (int )f1_2 == 1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:82:3-82:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:90:3-90:19)
[Info][Witness] unassume invariant: -2147483647 <= x_0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:90:3-90:19)
[Info][Witness] unassume invariant: (((int )f2_9 == 0 || (int )f2_9 == 1) && ((int )f1_8 == 0 || (int )f1_8 == 1)) && -2147483647 <= y_7 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:159:1-170:1)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:114:3-114:20)
[Info][Witness] unassume invariant: -2147483647 <= x_6 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:114:3-114:20)
[Info][Witness] unassume invariant: (int )f1_8 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:118:3-118:11)
[Info][Witness] unassume invariant: ((int )f2_9 == 0 || (int )f2_9 == 1) && ((int )f1_8 == 0 || (int )f1_8 == 1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:120:3-120:28)
[Info][Witness] unassume invariant: -2147483647 <= y_7 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:124:3-124:28)
[Info][Witness] unassume invariant: -2147483647 <= temp_10 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:125:3-125:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:128:3-128:20)
[Info][Witness] unassume invariant: -2147483647 <= y_7 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:128:3-128:20)
[Info][Witness] unassume invariant: -2147483647 <= y_7 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:135:3-135:28)
[Info][Witness] unassume invariant: -2147483647 <= temp_11 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:136:3-136:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:139:3-139:20)
[Info][Witness] unassume invariant: -2147483647 <= y_7 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:139:3-139:20)
[Info][Witness] unassume invariant: (int )f2_9 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:143:3-143:11)
[Info][Witness] unassume invariant: ((int )f2_9 == 0 || (int )f2_9 == 1) && ((int )f1_8 == 0 || (int )f1_8 == 1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:145:3-145:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:153:3-153:20)
[Info][Witness] unassume invariant: -2147483647 <= x_6 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:153:3-153:20)
[Info][Witness] unassume invariant: -2147483647 <= y_7 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:195:3-195:22)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
  on line 200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:200-200)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 120
  dead: 1
  total lines: 121
[Success][Witness] invariant confirmed: f1_8 == (_Bool)0 || f1_8 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:185:3)
[Success][Witness] invariant confirmed: -2147483647 <= x_0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:52:3)
[Success][Witness] invariant confirmed: -2147483647 <= y_7 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:197:3)
[Success][Witness] invariant confirmed: -2147483647 <= y_7 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:140:3)
[Success][Witness] invariant confirmed: f1_8 == (_Bool)0 || f1_8 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:121:3)
[Success][Witness] invariant confirmed: f2_9 == (_Bool)0 || f2_9 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:121:3)
[Success][Witness] invariant confirmed: -2147483647 <= y_7 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:125:3)
[Success][Witness] invariant confirmed: -2147483647 <= y_7 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:136:3)
[Success][Witness] invariant confirmed: -2147483647 <= x_6 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:115:3)
[Success][Witness] invariant confirmed: -2147483647 <= y_1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:66:3)
[Success][Witness] invariant confirmed: f1_2 == (_Bool)0 || f1_2 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:179:3)
[Success][Witness] invariant confirmed: -2147483647 <= x_6 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:154:3)
[Success][Witness] invariant confirmed: f1_8 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:119:3)
[Success][Witness] invariant confirmed: f1_2 == (_Bool)0 || f1_2 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:58:3)
[Success][Witness] invariant confirmed: f2_3 == (_Bool)0 || f2_3 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:58:3)
[Success][Witness] invariant confirmed: f2_9 == (_Bool)0 || f2_9 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:186:3)
[Success][Witness] invariant confirmed: -2147483647 <= y_7 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:162:3)
[Success][Witness] invariant confirmed: f1_8 == (_Bool)0 || f1_8 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:162:3)
[Success][Witness] invariant confirmed: f2_9 == (_Bool)0 || f2_9 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:162:3)
[Success][Witness] invariant confirmed: f2_3 == (_Bool)0 || f2_3 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:180:3)
[Success][Witness] invariant confirmed: f1_2 == (_Bool)0 || f1_2 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:83:3)
[Success][Witness] invariant confirmed: f2_3 == (_Bool)0 || f2_3 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:83:3)
[Success][Witness] invariant confirmed: -2147483647 <= temp_11 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:137:3)
[Success][Witness] invariant confirmed: f2_3 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:81:3)
[Success][Witness] invariant confirmed: -2147483647 <= y_1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:77:3)
[Success][Witness] invariant confirmed: y_7 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:190:3)
[Success][Witness] invariant confirmed: f1_2 == (_Bool)0 || f1_2 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:99:3)
[Success][Witness] invariant confirmed: f2_3 == (_Bool)0 || f2_3 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:99:3)
[Success][Witness] invariant confirmed: -2147483647 <= temp_10 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:126:3)
[Success][Witness] invariant confirmed: -2147483647 <= x_0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:91:3)
[Success][Witness] invariant confirmed: -2147483647 <= y_7 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:129:3)
[Success][Witness] invariant confirmed: f1_8 == (_Bool)0 || f1_8 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:146:3)
[Success][Witness] invariant confirmed: f2_9 == (_Bool)0 || f2_9 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:146:3)
[Success][Witness] invariant confirmed: f1_2 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:56:3)
[Success][Witness] invariant confirmed: f2_9 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-barrier.wvr.c:144:3)
[Info][Witness] witness validation summary:
  confirmed: 35
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 35
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 12
  vulnerable: 0
  unsafe: 0
  total memory locations: 12
