./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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-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, r1, 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, node2__m2___1, node3__m3___1, node3__m3___2, 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][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:241:2-241:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:328:2-328:28)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 149 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:149-149)
  on line 166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:166-166)
  on line 183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:183-183)
  on line 207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:207-207)
  on line 225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:225-225)
  on line 294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:294-294)
  on line 312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:312-312)
  on line 401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:401-401)
  on line 483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:483-483)
  on line 528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:528-528)
  on line 574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:574-574)
  on line 595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:595-595)
  on line 600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:600-600)
  on line 606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:606-606)
  on line 628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:628-628)
  on line 634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:634-634)
  on line 649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:649-649)
  on line 653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:653-653)
  on line 661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:661-661)
  on line 673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:673-673)
  on line 679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:679-679)
  on line 716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:716-716)
  on line 722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:722-722)
  on line 737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:737-737)
  on line 741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:741-741)
  on line 749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:749-749)
  on line 769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:769-769)
  on line 784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:784-784)
  on line 788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:788-788)
  on line 802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:802-802)
  on line 808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:808-808)
  on line 820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:820-820)
  on line 826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:826-826)
  on line 878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:878-878)
  on line 884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:884-884)
  on line 899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:899-899)
  on line 903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:903-903)
  on line 911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:911-911)
  on line 931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:931-931)
  on line 946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:946-946)
  on line 950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:950-950)
  on line 965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:965-965)
  on line 971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:971-971)
  on line 1006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1006-1006)
  on line 1021 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1021-1021)
  on line 1025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1025-1025)
  on line 1047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1047-1047)
  on line 1067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1067-1067)
  on line 1073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1073-1073)
  on line 1085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1085-1085)
  on line 1091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1091-1091)
  on line 1104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1104-1104)
  on line 1110 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1110-1110)
  on line 1116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1116-1116)
  on line 1123 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1123-1123)
  on line 1128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1128-1128)
  on line 1134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1134-1134)
  on line 1140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1140-1140)
  on lines 1145..1153 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1145-1153)
  on line 1156 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1156-1156)
  on line 1158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1158-1158)
  on line 1160 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1160-1160)
  on line 1164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1164-1164)
  on line 1166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1166-1166)
  on lines 1168..1170 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1168-1170)
  on line 1173 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1173-1173)
  on lines 1175..1176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1175-1176)
  on line 1178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1178-1178)
  on lines 1182..1184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1182-1184)
  on line 1191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1191-1191)
  on line 1196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1196-1196)
  on line 1202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1202-1202)
  on line 1211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1211-1211)
  on lines 1216..1218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1216-1218)
  on lines 1221..1222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1221-1222)
  on line 1224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1224-1224)
  on line 1229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1229-1229)
  on line 1231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1231-1231)
  on lines 1233..1241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1233-1241)
  on line 1244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1244-1244)
  on line 1246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1246-1246)
  on line 1248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1248-1248)
  on line 1252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1252-1252)
  on line 1254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1254-1254)
  on lines 1256..1258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1256-1258)
  on line 1261 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1261-1261)
  on lines 1263..1264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1263-1264)
  on line 1266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1266-1266)
  on lines 1270..1272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1270-1272)
  on line 1279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1279-1279)
  on line 1284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1284-1284)
  on line 1290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1290-1290)
  on line 1296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1296-1296)
  on lines 1301..1309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1301-1309)
  on line 1312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1312-1312)
  on line 1314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1314-1314)
  on line 1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1316-1316)
  on line 1320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1320-1320)
  on line 1322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1322-1322)
  on lines 1324..1326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1324-1326)
  on line 1329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1329-1329)
  on lines 1331..1332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1331-1332)
  on line 1334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1334-1334)
  on lines 1338..1340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1338-1340)
  on line 1347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1347-1347)
  on line 1352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1352-1352)
  on line 1358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1358-1358)
  on line 1370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1370-1370)
  on lines 1375..1377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1375-1377)
  on lines 1380..1381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1380-1381)
  on line 1383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1383-1383)
  on line 1388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1388-1388)
  on line 1390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1390-1390)
  on lines 1392..1394 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1392-1394)
  on lines 1397..1398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1397-1398)
  on line 1400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1400-1400)
  on line 1405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1405-1405)
  on line 1407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1407-1407)
  on lines 1409..1417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1409-1417)
  on line 1420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1420-1420)
  on line 1422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1422-1422)
  on line 1424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1424-1424)
  on line 1428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1428-1428)
  on line 1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1430-1430)
  on lines 1432..1434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1432-1434)
  on line 1437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1437-1437)
  on lines 1439..1440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1439-1440)
  on line 1442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1442-1442)
  on lines 1446..1448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1446-1448)
  on line 1455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1455-1455)
  on line 1460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1460-1460)
  on line 1466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1466-1466)
  on line 1472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1472-1472)
  on lines 1477..1485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1477-1485)
  on line 1488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1488-1488)
  on line 1490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1490-1490)
  on line 1492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1492-1492)
  on line 1496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1496-1496)
  on line 1498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1498-1498)
  on lines 1500..1502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1500-1502)
  on line 1505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1505-1505)
  on lines 1507..1508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1507-1508)
  on line 1510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1510-1510)
  on lines 1514..1516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1514-1516)
  on line 1523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1523-1523)
  on line 1528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1528-1528)
  on line 1534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1534-1534)
  on line 1543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1543-1543)
  on lines 1548..1550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1548-1550)
  on lines 1553..1554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1553-1554)
  on line 1556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1556-1556)
  on line 1561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1561-1561)
  on line 1563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1563-1563)
  on lines 1565..1573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1565-1573)
  on line 1576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1576-1576)
  on line 1578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1578-1578)
  on line 1580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1580-1580)
  on line 1584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1584-1584)
  on line 1586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1586-1586)
  on lines 1588..1590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1588-1590)
  on line 1593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1593-1593)
  on lines 1595..1596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1595-1596)
  on line 1598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1598-1598)
  on lines 1602..1604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1602-1604)
  on line 1611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1611-1611)
  on line 1616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1616-1616)
  on line 1622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1622-1622)
  on line 1628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1628-1628)
  on lines 1633..1641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1633-1641)
  on line 1644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1644-1644)
  on line 1646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1646-1646)
  on line 1648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1648-1648)
  on line 1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1652-1652)
  on line 1654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1654-1654)
  on lines 1656..1658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1656-1658)
  on line 1661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1661-1661)
  on lines 1663..1664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1663-1664)
  on line 1666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1666-1666)
  on lines 1670..1672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1670-1672)
  on line 1679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1679-1679)
  on line 1684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1684-1684)
  on line 1690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1690-1690)
  on line 1705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1705-1705)
  on line 1710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1710-1710)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 383
  dead: 289 (2 in uncalled functions)
  total lines: 672
