./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.3.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.3.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.3.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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1861:2-1861:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1897:2-1897:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1933:2-1933:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1969:2-1969: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:478-478)
  on line 521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:521-521)
  on line 564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:564-564)
  on line 607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:607-607)
  on line 685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:685-685)
  on line 695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:695-695)
  on line 713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:713-713)
  on line 751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:751-751)
  on line 786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:786-786)
  on line 821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:821-821)
  on line 856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:856-856)
  on line 899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:899-899)
  on line 909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:909-909)
  on line 927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:927-927)
  on line 938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:938-938)
  on line 981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:981-981)
  on line 1024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1024-1024)
  on line 1067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1067-1067)
  on line 1145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1145-1145)
  on line 1155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1155-1155)
  on line 1173 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1173-1173)
  on line 1211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1211-1211)
  on line 1246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1246-1246)
  on line 1281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1281-1281)
  on line 1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1316-1316)
  on line 1359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1359-1359)
  on line 1369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1369-1369)
  on line 1387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1387-1387)
  on line 1398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1398-1398)
  on line 1441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1441-1441)
  on line 1484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1484-1484)
  on line 1527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1527-1527)
  on line 1605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1605-1605)
  on line 1615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1615-1615)
  on line 1633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1633-1633)
  on line 1821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1821-1821)
  on line 1832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1832-1832)
  on line 1850 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1850-1850)
  on line 2232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2232-2232)
  on line 2249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2249-2249)
  on line 2266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2266-2266)
  on line 2371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2371-2371)
  on line 2388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2388-2388)
  on line 2405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2405-2405)
  on line 2510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2510-2510)
  on line 2527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2527-2527)
  on line 2544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2544-2544)
  on line 2649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2649-2649)
  on line 2666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2666-2666)
  on line 2683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2683-2683)
  on line 2728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2728-2728)
  on line 2734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2734-2734)
  on line 2748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2748-2748)
  on line 2786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2786-2786)
  on line 2821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2821-2821)
  on line 2833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2833-2833)
  on line 2868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2868-2868)
  on line 2880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2880-2880)
  on line 2915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2915-2915)
  on line 2927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2927-2927)
  on line 2962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2962-2962)
  on line 2968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2968-2968)
  on line 2975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2975-2975)
  on line 2980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2980-2980)
  on line 2986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2986-2986)
  on line 2991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2991-2991)
  on line 2997 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2997-2997)
  on line 3002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3002-3002)
  on line 3007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3007-3007)
  on line 3012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3012-3012)
  on line 3017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3017-3017)
  on line 3024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3024-3024)
  on line 3041 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3041-3041)
  on line 3058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3058-3058)
  on line 3074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3074-3074)
  on line 3082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3082-3082)
  on line 3099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3099-3099)
  on line 3116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3116-3116)
  on line 3132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3132-3132)
  on line 3140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3140-3140)
  on line 3157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3157-3157)
  on line 3174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3174-3174)
  on line 3190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3190-3190)
  on line 3198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3198-3198)
  on line 3215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3215-3215)
  on line 3232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3232-3232)
  on line 3248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3248-3248)
  on line 3255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3255-3255)
  on line 3262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3262-3262)
  on line 3267 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3267-3267)
  on line 3273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3273-3273)
  on line 3278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3278-3278)
  on line 3284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3284-3284)
  on line 3289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3289-3289)
  on line 3294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3294-3294)
  on line 3299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3299-3299)
  on line 3304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3304-3304)
  on line 3341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3341-3341)
  on line 3378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3378-3378)
  on line 3415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3415-3415)
  on line 3452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3452-3452)
  on line 3458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3458-3458)
  on line 3465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3465-3465)
  on line 3470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3470-3470)
  on line 3476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3476-3476)
  on line 3481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3481-3481)
  on line 3487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3487-3487)
  on line 3492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3492-3492)
  on line 3497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3497-3497)
  on line 3502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3502-3502)
  on line 3507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3507-3507)
  on line 3514 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3514-3514)
  on line 3531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3531-3531)
  on line 3548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3548-3548)
  on line 3564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3564-3564)
  on line 3572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3572-3572)
  on line 3589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3589-3589)
  on line 3606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3606-3606)
  on line 3622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3622-3622)
  on line 3630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3630-3630)
  on line 3647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3647-3647)
  on line 3664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3664-3664)
  on line 3680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3680-3680)
  on line 3688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3688-3688)
  on line 3705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3705-3705)
  on line 3722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3722-3722)
  on line 3738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3738-3738)
  on line 3745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3745-3745)
  on line 3752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3752-3752)
  on line 3757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3757-3757)
  on line 3763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3763-3763)
  on line 3768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3768-3768)
  on line 3774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3774-3774)
  on line 3779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3779-3779)
  on line 3784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3784-3784)
  on line 3789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3789-3789)
  on line 3794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3794-3794)
  on line 3831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3831-3831)
  on line 3868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3868-3868)
  on line 3905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3905-3905)
  on line 3942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3942-3942)
  on line 3948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3948-3948)
  on line 3955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3955-3955)
  on line 3960 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3960-3960)
  on line 3966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3966-3966)
  on line 3971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3971-3971)
  on line 3977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3977-3977)
  on line 3982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3982-3982)
  on line 3987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3987-3987)
  on line 3992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3992-3992)
  on line 3997 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3997-3997)
  on line 4004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4004-4004)
  on line 4021 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4021-4021)
  on line 4038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4038-4038)
  on line 4054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4054-4054)
  on line 4062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4062-4062)
  on line 4079 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4079-4079)
  on line 4096 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4096-4096)
  on line 4112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4112-4112)
  on line 4120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4120-4120)
  on line 4137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4137-4137)
  on line 4154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4154-4154)
  on line 4170 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4170-4170)
  on line 4178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4178-4178)
  on line 4195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4195-4195)
  on line 4212 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4212-4212)
  on line 4228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4228-4228)
  on line 4235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4235-4235)
  on line 4240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4240-4240)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 1374
  dead: 171 (2 in uncalled functions)
  total lines: 1545
