./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2544:2-2544:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2580:2-2580:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2616:2-2616:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2652:2-2652: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:493-493)
  on line 536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:536-536)
  on line 579 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:579-579)
  on line 622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:622-622)
  on line 700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:700-700)
  on line 710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:710-710)
  on line 728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:728-728)
  on line 766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:766-766)
  on line 801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:801-801)
  on line 836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:836-836)
  on line 871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:871-871)
  on line 914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:914-914)
  on line 924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:924-924)
  on line 942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:942-942)
  on line 953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:953-953)
  on line 996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:996-996)
  on line 1039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1039-1039)
  on line 1082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1082-1082)
  on line 1160 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1160-1160)
  on line 1170 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1170-1170)
  on line 1188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1188-1188)
  on line 1226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1226-1226)
  on line 1261 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1261-1261)
  on line 1296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1296-1296)
  on line 1331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1331-1331)
  on line 1374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1374-1374)
  on line 1384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1384-1384)
  on line 1402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1402-1402)
  on line 1413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1413-1413)
  on line 1419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1419-1419)
  on line 1427 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1427-1427)
  on line 1470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1470-1470)
  on line 1513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1513-1513)
  on line 1591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1591-1591)
  on line 1601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1601-1601)
  on line 1619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1619-1619)
  on line 1671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1671-1671)
  on line 1705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1705-1705)
  on line 1739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1739-1739)
  on line 1791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1791-1791)
  on line 1806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1806-1806)
  on line 1810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1810-1810)
  on line 1848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1848-1848)
  on line 1863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1863-1863)
  on line 1867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1867-1867)
  on line 1876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1876-1876)
  on line 1911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1911-1911)
  on line 1929 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1929-1929)
  on line 1981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1981-1981)
  on line 1996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1996-1996)
  on line 2000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2000-2000)
  on line 2038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2038-2038)
  on line 2053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2053-2053)
  on line 2057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2057-2057)
  on line 2066 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2066-2066)
  on line 2101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2101-2101)
  on line 2108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2108-2108)
  on line 2143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2143-2143)
  on line 2161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2161-2161)
  on line 2195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2195-2195)
  on line 2247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2247-2247)
  on line 2262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2262-2262)
  on line 2266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2266-2266)
  on line 2304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2304-2304)
  on line 2319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2319-2319)
  on line 2323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2323-2323)
  on line 2332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2332-2332)
  on line 2367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2367-2367)
  on line 2385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2385-2385)
  on line 2437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2437-2437)
  on line 2452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2452-2452)
  on line 2456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2456-2456)
  on line 2506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2506-2506)
  on line 2517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2517-2517)
  on line 2533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2533-2533)
  on line 2915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2915-2915)
  on line 2932 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2932-2932)
  on line 2949 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2949-2949)
  on line 3054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3054-3054)
  on line 3071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3071-3071)
  on line 3088 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3088-3088)
  on line 3193 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3193-3193)
  on line 3210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3210-3210)
  on line 3227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3227-3227)
  on line 3332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3332-3332)
  on line 3349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3349-3349)
  on line 3366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3366-3366)
  on line 3404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3404-3404)
  on line 3411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3411-3411)
  on line 3417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3417-3417)
  on line 3424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3424-3424)
  on line 3430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3430-3430)
  on line 3435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3435-3435)
  on line 3440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3440-3440)
  on line 3445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3445-3445)
  on line 3450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3450-3450)
  on line 3455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3455-3455)
  on line 3462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3462-3462)
  on line 3497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3497-3497)
  on line 3504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3504-3504)
  on line 3539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3539-3539)
  on line 3546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3546-3546)
  on line 3581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3581-3581)
  on line 3599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3599-3599)
  on line 3633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3633-3633)
  on line 3667 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3667-3667)
  on line 3719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3719-3719)
  on line 3734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3734-3734)
  on line 3738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3738-3738)
  on line 3776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3776-3776)
  on line 3791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3791-3791)
  on line 3795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3795-3795)
  on line 3804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3804-3804)
  on line 3839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3839-3839)
  on line 3857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3857-3857)
  on line 3909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3909-3909)
  on line 3924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3924-3924)
  on line 3928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3928-3928)
  on line 3978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3978-3978)
  on line 3989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3989-3989)
  on line 4006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4006-4006)
  on line 4013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4013-4013)
  on line 4019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4019-4019)
  on line 4026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4026-4026)
  on line 4032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4032-4032)
  on line 4037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4037-4037)
  on line 4042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4042-4042)
  on line 4047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4047-4047)
  on line 4052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4052-4052)
  on line 4057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4057-4057)
  on line 4064 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4064-4064)
  on line 4099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4099-4099)
  on line 4106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4106-4106)
  on line 4141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4141-4141)
  on line 4159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4159-4159)
  on line 4193 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4193-4193)
  on line 4245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4245-4245)
  on line 4260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4260-4260)
  on line 4264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4264-4264)
  on line 4314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4314-4314)
  on line 4325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4325-4325)
  on line 4342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4342-4342)
  on line 4349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4349-4349)
  on line 4355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4355-4355)
  on line 4362 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4362-4362)
  on line 4368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4368-4368)
  on line 4373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4373-4373)
  on line 4378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4378-4378)
  on line 4383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4383-4383)
  on line 4388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4388-4388)
  on line 4393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4393-4393)
  on line 4400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4400-4400)
  on line 4435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4435-4435)
  on line 4453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4453-4453)
  on line 4517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4517-4517)
  on line 4528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4528-4528)
  on line 4545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4545-4545)
  on line 4552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4552-4552)
  on line 4558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4558-4558)
  on line 4565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4565-4565)
  on line 4571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4571-4571)
  on line 4576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4576-4576)
  on line 4581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4581-4581)
  on line 4586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4586-4586)
  on line 4591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4591-4591)
  on line 4596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4596-4596)
  on line 4644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4644-4644)
  on line 4650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4650-4650)
  on line 4664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4664-4664)
  on line 4669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4669-4669)
  on line 4674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4674-4674)
  on line 4679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4679-4679)
  on line 4684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4684-4684)
  on line 4689 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4689-4689)
  on line 4696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4696-4696)
  on line 4731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4731-4731)
  on line 4738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4738-4738)
  on line 4773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4773-4773)
  on line 4780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4780-4780)
  on line 4815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4815-4815)
  on line 4822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4822-4822)
  on line 4857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4857-4857)
  on line 4863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4863-4863)
  on line 4870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4870-4870)
  on line 4875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4875-4875)
  on line 4881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4881-4881)
  on line 4886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4886-4886)
  on line 4892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4892-4892)
  on line 4897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4897-4897)
  on line 4902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4902-4902)
  on line 4907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4907-4907)
  on line 4912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4912-4912)
  on line 4919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4919-4919)
  on line 4936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4936-4936)
  on line 4953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4953-4953)
  on line 4969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4969-4969)
  on line 4977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4977-4977)
  on line 4994 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4994-4994)
  on line 5011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5011-5011)
  on line 5027 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5027-5027)
  on line 5035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5035-5035)
  on line 5052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5052-5052)
  on line 5069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5069-5069)
  on line 5085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5085-5085)
  on line 5095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5095-5095)
  on line 5102 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5102-5102)
  on line 5107 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5107-5107)
  on line 5113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5113-5113)
  on line 5118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5118-5118)
  on line 5124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5124-5124)
  on line 5129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5129-5129)
  on line 5134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5134-5134)
  on line 5139 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5139-5139)
  on line 5144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5144-5144)
  on line 5181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5181-5181)
  on line 5218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5218-5218)
  on line 5255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5255-5255)
  on line 5292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5292-5292)
  on line 5298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5298-5298)
  on line 5305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5305-5305)
  on line 5310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5310-5310)
  on line 5316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5316-5316)
  on line 5321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5321-5321)
  on line 5327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5327-5327)
  on line 5332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5332-5332)
  on line 5337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5337-5337)
  on line 5342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5342-5342)
  on line 5347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5347-5347)
  on line 5354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5354-5354)
  on line 5371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5371-5371)
  on line 5388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5388-5388)
  on line 5404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5404-5404)
  on line 5412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5412-5412)
  on line 5429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5429-5429)
  on line 5446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5446-5446)
  on line 5462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5462-5462)
  on line 5470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5470-5470)
  on line 5487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5487-5487)
  on line 5504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5504-5504)
  on line 5520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5520-5520)
  on line 5528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5528-5528)
  on line 5545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5545-5545)
  on line 5562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5562-5562)
  on line 5578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5578-5578)
  on line 5585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5585-5585)
  on line 5592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5592-5592)
  on line 5597 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5597-5597)
  on line 5603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5603-5603)
  on line 5608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5608-5608)
  on line 5614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5614-5614)
  on line 5619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5619-5619)
  on line 5624 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5624-5624)
  on line 5629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5629-5629)
  on line 5634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5634-5634)
  on line 5671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5671-5671)
  on line 5708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5708-5708)
  on line 5745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5745-5745)
  on line 5782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5782-5782)
  on line 5788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5788-5788)
  on line 5795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5795-5795)
  on line 5800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5800-5800)
  on line 5806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5806-5806)
  on line 5811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5811-5811)
  on line 5817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5817-5817)
  on line 5822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5822-5822)
  on line 5827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5827-5827)
  on line 5832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5832-5832)
  on line 5837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5837-5837)
  on line 5844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5844-5844)
  on line 5861 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5861-5861)
  on line 5878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5878-5878)
  on line 5894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5894-5894)
  on line 5902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5902-5902)
  on line 5919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5919-5919)
  on line 5936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5936-5936)
  on line 5952 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5952-5952)
  on line 5960 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5960-5960)
  on line 5977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5977-5977)
  on line 5994 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:5994-5994)
  on line 6010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:6010-6010)
  on line 6018 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:6018-6018)
  on line 6035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:6035-6035)
  on line 6052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:6052-6052)
  on line 6068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:6068-6068)
  on line 6075 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:6075-6075)
  on line 6080 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:6080-6080)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 2100
  dead: 288 (2 in uncalled functions)
  total lines: 2388
