./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] Enabled congruence domain.
[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_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:476-476)
  on line 519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:519-519)
  on line 562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:562-562)
  on line 605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:605-605)
  on line 683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:683-683)
  on line 693 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:693-693)
  on line 711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:711-711)
  on line 749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:749-749)
  on line 784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:784-784)
  on line 819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:819-819)
  on line 854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:854-854)
  on line 897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:897-897)
  on line 907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:907-907)
  on line 925 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:925-925)
  on line 936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:936-936)
  on line 979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:979-979)
  on line 1022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1022-1022)
  on line 1065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1065-1065)
  on line 1143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1143-1143)
  on line 1153 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1153-1153)
  on line 1171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1171-1171)
  on line 1244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1244-1244)
  on line 1279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1279-1279)
  on line 1314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1314-1314)
  on line 1357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1357-1357)
  on line 1367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1367-1367)
  on line 1392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1392-1392)
  on lines 1396..1398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1396-1398)
  on line 1401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1401-1401)
  on lines 1403..1404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1403-1404)
  on lines 1406..1408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1406-1408)
  on line 1410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1410-1410)
  on line 1412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1412-1412)
  on lines 1414..1416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1414-1416)
  on line 1418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1418-1418)
  on line 1420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1420-1420)
  on lines 1422..1424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1422-1424)
  on line 1426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1426-1426)
  on line 1428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1428-1428)
  on line 1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1430-1430)
  on line 1432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1432-1432)
  on line 1434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1434-1434)
  on line 1437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1437-1437)
  on lines 1439..1440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1439-1440)
  on lines 1442..1444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1442-1444)
  on line 1446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1446-1446)
  on line 1448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1448-1448)
  on lines 1450..1452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1450-1452)
  on line 1454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1454-1454)
  on line 1456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1456-1456)
  on lines 1458..1460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1458-1460)
  on line 1462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1462-1462)
  on line 1464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1464-1464)
  on line 1466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1466-1466)
  on line 1468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1468-1468)
  on line 1470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1470-1470)
  on line 1473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1473-1473)
  on lines 1475..1476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1475-1476)
  on lines 1478..1480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1478-1480)
  on line 1482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1482-1482)
  on line 1484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1484-1484)
  on lines 1486..1488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1486-1488)
  on line 1490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1490-1490)
  on line 1492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1492-1492)
  on lines 1494..1496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1494-1496)
  on line 1498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1498-1498)
  on line 1500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1500-1500)
  on line 1502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1502-1502)
  on line 1504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1504-1504)
  on line 1506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1506-1506)
  on line 1509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1509-1509)
  on lines 1511..1512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1511-1512)
  on lines 1514..1516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1514-1516)
  on line 1518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1518-1518)
  on line 1520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1520-1520)
  on lines 1522..1524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1522-1524)
  on line 1526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1526-1526)
  on line 1528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1528-1528)
  on lines 1530..1532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1530-1532)
  on line 1534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1534-1534)
  on line 1536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1536-1536)
  on line 1538 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1538-1538)
  on line 1540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1540-1540)
  on line 1542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1542-1542)
  on lines 1544..1567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1544-1567)
  on line 1570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1570-1570)
  on line 1572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1572-1572)
  on line 1574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1574-1574)
  on line 1576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1576-1576)
  on line 1578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1578-1578)
  on line 1580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1580-1580)
  on line 1583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1583-1583)
  on line 1586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1586-1586)
  on line 1589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1589-1589)
  on line 1591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1591-1591)
  on lines 1601..1603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1601-1603)
  on line 1608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1608-1608)
  on line 1610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1610-1610)
  on line 1615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1615-1615)
  on line 1622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1622-1622)
  on line 1628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1628-1628)
  on line 1635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1635-1635)
  on line 1641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1641-1641)
  on line 1648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1648-1648)
  on line 1654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1654-1654)
  on line 1661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1661-1661)
  on line 1667 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1667-1667)
  on line 1673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1673-1673)
  on line 1679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1679-1679)
  on line 1685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1685-1685)
  on line 1692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1692-1692)
  on line 1733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1733-1733)
  on line 1735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1735-1735)
  on line 1738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1738-1738)
  on line 1740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1740-1740)
  on line 1742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1742-1742)
  on line 1744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1744-1744)
  on line 1746 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1746-1746)
  on line 1749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1749-1749)
  on line 1751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1751-1751)
  on line 1753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1753-1753)
  on line 1755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1755-1755)
  on line 1757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1757-1757)
  on line 1760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1760-1760)
  on line 1762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1762-1762)
  on line 1764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1764-1764)
  on line 1766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1766-1766)
  on line 1768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1768-1768)
  on line 1774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1774-1774)
  on line 1791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1791-1791)
  on line 1808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1808-1808)
  on line 1831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1831-1831)
  on line 1872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1872-1872)
  on line 1874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1874-1874)
  on line 1877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1877-1877)
  on line 1879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1879-1879)
  on line 1881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1881-1881)
  on line 1883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1883-1883)
  on line 1885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1885-1885)
  on line 1888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1888-1888)
  on line 1890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1890-1890)
  on line 1892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1892-1892)
  on line 1894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1894-1894)
  on line 1896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1896-1896)
  on line 1899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1899-1899)
  on line 1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1901-1901)
  on line 1903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1903-1903)
  on line 1905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1905-1905)
  on line 1907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1907-1907)
  on line 1913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1913-1913)
  on line 1930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1930-1930)
  on line 1947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1947-1947)
  on line 1970 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1970-1970)
  on line 2011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2011-2011)
  on line 2013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2013-2013)
  on line 2016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2016-2016)
  on line 2018 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2018-2018)
  on line 2020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2020-2020)
  on line 2022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2022-2022)
  on line 2024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2024-2024)
  on line 2027 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2027-2027)
  on line 2029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2029-2029)
  on line 2031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2031-2031)
  on line 2033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2033-2033)
  on line 2035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2035-2035)
  on line 2038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2038-2038)
  on line 2040 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2040-2040)
  on line 2042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2042-2042)
  on line 2044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2044-2044)
  on line 2046 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2046-2046)
  on line 2052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2052-2052)
  on line 2069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2069-2069)
  on line 2086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2086-2086)
  on line 2109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2109-2109)
  on line 2150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2150-2150)
  on line 2152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2152-2152)
  on line 2155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2155-2155)
  on line 2157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2157-2157)
  on line 2159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2159-2159)
  on line 2161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2161-2161)
  on line 2163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2163-2163)
  on line 2166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2166-2166)
  on line 2168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2168-2168)
  on line 2170 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2170-2170)
  on line 2172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2172-2172)
  on line 2174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2174-2174)
  on line 2177 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2177-2177)
  on line 2179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2179-2179)
  on line 2181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2181-2181)
  on line 2183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2183-2183)
  on line 2185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2185-2185)
  on line 2191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2191-2191)
  on line 2208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2208-2208)
  on line 2225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2225-2225)
  on lines 2248..2249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2248-2249)
  on line 2258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2258-2258)
  on line 2270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2270-2270)
  on line 2275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2275-2275)
  on line 2280 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2280-2280)
  on line 2290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2290-2290)
  on line 2327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2327-2327)
  on line 2364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2364-2364)
  on line 2401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2401-2401)
  on line 2413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2413-2413)
  on line 2448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2448-2448)
  on line 2454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2454-2454)
  on line 2461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2461-2461)
  on line 2466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2466-2466)
  on line 2472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2472-2472)
  on line 2477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2477-2477)
  on line 2483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2483-2483)
  on line 2488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2488-2488)
  on line 2493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2493-2493)
  on line 2498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2498-2498)
  on line 2503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2503-2503)
  on line 2510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2510-2510)
  on line 2527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2527-2527)
  on line 2544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2544-2544)
  on line 2560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2560-2560)
  on line 2568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2568-2568)
  on line 2585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2585-2585)
  on line 2602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2602-2602)
  on line 2618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2618-2618)
  on line 2626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2626-2626)
  on line 2643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2643-2643)
  on line 2660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2660-2660)
  on line 2676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2676-2676)
  on line 2684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2684-2684)
  on line 2701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2701-2701)
  on line 2718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2718-2718)
  on line 2734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2734-2734)
  on line 2741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2741-2741)
  on line 2748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2748-2748)
  on line 2753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2753-2753)
  on line 2759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2759-2759)
  on line 2764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2764-2764)
  on line 2770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2770-2770)
  on line 2775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2775-2775)
  on line 2780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2780-2780)
  on line 2785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2785-2785)
  on line 2790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2790-2790)
  on line 2827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2827-2827)
  on line 2864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2864-2864)
  on line 2901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2901-2901)
  on line 2938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2938-2938)
  on line 2944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2944-2944)
  on line 2951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2951-2951)
  on line 2956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2956-2956)
  on line 2962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2962-2962)
  on line 2967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2967-2967)
  on line 2973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2973-2973)
  on line 2978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2978-2978)
  on line 2983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2983-2983)
  on line 2988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2988-2988)
  on line 2993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2993-2993)
  on line 3000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3000-3000)
  on line 3017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3017-3017)
  on line 3034 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3034-3034)
  on line 3050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3050-3050)
  on line 3058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3058-3058)
  on line 3075 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3075-3075)
  on line 3092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3092-3092)
  on line 3108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3108-3108)
  on line 3116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3116-3116)
  on line 3133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3133-3133)
  on line 3150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3150-3150)
  on line 3166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3166-3166)
  on line 3174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3174-3174)
  on line 3191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3191-3191)
  on line 3208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3208-3208)
  on line 3224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3224-3224)
  on line 3231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3231-3231)
  on line 3236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3236-3236)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 912
  dead: 331 (2 in uncalled functions)
  total lines: 1243
