./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.6.1.ufo.BOUNDED-12.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.6.1.ufo.BOUNDED-12.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.BOUNDED-12.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.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:504:2-504:28)
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:221-221)
  on line 239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:239-239)
  on line 257 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:257-257)
  on line 275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:275-275)
  on line 293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:293-293)
  on line 311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:311-311)
  on line 342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:342-342)
  on line 360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:360-360)
  on line 491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:491-491)
  on line 627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:627-627)
  on line 672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:672-672)
  on line 717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:717-717)
  on line 762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:762-762)
  on line 807 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:807-807)
  on line 853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:853-853)
  on line 926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:926-926)
  on line 950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:950-950)
  on line 974 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:974-974)
  on line 998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:998-998)
  on line 1022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1022-1022)
  on line 1047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1047-1047)
  on line 1053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1053-1053)
  on line 1060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1060-1060)
  on line 1065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1065-1065)
  on line 1071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1071-1071)
  on line 1077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1077-1077)
  on line 1082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1082-1082)
  on line 1090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1090-1090)
  on line 1095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1095-1095)
  on line 1103 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1103-1103)
  on line 1108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1108-1108)
  on line 1116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1116-1116)
  on line 1121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1121-1121)
  on line 1129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1129-1129)
  on line 1134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1134-1134)
  on line 1142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1142-1142)
  on line 1147 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1147-1147)
  on line 1155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1155-1155)
  on line 1160 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:1160-1160)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 385
  dead: 41 (2 in uncalled functions)
  total lines: 426
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:840:6-840:20)
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:199:6-199: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.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:842:6-842:21)
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:400:6-400: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.BOUNDED-12.pals.c.v+nlh-reducer.c:404:7-404: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.BOUNDED-12.pals.c.v+nlh-reducer.c:414:6-414:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 12' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:214:6-214: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.BOUNDED-12.pals.c.v+nlh-reducer.c:418:7-418: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.BOUNDED-12.pals.c.v+nlh-reducer.c:219:6-219: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.BOUNDED-12.pals.c.v+nlh-reducer.c:226:6-226: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.BOUNDED-12.pals.c.v+nlh-reducer.c:228:6-228: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.BOUNDED-12.pals.c.v+nlh-reducer.c:428:6-428:19)
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:237:6-237: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.BOUNDED-12.pals.c.v+nlh-reducer.c:432:7-432: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.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:244:6-244: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.BOUNDED-12.pals.c.v+nlh-reducer.c:246:6-246:21)
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:614:6-614:20)
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:442:6-442:19)
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:616:6-616:21)
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:255:6-255: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.BOUNDED-12.pals.c.v+nlh-reducer.c:446:7-446:38)
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:262:6-262: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.BOUNDED-12.pals.c.v+nlh-reducer.c:264:6-264:21)
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:273:6-273: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.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:280:6-280: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.BOUNDED-12.pals.c.v+nlh-reducer.c:282:6-282: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.BOUNDED-12.pals.c.v+nlh-reducer.c:659:6-659: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.BOUNDED-12.pals.c.v+nlh-reducer.c:661:6-661: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.BOUNDED-12.pals.c.v+nlh-reducer.c:291:6-291: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.BOUNDED-12.pals.c.v+nlh-reducer.c:298:6-298: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.BOUNDED-12.pals.c.v+nlh-reducer.c:300:6-300: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.BOUNDED-12.pals.c.v+nlh-reducer.c:309:6-309: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.BOUNDED-12.pals.c.v+nlh-reducer.c:316:6-316: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.BOUNDED-12.pals.c.v+nlh-reducer.c:318:6-318: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.BOUNDED-12.pals.c.v+nlh-reducer.c:704:6-704: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.BOUNDED-12.pals.c.v+nlh-reducer.c:706:6-706: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.BOUNDED-12.pals.c.v+nlh-reducer.c:338:12-338:96)
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:749:6-749:20)
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:340:7-340: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.BOUNDED-12.pals.c.v+nlh-reducer.c:751:6-751:21)
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:346:12-346: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.BOUNDED-12.pals.c.v+nlh-reducer.c:348:7-348: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.BOUNDED-12.pals.c.v+nlh-reducer.c:358:6-358:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 12' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:366:6-366: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.6.1.ufo.BOUNDED-12.pals.c.v+nlh-reducer.c:794:6-794:20)
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:371:6-371:19)
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:796:6-796:21)
[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.BOUNDED-12.pals.c.v+nlh-reducer.c:376:7-376: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.BOUNDED-12.pals.c.v+nlh-reducer.c:386:6-386: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.BOUNDED-12.pals.c.v+nlh-reducer.c:390:7-390:38)
[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)
