./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/13-privatized_04-priv_multi_true.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/13-privatized_04-priv_multi_true.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/goblint-regression/13-privatized_04-priv_multi_true.i


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


[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] pthread_mutex_unlock, pthread_mutex_lock, i, key, count, a, tmp, count, i, j, i___0, j___0, k, size, r, top, i, p, i
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: ((unsigned long )arg == 0UL && i <= 100) && 1 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1157:7-1157:23)
[Info][Witness] unassume invariant: i <= 99 && 1 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1158:5-1158:33)
[Info][Witness] unassume invariant: A <= 99 && 1 <= A (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1159:5-1159:10)
[Info][Witness] unassume invariant: A == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1160:5-1160:10)
[Info][Witness] unassume invariant: ((unsigned long )arg == 0UL && i <= 100) && 1 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1157:7-1157:23)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1166:1-1183:1)
[Info][Witness] unassume invariant: A == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1168:5-1168:33)
[Info][Witness] unassume invariant: A == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1169:9-1169:14)
[Info][Witness] unassume invariant: A == 6 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1170:7-1170:10)
[Info][Witness] unassume invariant: A == 6 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1171:7-1171:35)
[Info][Witness] unassume invariant: B == 6 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1172:7-1172:12)
[Info][Witness] unassume invariant: B == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1173:7-1173:10)
[Info][Witness] unassume invariant: A == 6 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1174:7-1174:37)
[Info][Witness] unassume invariant: A == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1175:7-1175:10)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1180:5-1180:13)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1184:1-1198:1)
[Info][Witness] unassume invariant: B == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1187:5-1187:33)
[Info][Witness] unassume invariant: B == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1188:9-1188:14)
[Info][Witness] unassume invariant: p == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1189:7-1189:12)
[Info][Witness] unassume invariant: p == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1190:7-1190:37)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1195:5-1195:13)
[Info][Witness] unassume invariant: i <= 10 && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1205:7-1205:22)
[Info][Witness] unassume invariant: B == 5 && A == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1207:5-1207:33)
[Info][Witness] unassume invariant: i <= 10 && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1205:7-1205:22)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:18:1-18:185)
[Warning][Deadcode] Function 'dispose' has dead code:
  on line 1194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1194-1194)
  on line 1197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1197-1197)
[Warning][Deadcode] Function 'process' has dead code:
  on line 1179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1179-1179)
  on line 1182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1182-1182)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 41
  dead: 5 (1 in uncalled functions)
  total lines: 46
[Warning][Deadcode][CWE-570] condition '! cond' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:19:39-19:46)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1167:10-1167:11)
[Warning][Deadcode][CWE-571] condition 'A > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1169:9-1169:14)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1186:10-1186:11)
[Warning][Deadcode][CWE-571] condition 'B > 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1188:9-1188:14)
[Success][Witness] invariant confirmed: 1 <= A (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1160:5)
[Success][Witness] invariant confirmed: A <= 99 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1160:5)
[Success][Witness] invariant confirmed: A == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1176:7)
[Success][Witness] invariant confirmed: B == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1189:7)
[Success][Witness] invariant confirmed: A == 6 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1171:7)
[Success][Witness] invariant confirmed: A == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1208:5)
[Success][Witness] invariant confirmed: B == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1208:5)
[Success][Witness] invariant confirmed: B == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1188:5)
[Success][Witness] invariant confirmed: A == 6 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1175:7)
[Success][Witness] invariant confirmed: A == 6 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1172:7)
[Success][Witness] invariant confirmed: p == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1191:7)
[Success][Witness] invariant confirmed: p == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1190:7)
[Success][Witness] invariant confirmed: B == 6 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1173:7)
[Success][Witness] invariant confirmed: A == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1161:5)
[Success][Witness] invariant confirmed: 1 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1159:5)
[Success][Witness] invariant confirmed: i <= 99 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1159:5)
[Success][Witness] invariant confirmed: A == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1170:7)
[Success][Witness] invariant confirmed: B == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1174:7)
[Success][Witness] invariant confirmed: A == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1169:5)
[Success][Witness] invariant confirmed: 1 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1157:3)
[Success][Witness] invariant confirmed: i <= 100 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1157:3)
[Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1157:3)
[Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1186:3)
[Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1167:3)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1205:3)
[Success][Witness] invariant confirmed: i <= 10 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_04-priv_multi_true.i:1205:3)
[Info][Witness] witness validation summary:
  confirmed: 26
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 26
SV-COMP result: true
[Info][Race] Memory locations race summary:
  safe: 2
  vulnerable: 0
  unsafe: 0
  total memory locations: 2