[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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1131:10-1131: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1133:8-1133: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1135:8-1135: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1137:8-1137: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1139:8-1139:36)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:782:7-782: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1141:7-1141: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1147:10-1147: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1149:7-1149: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:790:6-790: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1151:7-1151: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1157:10-1157: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1159:7-1159: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:444:6-444:19)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1169:6-1169: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1177:6-1177: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1180:6-1180:19)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:817:7-817:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:825:6-825: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:471:6-471:18)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:474:6-474: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:480:7-480: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:485:6-485: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:487:6-487:22)
[Warning][Deadcode][CWE-571] condition '(int )r1 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1207:7-1207: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:496:6-496: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:498:6-498: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1215:6-1215: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:507:6-507: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:509:6-509: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:852:7-852:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:517:6-517: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:523:7-523: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:528:6-528: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:530:6-530: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:539:6-539: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:541:6-541: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1242:7-1242: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1250:6-1250: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:550:6-550: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:552:6-552: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:885:10-885: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:887:8-887: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:889:8-889:36)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:560:6-560: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:891:8-891: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:893:8-893:36)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:566:7-566: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:895:7-895: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:571:6-571: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:901:10-901:66)
[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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:573:6-573: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:903:7-903: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:905:7-905: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:911:10-911: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:913:7-913: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:582:6-582: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:584:6-584:22)
[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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:923:6-923: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1277:7-1277: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:593:6-593: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:595:6-595: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:931:6-931: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1285:6-1285: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:934:6-934: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:940:7-940: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:945:6-945: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:947:6-947:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode4 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:603:6-603: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:609:7-609: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:614:6-614: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:616:6-616: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:956:6-956: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:958:6-958: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:625:6-625: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:627:6-627: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:967:6-967: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:969:6-969: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:636:6-636: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:638:6-638: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1312:7-1312:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:977:6-977: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:983:7-983: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:988:6-988: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:990:6-990: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:999:6-999: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1001:6-1001: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1010:6-1010: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1012:6-1012: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1345:10-1345: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1020:6-1020:19)
[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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1349:8-1349: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:671:10-671: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1351:8-1351:36)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1026:7-1026: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:673:8-673: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1353:8-1353: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:675:8-675: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1355:7-1355: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1031:6-1031: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:677:8-677:36)
[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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1033:6-1033: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:679:8-679: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:681:7-681:20)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1363:7-1363: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1365:7-1365: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:687:10-687: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:689:7-689: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:691:7-691: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1042:6-1042: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:697:10-697:66)
[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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1044:6-1044: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:699:7-699: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1053:6-1053:19)
[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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:709:6-709:22)
[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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1055:6-1055: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_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1389:6-1389: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:717:6-717: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:720:6-720:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode4 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1063:6-1063: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1069:7-1069: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1074:6-1074: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1076:6-1076: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1085:6-1085: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1087:6-1087: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1096:6-1096: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1098:6-1098:22)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.4.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:747:7-747: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.2.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:755:6-755:19)
[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)
