./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.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/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.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] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] nomsg, __return_main, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, main__i2, node1__m1___0, node1__m1___1, node2__m2___0, node3__m3___0, node4__m4___0, node5__m5___0, node6__m6___0, cond
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:575:2-575:28)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:255-255)
  on line 273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:273-273)
  on line 291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:291-291)
  on line 309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:309-309)
  on line 327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:327-327)
  on line 345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:345-345)
  on line 363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:363-363)
  on line 396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:396-396)
  on line 414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:414-414)
  on line 562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:562-562)
  on line 698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:698-698)
  on line 743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:743-743)
  on line 788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:788-788)
  on line 833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:833-833)
  on line 878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:878-878)
  on line 924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:924-924)
  on line 1011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1011-1011)
  on line 1042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1042-1042)
  on line 1066 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1066-1066)
  on line 1090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1090-1090)
  on line 1114 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1114-1114)
  on line 1138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1138-1138)
  on line 1163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1163-1163)
  on line 1169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1169-1169)
  on line 1176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1176-1176)
  on line 1181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1181-1181)
  on line 1187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1187-1187)
  on line 1193 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1193-1193)
  on line 1198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1198-1198)
  on line 1206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1206-1206)
  on line 1211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1211-1211)
  on line 1219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1219-1219)
  on line 1224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1224-1224)
  on line 1232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1232-1232)
  on line 1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1237-1237)
  on line 1245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1245-1245)
  on line 1250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1250-1250)
  on line 1258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1258-1258)
  on line 1263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1263-1263)
  on line 1271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1271-1271)
  on line 1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1276-1276)
  on line 1284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1284-1284)
  on line 1289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1289-1289)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 437
  dead: 45 (2 in uncalled functions)
  total lines: 482
[Warning][Deadcode][CWE-570] condition '(int )assert__arg == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:412:6-412:22)
[Warning][Deadcode][CWE-571] condition '(int )send3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:820:6-820:20)
[Warning][Deadcode][CWE-571] condition '(int )p3_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:822:6-822:21)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:420:6-420:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:425:6-425:19)
[Warning][Deadcode][CWE-571] condition '(int )node1__m1___0 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:430:7-430:38)
[Warning][Deadcode][CWE-571] condition 'main__i2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:231:6-231:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:440:6-440:19)
[Warning][Deadcode][CWE-571] condition '(int )send2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:865:6-865:20)
[Warning][Deadcode][CWE-571] condition '(int )p2_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:867:6-867:21)
[Warning][Deadcode][CWE-571] condition '(int )node2__m2___0 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:444:7-444:38)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:454:6-454:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:248:6-248:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:253:6-253:19)
[Warning][Deadcode][CWE-571] condition '(int )node3__m3___0 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:458:7-458:38)
[Warning][Deadcode][CWE-571] condition '(int )send1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:260:6-260:20)
[Warning][Deadcode][CWE-571] condition '(int )p1_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:262:6-262:21)
[Warning][Deadcode][CWE-571] condition '(int )send1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:911:6-911:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:468:6-468:19)
[Warning][Deadcode][CWE-571] condition '(int )p1_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:913:6-913:21)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:271:6-271:19)
[Warning][Deadcode][CWE-571] condition '(int )node4__m4___0 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:472:7-472:38)
[Warning][Deadcode][CWE-571] condition '(int )send2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:278:6-278:20)
[Warning][Deadcode][CWE-571] condition '(int )p2_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:280:6-280:21)
[Warning][Deadcode][CWE-571] condition '! ((int )mode5 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:482:6-482:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:289:6-289:19)
[Warning][Deadcode][CWE-571] condition '(int )send3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:296:6-296:20)
[Warning][Deadcode][CWE-571] condition '(int )node5__m5___0 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:486:7-486:38)
[Warning][Deadcode][CWE-571] condition '(int )p3_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:298:6-298:21)
[Warning][Deadcode][CWE-571] condition '! ((int )mode6 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:496:6-496:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode4 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:307:6-307:19)
[Warning][Deadcode][CWE-571] condition '(int )send4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:314:6-314:20)
[Warning][Deadcode][CWE-571] condition '(int )p4_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:316:6-316:21)
[Warning][Deadcode][CWE-571] condition '(int )node6__m6___0 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:500:7-500:38)
[Warning][Deadcode][CWE-570] condition '! ((int )mode5 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:325:6-325:19)
[Warning][Deadcode][CWE-571] condition '(int )send5 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:332:6-332:20)
[Warning][Deadcode][CWE-571] condition '(int )p5_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:334:6-334:21)
[Warning][Deadcode][CWE-571] condition '(int )send7 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:998:6-998:20)
[Warning][Deadcode][CWE-571] condition '(int )send6 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:685:6-685:20)
[Warning][Deadcode][CWE-571] condition '(int )p7_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:1000:6-1000:21)
[Warning][Deadcode][CWE-571] condition '(int )p6_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:687:6-687:21)
[Warning][Deadcode][CWE-570] condition '! ((int )mode6 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:343:6-343:19)
[Warning][Deadcode][CWE-571] condition '(int )send6 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:350:6-350:20)
[Warning][Deadcode][CWE-571] condition '(int )p6_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:352:6-352:21)
[Warning][Deadcode][CWE-570] condition '! ((int )mode7 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:361:6-361:19)
[Warning][Deadcode][CWE-571] condition '(int )send5 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:730:6-730:20)
[Warning][Deadcode][CWE-571] condition '(int )send7 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:368:6-368:20)
[Warning][Deadcode][CWE-571] condition '(int )p5_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:732:6-732:21)
[Warning][Deadcode][CWE-571] condition '(int )p7_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:370:6-370:21)
[Warning][Deadcode][CWE-571] condition '(int )send4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:775:6-775:20)
[Warning][Deadcode][CWE-571] condition '(int )p4_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:777:6-777:21)
[Warning][Deadcode][CWE-571] condition '((((((int )st1 + (int )st2) + (int )st3) + (int )st4) + (int )st5) + (int )st6) + (int )st7 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:392:13-392:111)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 7' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:394:7-394:20)
[Warning][Deadcode][CWE-571] condition '((((((int )st1 + (int )st2) + (int )st3) + (int )st4) + (int )st5) + (int )st6) + (int )st7 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:400:13-400:111)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 7' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.7.1.ufo.BOUNDED-14.pals.c.v+nlh-reducer.c:402:7-402:19)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