[Warning][Deadcode][CWE-571] condition '(int )r4 == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3685:7-3685: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1148:10-1148: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1150:8-1150: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1152:8-1152: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1154:8-1154: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1156:8-1156: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1158:7-1158: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1164:10-1164: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1166:7-1166: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1168:7-1168: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1174:10-1174: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1176:7-1176: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:461:6-461:19)
[Warning][Deadcode][CWE-570] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1846:10-1846:66)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1186:6-1186: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1194:6-1194:18)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___5 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1860:6-1860:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1197:6-1197:19)
[Warning][Deadcode][CWE-570] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3717:10-3717:66)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4630:10-4630: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4632:8-4632:36)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3731:6-3731: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4634:8-4634: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4636:8-4636: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4638:8-4638: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4640:7-4640: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:488:6-488:18)
[Warning][Deadcode][CWE-571] condition '! ((int )mode4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1920:6-1920: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4642:7-4642:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:491:6-491:19)
[Warning][Deadcode][CWE-570] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4648:10-4648:66)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:497:7-497: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:502:6-502: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:504:6-504:22)
[Warning][Deadcode][CWE-570] condition '(int )m4 > (int )max4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1927:7-1927:29)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1224:7-1224: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:513:6-513: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:515:6-515: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1232:6-1232: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:524:6-524: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:526:6-526: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1947:7-1947:20)
[Warning][Deadcode][CWE-570] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3774:10-3774:66)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:534:6-534: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:540:7-540: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:545:6-545: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:547:6-547:22)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___13 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3788:6-3788: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:556:6-556: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:558:6-558: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1259:7-1259: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1267:6-1267: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:567:6-567: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:569:6-569: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3848:6-3848:19)
[Warning][Deadcode][CWE-570] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1979:10-1979:66)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:577:6-577: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:583:7-583:19)
[Warning][Deadcode][CWE-570] condition '(int )m4 > (int )max4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3855:7-3855:29)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:588:6-588: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:590:6-590:22)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___6 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1993:6-1993: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:599:6-599: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:601:6-601: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1294:7-1294: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:610:6-610: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1302:6-1302: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:612:6-612: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3875:7-3875:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode4 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:620:6-620: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:626:7-626: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:631:6-631: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:633:6-633:22)
[Warning][Deadcode][CWE-570] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2036:10-2036:66)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:642:6-642: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:644:6-644:22)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___7 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2050:6-2050: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1329:7-1329: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:653:6-653: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:655:6-655:22)
[Warning][Deadcode][CWE-570] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3907:10-3907:66)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___14 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3921:6-3921:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2152:6-2152: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2879:6-2879: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2881:6-2881: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1362:10-1362: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1364:8-1364: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1366:8-1366:36)
[Warning][Deadcode][CWE-570] condition '(int )m3 > (int )max3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2159:7-2159:29)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1368:8-1368: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1370:8-1370: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:688:10-688: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1372:7-1372: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:690:8-690: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:692:8-692:36)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2890:6-2890: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1378:10-1378: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:694:8-694:36)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2892:6-2892: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1380:7-1380: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:696:8-696: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1382:7-1382: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:698:7-698: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1388:10-1388: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:704:10-704: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1390:7-1390: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:706:7-706: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:708:7-708: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2901:6-2901:19)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:714:10-714:66)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3964:10-3964:66)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2903:6-2903: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:716:7-716:19)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3966:8-3966: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3968:8-3968: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3970:8-3970:36)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1400:6-1400:22)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3972:8-3972: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3974:7-3974: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3976:7-3976: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2179:7-2179:20)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:726:6-726: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3982:10-3982: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1408:6-1408: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3984:7-3984:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1411:6-1411: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3987:7-3987:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1417:7-1417: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2186:6-2186: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:734:6-734: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:737:6-737:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1425:6-1425: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1431:7-1431:19)
[Warning][Deadcode][CWE-570] condition '(int )m4 > (int )max4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2193:7-2193:29)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1436:6-1436:19)
[Warning][Deadcode][CWE-571] condition '(((int )nl1 + (int )nl2) + (int )nl3) + (int )nl4 == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3999:10-3999:66)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1438:6-1438: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1447:6-1447: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1449:6-1449: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1458:6-1458: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3018:6-3018: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1460:6-1460:22)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3020:6-3020: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2213:7-2213: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:764:7-764:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1468:6-1468: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3029:6-3029:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:772:6-772: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3031:6-3031: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1474:7-1474: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1479:6-1479: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1481:6-1481: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3040:6-3040: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3042:6-3042: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1490:6-1490: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1492:6-1492:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4150:6-4150: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1501:6-1501: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1503:6-1503:22)
[Warning][Deadcode][CWE-570] condition '(int )m3 > (int )max3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4157:7-4157:29)
[Warning][Deadcode][CWE-570] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2245:10-2245:66)
[Warning][Deadcode][CWE-570] condition '! ((int )mode4 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1511:6-1511:19)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:799:7-799:20)
[Warning][Deadcode][CWE-571] condition '(int )r4 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1517:7-1517: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1522:6-1522: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:807:6-807:19)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___8 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2259:6-2259:22)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1524:6-1524: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1533:6-1533: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1535:6-1535: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4177:7-4177: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3157:6-3157: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4184:6-4184: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3159:6-3159: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1544:6-1544: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1546:6-1546:22)
[Warning][Deadcode][CWE-570] condition '(int )m4 > (int )max4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4191:7-4191:29)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3168:6-3168: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3170:6-3170: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:834:7-834: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3179:6-3179: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3181:6-3181: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:842:6-842:19)
[Warning][Deadcode][CWE-570] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2302:10-2302:66)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___9 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2316:6-2316: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4211:7-4211: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1579:10-1579: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1581:8-1581: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1583:8-1583: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1585:8-1585: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1587:8-1587: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1589:7-1589: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.4.ufo.BOUNDED-8.pals.c.v+lhb-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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1597:7-1597: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2376:6-2376: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1599:7-1599:20)
[Warning][Deadcode][CWE-570] condition '(int )r4 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:869:7-869: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1605:10-1605: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1607:7-1607:19)
[Warning][Deadcode][CWE-570] condition '(int )m4 > (int )max4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2383:7-2383:29)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3296:6-3296:19)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1617:6-1617:22)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3298:6-3298:22)
[Warning][Deadcode][CWE-570] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4243:10-4243: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1625:6-1625: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1628:6-1628: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3307:6-3307: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3309:6-3309:22)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___15 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4257:6-4257: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3318:6-3318: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3320:6-3320: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2403:7-2403: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:902:10-902: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:904:8-904: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:906:8-906: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:908:8-908: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:910:8-910: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:912:7-912: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:918:10-918: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:920:7-920: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:922:7-922: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:928:10-928: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:930:7-930: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1655:7-1655:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1662:6-1662: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:940:6-940:22)
[Warning][Deadcode][CWE-571] condition '(((int )nl1 + (int )nl2) + (int )nl3) + (int )nl4 == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3397:10-3397: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:948:6-948:18)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4300:10-4300:66)
[Warning][Deadcode][CWE-570] condition '(int )m2 > (int )max2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1669:7-1669:29)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:951:6-951:19)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4302:8-4302:36)
[Warning][Deadcode][CWE-570] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2435:10-2435:66)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4304:8-4304:36)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:957:7-957:19)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4306:8-4306: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4308:8-4308:36)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:962:6-962: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4310:7-4310:20)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:964:6-964: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4312:7-4312: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4318:10-4318: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4320:7-4320:20)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___10 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2449:6-2449: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4323:7-4323: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:973:6-973: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:975:6-975:22)
[Warning][Deadcode][CWE-571] condition '(((int )nl1 + (int )nl2) + (int )nl3) + (int )nl4 == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4335:10-4335:66)
[Warning][Deadcode][CWE-571] condition '(int )r2 == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1689:7-1689: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:984:6-984: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:986:6-986:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1696:6-1696:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:994:6-994: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1000:7-1000:19)
[Warning][Deadcode][CWE-570] condition '(int )m3 > (int )max3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1703:7-1703:29)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1005:6-1005: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1007:6-1007: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1016:6-1016: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2492:10-2492:66)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1018:6-1018:22)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2494:8-2494: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2496:8-2496: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2498:8-2498:36)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3590:6-3590: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2500:8-2500: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2502:7-2502: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2504:7-2504: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1027:6-1027: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2510:10-2510:66)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1029:6-1029: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4444:6-4444: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2512:7-2512:20)
[Warning][Deadcode][CWE-570] condition '(int )m2 > (int )max2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3597:7-3597:29)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2515:7-2515: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1723:7-1723:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1037:6-1037:19)
[Warning][Deadcode][CWE-570] condition '(int )m4 > (int )max4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4451:7-4451:29)
[Warning][Deadcode][CWE-571] condition '! ((int )mode4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1730:6-1730: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1043:7-1043: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1048:6-1048: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1050:6-1050:22)
[Warning][Deadcode][CWE-570] condition '(int )m4 > (int )max4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1737:7-1737:29)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1059:6-1059: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1061:6-1061: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3617:7-3617: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1070:6-1070: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4471:7-4471: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3624:6-3624: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1072:6-1072:22)
[Warning][Deadcode][CWE-570] condition '(int )m3 > (int )max3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3631:7-3631:29)
[Warning][Deadcode][CWE-571] condition '(int )r4 == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1757:7-1757:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode4 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1080:6-1080: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1086:7-1086: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1091:6-1091: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1093:6-1093: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1102:6-1102: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1104:6-1104: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3651:7-3651: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1113:6-1113: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1115:6-1115: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4503:10-4503: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4505:8-4505: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4507:8-4507: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4509:8-4509:36)
[Warning][Deadcode][CWE-571] condition '! ((int )mode4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3658:6-3658: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4511:8-4511: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4513:7-4513: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4515:7-4515:19)
[Warning][Deadcode][CWE-570] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1789:10-1789:66)
[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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4521:10-4521: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.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4523:7-4523:20)
[Warning][Deadcode][CWE-570] condition '(int )m4 > (int )max4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3665:7-3665:29)
[Warning][Deadcode][CWE-570] condition '(int )r1 < 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4526:7-4526:19)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1803:6-1803:22)
[Warning][Deadcode][CWE-571] condition '(((int )nl1 + (int )nl2) + (int )nl3) + (int )nl4 == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.4.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:4538:10-4538:66)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
