./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/benchexec/results/155-concurrency-fix-locations/goblint.2024-03-01_08-09-03.files/SV-COMP24_unreach-call/dekker.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/benchexec/results/155-concurrency-fix-locations/goblint.2024-03-01_08-09-03.files/SV-COMP24_unreach-call/dekker.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/dekker.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, tmp, t, f1, t, f2, __x, __x, __x
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: turn == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:789:1-797:1)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )f2) - (long long )t >= 0LL && (4294967295LL + (long long )f2) - (long long )t >= 0LL) && (4294967295LL - (long long )f2) + (long long )t >= 0LL) && (4294967296LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:707:1-747:1)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )f2) - (long long )t >= 0LL && (4294967295LL + (long long )f2) - (long long )t >= 0LL) && (4294967295LL - (long long )f2) + (long long )t >= 0LL) && (4294967296LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:708:5-708:30)
[Info][Witness] unassume invariant: (((flag1 == 1 && (4294967294LL - (long long )f2) - (long long )t >= 0LL) && (4294967295LL + (long long )f2) - (long long )t >= 0LL) && (4294967295LL - (long long )f2) + (long long )t >= 0LL) && (4294967296LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:709:5-709:14)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )f2) - (long long )t >= 0LL && (4294967295LL + (long long )f2) - (long long )t >= 0LL) && (4294967295LL - (long long )f2) + (long long )t >= 0LL) && (4294967296LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:710:5-710:28)
[Info][Witness] unassume invariant: ((((((flag2 == 0 || flag2 == 1) && (4294967294LL - (long long )f2) - (long long )t >= 0LL) && (4294967295LL + (long long )f2) - (long long )t >= 0LL) && (4294967295LL - (long long )f2) + (long long )t >= 0LL) && (4294967296LL + (long long )f2) + (long long )t >= 0LL) && flag2 <= 1) && 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:711:5-711:30)
[Info][Witness] unassume invariant: ((f2 == 0 || f2 == 1) && f2 <= 1) && 0 <= f2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:712:9-712:19)
[Info][Witness] unassume invariant: (((f2 == 0 || f2 == 1) && (unsigned long )_ == 0UL) && f2 <= 1) && 0 <= f2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:713:5-713:28)
[Info][Witness] unassume invariant: ((turn == 0 || turn == 1) && turn <= 1) && 0 <= turn (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:726:17-726:42)
[Info][Witness] unassume invariant: ((t == 0 || t == 1) && t <= 1) && 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:727:17-727:25)
[Info][Witness] unassume invariant: ((((t == 0 || t == 1) && (unsigned long )_ == 0UL) && f2 == 1) && t <= 1) && 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:728:17-728:40)
[Info][Witness] unassume invariant: (2147483646LL + (long long )f2) - (long long )t >= 0LL && (2147483647LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:714:12-714:19)
[Info][Witness] unassume invariant: ((((turn == 0 || turn == 1) && (2147483646LL + (long long )f2) - (long long )t >= 0LL) && (2147483647LL + (long long )f2) + (long long )t >= 0LL) && turn <= 1) && 0 <= turn (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:715:9-715:34)
[Info][Witness] unassume invariant: ((t == 0 || t == 1) && t <= 1) && 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:716:13-716:21)
[Info][Witness] unassume invariant: ((t == 0 || t == 1) && t <= 1) && 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:717:9-717:32)
[Info][Witness] unassume invariant: flag1 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:720:13-720:22)
[Info][Witness] unassume invariant: ((turn == 0 || turn == 1) && turn <= 1) && 0 <= turn (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:722:13-722:38)
[Info][Witness] unassume invariant: ((t == 0 || t == 1) && t <= 1) && 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:723:13-723:21)
[Info][Witness] unassume invariant: ((((t == 0 || t == 1) && (unsigned long )_ == 0UL) && f2 == 1) && t <= 1) && 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:724:13-724:36)
[Info][Witness] unassume invariant: (-1LL + (long long )f2) - (long long )t >= 0LL && (-1LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:725:20-725:26)
[Info][Witness] unassume invariant: (-1LL + (long long )f2) - (long long )t >= 0LL && (-1LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:730:13-730:38)
[Info][Witness] unassume invariant: ((t == 0 && flag1 == 1) && (-1LL + (long long )f2) - (long long )t >= 0LL) && (-1LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:731:13-731:22)
[Info][Witness] unassume invariant: (-1LL + (long long )f2) - (long long )t >= 0LL && (-1LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:732:13-732:36)
[Info][Witness] unassume invariant: (-1LL + (long long )f2) - (long long )t >= 0LL && (-1LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:718:13-718:19)
[Info][Witness] unassume invariant: ((((flag2 == 0 || flag2 == 1) && (-1LL + (long long )f2) - (long long )t >= 0LL) && (-1LL + (long long )f2) + (long long )t >= 0LL) && flag2 <= 1) && 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:734:9-734:34)
[Info][Witness] unassume invariant: ((f2 == 0 || f2 == 1) && f2 <= 1) && 0 <= f2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:735:9-735:19)
[Info][Witness] unassume invariant: (((f2 == 0 || f2 == 1) && (unsigned long )_ == 0UL) && f2 <= 1) && 0 <= f2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:736:9-736:32)
[Info][Witness] unassume invariant: (2147483647LL - (long long )f2) - (long long )t >= 0LL && (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:714:12-714:19)
[Info][Witness] unassume invariant: ((((x == 0 || x == 1) && (2147483647LL - (long long )f2) - (long long )t >= 0LL) && (2147483648LL - (long long )f2) + (long long )t >= 0LL) && x <= 1) && 0 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:738:5-738:10)
[Info][Witness] unassume invariant: (2147483647LL - (long long )f2) - (long long )t >= 0LL && (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:739:9-739:16)
[Info][Witness] unassume invariant: ((((x == 0 || x == 1) && (2147483647LL - (long long )f2) - (long long )t >= 0LL) && (2147483648LL - (long long )f2) + (long long )t >= 0LL) && x <= 1) && 0 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:739:9-739:16)
[Info][Witness] unassume invariant: (2147483647LL - (long long )f2) - (long long )t >= 0LL && (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:740:5-740:30)
[Info][Witness] unassume invariant: (turn == 1 && (2147483647LL - (long long )f2) - (long long )t >= 0LL) && (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:741:5-741:13)
[Info][Witness] unassume invariant: (2147483647LL - (long long )f2) - (long long )t >= 0LL && (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:742:5-742:28)
[Info][Witness] unassume invariant: (2147483647LL - (long long )f2) - (long long )t >= 0LL && (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:743:5-743:30)
[Info][Witness] unassume invariant: (flag1 == 0 && (2147483647LL - (long long )f2) - (long long )t >= 0LL) && (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:744:5-744:14)
[Info][Witness] unassume invariant: (2147483647LL - (long long )f2) - (long long )t >= 0LL && (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:745:5-745:28)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )f1) - (long long )t >= 0LL && (4294967295LL + (long long )f1) - (long long )t >= 0LL) && (4294967295LL - (long long )f1) + (long long )t >= 0LL) && (4294967296LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:748:1-788:1)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )f1) - (long long )t >= 0LL && (4294967295LL + (long long )f1) - (long long )t >= 0LL) && (4294967295LL - (long long )f1) + (long long )t >= 0LL) && (4294967296LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:749:5-749:30)
[Info][Witness] unassume invariant: (((flag2 == 1 && (4294967294LL - (long long )f1) - (long long )t >= 0LL) && (4294967295LL + (long long )f1) - (long long )t >= 0LL) && (4294967295LL - (long long )f1) + (long long )t >= 0LL) && (4294967296LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:750:5-750:14)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )f1) - (long long )t >= 0LL && (4294967295LL + (long long )f1) - (long long )t >= 0LL) && (4294967295LL - (long long )f1) + (long long )t >= 0LL) && (4294967296LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:751:5-751:28)
[Info][Witness] unassume invariant: ((((((flag1 == 0 || flag1 == 1) && (4294967294LL - (long long )f1) - (long long )t >= 0LL) && (4294967295LL + (long long )f1) - (long long )t >= 0LL) && (4294967295LL - (long long )f1) + (long long )t >= 0LL) && (4294967296LL + (long long )f1) + (long long )t >= 0LL) && flag1 <= 1) && 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:752:5-752:30)
[Info][Witness] unassume invariant: ((f1 == 0 || f1 == 1) && f1 <= 1) && 0 <= f1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:753:9-753:19)
[Info][Witness] unassume invariant: (((f1 == 0 || f1 == 1) && (unsigned long )_ == 0UL) && f1 <= 1) && 0 <= f1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:754:5-754:28)
[Info][Witness] unassume invariant: ((turn == 0 || turn == 1) && turn <= 1) && 0 <= turn (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:767:17-767:42)
[Info][Witness] unassume invariant: ((t == 0 || t == 1) && t <= 1) && 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:768:17-768:25)
[Info][Witness] unassume invariant: ((((t == 0 || t == 1) && (unsigned long )_ == 0UL) && f1 == 1) && t <= 1) && 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:769:17-769:40)
[Info][Witness] unassume invariant: (2147483646LL + (long long )f1) - (long long )t >= 0LL && (2147483647LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:755:12-755:19)
[Info][Witness] unassume invariant: ((((turn == 0 || turn == 1) && (2147483646LL + (long long )f1) - (long long )t >= 0LL) && (2147483647LL + (long long )f1) + (long long )t >= 0LL) && turn <= 1) && 0 <= turn (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:756:9-756:34)
[Info][Witness] unassume invariant: ((t == 0 || t == 1) && t <= 1) && 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:757:13-757:21)
[Info][Witness] unassume invariant: ((t == 0 || t == 1) && t <= 1) && 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:758:9-758:32)
[Info][Witness] unassume invariant: flag2 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:761:13-761:22)
[Info][Witness] unassume invariant: ((turn == 0 || turn == 1) && turn <= 1) && 0 <= turn (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:763:13-763:38)
[Info][Witness] unassume invariant: ((t == 0 || t == 1) && t <= 1) && 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:764:13-764:21)
[Info][Witness] unassume invariant: ((((t == 0 || t == 1) && (unsigned long )_ == 0UL) && f1 == 1) && t <= 1) && 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:765:13-765:36)
[Info][Witness] unassume invariant: (long long )f1 - (long long )t >= 0LL && (-2LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:766:20-766:26)
[Info][Witness] unassume invariant: (long long )f1 - (long long )t >= 0LL && (-2LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:771:13-771:38)
[Info][Witness] unassume invariant: ((t == 1 && flag2 == 1) && (long long )f1 - (long long )t >= 0LL) && (-2LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:772:13-772:22)
[Info][Witness] unassume invariant: (long long )f1 - (long long )t >= 0LL && (-2LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:773:13-773:36)
[Info][Witness] unassume invariant: (long long )f1 - (long long )t >= 0LL && (-2LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:759:13-759:19)
[Info][Witness] unassume invariant: ((((flag1 == 0 || flag1 == 1) && (long long )f1 - (long long )t >= 0LL) && (-2LL + (long long )f1) + (long long )t >= 0LL) && flag1 <= 1) && 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:775:9-775:34)
[Info][Witness] unassume invariant: ((f1 == 0 || f1 == 1) && f1 <= 1) && 0 <= f1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:776:9-776:19)
[Info][Witness] unassume invariant: (((f1 == 0 || f1 == 1) && (unsigned long )_ == 0UL) && f1 <= 1) && 0 <= f1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:777:9-777:32)
[Info][Witness] unassume invariant: (2147483647LL - (long long )f1) - (long long )t >= 0LL && (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:755:12-755:19)
[Info][Witness] unassume invariant: ((((x == 0 || x == 1) && (2147483647LL - (long long )f1) - (long long )t >= 0LL) && (2147483648LL - (long long )f1) + (long long )t >= 0LL) && x <= 1) && 0 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:779:5-779:10)
[Info][Witness] unassume invariant: (2147483647LL - (long long )f1) - (long long )t >= 0LL && (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:780:9-780:16)
[Info][Witness] unassume invariant: ((((x == 0 || x == 1) && (2147483647LL - (long long )f1) - (long long )t >= 0LL) && (2147483648LL - (long long )f1) + (long long )t >= 0LL) && x <= 1) && 0 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:780:9-780:16)
[Info][Witness] unassume invariant: (2147483647LL - (long long )f1) - (long long )t >= 0LL && (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:781:5-781:30)
[Info][Witness] unassume invariant: (turn == 1 && (2147483647LL - (long long )f1) - (long long )t >= 0LL) && (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:782:5-782:13)
[Info][Witness] unassume invariant: (2147483647LL - (long long )f1) - (long long )t >= 0LL && (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:783:5-783:28)
[Info][Witness] unassume invariant: (2147483647LL - (long long )f1) - (long long )t >= 0LL && (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:784:5-784:30)
[Info][Witness] unassume invariant: (flag2 == 0 && (2147483647LL - (long long )f1) - (long long )t >= 0LL) && (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:785:5-785:14)
[Info][Witness] unassume invariant: (2147483647LL - (long long )f1) - (long long )t >= 0LL && (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:786:5-786:28)
[Warning][Deadcode] Function '__bswap_16' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:82:1-86:1)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:87:1-91:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:92:15-96:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:97:1-101:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:102:1-106:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:107:1-111:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 85
  dead: 6 (6 in uncalled functions)
  total lines: 91
