./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/benchexec/results/156-concurrency-fix-locations-all-locals/goblint.2024-03-01_08-44-30.files/SV-COMP24_unreach-call/szymanski.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/benchexec/results/156-concurrency-fix-locations-all-locals/goblint.2024-03-01_08-44-30.files/SV-COMP24_unreach-call/szymanski.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/pthread-atomic/szymanski.i


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


[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] Enabled congruence domain.
[Info] Enabled widening thresholds
[Info] Enabled octagon domain for:
[Info] __VERIFIER_atomic_begin, __VERIFIER_atomic_end, i, key, count, a, tmp, count, i, j, i___0, j___0, k, size, r, top, t1, t2, f12, f21, __x, __x, __x
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: flag1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:704:5-704:14)
[Info][Witness] unassume invariant: ((((((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4) && flag2 <= 127) && flag2 <= 4) && 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:706:5-706:30)
[Info][Witness] unassume invariant: ((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:707:9-707:20)
[Info][Witness] unassume invariant: (((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && (unsigned long )_ == 0UL) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:708:5-708:28)
[Info][Witness] unassume invariant: ((((((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4) && flag2 <= 127) && flag2 <= 4) && 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:710:9-710:34)
[Info][Witness] unassume invariant: ((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:711:9-711:20)
[Info][Witness] unassume invariant: (((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && (unsigned long )_ == 0UL) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:712:9-712:32)
[Info][Witness] unassume invariant: flag1 == 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:715:5-715:14)
[Info][Witness] unassume invariant: ((((((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4) && flag2 <= 127) && flag2 <= 4) && 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:717:5-717:30)
[Info][Witness] unassume invariant: ((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:718:5-718:16)
[Info][Witness] unassume invariant: ((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:719:5-719:28)
[Info][Witness] unassume invariant: flag1 == 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:722:9-722:18)
[Info][Witness] unassume invariant: ((((((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4) && flag2 <= 127) && flag2 <= 4) && 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:724:9-724:34)
[Info][Witness] unassume invariant: ((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:725:9-725:20)
[Info][Witness] unassume invariant: (((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && (unsigned long )_ == 0UL) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:726:9-726:32)
[Info][Witness] unassume invariant: ((((((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4) && flag2 <= 127) && flag2 <= 4) && 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:728:13-728:38)
[Info][Witness] unassume invariant: ((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:729:13-729:24)
[Info][Witness] unassume invariant: (((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && (unsigned long )_ == 0UL) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:730:13-730:36)
[Info][Witness] unassume invariant: flag1 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:734:5-734:14)
[Info][Witness] unassume invariant: ((((((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4) && flag2 <= 127) && flag2 <= 4) && 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:736:5-736:30)
[Info][Witness] unassume invariant: ((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:737:5-737:16)
[Info][Witness] unassume invariant: (((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && (unsigned long )_ == 0UL) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:738:5-738:28)
[Info][Witness] unassume invariant: ((((((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4) && flag2 <= 127) && flag2 <= 4) && 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:740:9-740:34)
[Info][Witness] unassume invariant: ((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:741:9-741:20)
[Info][Witness] unassume invariant: (((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && (unsigned long )_ == 0UL) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:742:9-742:32)
[Info][Witness] unassume invariant: ((x == 0 || x == 1) && x <= 1) && 0 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:744:5-744:10)
[Info][Witness] unassume invariant: ((x == 0 || x == 1) && x <= 1) && 0 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:745:9-745:16)
[Info][Witness] unassume invariant: ((((((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4) && flag2 <= 127) && flag2 <= 4) && 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:746:5-746:30)
[Info][Witness] unassume invariant: ((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:747:5-747:16)
[Info][Witness] unassume invariant: (((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && (unsigned long )_ == 0UL) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:748:5-748:28)
[Info][Witness] unassume invariant: ((((((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4) && flag2 <= 127) && flag2 <= 4) && 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:750:9-750:34)
[Info][Witness] unassume invariant: ((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:751:9-751:20)
[Info][Witness] unassume invariant: (((((((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4) && (unsigned long )_ == 0UL) && f21 <= 127) && f21 <= 4) && 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:752:9-752:32)
[Info][Witness] unassume invariant: flag1 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:755:5-755:14)
[Info][Witness] unassume invariant: flag2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:761:5-761:14)
[Info][Witness] unassume invariant: ((((((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4) && flag1 <= 127) && flag1 <= 4) && 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:763:5-763:30)
[Info][Witness] unassume invariant: ((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:764:9-764:20)
[Info][Witness] unassume invariant: (((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && (unsigned long )_ == 0UL) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:765:5-765:28)
[Info][Witness] unassume invariant: ((((((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4) && flag1 <= 127) && flag1 <= 4) && 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:767:9-767:34)
[Info][Witness] unassume invariant: ((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:768:9-768:20)
[Info][Witness] unassume invariant: (((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && (unsigned long )_ == 0UL) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:769:9-769:32)
[Info][Witness] unassume invariant: flag2 == 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:772:5-772:14)
[Info][Witness] unassume invariant: ((((((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4) && flag1 <= 127) && flag1 <= 4) && 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:774:5-774:30)
[Info][Witness] unassume invariant: ((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:775:5-775:16)
[Info][Witness] unassume invariant: ((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:776:5-776:28)
[Info][Witness] unassume invariant: flag2 == 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:779:9-779:18)
[Info][Witness] unassume invariant: ((((((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4) && flag1 <= 127) && flag1 <= 4) && 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:781:9-781:34)
[Info][Witness] unassume invariant: ((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:782:9-782:20)
[Info][Witness] unassume invariant: (((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && (unsigned long )_ == 0UL) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:783:9-783:32)
[Info][Witness] unassume invariant: ((((((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4) && flag1 <= 127) && flag1 <= 4) && 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:785:13-785:38)
[Info][Witness] unassume invariant: ((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:786:13-786:24)
[Info][Witness] unassume invariant: (((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && (unsigned long )_ == 0UL) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:787:13-787:36)
[Info][Witness] unassume invariant: flag2 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:791:5-791:14)
[Info][Witness] unassume invariant: ((((((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4) && flag1 <= 127) && flag1 <= 4) && 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:793:5-793:30)
[Info][Witness] unassume invariant: ((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:794:5-794:16)
[Info][Witness] unassume invariant: (((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && (unsigned long )_ == 0UL) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:795:5-795:28)
[Info][Witness] unassume invariant: ((((((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4) && flag1 <= 127) && flag1 <= 4) && 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:797:9-797:34)
[Info][Witness] unassume invariant: ((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:798:9-798:20)
[Info][Witness] unassume invariant: (((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && (unsigned long )_ == 0UL) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:799:9-799:32)
[Info][Witness] unassume invariant: ((x == 0 || x == 1) && x <= 1) && 0 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:801:5-801:10)
[Info][Witness] unassume invariant: ((x == 0 || x == 1) && x <= 1) && 0 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:802:9-802:16)
[Info][Witness] unassume invariant: ((((((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4) && flag1 <= 127) && flag1 <= 4) && 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:803:5-803:30)
[Info][Witness] unassume invariant: ((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:804:5-804:16)
[Info][Witness] unassume invariant: (((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && (unsigned long )_ == 0UL) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:805:5-805:28)
[Info][Witness] unassume invariant: ((((((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4) && flag1 <= 127) && flag1 <= 4) && 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:807:9-807:34)
[Info][Witness] unassume invariant: ((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:808:9-808:20)
[Info][Witness] unassume invariant: (((((((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4) && (unsigned long )_ == 0UL) && f12 <= 127) && f12 <= 4) && 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:809:9-809:32)
[Info][Witness] unassume invariant: flag2 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:812:5-812:14)
[Warning][Deadcode] Function '__bswap_16' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:78:1-82:1)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:83:1-87:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:88:15-92:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:93:1-97:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:98:1-102:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:103:1-107:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 109
  dead: 6 (6 in uncalled functions)
  total lines: 115
[Warning][Race] Memory location x (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:701:5-701:6)
  write with [region:{x}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:818:3-818:34]] (conf. 110)  (exp: & x) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:744:5-744:10)
  write with [region:{x}, thread:[main, thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:819:3-819:34]] (conf. 110)  (exp: & x) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:801:5-801:10)
  read with [region:{x}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:818:3-818:34]] (conf. 110)  (exp: & x) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:745:9-745:16)
  read with [region:{x}, thread:[main, thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:819:3-819:34]] (conf. 110)  (exp: & x) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:802:9-802:16)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:12:73-12:74)
[Success][Witness] invariant confirmed: 0 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:802:5)
[Success][Witness] invariant confirmed: x <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:802:5)
[Success][Witness] invariant confirmed: x == 0 || x == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:802:5)
[Success][Witness] invariant confirmed: 0 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:802:25)
[Success][Witness] invariant confirmed: x <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:802:25)
[Success][Witness] invariant confirmed: x == 0 || x == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:802:25)
[Success][Witness] invariant confirmed: 0 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:745:25)
[Success][Witness] invariant confirmed: x <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:745:25)
[Success][Witness] invariant confirmed: x == 0 || x == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:745:25)
[Success][Witness] invariant confirmed: 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:795:5)
[Success][Witness] invariant confirmed: f12 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:795:5)
[Success][Witness] invariant confirmed: f12 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:795:5)
[Success][Witness] invariant confirmed: (((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:795:5)
[Success][Witness] invariant confirmed: 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:769:9)
[Success][Witness] invariant confirmed: f12 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:769:9)
[Success][Witness] invariant confirmed: f12 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:769:9)
[Success][Witness] invariant confirmed: (((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:769:9)
[Success][Witness] invariant confirmed: 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:725:9)
[Success][Witness] invariant confirmed: flag2 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:725:9)
[Success][Witness] invariant confirmed: flag2 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:725:9)
[Success][Witness] invariant confirmed: (((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:725:9)
[Success][Witness] invariant confirmed: 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:777:5)
[Success][Witness] invariant confirmed: f12 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:777:5)
[Success][Witness] invariant confirmed: f12 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:777:5)
[Success][Witness] invariant confirmed: (((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:777:5)
[Success][Witness] invariant confirmed: flag1 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:756:5)
[Success][Witness] invariant confirmed: 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:775:5)
[Success][Witness] invariant confirmed: flag1 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:775:5)
[Success][Witness] invariant confirmed: flag1 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:775:5)
[Success][Witness] invariant confirmed: (((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:775:5)
[Success][Witness] invariant confirmed: 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:787:13)
[Success][Witness] invariant confirmed: f12 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:787:13)
[Success][Witness] invariant confirmed: f12 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:787:13)
[Success][Witness] invariant confirmed: (((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:787:13)
[Success][Witness] invariant confirmed: 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:783:9)
[Success][Witness] invariant confirmed: f12 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:783:9)
[Success][Witness] invariant confirmed: f12 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:783:9)
[Success][Witness] invariant confirmed: (((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:783:9)
[Success][Witness] invariant confirmed: flag2 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:813:5)
[Success][Witness] invariant confirmed: 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:742:9)
[Success][Witness] invariant confirmed: f21 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:742:9)
[Success][Witness] invariant confirmed: f21 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:742:9)
[Success][Witness] invariant confirmed: (((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:742:9)
[Success][Witness] invariant confirmed: 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:747:5)
[Success][Witness] invariant confirmed: flag2 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:747:5)
[Success][Witness] invariant confirmed: flag2 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:747:5)
[Success][Witness] invariant confirmed: (((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:747:5)
[Success][Witness] invariant confirmed: 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:786:13)
[Success][Witness] invariant confirmed: flag1 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:786:13)
[Success][Witness] invariant confirmed: flag1 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:786:13)
[Success][Witness] invariant confirmed: (((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:786:13)
[Success][Witness] invariant confirmed: flag2 == 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:780:9)
[Success][Witness] invariant confirmed: 0 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:745:5)
[Success][Witness] invariant confirmed: x <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:745:5)
[Success][Witness] invariant confirmed: x == 0 || x == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:745:5)
[Success][Witness] invariant confirmed: 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:805:5)
[Success][Witness] invariant confirmed: f12 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:805:5)
[Success][Witness] invariant confirmed: f12 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:805:5)
[Success][Witness] invariant confirmed: (((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:805:5)
[Success][Witness] invariant confirmed: 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:712:9)
[Success][Witness] invariant confirmed: f21 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:712:9)
[Success][Witness] invariant confirmed: f21 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:712:9)
[Success][Witness] invariant confirmed: (((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:712:9)
[Success][Witness] invariant confirmed: 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:707:5)
[Success][Witness] invariant confirmed: flag2 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:707:5)
[Success][Witness] invariant confirmed: flag2 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:707:5)
[Success][Witness] invariant confirmed: (((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:707:5)
[Success][Witness] invariant confirmed: 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:730:13)
[Success][Witness] invariant confirmed: f21 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:730:13)
[Success][Witness] invariant confirmed: f21 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:730:13)
[Success][Witness] invariant confirmed: (((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:730:13)
[Success][Witness] invariant confirmed: 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:708:5)
[Success][Witness] invariant confirmed: f21 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:708:5)
[Success][Witness] invariant confirmed: f21 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:708:5)
[Success][Witness] invariant confirmed: (((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:708:5)
[Success][Witness] invariant confirmed: 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:748:5)
[Success][Witness] invariant confirmed: f21 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:748:5)
[Success][Witness] invariant confirmed: f21 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:748:5)
[Success][Witness] invariant confirmed: (((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:748:5)
[Success][Witness] invariant confirmed: 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:738:5)
[Success][Witness] invariant confirmed: f21 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:738:5)
[Success][Witness] invariant confirmed: f21 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:738:5)
[Success][Witness] invariant confirmed: (((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:738:5)
[Success][Witness] invariant confirmed: 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:809:9)
[Success][Witness] invariant confirmed: f12 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:809:9)
[Success][Witness] invariant confirmed: f12 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:809:9)
[Success][Witness] invariant confirmed: (((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:809:9)
[Success][Witness] invariant confirmed: 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:768:9)
[Success][Witness] invariant confirmed: flag1 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:768:9)
[Success][Witness] invariant confirmed: flag1 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:768:9)
[Success][Witness] invariant confirmed: (((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:768:9)
[Success][Witness] invariant confirmed: 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:751:9)
[Success][Witness] invariant confirmed: flag2 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:751:9)
[Success][Witness] invariant confirmed: flag2 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:751:9)
[Success][Witness] invariant confirmed: (((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:751:9)
[Success][Witness] invariant confirmed: 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:798:9)
[Success][Witness] invariant confirmed: flag1 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:798:9)
[Success][Witness] invariant confirmed: flag1 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:798:9)
[Success][Witness] invariant confirmed: (((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:798:9)
[Success][Witness] invariant confirmed: flag1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:705:5)
[Success][Witness] invariant confirmed: 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:764:5)
[Success][Witness] invariant confirmed: flag1 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:764:5)
[Success][Witness] invariant confirmed: flag1 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:764:5)
[Success][Witness] invariant confirmed: (((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:764:5)
[Success][Witness] invariant confirmed: 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:729:13)
[Success][Witness] invariant confirmed: flag2 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:729:13)
[Success][Witness] invariant confirmed: flag2 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:729:13)
[Success][Witness] invariant confirmed: (((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:729:13)
[Success][Witness] invariant confirmed: 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:711:9)
[Success][Witness] invariant confirmed: flag2 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:711:9)
[Success][Witness] invariant confirmed: flag2 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:711:9)
[Success][Witness] invariant confirmed: (((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:711:9)
[Success][Witness] invariant confirmed: 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:808:9)
[Success][Witness] invariant confirmed: flag1 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:808:9)
[Success][Witness] invariant confirmed: flag1 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:808:9)
[Success][Witness] invariant confirmed: (((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:808:9)
[Success][Witness] invariant confirmed: 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:776:5)
[Success][Witness] invariant confirmed: f12 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:776:5)
[Success][Witness] invariant confirmed: f12 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:776:5)
[Success][Witness] invariant confirmed: (((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:776:5)
[Success][Witness] invariant confirmed: 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:718:5)
[Success][Witness] invariant confirmed: flag2 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:718:5)
[Success][Witness] invariant confirmed: flag2 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:718:5)
[Success][Witness] invariant confirmed: (((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:718:5)
[Success][Witness] invariant confirmed: 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:782:9)
[Success][Witness] invariant confirmed: flag1 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:782:9)
[Success][Witness] invariant confirmed: flag1 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:782:9)
[Success][Witness] invariant confirmed: (((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:782:9)
[Success][Witness] invariant confirmed: 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:719:5)
[Success][Witness] invariant confirmed: f21 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:719:5)
[Success][Witness] invariant confirmed: f21 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:719:5)
[Success][Witness] invariant confirmed: (((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:719:5)
[Success][Witness] invariant confirmed: flag1 == 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:716:5)
[Success][Witness] invariant confirmed: flag2 == 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:773:5)
[Success][Witness] invariant confirmed: 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:804:5)
[Success][Witness] invariant confirmed: flag1 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:804:5)
[Success][Witness] invariant confirmed: flag1 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:804:5)
[Success][Witness] invariant confirmed: (((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:804:5)
[Success][Witness] invariant confirmed: 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:765:5)
[Success][Witness] invariant confirmed: f12 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:765:5)
[Success][Witness] invariant confirmed: f12 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:765:5)
[Success][Witness] invariant confirmed: (((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:765:5)
[Success][Witness] invariant confirmed: flag1 == 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:723:9)
[Success][Witness] invariant confirmed: 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:726:9)
[Success][Witness] invariant confirmed: f21 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:726:9)
[Success][Witness] invariant confirmed: f21 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:726:9)
[Success][Witness] invariant confirmed: (((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:726:9)
[Success][Witness] invariant confirmed: 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:720:5)
[Success][Witness] invariant confirmed: f21 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:720:5)
[Success][Witness] invariant confirmed: f21 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:720:5)
[Success][Witness] invariant confirmed: (((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:720:5)
[Success][Witness] invariant confirmed: flag2 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:792:5)
[Success][Witness] invariant confirmed: 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:741:9)
[Success][Witness] invariant confirmed: flag2 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:741:9)
[Success][Witness] invariant confirmed: flag2 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:741:9)
[Success][Witness] invariant confirmed: (((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:741:9)
[Success][Witness] invariant confirmed: 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:752:9)
[Success][Witness] invariant confirmed: f21 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:752:9)
[Success][Witness] invariant confirmed: f21 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:752:9)
[Success][Witness] invariant confirmed: (((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:752:9)
[Success][Witness] invariant confirmed: flag1 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:735:5)
[Success][Witness] invariant confirmed: 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:794:5)
[Success][Witness] invariant confirmed: flag1 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:794:5)
[Success][Witness] invariant confirmed: flag1 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:794:5)
[Success][Witness] invariant confirmed: (((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:794:5)
[Success][Witness] invariant confirmed: 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:799:9)
[Success][Witness] invariant confirmed: f12 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:799:9)
[Success][Witness] invariant confirmed: f12 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:799:9)
[Success][Witness] invariant confirmed: (((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:799:9)
[Success][Witness] invariant confirmed: flag2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:762:5)
[Success][Witness] invariant confirmed: 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:737:5)
[Success][Witness] invariant confirmed: flag2 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:737:5)
[Success][Witness] invariant confirmed: flag2 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:737:5)
[Success][Witness] invariant confirmed: (((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:737:5)
[Success][Witness] invariant confirmed: 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:739:5)
[Success][Witness] invariant confirmed: f21 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:739:5)
[Success][Witness] invariant confirmed: f21 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:739:5)
[Success][Witness] invariant confirmed: (unsigned long )_ == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:739:5)
[Success][Witness] invariant confirmed: (((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:739:5)
[Success][Witness] invariant confirmed: 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:784:9)
[Success][Witness] invariant confirmed: f12 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:784:9)
[Success][Witness] invariant confirmed: f12 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:784:9)
[Success][Witness] invariant confirmed: (unsigned long )_ == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:784:9)
[Success][Witness] invariant confirmed: (((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:784:9)
[Success][Witness] invariant confirmed: 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:749:5)
[Success][Witness] invariant confirmed: f21 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:749:5)
[Success][Witness] invariant confirmed: f21 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:749:5)
[Success][Witness] invariant confirmed: (unsigned long )_ == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:749:5)
[Success][Witness] invariant confirmed: (((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:749:5)
[Success][Witness] invariant confirmed: 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:727:9)
[Success][Witness] invariant confirmed: f21 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:727:9)
[Success][Witness] invariant confirmed: f21 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:727:9)
[Success][Witness] invariant confirmed: (unsigned long )_ == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:727:9)
[Success][Witness] invariant confirmed: (((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:727:9)
[Success][Witness] invariant confirmed: 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:806:5)
[Success][Witness] invariant confirmed: f12 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:806:5)
[Success][Witness] invariant confirmed: f12 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:806:5)
[Success][Witness] invariant confirmed: (unsigned long )_ == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:806:5)
[Success][Witness] invariant confirmed: (((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:806:5)
[Success][Witness] invariant confirmed: 0 <= f21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:709:5)
[Success][Witness] invariant confirmed: f21 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:709:5)
[Success][Witness] invariant confirmed: f21 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:709:5)
[Success][Witness] invariant confirmed: (unsigned long )_ == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:709:5)
[Success][Witness] invariant confirmed: (((f21 == 0 || f21 == 1) || f21 == 2) || f21 == 3) || f21 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:709:5)
[Success][Witness] invariant confirmed: 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:796:5)
[Success][Witness] invariant confirmed: f12 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:796:5)
[Success][Witness] invariant confirmed: f12 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:796:5)
[Success][Witness] invariant confirmed: (unsigned long )_ == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:796:5)
[Success][Witness] invariant confirmed: (((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:796:5)
[Success][Witness] invariant confirmed: 0 <= f12 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:766:5)
[Success][Witness] invariant confirmed: f12 <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:766:5)
[Success][Witness] invariant confirmed: f12 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:766:5)
[Success][Witness] invariant confirmed: (unsigned long )_ == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:766:5)
[Success][Witness] invariant confirmed: (((f12 == 0 || f12 == 1) || f12 == 2) || f12 == 3) || f12 == 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i:766:5)
[Info][Witness] witness validation summary:
  confirmed: 214
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 214
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 2
  vulnerable: 0
  unsafe: 1
  total memory locations: 3