[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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1133:10-1133: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1135:8-1135: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1137:8-1137: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1139:8-1139: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1141:8-1141: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1143:7-1143: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1149:10-1149: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1817:7-1817: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1151:7-1151: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1819:7-1819: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1153:7-1153: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1159:10-1159: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1827:7-1827: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1161:7-1161: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:446:6-446: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1830:7-1830: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1171:6-1171: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1179:6-1179: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1182:6-1182: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:473:6-473: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:476:6-476: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:482:7-482: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:487:6-487: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:489:6-489: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1209:7-1209: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:498:6-498: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:500:6-500: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1217:6-1217: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:509:6-509: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:511:6-511: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:519:6-519: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:525:7-525: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:530:6-530: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:532:6-532: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:541:6-541: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:543:6-543: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1244:7-1244: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1252:6-1252: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:552:6-552: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:554:6-554: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:562:6-562: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:568:7-568: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:573:6-573: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:575:6-575: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:584:6-584: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:586:6-586: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1279:7-1279: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:595:6-595: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1287:6-1287: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:597:6-597: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:605:6-605: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:611:7-611: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:616:6-616: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:618:6-618: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:627:6-627: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:629:6-629: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1314:7-1314: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:638:6-638: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:640:6-640: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1347:10-1347: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1349:8-1349: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1351:8-1351: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1353:8-1353: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1355:8-1355: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:673:10-673: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1357:7-1357: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:675:8-675: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:677:8-677: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1363:10-1363: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:679:8-679: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1365:7-1365: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:681:8-681: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1367:7-1367: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:683:7-683: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1373:10-1373: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:689:10-689: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1375:7-1375: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:691:7-691: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:693:7-693: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:699:10-699: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:701:7-701: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1385:6-1385: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:711:6-711: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1393:6-1393: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1396:6-1396: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1402:7-1402: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:719:6-719: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1407:6-1407: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:722:6-722: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1409:6-1409: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1418:6-1418: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1420:6-1420: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1429:6-1429: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1431:6-1431: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1439:6-1439: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1445:7-1445: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:749:7-749: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1450:6-1450: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1452:6-1452: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:757:6-757: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1461:6-1461: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1463:6-1463: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1472:6-1472: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1474:6-1474: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1482:6-1482: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1488:7-1488: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1493:6-1493: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1495:6-1495: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:784:7-784: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:792:6-792: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1504:6-1504: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1506:6-1506: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2196:6-2196: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2198:6-2198: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1515:6-1515: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1517:6-1517: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2207:6-2207: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2209:6-2209: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1525:6-1525: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1531:7-1531: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1536:6-1536: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1538:6-1538: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2218:6-2218: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2220:6-2220: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:819:7-819: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1547:6-1547: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1549:6-1549: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:827:6-827: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1558:6-1558: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1560:6-1560: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:854:7-854: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2335:6-2335: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2337:6-2337: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2346:6-2346: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2348:6-2348: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1593:10-1593: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1595:8-1595: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1597:8-1597: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1599:8-1599: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1601:8-1601: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1603:7-1603: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2357:6-2357: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1609:10-1609: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2359:6-2359: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1611:7-1611: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1613:7-1613: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1619:10-1619: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1621:7-1621: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:887:10-887: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:889:8-889: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1631:6-1631:22)
[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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:891:8-891: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:893:8-893: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:895:8-895: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:897:7-897:20)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1639:6-1639:18)
[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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:903:10-903:66)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1642:6-1642: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:905:7-905: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:907:7-907: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:913:10-913: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:915:7-915: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:925:6-925: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:933:6-933: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:936:6-936: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2474:6-2474: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:942:7-942: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2476:6-2476: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:947:6-947: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:949:6-949: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2485:6-2485: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1669:7-1669: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2487:6-2487: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:958:6-958: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:960:6-960: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1677:6-1677: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2496:6-2496: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2498:6-2498: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:969:6-969: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:971:6-971: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:979:6-979: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:985:7-985: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:990:6-990: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:992:6-992: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1001:6-1001: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1003:6-1003: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1704:7-1704: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1012:6-1012: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1712:6-1712: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1014:6-1014: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2613:6-2613: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2615:6-2615: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1022:6-1022: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1028:7-1028: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1033:6-1033: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1035:6-1035: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2624:6-2624: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2626:6-2626: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1044:6-1044: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1046:6-1046: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2635:6-2635: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2637:6-2637: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1739:7-1739: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1055:6-1055: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1057:6-1057: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1747:6-1747: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1065:6-1065: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1071:7-1071: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1076:6-1076: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1078:6-1078: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1087:6-1087: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1089:6-1089: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1098:6-1098: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1100:6-1100: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.3.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1774:7-1774:20)
[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)
