./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pals_opt-floodmax.4.2.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_opt-floodmax.4.2.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] couldn't parse entry: find uuid
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:495-495)
  on line 546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:546-546)
  on line 597 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:597-597)
  on line 648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:648-648)
  on line 732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:732-732)
  on line 742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:742-742)
  on line 760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:760-760)
  on line 804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:804-804)
  on line 845 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:845-845)
  on line 886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:886-886)
  on line 927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:927-927)
  on line 970 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:970-970)
  on line 980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:980-980)
  on line 998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:998-998)
  on line 1011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1011-1011)
  on line 1062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1062-1062)
  on line 1113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1113-1113)
  on line 1164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1164-1164)
  on line 1248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1248-1248)
  on line 1258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1258-1258)
  on line 1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1276-1276)
  on line 1360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1360-1360)
  on line 1401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1401-1401)
  on line 1442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1442-1442)
  on line 1485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1485-1485)
  on line 1491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1491-1491)
  on line 1506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1506-1506)
  on line 1510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1510-1510)
  on line 1518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1518-1518)
  on line 1523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1523-1523)
  on line 1528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1528-1528)
  on line 1533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1533-1533)
  on line 1538 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1538-1538)
  on line 1575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1575-1575)
  on line 1612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1612-1612)
  on line 1649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1649-1649)
  on line 1693 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1693-1693)
  on line 1734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1734-1734)
  on line 1775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1775-1775)
  on line 1818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1818-1818)
  on line 1828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1828-1828)
  on line 1834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1834-1834)
  on line 1852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1852-1852)
  on lines 1856..1858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1856-1858)
  on lines 1862..1863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1862-1863)
  on lines 1865..1866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1865-1866)
  on lines 1868..1870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1868-1870)
  on lines 1872..1873 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1872-1873)
  on line 1875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1875-1875)
  on lines 1877..1879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1877-1879)
  on lines 1881..1882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1881-1882)
  on line 1884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1884-1884)
  on lines 1886..1888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1886-1888)
  on lines 1890..1891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1890-1891)
  on lines 1893..1894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1893-1894)
  on line 1896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1896-1896)
  on line 1898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1898-1898)
  on line 1900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1900-1900)
  on lines 1904..1905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1904-1905)
  on lines 1907..1908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1907-1908)
  on lines 1910..1912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1910-1912)
  on lines 1914..1915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1914-1915)
  on line 1917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1917-1917)
  on lines 1919..1921 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1919-1921)
  on lines 1923..1924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1923-1924)
  on line 1926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1926-1926)
  on lines 1928..1930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1928-1930)
  on lines 1932..1933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1932-1933)
  on lines 1935..1936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1935-1936)
  on line 1938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1938-1938)
  on line 1940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1940-1940)
  on line 1942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1942-1942)
  on lines 1946..1947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1946-1947)
  on lines 1949..1950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1949-1950)
  on lines 1952..1954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1952-1954)
  on lines 1956..1957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1956-1957)
  on line 1959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1959-1959)
  on lines 1961..1963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1961-1963)
  on lines 1965..1966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1965-1966)
  on line 1968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1968-1968)
  on lines 1970..1972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1970-1972)
  on lines 1974..1975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1974-1975)
  on lines 1977..1978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1977-1978)
  on line 1980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1980-1980)
  on line 1982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1982-1982)
  on line 1984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1984-1984)
  on lines 1988..1989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1988-1989)
  on lines 1991..1992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1991-1992)
  on lines 1994..1996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1994-1996)
  on lines 1998..1999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1998-1999)
  on line 2001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2001-2001)
  on lines 2003..2005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2003-2005)
  on lines 2007..2008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2007-2008)
  on line 2010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2010-2010)
  on lines 2012..2014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2012-2014)
  on lines 2016..2017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2016-2017)
  on lines 2019..2020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2019-2020)
  on line 2022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2022-2022)
  on line 2024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2024-2024)
  on line 2026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2026-2026)
  on lines 2028..2051 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2028-2051)
  on line 2054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2054-2054)
  on line 2056 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2056-2056)
  on line 2058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2058-2058)
  on line 2060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2060-2060)
  on line 2062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2062-2062)
  on line 2064 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2064-2064)
  on line 2067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2067-2067)
  on line 2070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2070-2070)
  on line 2073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2073-2073)
  on line 2075 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2075-2075)
  on lines 2085..2087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2085-2087)
  on line 2092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2092-2092)
  on line 2094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2094-2094)
  on line 2099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2099-2099)
  on line 2106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2106-2106)
  on line 2112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2112-2112)
  on line 2119 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2119-2119)
  on line 2125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2125-2125)
  on line 2132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2132-2132)
  on line 2138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2138-2138)
  on line 2145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2145-2145)
  on line 2151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2151-2151)
  on line 2157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2157-2157)
  on line 2163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2163-2163)
  on line 2169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2169-2169)
  on line 2176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2176-2176)
  on line 2217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2217-2217)
  on line 2219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2219-2219)
  on line 2221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2221-2221)
  on line 2224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2224-2224)
  on line 2226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2226-2226)
  on line 2228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2228-2228)
  on line 2230 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2230-2230)
  on line 2232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2232-2232)
  on line 2234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2234-2234)
  on line 2237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2237-2237)
  on line 2239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2239-2239)
  on line 2241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2241-2241)
  on line 2243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2243-2243)
  on line 2245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2245-2245)
  on line 2247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2247-2247)
  on line 2250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2250-2250)
  on line 2252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2252-2252)
  on line 2254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2254-2254)
  on line 2256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2256-2256)
  on line 2258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2258-2258)
  on line 2264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2264-2264)
  on line 2286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2286-2286)
  on line 2308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2308-2308)
  on line 2336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2336-2336)
  on line 2377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2377-2377)
  on line 2379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2379-2379)
  on line 2381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2381-2381)
  on line 2384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2384-2384)
  on line 2386 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2386-2386)
  on line 2388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2388-2388)
  on line 2390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2390-2390)
  on line 2392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2392-2392)
  on line 2394 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2394-2394)
  on line 2397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2397-2397)
  on line 2399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2399-2399)
  on line 2401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2401-2401)
  on line 2403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2403-2403)
  on line 2405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2405-2405)
  on line 2407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2407-2407)
  on line 2410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2410-2410)
  on line 2412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2412-2412)
  on line 2414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2414-2414)
  on line 2416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2416-2416)
  on line 2418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2418-2418)
  on line 2424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2424-2424)
  on line 2446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2446-2446)
  on line 2468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2468-2468)
  on line 2496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2496-2496)
  on line 2537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2537-2537)
  on line 2539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2539-2539)
  on line 2541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2541-2541)
  on line 2544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2544-2544)
  on line 2546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2546-2546)
  on line 2548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2548-2548)
  on line 2550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2550-2550)
  on line 2552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2552-2552)
  on line 2554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2554-2554)
  on line 2557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2557-2557)
  on line 2559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2559-2559)
  on line 2561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2561-2561)
  on line 2563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2563-2563)
  on line 2565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2565-2565)
  on line 2567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2567-2567)
  on line 2570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2570-2570)
  on line 2572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2572-2572)
  on line 2574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2574-2574)
  on line 2576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2576-2576)
  on line 2578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2578-2578)
  on line 2584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2584-2584)
  on line 2606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2606-2606)
  on line 2628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2628-2628)
  on line 2656 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2656-2656)
  on line 2697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2697-2697)
  on line 2699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2699-2699)
  on line 2701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2701-2701)
  on line 2704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2704-2704)
  on line 2706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2706-2706)
  on line 2708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2708-2708)
  on line 2710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2710-2710)
  on line 2712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2712-2712)
  on line 2714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2714-2714)
  on line 2717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2717-2717)
  on line 2719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2719-2719)
  on line 2721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2721-2721)
  on line 2723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2723-2723)
  on line 2725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2725-2725)
  on line 2727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2727-2727)
  on line 2730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2730-2730)
  on line 2732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2732-2732)
  on line 2734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2734-2734)
  on line 2736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2736-2736)
  on line 2738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2738-2738)
  on line 2744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2744-2744)
  on line 2766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2766-2766)
  on line 2788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2788-2788)
  on lines 2816..2817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2816-2817)
  on line 2826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2826-2826)
  on line 2831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2831-2831)
  on line 2837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2837-2837)
  on line 2842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2842-2842)
  on line 2847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2847-2847)
  on line 2852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2852-2852)
  on line 2857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2857-2857)
  on line 2894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2894-2894)
  on line 2931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2931-2931)
  on line 2968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2968-2968)
  on line 2975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:2975-2975)
  on line 3010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3010-3010)
  on line 3016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3016-3016)
  on line 3023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3023-3023)
  on line 3028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3028-3028)
  on line 3034 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3034-3034)
  on line 3039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3039-3039)
  on line 3045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3045-3045)
  on line 3050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3050-3050)
  on line 3055 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3055-3055)
  on line 3060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3060-3060)
  on line 3065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3065-3065)
  on line 3072 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3072-3072)
  on line 3094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3094-3094)
  on line 3116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3116-3116)
  on line 3137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3137-3137)
  on line 3145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3145-3145)
  on line 3167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3167-3167)
  on line 3189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3189-3189)
  on line 3210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3210-3210)
  on line 3218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3218-3218)
  on line 3240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3240-3240)
  on line 3262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3262-3262)
  on line 3283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3283-3283)
  on line 3291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3291-3291)
  on line 3313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3313-3313)
  on line 3335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3335-3335)
  on line 3356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3356-3356)
  on line 3363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3363-3363)
  on line 3370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3370-3370)
  on line 3375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3375-3375)
  on line 3381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3381-3381)
  on line 3386 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3386-3386)
  on line 3392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3392-3392)
  on line 3397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3397-3397)
  on line 3402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3402-3402)
  on line 3407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3407-3407)
  on line 3412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3412-3412)
  on line 3449 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3449-3449)
  on line 3486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3486-3486)
  on line 3523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3523-3523)
  on line 3560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3560-3560)
  on line 3566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3566-3566)
  on line 3573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3573-3573)
  on line 3578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3578-3578)
  on line 3584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3584-3584)
  on line 3589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3589-3589)
  on line 3595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3595-3595)
  on line 3600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3600-3600)
  on line 3605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3605-3605)
  on line 3610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3610-3610)
  on line 3615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3615-3615)
  on line 3622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3622-3622)
  on line 3644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3644-3644)
  on line 3666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3666-3666)
  on line 3687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3687-3687)
  on line 3695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3695-3695)
  on line 3717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3717-3717)
  on line 3739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3739-3739)
  on line 3760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3760-3760)
  on line 3768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3768-3768)
  on line 3790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3790-3790)
  on line 3812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3812-3812)
  on line 3833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3833-3833)
  on line 3841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3841-3841)
  on line 3863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3863-3863)
  on line 3885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3885-3885)
  on line 3906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3906-3906)
  on line 3913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3913-3913)
  on line 3918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:3918-3918)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 1104
  dead: 381 (2 in uncalled functions)
  total lines: 1485
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1137:6-1137: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1139:6-1139:22)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1150:6-1150: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1152:6-1152: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1473:10-1473: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1475:8-1475: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1477:8-1477:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:802:7-802:20)
[Warning][Deadcode][CWE-571] condition '(int )st3 + (int )nl3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1479:8-1479: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1481:8-1481:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1483:7-1483:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode4 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1162:6-1162:19)
[Warning][Deadcode][CWE-570] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1489:10-1489:66)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:812:6-812:19)
[Warning][Deadcode][CWE-571] condition '(int )r4 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1168:7-1168:19)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1175:6-1175: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1177:6-1177:22)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___2 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1503:6-1503:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:461:6-461:19)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1188:6-1188: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1190:6-1190:22)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1201:6-1201: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1203:6-1203:22)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:843:7-843:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:853:6-853:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:488:6-488:18)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:493:6-493:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1660:6-1660:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:499:7-499:19)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:503:6-503:21)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:506:6-506: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:508:6-508: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1236:10-1236: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1238:8-1238:36)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:516:6-516:21)
[Warning][Deadcode][CWE-571] condition '(int )st2 + (int )nl2 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1240:8-1240:36)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:519:6-519: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1242:8-1242:36)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:521:6-521: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1244:8-1244:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1246:7-1246: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1252:10-1252:66)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1254:7-1254:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1256:7-1256:20)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:529:6-529:21)
[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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1262:10-1262:66)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:532:6-532:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1264:7-1264: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:534:6-534:22)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:884:7-884:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:894:6-894:19)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1274:6-1274:22)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1691:7-1691:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:544:6-544:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:550:7-550:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1282:6-1282:18)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:554:6-554:21)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1701:6-1701:19)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:557:6-557: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:559:6-559:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1287:6-1287:19)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:567:6-567:21)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:570:6-570: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:572:6-572:22)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:580:6-580:21)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:583:6-583: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:585:6-585:22)
[Warning][Deadcode][CWE-570] condition '(int )r4 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:925:7-925:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:595:6-595:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:601:7-601:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1732:7-1732:20)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:605:6-605:21)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:608:6-608:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1318:7-1318:20)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:610:6-610:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1742:6-1742:19)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1327:6-1327:19)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:618:6-618:21)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:621:6-621: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:623:6-623:22)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:631:6-631:21)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:634:6-634: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:636:6-636: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:958:10-958: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:960:8-960: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:962:8-962: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:964:8-964: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:966:8-966:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:968:7-968:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode4 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:646:6-646: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:974:10-974:66)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:976:7-976:19)
[Warning][Deadcode][CWE-571] condition '(int )r4 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:652:7-652:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:978:7-978:20)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:656:6-656:21)
[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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:984:10-984:66)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:659:6-659:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:986:7-986: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:661:6-661:22)
[Warning][Deadcode][CWE-570] condition '(int )r4 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1773:7-1773:20)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1358:7-1358:20)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___0 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:996:6-996:22)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:669:6-669:21)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:672:6-672: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:674:6-674:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1368:6-1368:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1004:6-1004:18)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1009:6-1009:19)
[Warning][Deadcode][CWE-571] condition '! ((int )newmax4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:682:6-682:21)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1015:7-1015:19)
[Warning][Deadcode][CWE-571] condition '(int )max4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:685:6-685: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:687:6-687:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1022:6-1022: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1024:6-1024:22)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1035:6-1035: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1806:10-1806:66)
[Warning][Deadcode][CWE-571] condition '(int )p13_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1037:6-1037: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1808:8-1808: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1810:8-1810: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1812:8-1812: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1814:8-1814:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1816:7-1816: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1822:10-1822:66)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1824:7-1824:19)
[Warning][Deadcode][CWE-571] condition '(int )max1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1048:6-1048:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1826:7-1826:20)
[Warning][Deadcode][CWE-571] condition '(int )p14_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1050:6-1050:22)
[Warning][Deadcode][CWE-570] condition '(((int )nl1 + (int )nl2) + (int )nl3) + (int )nl4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1832:10-1832:66)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1399:7-1399:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1409:6-1409:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1060:6-1060:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1066:7-1066: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:720:10-720: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:722:8-722: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:724:8-724:36)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1849:6-1849:22)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1073:6-1073: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:726:8-726:36)
[Warning][Deadcode][CWE-571] condition '(int )p21_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1075:6-1075: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:728:8-728:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:730:7-730: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:736:10-736:66)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:738:7-738:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:740:7-740: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:746:10-746:66)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1086:6-1086:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:748:7-748: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1088:6-1088:22)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:758:6-758:22)
[Warning][Deadcode][CWE-571] condition '(int )max2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1099:6-1099: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1101:6-1101:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:766:6-766:18)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:771:6-771:19)
[Warning][Deadcode][CWE-570] condition '(int )r4 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1440:7-1440:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1111:6-1111:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1117:7-1117:19)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1124:6-1124: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_opt-floodmax.4.2.ufo.BOUNDED-8.pals.c.v+lhb-reducer.c:1126:6-1126:22)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
