./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/pals_lcr.6.1.ufo.UNBOUNDED.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.6.1.ufo.UNBOUNDED.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, node1__m1___0, node1__m1___1, node2__m2___0, node3__m3___0, node4__m4___0, node5__m5___0, node6__m6___0, node2__m2___1, cond
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:19:1-21:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:218-218)
  on line 236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:236-236)
  on line 254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:254-254)
  on line 272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:272-272)
  on line 290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:290-290)
  on line 308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:308-308)
  on line 339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:339-339)
  on line 357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:357-357)
  on line 368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:368-368)
  on line 488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:488-488)
  on line 623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:623-623)
  on line 668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:668-668)
  on line 713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:713-713)
  on line 758 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:758-758)
  on line 803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:803-803)
  on line 854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:854-854)
  on line 921 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:921-921)
  on line 945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:945-945)
  on line 969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:969-969)
  on line 993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:993-993)
  on line 1017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1017-1017)
  on line 1043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1043-1043)
  on line 1051 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1051-1051)
  on line 1056 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1056-1056)
  on line 1062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1062-1062)
  on line 1068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1068-1068)
  on line 1073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1073-1073)
  on line 1081 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1081-1081)
  on line 1086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1086-1086)
  on line 1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1094-1094)
  on line 1099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1099-1099)
  on line 1107 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1107-1107)
  on line 1112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1112-1112)
  on line 1120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1120-1120)
  on line 1125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1125-1125)
  on line 1133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1133-1133)
  on line 1138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1138-1138)
  on line 1146 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:1146-1146)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 377
  dead: 40 (2 in uncalled functions)
  total lines: 417
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:399:6-399:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:198:6-198: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:403:7-403:38)
[Warning][Deadcode][CWE-571] condition '! ((int )mode4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:413:6-413: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:417:7-417:38)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:216:6-216:19)
[Warning][Deadcode][CWE-571] condition '(int )send1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:223:6-223: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:225:6-225:21)
[Warning][Deadcode][CWE-571] condition '! ((int )mode5 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:427:6-427:19)
[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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:431:7-431:38)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:234:6-234: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:610:6-610:20)
[Warning][Deadcode][CWE-571] condition '(int )send2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:241:6-241: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:612:6-612:21)
[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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:243:6-243:21)
[Warning][Deadcode][CWE-571] condition '! ((int )mode6 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:441:6-441:19)
[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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:445:7-445:38)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:252:6-252: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:259:6-259: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:261:6-261:21)
[Warning][Deadcode][CWE-571] condition '(int )send5 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:655:6-655:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode4 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:270:6-270:19)
[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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:657:6-657: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:277:6-277: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:279:6-279:21)
[Warning][Deadcode][CWE-570] condition '! ((int )mode5 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:288:6-288: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:295:6-295: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:297:6-297: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:700:6-700: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:702:6-702:21)
[Warning][Deadcode][CWE-570] condition '! ((int )mode6 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:306:6-306: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:313:6-313: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:315:6-315:21)
[Warning][Deadcode][CWE-571] condition '(int )send3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:745:6-745: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:747:6-747:21)
[Warning][Deadcode][CWE-571] condition '(((((int )st1 + (int )st2) + (int )st3) + (int )st4) + (int )st5) + (int )st6 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:335:12-335:96)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:337:7-337:20)
[Warning][Deadcode][CWE-571] condition '(((((int )st1 + (int )st2) + (int )st3) + (int )st4) + (int )st5) + (int )st6 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:343:12-343:96)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:345:7-345:19)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:355:6-355:22)
[Warning][Deadcode][CWE-571] condition '(int )send2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:790:6-790: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:792:6-792:21)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:364:6-364:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:366:6-366:15)
[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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:375:7-375:38)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:385:6-385:19)
[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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:389:7-389: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:841:6-841: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.6.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:843:6-843:21)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