[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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:190:6-190:21)
[Warning][Deadcode][CWE-570] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:882:9-882:51)
[Warning][Deadcode][CWE-570] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:632:9-632:51)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___5 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:896:6-896:22)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___2 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:646:6-646:22)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:203:9-203:51)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:205:7-205:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:211:9-211:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:213:7-213: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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:223:6-223:22)
[Warning][Deadcode][CWE-570] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:929:9-929:51)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:692:6-692:19)
[Warning][Deadcode][CWE-571] condition '(int )node3__m3___2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:696:7-696:38)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:234:6-234:18)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___6 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:943:6-943:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:239:6-239: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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:244:7-244:38)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:712:9-712:51)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:714:7-714:20)
[Warning][Deadcode][CWE-570] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:720:9-720:51)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:255:6-255:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:984:6-984: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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:259:7-259:38)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:734:6-734:22)
[Warning][Deadcode][CWE-571] condition '(int )node3__m3___4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:988:7-988:38)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:270:6-270: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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:470:6-470: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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:472:6-472:21)
[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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:274:7-274:38)
[Warning][Deadcode][CWE-570] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1004:9-1004:51)
[Warning][Deadcode][CWE-570] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:767:9-767:51)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___7 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1018:6-1018:22)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:290:9-290:51)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:292:7-292:20)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:781:6-781: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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:515:6-515:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:298:9-298:51)
[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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:517:6-517:21)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:300:7-300:19)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___0 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:310:6-310:22)
[Warning][Deadcode][CWE-570] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:1045:9-1045:51)
[Warning][Deadcode][CWE-571] condition 'main__i2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:133:6-133:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:839:6-839: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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:561:6-561: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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:563:6-563:21)
[Warning][Deadcode][CWE-571] condition '(int )node2__m2___2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:843:7-843:38)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:142:6-142:18)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:147:6-147:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:854:6-854: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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:154:6-154: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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:156:6-156:21)
[Warning][Deadcode][CWE-571] condition '(int )node3__m3___3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:858:7-858:38)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:164:6-164: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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:171:6-171: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.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:173:6-173:21)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:181:6-181:19)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:874:9-874:51)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:624:9-624:51)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:876:7-876:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:626:7-626:20)
[Warning][Deadcode][CWE-571] condition '(int )send3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+lhb-reducer.c:188:6-188:20)
[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
