./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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2023:2-2023:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2065:2-2065:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2107:2-2107:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2149:2-2149:28)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:472-472)
  on line 523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:523-523)
  on line 574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:574-574)
  on line 625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:625-625)
  on line 709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:709-709)
  on line 719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:719-719)
  on line 737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:737-737)
  on line 781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:781-781)
  on line 822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:822-822)
  on line 863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:863-863)
  on line 904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:904-904)
  on line 947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:947-947)
  on line 957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:957-957)
  on line 975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:975-975)
  on line 988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:988-988)
  on line 1039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1039-1039)
  on line 1090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1090-1090)
  on line 1141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1141-1141)
  on line 1225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1225-1225)
  on line 1235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1235-1235)
  on line 1253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1253-1253)
  on line 1297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1297-1297)
  on line 1338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1338-1338)
  on line 1379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1379-1379)
  on line 1420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1420-1420)
  on line 1463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1463-1463)
  on line 1473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1473-1473)
  on line 1491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1491-1491)
  on line 1504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1504-1504)
  on line 1555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1555-1555)
  on line 1606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1606-1606)
  on line 1657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1657-1657)
  on line 1741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1741-1741)
  on line 1751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1751-1751)
  on line 1769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1769-1769)
  on line 1981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1981-1981)
  on line 1992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1992-1992)
  on line 2010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2010-2010)
  on line 2422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2422-2422)
  on line 2444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2444-2444)
  on line 2466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2466-2466)
  on line 2582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2582-2582)
  on line 2604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2604-2604)
  on line 2626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2626-2626)
  on line 2742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2742-2742)
  on line 2764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2764-2764)
  on line 2786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2786-2786)
  on line 2902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2902-2902)
  on line 2924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2924-2924)
  on line 2946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2946-2946)
  on line 2996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2996-2996)
  on line 3002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3002-3002)
  on line 3016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3016-3016)
  on line 3054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3054-3054)
  on line 3089 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3089-3089)
  on line 3101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3101-3101)
  on line 3136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3136-3136)
  on line 3148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3148-3148)
  on line 3183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3183-3183)
  on line 3195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3195-3195)
  on line 3230 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3230-3230)
  on line 3236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3236-3236)
  on line 3243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3243-3243)
  on line 3248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3248-3248)
  on line 3254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3254-3254)
  on line 3259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3259-3259)
  on line 3265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3265-3265)
  on line 3270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3270-3270)
  on line 3275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3275-3275)
  on line 3280 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3280-3280)
  on line 3285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3285-3285)
  on line 3292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3292-3292)
  on line 3314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3314-3314)
  on line 3336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3336-3336)
  on line 3357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3357-3357)
  on line 3365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3365-3365)
  on line 3387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3387-3387)
  on line 3409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3409-3409)
  on line 3430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3430-3430)
  on line 3438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3438-3438)
  on line 3460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3460-3460)
  on line 3482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3482-3482)
  on line 3503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3503-3503)
  on line 3511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3511-3511)
  on line 3533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3533-3533)
  on line 3555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3555-3555)
  on line 3576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3576-3576)
  on line 3583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3583-3583)
  on line 3590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3590-3590)
  on line 3595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3595-3595)
  on line 3601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3601-3601)
  on line 3606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3606-3606)
  on line 3612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3612-3612)
  on line 3617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3617-3617)
  on line 3622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3622-3622)
  on line 3627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3627-3627)
  on line 3632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3632-3632)
  on line 3669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3669-3669)
  on line 3706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3706-3706)
  on line 3743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3743-3743)
  on line 3780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3780-3780)
  on line 3786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3786-3786)
  on line 3793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3793-3793)
  on line 3798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3798-3798)
  on line 3804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3804-3804)
  on line 3809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3809-3809)
  on line 3815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3815-3815)
  on line 3820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3820-3820)
  on line 3825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3825-3825)
  on line 3830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3830-3830)
  on line 3835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3835-3835)
  on line 3842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3842-3842)
  on line 3864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3864-3864)
  on line 3886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3886-3886)
  on line 3907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3907-3907)
  on line 3915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3915-3915)
  on line 3937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3937-3937)
  on line 3959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3959-3959)
  on line 3980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3980-3980)
  on line 3988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:3988-3988)
  on line 4010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4010-4010)
  on line 4032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4032-4032)
  on line 4053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4053-4053)
  on line 4061 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4061-4061)
  on line 4083 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4083-4083)
  on line 4105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4105-4105)
  on line 4126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4126-4126)
  on line 4133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4133-4133)
  on line 4140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4140-4140)
  on line 4145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4145-4145)
  on line 4151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4151-4151)
  on line 4156 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4156-4156)
  on line 4162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4162-4162)
  on line 4167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4167-4167)
  on line 4172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4172-4172)
  on line 4177 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4177-4177)
  on line 4182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4182-4182)
  on line 4219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4219-4219)
  on line 4256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4256-4256)
  on line 4293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4293-4293)
  on line 4330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4330-4330)
  on line 4336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4336-4336)
  on line 4343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4343-4343)
  on line 4348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4348-4348)
  on line 4354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4354-4354)
  on line 4359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4359-4359)
  on line 4365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4365-4365)
  on line 4370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4370-4370)
  on line 4375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4375-4375)
  on line 4380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4380-4380)
  on line 4385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4385-4385)
  on line 4392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4392-4392)
  on line 4414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4414-4414)
  on line 4436 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4436-4436)
  on line 4457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4457-4457)
  on line 4465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4465-4465)
  on line 4487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4487-4487)
  on line 4509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4509-4509)
  on line 4530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4530-4530)
  on line 4538 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4538-4538)
  on line 4560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4560-4560)
  on line 4582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4582-4582)
  on line 4603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4603-4603)
  on line 4611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4611-4611)
  on line 4633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4633-4633)
  on line 4655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4655-4655)
  on line 4676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4676-4676)
  on line 4683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4683-4683)
  on line 4688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:4688-4688)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 1502
  dead: 171 (2 in uncalled functions)
  total lines: 1673
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1139:6-1139: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1145:7-1145: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1152:6-1152: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1154:6-1154:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1852:7-1852:20)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:438:6-438: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2702:6-2702: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1165:6-1165: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2704:6-2704:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1167:6-1167: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1862:6-1862: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2715:6-2715: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1178:6-1178: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2717:6-2717:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1180:6-1180: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2728:6-2728: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2730:6-2730: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:465:6-465: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:470:6-470: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:476:7-476: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:480:6-480: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:483:6-483: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1893:7-1893:20)
[Warning][Deadcode][CWE-571] condition '(int )p12_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:485:6-485: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1213:10-1213:66)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1903:6-1903: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_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1215:8-1215: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:493:6-493: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1217:8-1217: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:496:6-496: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1219:8-1219: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:498:6-498: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1221:8-1221: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1223:7-1223: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1229:10-1229: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1231:7-1231: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1233:7-1233: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:506:6-506: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1239:10-1239: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:509:6-509: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1241:7-1241: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:511:6-511: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2862:6-2862: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2864:6-2864:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1251:6-1251:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:521:6-521: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:527:7-527: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1259:6-1259: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:531:6-531: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:534:6-534: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:536:6-536: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2875:6-2875:19)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1264:6-1264: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_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2877:6-2877:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1934:7-1934:20)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:544:6-544: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:547:6-547: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:549:6-549: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2888:6-2888: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2890:6-2890: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:557:6-557: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:560:6-560: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:562:6-562:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:572:6-572: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:578:7-578: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:582:6-582: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:585:6-585: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1295:7-1295: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:587:6-587:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1305:6-1305: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:595:6-595: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:598:6-598: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1977:7-1977:20)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:600:6-600:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1979:7-1979: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1987:7-1987:20)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1990:7-1990: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:608:6-608: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:611:6-611: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:613:6-613:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:623:6-623: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:629:7-629: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:633:6-633: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:636:6-636: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:638:6-638: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1336:7-1336: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:646:6-646: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:649:6-649:19)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1346:6-1346: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:651:6-651: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:659:6-659: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:662:6-662: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:664:6-664: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1377:7-1377: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1387:6-1387: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:697:10-697: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:699:8-699: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:701:8-701: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:703:8-703: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:705:8-705: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:707:7-707: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:713:10-713: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:715:7-715: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:717:7-717: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:723:10-723: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:725:7-725:19)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:735:6-735: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:743:6-743:18)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1418:7-1418:20)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:748:6-748: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1451:10-1451: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1453:8-1453: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1455:8-1455: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1457:8-1457: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:779:7-779:20)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1459:8-1459: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1461:7-1461: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1467:10-1467: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1469:7-1469: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:789:6-789: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1471:7-1471: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1477:10-1477: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1479:7-1479:19)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1489:6-1489: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1497:6-1497: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1502:6-1502: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1508:7-1508: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1515:6-1515: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1517:6-1517: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:820:7-820:20)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1528:6-1528: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_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1530:6-1530: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:830:6-830: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1541:6-1541: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1543:6-1543:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1553:6-1553: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1559:7-1559: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1566:6-1566: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1568:6-1568: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1579:6-1579: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1581:6-1581: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:861:7-861: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:871:6-871: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1592:6-1592: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1594:6-1594:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1604:6-1604: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1610:7-1610: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1617:6-1617: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1619:6-1619: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1630:6-1630: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1632:6-1632: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:902:7-902:20)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1643:6-1643: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1645:6-1645:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1655:6-1655: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1661:7-1661: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1668:6-1668: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1670:6-1670: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1681:6-1681: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1683:6-1683: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:935:10-935: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:937:8-937: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:939:8-939: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:941:8-941: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:943:8-943: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:945:7-945:20)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1694:6-1694: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1696:6-1696:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:951:10-951: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:953:7-953: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:955:7-955: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:961:10-961: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:963:7-963: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2382:6-2382:19)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___0 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:973:6-973:22)
[Warning][Deadcode][CWE-571] condition '(int )p41_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2384:6-2384: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:981:6-981: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:986:6-986: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2395:6-2395: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2397:6-2397:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:992:7-992: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:999:6-999: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1001:6-1001: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2408:6-2408: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2410:6-2410: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1729:10-1729: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1731:8-1731: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1733:8-1733: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1735:8-1735: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1012:6-1012:19)
[Warning][Deadcode][CWE-571] condition '(int )st4 + (int )nl4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1737:8-1737: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1014:6-1014:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1739:7-1739: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1745:10-1745: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1747:7-1747: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1749:7-1749: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1755:10-1755: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1757:7-1757: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1025:6-1025: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1027:6-1027:22)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1767:6-1767:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1037:6-1037: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1043:7-1043: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1775:6-1775:18)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1050:6-1050:19)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1780:6-1780: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1052:6-1052: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1063:6-1063: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1065:6-1065: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2542:6-2542: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2544:6-2544: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1076:6-1076: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1078:6-1078: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2555:6-2555: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2557:6-2557:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1088:6-1088: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1094:7-1094: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2568:6-2568: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1811:7-1811:20)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1101:6-1101: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:2570:6-2570:22)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1103:6-1103:22)
[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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1821:6-1821: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1114:6-1114: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1116:6-1116: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1127:6-1127: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.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:1129:6-1129: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)
