./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/test-easy10.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/test-easy10.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/test-easy10.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 widening thresholds
[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, t2, t3, t4, tmp, tmp___0, tmp, tmp, tmp, tmp
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:43:3-43:15)
[Info][Witness] unassume invariant: (int )t11 == 0 || (int )t11 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:43:3-43:15)
[Info][Witness] unassume invariant: (int )t11 == 0 || (int )t11 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:45:3-45:28)
[Info][Witness] unassume invariant: (x1 == 0U || x1 == 1U) && x1 <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:46:3-46:11)
[Info][Witness] unassume invariant: (int )f11 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:49:3-49:10)
[Info][Witness] unassume invariant: ((int )f21 == 0 || (int )f21 == 1) && ((int )f11 == 0 || (int )f11 == 1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:51:3-51:28)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:55:3-55:15)
[Info][Witness] unassume invariant: (int )t11 == 0 || (int )t11 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:55:3-55:15)
[Info][Witness] unassume invariant: (int )t11 == 0 || (int )t11 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:57:3-57:28)
[Info][Witness] unassume invariant: (y1 == 0U || y1 == 1U) && y1 <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:58:3-58:11)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:66:3-66:15)
[Info][Witness] unassume invariant: (int )t21 == 0 || (int )t21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:66:3-66:15)
[Info][Witness] unassume invariant: (int )t21 == 0 || (int )t21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:68:3-68:28)
[Info][Witness] unassume invariant: (y1 == 0U || y1 == 1U) && y1 <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:69:3-69:11)
[Info][Witness] unassume invariant: (int )f21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:72:3-72:10)
[Info][Witness] unassume invariant: ((int )f21 == 0 || (int )f21 == 1) && ((int )f11 == 0 || (int )f11 == 1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:74:3-74:28)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:78:3-78:15)
[Info][Witness] unassume invariant: (int )t21 == 0 || (int )t21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:78:3-78:15)
[Info][Witness] unassume invariant: (int )t21 == 0 || (int )t21 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:80:3-80:28)
[Info][Witness] unassume invariant: (x1 == 0U || x1 == 1U) && x1 <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:81:3-81:11)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:89:3-89:15)
[Info][Witness] unassume invariant: (int )t12 == 0 || (int )t12 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:89:3-89:15)
[Info][Witness] unassume invariant: (int )t12 == 0 || (int )t12 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:91:3-91:28)
[Info][Witness] unassume invariant: (x2 == 0U || x2 == 1U) && x2 <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:92:3-92:11)
[Info][Witness] unassume invariant: (int )f12 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:95:3-95:10)
[Info][Witness] unassume invariant: ((int )f22 == 0 || (int )f22 == 1) && ((int )f12 == 0 || (int )f12 == 1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:97:3-97:28)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:101:3-101:15)
[Info][Witness] unassume invariant: (int )t12 == 0 || (int )t12 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:101:3-101:15)
[Info][Witness] unassume invariant: (int )t12 == 0 || (int )t12 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:103:3-103:28)
[Info][Witness] unassume invariant: (y2 == 0U || y2 == 1U) && y2 <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:104:3-104:11)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:112:3-112:15)
[Info][Witness] unassume invariant: (int )t22 == 0 || (int )t22 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:112:3-112:15)
[Info][Witness] unassume invariant: (int )t22 == 0 || (int )t22 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:114:3-114:28)
[Info][Witness] unassume invariant: (y2 == 0U || y2 == 1U) && y2 <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:115:3-115:11)
[Info][Witness] unassume invariant: (int )f22 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:118:3-118:10)
[Info][Witness] unassume invariant: ((int )f22 == 0 || (int )f22 == 1) && ((int )f12 == 0 || (int )f12 == 1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:120:3-120:28)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:124:3-124:15)
[Info][Witness] unassume invariant: (int )t22 == 0 || (int )t22 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:124:3-124:15)
[Info][Witness] unassume invariant: (int )t22 == 0 || (int )t22 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:126:3-126:28)
[Info][Witness] unassume invariant: (x2 == 0U || x2 == 1U) && x2 <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:127:3-127:11)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
  on line 155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:155-155)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 101
  dead: 1
  total lines: 102
