./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_floodmax.4.1.ufo.BOUNDED-8.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_floodmax.4.1.ufo.BOUNDED-8.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_floodmax.4.1.ufo.BOUNDED-8.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] 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_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1837:2-1837:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1873:2-1873:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1909:2-1909:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1945:2-1945:28)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:454-454)
  on line 497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:497-497)
  on line 540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:540-540)
  on line 583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:583-583)
  on line 661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:661-661)
  on line 671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:671-671)
  on line 689 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:689-689)
  on line 727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:727-727)
  on line 762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:762-762)
  on line 797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:797-797)
  on line 832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:832-832)
  on line 875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:875-875)
  on line 885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:885-885)
  on line 903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:903-903)
  on line 914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:914-914)
  on line 957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:957-957)
  on line 1000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1000-1000)
  on line 1043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1043-1043)
  on line 1121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1121-1121)
  on line 1131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1131-1131)
  on line 1149 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1149-1149)
  on line 1187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1187-1187)
  on line 1222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1222-1222)
  on line 1257 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1257-1257)
  on line 1292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1292-1292)
  on line 1335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1335-1335)
  on line 1345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1345-1345)
  on line 1363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1363-1363)
  on line 1374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1374-1374)
  on line 1417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1417-1417)
  on line 1460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1460-1460)
  on line 1503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1503-1503)
  on line 1581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1581-1581)
  on line 1591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1591-1591)
  on line 1609 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1609-1609)
  on line 1797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1797-1797)
  on line 1808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1808-1808)
  on line 1826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1826-1826)
  on line 2208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2208-2208)
  on line 2225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2225-2225)
  on line 2242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2242-2242)
  on line 2347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2347-2347)
  on line 2364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2364-2364)
  on line 2381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2381-2381)
  on line 2486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2486-2486)
  on line 2503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2503-2503)
  on line 2520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2520-2520)
  on line 2625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2625-2625)
  on line 2642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2642-2642)
  on line 2659 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2659-2659)
  on line 2704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2704-2704)
  on line 2710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2710-2710)
  on line 2724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2724-2724)
  on line 2762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2762-2762)
  on line 2797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2797-2797)
  on line 2809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2809-2809)
  on line 2844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2844-2844)
  on line 2856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2856-2856)
  on line 2891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2891-2891)
  on line 2903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2903-2903)
  on line 2938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2938-2938)
  on line 2944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2944-2944)
  on line 2951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2951-2951)
  on line 2956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2956-2956)
  on line 2962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2962-2962)
  on line 2967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2967-2967)
  on line 2973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2973-2973)
  on line 2978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2978-2978)
  on line 2983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2983-2983)
  on line 2988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2988-2988)
  on line 2993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2993-2993)
  on line 3000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3000-3000)
  on line 3017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3017-3017)
  on line 3034 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3034-3034)
  on line 3050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3050-3050)
  on line 3058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3058-3058)
  on line 3075 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3075-3075)
  on line 3092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3092-3092)
  on line 3108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3108-3108)
  on line 3116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3116-3116)
  on line 3133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3133-3133)
  on line 3150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3150-3150)
  on line 3166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3166-3166)
  on line 3174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3174-3174)
  on line 3191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3191-3191)
  on line 3208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3208-3208)
  on line 3224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3224-3224)
  on line 3231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3231-3231)
  on line 3238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3238-3238)
  on line 3243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3243-3243)
  on line 3249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3249-3249)
  on line 3254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3254-3254)
  on line 3260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3260-3260)
  on line 3265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3265-3265)
  on line 3270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3270-3270)
  on line 3275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3275-3275)
  on line 3280 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3280-3280)
  on line 3317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3317-3317)
  on line 3354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3354-3354)
  on line 3391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3391-3391)
  on line 3428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3428-3428)
  on line 3434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3434-3434)
  on line 3441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3441-3441)
  on line 3446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3446-3446)
  on line 3452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3452-3452)
  on line 3457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3457-3457)
  on line 3463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3463-3463)
  on line 3468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3468-3468)
  on line 3473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3473-3473)
  on line 3478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3478-3478)
  on line 3483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3483-3483)
  on line 3490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3490-3490)
  on line 3507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3507-3507)
  on line 3524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3524-3524)
  on line 3540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3540-3540)
  on line 3548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3548-3548)
  on line 3565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3565-3565)
  on line 3582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3582-3582)
  on line 3598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3598-3598)
  on line 3606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3606-3606)
  on line 3623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3623-3623)
  on line 3640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3640-3640)
  on line 3656 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3656-3656)
  on line 3664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3664-3664)
  on line 3681 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3681-3681)
  on line 3698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3698-3698)
  on line 3714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3714-3714)
  on line 3721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3721-3721)
  on line 3728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3728-3728)
  on line 3733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3733-3733)
  on line 3739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3739-3739)
  on line 3744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3744-3744)
  on line 3750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3750-3750)
  on line 3755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3755-3755)
  on line 3760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3760-3760)
  on line 3765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3765-3765)
  on line 3770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3770-3770)
  on line 3807 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3807-3807)
  on line 3844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3844-3844)
  on line 3881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3881-3881)
  on line 3918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3918-3918)
  on line 3924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3924-3924)
  on line 3931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3931-3931)
  on line 3936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3936-3936)
  on line 3942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3942-3942)
  on line 3947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3947-3947)
  on line 3953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3953-3953)
  on line 3958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3958-3958)
  on line 3963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3963-3963)
  on line 3968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3968-3968)
  on line 3973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3973-3973)
  on line 3980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3980-3980)
  on line 3997 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3997-3997)
  on line 4014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4014-4014)
  on line 4030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4030-4030)
  on line 4038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4038-4038)
  on line 4055 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4055-4055)
  on line 4072 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4072-4072)
  on line 4088 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4088-4088)
  on line 4096 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4096-4096)
  on line 4113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4113-4113)
  on line 4130 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4130-4130)
  on line 4146 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4146-4146)
  on line 4154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4154-4154)
  on line 4171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4171-4171)
  on line 4188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4188-4188)
  on line 4204 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4204-4204)
  on line 4211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4211-4211)
  on line 4216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4216-4216)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 1350
  dead: 171 (2 in uncalled functions)
  total lines: 1521
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1113:8-1113:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1115:8-1115:36)
[Warning][Deadcode][CWE-571] condition '(int )st4 + (int )nl4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1117:8-1117:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1119:7-1119:20)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1125:10-1125:66)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1793:7-1793:20)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1127:7-1127:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1795:7-1795:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1129:7-1129:20)
[Warning][Deadcode][CWE-571] condition '(((int )nl1 + (int )nl2) + (int )nl3) + (int )nl4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1135:10-1135:66)
[Warning][Deadcode][CWE-571] condition '(int )r1 >= 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1803:7-1803:20)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1137:7-1137:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:422:6-422:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1806:7-1806:19)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1147:6-1147:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1155:6-1155:18)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1158:6-1158:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:449:6-449:18)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:452:6-452:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:458:7-458:19)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:463:6-463:19)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:465:6-465:22)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1185:7-1185:20)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:474:6-474:19)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:476:6-476:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1193:6-1193:19)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:485:6-485:19)
[Warning][Deadcode][CWE-571] condition '(int )p14_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:487:6-487:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:495:6-495:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:501:7-501:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:506:6-506:19)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:508:6-508:22)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:517:6-517:19)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:519:6-519:22)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1220:7-1220:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1228:6-1228:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:528:6-528:19)
[Warning][Deadcode][CWE-571] condition '(int )p24_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:530:6-530:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:538:6-538:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:544:7-544:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:549:6-549:19)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:551:6-551:22)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:560:6-560:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:562:6-562:22)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1255:7-1255:20)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:571:6-571:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1263:6-1263:19)
[Warning][Deadcode][CWE-571] condition '(int )p34_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:573:6-573:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode4 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:581:6-581:19)
[Warning][Deadcode][CWE-571] condition '(int )r4 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:587:7-587:19)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:592:6-592:19)
[Warning][Deadcode][CWE-571] condition '(int )p41_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:594:6-594:22)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:603:6-603:19)
[Warning][Deadcode][CWE-571] condition '(int )p42_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:605:6-605:22)
[Warning][Deadcode][CWE-570] condition '(int )r4 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1290:7-1290:20)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:614:6-614:19)
[Warning][Deadcode][CWE-571] condition '(int )p43_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:616:6-616:22)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1323:10-1323:66)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1325:8-1325:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1327:8-1327:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1329:8-1329:36)
[Warning][Deadcode][CWE-571] condition '(int )st4 + (int )nl4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1331:8-1331:36)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:649:10-649:66)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1333:7-1333:20)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:651:8-651:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:653:8-653:36)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1339:10-1339:66)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:655:8-655:36)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1341:7-1341:19)
[Warning][Deadcode][CWE-571] condition '(int )st4 + (int )nl4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:657:8-657:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1343:7-1343:20)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:659:7-659:20)
[Warning][Deadcode][CWE-571] condition '(((int )nl1 + (int )nl2) + (int )nl3) + (int )nl4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1349:10-1349:66)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:665:10-665:66)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1351:7-1351:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:667:7-667:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:669:7-669:20)
[Warning][Deadcode][CWE-571] condition '(((int )nl1 + (int )nl2) + (int )nl3) + (int )nl4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:675:10-675:66)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:677:7-677:19)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1361:6-1361:22)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:687:6-687:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1369:6-1369:18)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1372:6-1372:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1378:7-1378:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:695:6-695:18)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1383:6-1383:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:698:6-698:19)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1385:6-1385:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1394:6-1394:19)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1396:6-1396:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1405:6-1405:19)
[Warning][Deadcode][CWE-571] condition '(int )p14_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1407:6-1407:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1415:6-1415:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1421:7-1421:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:725:7-725:20)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1426:6-1426:19)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1428:6-1428:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:733:6-733:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1437:6-1437:19)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1439:6-1439:22)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1448:6-1448:19)
[Warning][Deadcode][CWE-571] condition '(int )p24_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1450:6-1450:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1458:6-1458:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1464:7-1464:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1469:6-1469:19)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1471:6-1471:22)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:760:7-760:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:768:6-768:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1480:6-1480:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1482:6-1482:22)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2172:6-2172:19)
[Warning][Deadcode][CWE-571] condition '(int )p41_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2174:6-2174:22)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1491:6-1491:19)
[Warning][Deadcode][CWE-571] condition '(int )p34_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1493:6-1493:22)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2183:6-2183:19)
[Warning][Deadcode][CWE-571] condition '(int )p42_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2185:6-2185:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode4 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1501:6-1501:19)
[Warning][Deadcode][CWE-571] condition '(int )r4 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1507:7-1507:19)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1512:6-1512:19)
[Warning][Deadcode][CWE-571] condition '(int )p41_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1514:6-1514:22)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2194:6-2194:19)
[Warning][Deadcode][CWE-571] condition '(int )p43_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2196:6-2196:22)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:795:7-795:20)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1523:6-1523:19)
[Warning][Deadcode][CWE-571] condition '(int )p42_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1525:6-1525:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:803:6-803:19)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1534:6-1534:19)
[Warning][Deadcode][CWE-571] condition '(int )p43_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1536:6-1536:22)
[Warning][Deadcode][CWE-570] condition '(int )r4 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:830:7-830:20)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2311:6-2311:19)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2313:6-2313:22)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2322:6-2322:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2324:6-2324:22)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1569:10-1569:66)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1571:8-1571:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1573:8-1573:36)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1575:8-1575:36)
[Warning][Deadcode][CWE-571] condition '(int )st4 + (int )nl4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1577:8-1577:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1579:7-1579:20)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2333:6-2333:19)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1585:10-1585:66)
[Warning][Deadcode][CWE-571] condition '(int )p34_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2335:6-2335:22)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1587:7-1587:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1589:7-1589:20)
[Warning][Deadcode][CWE-571] condition '(((int )nl1 + (int )nl2) + (int )nl3) + (int )nl4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1595:10-1595:66)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1597:7-1597:19)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:863:10-863:66)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:865:8-865:36)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:867:8-867:36)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1607:6-1607:22)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:869:8-869:36)
[Warning][Deadcode][CWE-571] condition '(int )st4 + (int )nl4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:871:8-871:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:873:7-873:20)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:879:10-879:66)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1615:6-1615:18)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:881:7-881:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1618:6-1618:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:883:7-883:20)
[Warning][Deadcode][CWE-571] condition '(((int )nl1 + (int )nl2) + (int )nl3) + (int )nl4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:889:10-889:66)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:891:7-891: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_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:901:6-901:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:909:6-909:18)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:912:6-912:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2450:6-2450:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:918:7-918:19)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2452:6-2452:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:923:6-923:19)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:925:6-925:22)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2461:6-2461:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1645:7-1645:20)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2463:6-2463:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:934:6-934:19)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:936:6-936:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1653:6-1653:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2472:6-2472:19)
[Warning][Deadcode][CWE-571] condition '(int )p24_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2474:6-2474:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:945:6-945:19)
[Warning][Deadcode][CWE-571] condition '(int )p14_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:947:6-947:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:955:6-955:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:961:7-961:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:966:6-966:19)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:968:6-968:22)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:977:6-977:19)
[Warning][Deadcode][CWE-571] condition '(int )p23_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:979:6-979:22)
[Warning][Deadcode][CWE-571] condition '(int )r2 == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1680:7-1680:20)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:988:6-988:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1688:6-1688:19)
[Warning][Deadcode][CWE-571] condition '(int )p24_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:990:6-990:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2589:6-2589:19)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2591:6-2591:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:998:6-998:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1004:7-1004:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1009:6-1009:19)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1011:6-1011:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2600:6-2600:19)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2602:6-2602:22)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1020:6-1020:19)
[Warning][Deadcode][CWE-571] condition '(int )p32_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1022:6-1022:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2611:6-2611:19)
[Warning][Deadcode][CWE-571] condition '(int )p14_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2613:6-2613:22)
[Warning][Deadcode][CWE-571] condition '(int )r3 == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1715:7-1715:20)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1031:6-1031:19)
[Warning][Deadcode][CWE-571] condition '(int )p34_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1033:6-1033:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1723:6-1723:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode4 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1041:6-1041:19)
[Warning][Deadcode][CWE-571] condition '(int )r4 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1047:7-1047:19)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1052:6-1052:19)
[Warning][Deadcode][CWE-571] condition '(int )p41_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1054:6-1054:22)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1063:6-1063:19)
[Warning][Deadcode][CWE-571] condition '(int )p42_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1065:6-1065:22)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1074:6-1074:19)
[Warning][Deadcode][CWE-571] condition '(int )p43_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1076:6-1076:22)
[Warning][Deadcode][CWE-571] condition '(int )r4 == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1750:7-1750:20)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1109:10-1109:66)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1111:8-1111:36)
[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)
