./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.3.2.ufo.BOUNDED-6.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.3.2.ufo.BOUNDED-6.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.3.2.ufo.BOUNDED-6.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] Enabled octagon domain ONLY for:
[Info] nomsg, r1, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, main__i2, init__r121, init__r131, init__r211, init__r231, init__r311, init__r321, init__r122, cond
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:405:2-405:28)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:249-249)
  on line 281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:281-281)
  on line 313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:313-313)
  on line 366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:366-366)
  on line 376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:376-376)
  on line 394 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:394-394)
  on line 451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:451-451)
  on line 478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:478-478)
  on line 507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:507-507)
  on line 517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:517-517)
  on line 542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:542-542)
  on lines 546..548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:546-548)
  on line 551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:551-551)
  on lines 553..554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:553-554)
  on lines 556..558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:556-558)
  on line 560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:560-560)
  on line 562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:562-562)
  on lines 564..566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:564-566)
  on line 568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:568-568)
  on line 570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:570-570)
  on line 572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:572-572)
  on line 574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:574-574)
  on line 576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:576-576)
  on line 579 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:579-579)
  on lines 581..582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:581-582)
  on lines 584..586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:584-586)
  on line 588 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:588-588)
  on line 590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:590-590)
  on lines 592..594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:592-594)
  on line 596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:596-596)
  on line 598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:598-598)
  on line 600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:600-600)
  on line 602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:602-602)
  on line 604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:604-604)
  on line 607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:607-607)
  on lines 609..610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:609-610)
  on lines 612..614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:612-614)
  on line 616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:616-616)
  on line 618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:618-618)
  on lines 620..622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:620-622)
  on line 624 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:624-624)
  on line 626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:626-626)
  on line 628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:628-628)
  on line 630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:630-630)
  on line 632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:632-632)
  on lines 634..645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:634-645)
  on line 648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:648-648)
  on line 650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:650-650)
  on line 652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:652-652)
  on line 654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:654-654)
  on line 656 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:656-656)
  on line 659 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:659-659)
  on line 662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:662-662)
  on line 665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:665-665)
  on line 667 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:667-667)
  on lines 676..678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:676-678)
  on line 683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:683-683)
  on line 685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:685-685)
  on line 690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:690-690)
  on line 697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:697-697)
  on line 703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:703-703)
  on line 710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:710-710)
  on line 716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:716-716)
  on line 723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:723-723)
  on line 729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:729-729)
  on line 736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:736-736)
  on line 742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:742-742)
  on line 748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:748-748)
  on line 754 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:754-754)
  on line 761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:761-761)
  on line 792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:792-792)
  on line 794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:794-794)
  on line 797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:797-797)
  on line 799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:799-799)
  on line 801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:801-801)
  on line 803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:803-803)
  on line 805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:805-805)
  on line 808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:808-808)
  on line 810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:810-810)
  on line 812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:812-812)
  on line 814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:814-814)
  on line 816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:816-816)
  on line 822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:822-822)
  on line 839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:839-839)
  on line 862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:862-862)
  on line 893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:893-893)
  on line 895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:895-895)
  on line 898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:898-898)
  on line 900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:900-900)
  on line 902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:902-902)
  on line 904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:904-904)
  on line 906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:906-906)
  on line 909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:909-909)
  on line 911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:911-911)
  on line 913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:913-913)
  on line 915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:915-915)
  on line 917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:917-917)
  on line 923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:923-923)
  on line 940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:940-940)
  on line 963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:963-963)
  on line 994 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:994-994)
  on line 996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:996-996)
  on line 999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:999-999)
  on line 1001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1001-1001)
  on line 1003 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1003-1003)
  on line 1005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1005-1005)
  on line 1007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1007-1007)
  on line 1010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1010-1010)
  on line 1012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1012-1012)
  on line 1014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1014-1014)
  on line 1016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1016-1016)
  on line 1018 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1018-1018)
  on line 1024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1024-1024)
  on line 1041 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1041-1041)
  on lines 1064..1065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1064-1065)
  on line 1074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1074-1074)
  on line 1086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1086-1086)
  on line 1091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1091-1091)
  on line 1101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1101-1101)
  on line 1128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1128-1128)
  on line 1155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1155-1155)
  on line 1167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1167-1167)
  on line 1192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1192-1192)
  on line 1198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1198-1198)
  on line 1205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1205-1205)
  on line 1210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1210-1210)
  on line 1216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1216-1216)
  on line 1221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1221-1221)
  on line 1227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1227-1227)
  on line 1232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1232-1232)
  on line 1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1237-1237)
  on line 1242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1242-1242)
  on line 1249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1249-1249)
  on line 1266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1266-1266)
  on line 1282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1282-1282)
  on line 1290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1290-1290)
  on line 1307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1307-1307)
  on line 1323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1323-1323)
  on line 1331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1331-1331)
  on line 1348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1348-1348)
  on line 1364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1364-1364)
  on line 1371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1371-1371)
  on line 1376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:1376-1376)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 306
  dead: 176 (2 in uncalled functions)
  total lines: 482
[Warning][Deadcode][CWE-570] condition '(int )assert__arg == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:392:6-392:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:400:6-400:18)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:403:6-403:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:229:6-229:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:422:7-422:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:430:6-430:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:244:6-244:18)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:247:6-247:19)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:253:7-253: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.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:258:6-258: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.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:260:6-260:22)
[Warning][Deadcode][CWE-570] condition '(int )r2 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:449:7-449: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.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:269:6-269: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.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:271:6-271:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:457:6-457:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:279:6-279:19)
[Warning][Deadcode][CWE-571] condition '(int )r2 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:285:7-285: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.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:290:6-290: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.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:292:6-292: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.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:301:6-301: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.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:303:6-303:22)
[Warning][Deadcode][CWE-570] condition '(int )r3 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:476:7-476:20)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:311:6-311:19)
[Warning][Deadcode][CWE-571] condition '(int )r3 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:317:7-317: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.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:322:6-322:19)
[Warning][Deadcode][CWE-571] condition '(int )p31_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:324:6-324:22)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:497:9-497:51)
[Warning][Deadcode][CWE-571] condition '(int )max3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:333:6-333: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.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:501:8-501:36)
[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.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:335:6-335:22)
[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.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:503:8-503:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:505:7-505:20)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:513:7-513:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:515:7-515:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:356:9-356:51)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___0 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:539:6-539:22)
[Warning][Deadcode][CWE-571] condition '(int )st1 + (int )nl1 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:358:8-358: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.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:360:8-360: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.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:362:8-362:36)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:364:7-364:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:370:9-370:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:372:7-372:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:374:7-374:20)
[Warning][Deadcode][CWE-571] condition '((int )nl1 + (int )nl2) + (int )nl3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:380:9-380:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:382:7-382: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)