[Warning][Race] Memory location x (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:706:5-706:6)
  write with [region:{x}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:792:3-792:34]] (conf. 110)  (exp: & x) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:738:5-738:10)
  write with [region:{x}, thread:[main, thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:793:3-793:34]] (conf. 110)  (exp: & x) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:779:5-779:10)
  read with [region:{x}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:792:3-792:34]] (conf. 110)  (exp: & x) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:739:9-739:16)
  read with [region:{x}, thread:[main, thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:793:3-793:34]] (conf. 110)  (exp: & x) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:780:9-780:16)
[Warning][Deadcode][CWE-570] condition '! cond' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:3:6-3:11)
[Warning][Deadcode][CWE-571] condition '0 <= turn' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:791:3-791:42)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:16:73-16:74)
[Warning][Deadcode][CWE-571] condition 'turn <= 1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:791:3-791:42)
[Success][Witness] invariant confirmed: 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:776:9)
[Success][Witness] invariant confirmed: flag1 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:776:9)
[Warning][Witness] invariant unconfirmed: (-2LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:776:9)
[Warning][Witness] invariant unconfirmed: (long long )f1 - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:776:9)
[Success][Witness] invariant confirmed: flag1 == 0 || flag1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:776:9)
[Success][Witness] invariant confirmed: 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:765:13)
[Success][Witness] invariant confirmed: t <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:765:13)
[Success][Witness] invariant confirmed: t == 0 || t == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:765:13)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:745:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:745:5)
[Success][Witness] invariant confirmed: flag1 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:745:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:715:9)
[Warning][Witness] invariant unconfirmed: (2147483646LL + (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:715:9)
[Warning][Witness] invariant unconfirmed: (-2LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:771:13)
[Warning][Witness] invariant unconfirmed: (long long )f1 - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:771:13)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:783:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:783:5)
[Success][Witness] invariant confirmed: turn == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:783:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:731:13)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:731:13)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:786:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:786:5)
[Success][Witness] invariant confirmed: flag2 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:786:5)
[Success][Witness] invariant confirmed: 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:769:17)
[Success][Witness] invariant confirmed: t <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:769:17)
[Success][Witness] invariant confirmed: t == 0 || t == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:769:17)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:738:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:738:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:751:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:751:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:751:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:751:5)
[Success][Witness] invariant confirmed: flag2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:751:5)
[Warning][Witness] invariant unconfirmed: (-2LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:775:9)
[Warning][Witness] invariant unconfirmed: (long long )f1 - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:775:9)
[Success][Witness] invariant confirmed: 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:724:13)
[Success][Witness] invariant confirmed: t <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:724:13)
[Success][Witness] invariant confirmed: t == 0 || t == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:724:13)
[Success][Witness] invariant confirmed: 0 <= turn (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:723:13)
[Success][Witness] invariant confirmed: turn <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:723:13)
[Success][Witness] invariant confirmed: turn == 0 || turn == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:723:13)
[Success][Witness] invariant confirmed: 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:712:5)
[Success][Witness] invariant confirmed: flag2 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:712:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:712:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:712:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:712:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:712:5)
[Success][Witness] invariant confirmed: flag2 == 0 || flag2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:712:5)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:782:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:782:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:734:9)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:734:9)
[Success][Witness] invariant confirmed: 0 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:780:5)
[Success][Witness] invariant confirmed: x <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:780:5)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:780:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:780:5)
[Success][Witness] invariant confirmed: x == 0 || x == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:780:5)
[Success][Witness] invariant confirmed: 0 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:739:5)
[Success][Witness] invariant confirmed: x <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:739:5)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:739:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:739:5)
[Success][Witness] invariant confirmed: x == 0 || x == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:739:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:732:13)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:732:13)
[Success][Witness] invariant confirmed: flag1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:732:13)
[Warning][Witness] invariant unconfirmed: t == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:732:13)
[Warning][Witness] invariant unconfirmed: (2147483647LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:756:9)
[Warning][Witness] invariant unconfirmed: (2147483646LL + (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:756:9)
[Success][Witness] invariant confirmed: 0 <= f2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:713:5)
[Success][Witness] invariant confirmed: f2 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:713:5)
[Success][Witness] invariant confirmed: f2 == 0 || f2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:713:5)
[Success][Witness] invariant confirmed: 0 <= turn (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:757:9)
[Success][Witness] invariant confirmed: turn <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:757:9)
[Warning][Witness] invariant unconfirmed: (2147483647LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:757:9)
[Warning][Witness] invariant unconfirmed: (2147483646LL + (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:757:9)
[Success][Witness] invariant confirmed: turn == 0 || turn == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:757:9)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:742:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:742:5)
[Success][Witness] invariant confirmed: turn == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:742:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:711:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:711:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:711:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:711:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:730:13)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:730:13)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:746:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:746:5)
[Success][Witness] invariant confirmed: 0 <= flag2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:735:9)
[Success][Witness] invariant confirmed: flag2 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:735:9)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:735:9)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:735:9)
[Success][Witness] invariant confirmed: flag2 == 0 || flag2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:735:9)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:710:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:710:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:710:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:710:5)
[Success][Witness] invariant confirmed: flag1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:710:5)
[Success][Witness] invariant confirmed: 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:717:9)
[Success][Witness] invariant confirmed: t <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:717:9)
[Success][Witness] invariant confirmed: t == 0 || t == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:717:9)
[Success][Witness] invariant confirmed: turn == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:791:3)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:749:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:749:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:749:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:749:5)
[Success][Witness] invariant confirmed: 0 <= f1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:777:9)
[Success][Witness] invariant confirmed: f1 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:777:9)
[Success][Witness] invariant confirmed: f1 == 0 || f1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:777:9)
[Success][Witness] invariant confirmed: 0 <= turn (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:764:13)
[Success][Witness] invariant confirmed: turn <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:764:13)
[Success][Witness] invariant confirmed: turn == 0 || turn == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:764:13)
[Success][Witness] invariant confirmed: flag1 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:721:13)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:744:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:744:5)
[Success][Witness] invariant confirmed: 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:718:9)
[Success][Witness] invariant confirmed: t <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:718:9)
[Success][Witness] invariant confirmed: t == 0 || t == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:718:9)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:781:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:781:5)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:741:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:741:5)
[Success][Witness] invariant confirmed: 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:728:17)
[Success][Witness] invariant confirmed: t <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:728:17)
[Success][Witness] invariant confirmed: t == 0 || t == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:728:17)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:743:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:743:5)
[Success][Witness] invariant confirmed: flag2 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:762:13)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:709:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:709:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:709:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:709:5)
[Warning][Witness] invariant unconfirmed: (-2LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:773:13)
[Warning][Witness] invariant unconfirmed: (long long )f1 - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:773:13)
[Success][Witness] invariant confirmed: flag2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:773:13)
[Warning][Witness] invariant unconfirmed: t == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:773:13)
[Success][Witness] invariant confirmed: 0 <= f1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:754:5)
[Success][Witness] invariant confirmed: f1 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:754:5)
[Success][Witness] invariant confirmed: f1 == 0 || f1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:754:5)
[Success][Witness] invariant confirmed: 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:759:9)
[Success][Witness] invariant confirmed: t <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:759:9)
[Success][Witness] invariant confirmed: t == 0 || t == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:759:9)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:740:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:740:5)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:787:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:787:5)
[Success][Witness] invariant confirmed: 0 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:739:25)
[Success][Witness] invariant confirmed: x <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:739:25)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:739:25)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:739:25)
[Success][Witness] invariant confirmed: x == 0 || x == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:739:25)
[Success][Witness] invariant confirmed: 0 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:780:25)
[Success][Witness] invariant confirmed: x <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:780:25)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:780:25)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:780:25)
[Success][Witness] invariant confirmed: x == 0 || x == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:780:25)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:752:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:752:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:752:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:752:5)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:779:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:779:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:708:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:708:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:708:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:708:5)
[Warning][Witness] invariant unconfirmed: (-2LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:772:13)
[Warning][Witness] invariant unconfirmed: (long long )f1 - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:772:13)
[Success][Witness] invariant confirmed: 0 <= f2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:736:9)
[Success][Witness] invariant confirmed: f2 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:736:9)
[Success][Witness] invariant confirmed: f2 == 0 || f2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:736:9)
[Success][Witness] invariant confirmed: 0 <= turn (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:716:9)
[Success][Witness] invariant confirmed: turn <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:716:9)
[Warning][Witness] invariant unconfirmed: (2147483647LL + (long long )f2) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:716:9)
[Warning][Witness] invariant unconfirmed: (2147483646LL + (long long )f2) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:716:9)
[Success][Witness] invariant confirmed: turn == 0 || turn == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:716:9)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:750:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:750:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:750:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:750:5)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:785:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:785:5)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:784:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:784:5)
[Success][Witness] invariant confirmed: 0 <= turn (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:768:17)
[Success][Witness] invariant confirmed: turn <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:768:17)
[Success][Witness] invariant confirmed: turn == 0 || turn == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:768:17)
[Success][Witness] invariant confirmed: 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:758:9)
[Success][Witness] invariant confirmed: t <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:758:9)
[Success][Witness] invariant confirmed: t == 0 || t == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:758:9)
[Success][Witness] invariant confirmed: 0 <= turn (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:727:17)
[Success][Witness] invariant confirmed: turn <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:727:17)
[Success][Witness] invariant confirmed: turn == 0 || turn == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:727:17)
[Success][Witness] invariant confirmed: 0 <= flag1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:753:5)
[Success][Witness] invariant confirmed: flag1 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:753:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:753:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )f1) + (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:753:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:753:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )f1) - (long long )t >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:753:5)
[Success][Witness] invariant confirmed: flag1 == 0 || flag1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:753:5)
[Success][Witness] invariant confirmed: 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:766:13)
[Success][Witness] invariant confirmed: t <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:766:13)
[Warning][Witness] invariant unconfirmed: f1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:766:13)
[Success][Witness] invariant confirmed: (unsigned long )_ == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:766:13)
[Success][Witness] invariant confirmed: t == 0 || t == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:766:13)
[Success][Witness] invariant confirmed: 0 <= f1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:755:5)
[Success][Witness] invariant confirmed: f1 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:755:5)
[Success][Witness] invariant confirmed: (unsigned long )_ == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:755:5)
[Success][Witness] invariant confirmed: f1 == 0 || f1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:755:5)
[Success][Witness] invariant confirmed: 0 <= f2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:714:5)
[Success][Witness] invariant confirmed: f2 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:714:5)
[Success][Witness] invariant confirmed: (unsigned long )_ == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:714:5)
[Success][Witness] invariant confirmed: f2 == 0 || f2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:714:5)
[Success][Witness] invariant confirmed: 0 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:725:13)
[Success][Witness] invariant confirmed: t <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:725:13)
[Warning][Witness] invariant unconfirmed: f2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:725:13)
[Success][Witness] invariant confirmed: (unsigned long )_ == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:725:13)
[Success][Witness] invariant confirmed: t == 0 || t == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i:725:13)
[Info][Witness] witness validation summary:
  confirmed: 145
  unconfirmed: 72
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 217
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 3
  vulnerable: 0
  unsafe: 1
  total memory locations: 4