[Success][Witness] invariant confirmed: t22 == (_Bool)0 || t22 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:113:3)
[Success][Witness] invariant confirmed: x1 <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:47:3)
[Success][Witness] invariant confirmed: x1 == 0U || x1 == 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:47:3)
[Success][Witness] invariant confirmed: t11 == (_Bool)0 || t11 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:44:3)
[Success][Witness] invariant confirmed: t12 == (_Bool)0 || t12 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:90:3)
[Success][Witness] invariant confirmed: y2 <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:116:3)
[Success][Witness] invariant confirmed: y2 == 0U || y2 == 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:116:3)
[Success][Witness] invariant confirmed: t12 == (_Bool)0 || t12 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:92:3)
[Success][Witness] invariant confirmed: t11 == (_Bool)0 || t11 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:46:3)
[Success][Witness] invariant confirmed: t11 == (_Bool)0 || t11 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:58:3)
[Success][Witness] invariant confirmed: y2 <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:105:3)
[Success][Witness] invariant confirmed: y2 == 0U || y2 == 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:105:3)
[Success][Witness] invariant confirmed: t22 == (_Bool)0 || t22 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:127:3)
[Success][Witness] invariant confirmed: f12 == (_Bool)0 || f12 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:121:3)
[Success][Witness] invariant confirmed: f22 == (_Bool)0 || f22 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:121:3)
[Success][Witness] invariant confirmed: f12 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:96:3)
[Success][Witness] invariant confirmed: t21 == (_Bool)0 || t21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:81:3)
[Success][Witness] invariant confirmed: t21 == (_Bool)0 || t21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:79:3)
[Success][Witness] invariant confirmed: f11 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:50:3)
[Success][Witness] invariant confirmed: y1 <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:70:3)
[Success][Witness] invariant confirmed: y1 == 0U || y1 == 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:70:3)
[Success][Witness] invariant confirmed: t11 == (_Bool)0 || t11 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:56:3)
[Success][Witness] invariant confirmed: x2 <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:128:3)
[Success][Witness] invariant confirmed: x2 == 0U || x2 == 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:128:3)
[Success][Witness] invariant confirmed: t22 == (_Bool)0 || t22 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:125:3)
[Success][Witness] invariant confirmed: y1 <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:59:3)
[Success][Witness] invariant confirmed: y1 == 0U || y1 == 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:59:3)
[Success][Witness] invariant confirmed: x2 <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:93:3)
[Success][Witness] invariant confirmed: x2 == 0U || x2 == 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:93:3)
[Success][Witness] invariant confirmed: f22 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:119:3)
[Success][Witness] invariant confirmed: f11 == (_Bool)0 || f11 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:52:3)
[Success][Witness] invariant confirmed: f21 == (_Bool)0 || f21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:52:3)
[Success][Witness] invariant confirmed: t22 == (_Bool)0 || t22 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:115:3)
[Success][Witness] invariant confirmed: x1 <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:82:3)
[Success][Witness] invariant confirmed: x1 == 0U || x1 == 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:82:3)
[Success][Witness] invariant confirmed: f21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:73:3)
[Success][Witness] invariant confirmed: t21 == (_Bool)0 || t21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:69:3)
[Success][Witness] invariant confirmed: t21 == (_Bool)0 || t21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:67:3)
[Success][Witness] invariant confirmed: f12 == (_Bool)0 || f12 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:98:3)
[Success][Witness] invariant confirmed: f22 == (_Bool)0 || f22 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:98:3)
[Success][Witness] invariant confirmed: t12 == (_Bool)0 || t12 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:104:3)
[Success][Witness] invariant confirmed: t12 == (_Bool)0 || t12 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:102:3)
[Success][Witness] invariant confirmed: f11 == (_Bool)0 || f11 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:75:3)
[Success][Witness] invariant confirmed: f21 == (_Bool)0 || f21 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/test-easy10.wvr.c:75:3)
[Info][Witness] witness validation summary:
  confirmed: 44
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 44
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 12
  vulnerable: 0
  unsafe: 0
  total memory locations: 12
