./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/26_stack_cas_longest-1.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/26_stack_cas_longest-1.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-ext/26_stack_cas_longest-1.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] abort, __VERIFIER_atomic_release, i, key, count, a, tmp, count, i, j, i___0, j___0, k, size, r, top___0, r, arg, tmp, tmp, newTop, oldTop, d, casret, curr_alloc_idx, r, v, e, u, m___0, m___0, __x, __x, __x
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Error][Witness] CIL couldn't parse invariant: 0 <= *m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699:2)
[Info][Witness] invariant has undefined variables or side effects: 0 <= *m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

[Error][Witness] CIL couldn't parse invariant: *m <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699:2)
[Info][Witness] invariant has undefined variables or side effects: *m <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

[Error][Witness] CIL couldn't parse invariant: *m == 0 || *m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699:2)
[Info][Witness] invariant has undefined variables or side effects: *m == 0 || *m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

[Error][Witness] CIL couldn't parse invariant: (m == & m2 && (((0 <= *m && *m <= 1) && (0 <= *m && *m <= 1)) && (*m == 0 || *m == 1))) || (m == & m && (((0 <= *m && *m <= 1) && (0 <= *m && *m <= 1)) && (*m == 0 || *m == 1))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698:2)
[Info][Witness] invariant has undefined variables or side effects: (m == & m2 && (((0 <= *m && *m <= 1) && (0 <= *m && *m <= 1)) && (*m == 0 || *m == 1))) || (m == & m && (((0 <= *m && *m <= 1) && (0 <= *m && *m <= 1)) && (*m == 0 || *m == 1))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

[Error][Witness] CIL couldn't parse invariant: 0 <= *m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694:2)
[Info][Witness] invariant has undefined variables or side effects: 0 <= *m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

[Error][Witness] CIL couldn't parse invariant: *m <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694:2)
[Info][Witness] invariant has undefined variables or side effects: *m <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

[Error][Witness] CIL couldn't parse invariant: *m == 0 || *m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694:2)
[Info][Witness] invariant has undefined variables or side effects: *m == 0 || *m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

[Error][Witness] CIL couldn't parse invariant: (m == & m2 && (((0 <= *m && *m <= 1) && (0 <= *m && *m <= 1)) && (*m == 0 || *m == 1))) || (m == & m && (((0 <= *m && *m <= 1) && (0 <= *m && *m <= 1)) && (*m == 0 || *m == 1))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693:2)
[Info][Witness] invariant has undefined variables or side effects: (m == & m2 && (((0 <= *m && *m <= 1) && (0 <= *m && *m <= 1)) && (*m == 0 || *m == 1))) || (m == & m && (((0 <= *m && *m <= 1) && (0 <= *m && *m <= 1)) && (*m == 0 || *m == 1))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

[Info][Witness] unassume invariant: (((((m2 == 0 || m2 == 1) && (m == 0 || m == 1)) && m2 <= 1) && m <= 1) && 0 <= m2) && 0 <= m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:691:1-695:1)
[Info][Witness] unassume invariant: (unsigned long )m == (unsigned long )(& m2) || (unsigned long )m == (unsigned long )(& m) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693:2-693:28)
[Info][Witness] unassume invariant: (((((m2 == 0 || m2 == 1) && (m == 0 || m == 1)) && m2 <= 1) && m <= 1) && 0 <= m2) && 0 <= m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694:2-694:8)
[Info][Witness] unassume invariant: ((state == 0 || state == 1) && state <= 1) && 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:777:2-777:32)
[Info][Witness] unassume invariant: ((state == 0 || state == 1) && state <= 1) && 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:780:2-780:8)
[Info][Witness] unassume invariant: ((state == 0 || state == 1) && state <= 1) && 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:783:2-783:8)
[Info][Witness] unassume invariant: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:734:2-734:9)
[Info][Witness] unassume invariant: ((state == 0 || state == 1) && state <= 1) && 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:781:3-781:17)
[Info][Witness] unassume invariant: ((state == 0 || state == 1) && state <= 1) && 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:782:3-782:12)
[Info][Witness] unassume invariant: (((((m2 == 0 || m2 == 1) && (m == 0 || m == 1)) && m2 <= 1) && m <= 1) && 0 <= m2) && 0 <= m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:696:1-700:1)
[Info][Witness] unassume invariant: (unsigned long )m == (unsigned long )(& m2) || (unsigned long )m == (unsigned long )(& m) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698:2-698:28)
[Info][Witness] unassume invariant: (((((m2 == 0 || m2 == 1) && (m == 0 || m == 1)) && m2 <= 1) && m <= 1) && 0 <= m2) && 0 <= m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699:2-699:8)
[Info][Witness] unassume invariant: ((state == 0 || state == 1) && state <= 1) && 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:784:3-784:33)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )arg) - (long long )r >= 0LL && (4294967295LL + (long long )arg) - (long long )r >= 0LL) && (4294967295LL - (long long )arg) + (long long )r >= 0LL) && (4294967296LL + (long long )arg) + (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:765:1-772:1)
[Info][Witness] unassume invariant: ((((r == -1 && -1 == r) && (2147483646LL - (long long )arg) - (long long )r >= 0LL) && (2147483647LL + (long long )arg) - (long long )r >= 0LL) && (2147483648LL - (long long )arg) + (long long )r >= 0LL) && (2147483649LL + (long long )arg) + (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:766:6-766:12)
[Info][Witness] unassume invariant: (((((r == -1 || r == 0) || r == 1) && r <= 127) && r <= 1) && -1 <= r) && -128 <= r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:767:6-767:35)
[Info][Witness] unassume invariant: (((((((((((4294967294LL - (long long )casret) - (long long )newTop >= 0LL && (4294967294LL - (long long )casret) - (long long )oldTop >= 0LL) && (4294967294LL - (long long )newTop) - (long long )oldTop >= 0LL) && (4294967295LL + (long long )casret) - (long long )newTop >= 0LL) && (4294967295LL + (long long )casret) - (long long )oldTop >= 0LL) && (4294967295LL + (long long )newTop) - (long long )oldTop >= 0LL) && (4294967295LL - (long long )casret) + (long long )newTop >= 0LL) && (4294967295LL - (long long )casret) + (long long )oldTop >= 0LL) && (4294967295LL - (long long )newTop) + (long long )oldTop >= 0LL) && (4294967296LL + (long long )casret) + (long long )newTop >= 0LL) && (4294967296LL + (long long )casret) + (long long )oldTop >= 0LL) && (4294967296LL + (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:742:1-760:1)
[Info][Witness] unassume invariant: (((((((((((((((((casret == -1 && newTop == casret) && oldTop == casret) && oldTop == newTop) && -1 == casret) && -1 == newTop) && -1 == oldTop) && (long long )casret - (long long )newTop >= 0LL) && (long long )casret - (long long )oldTop >= 0LL) && (long long )newTop - (long long )oldTop >= 0LL) && (-2LL - (long long )casret) - (long long )newTop >= 0LL) && (-2LL - (long long )casret) - (long long )oldTop >= 0LL) && (-2LL - (long long )newTop) - (long long )oldTop >= 0LL) && (0LL - (long long )casret) + (long long )newTop >= 0LL) && (0LL - (long long )casret) + (long long )oldTop >= 0LL) && (0LL - (long long )newTop) + (long long )oldTop >= 0LL) && (2LL + (long long )casret) + (long long )newTop >= 0LL) && (2LL + (long long )casret) + (long long )oldTop >= 0LL) && (2LL + (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:743:32-743:43)
[Info][Witness] unassume invariant: curr_alloc_idx == -1 && -1 == curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:721:6-721:25)
[Info][Witness] unassume invariant: (next_alloc_idx % 2 == 1 && -1 == curr_alloc_idx) && 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:722:2-722:31)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:723:5-723:35)
[Info][Witness] unassume invariant: -1 == curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:723:5-723:35)
[Info][Witness] unassume invariant: -1 == curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:724:3-724:32)
[Info][Witness] unassume invariant: 0 <= curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:725:3-725:21)
[Info][Witness] unassume invariant: (next_alloc_idx % 2 == 1 && -1 == curr_alloc_idx) && 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:723:5-723:35)
[Info][Witness] unassume invariant: ((curr_alloc_idx % 2 == 1 && next_alloc_idx % 2 == 1) && 1 <= curr_alloc_idx) && 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:727:3-727:34)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:728:3-728:22)
[Info][Witness] unassume invariant: next_alloc_idx % 2 == 1 && 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:728:3-728:22)
[Info][Witness] unassume invariant: 0 <= curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:729:3-729:32)
[Info][Witness] unassume invariant: ((((((oldTop == casret && -1 == casret) && -1 == oldTop) && (long long )casret - (long long )oldTop >= 0LL) && (-2LL - (long long )casret) - (long long )oldTop >= 0LL) && (0LL - (long long )casret) + (long long )oldTop >= 0LL) && (2LL + (long long )casret) + (long long )oldTop >= 0LL) && 0 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2-744:25)
[Info][Witness] unassume invariant: (((((((((((((oldTop == casret && -1 == casret) && -1 == oldTop) && (long long )casret - (long long )oldTop >= 0LL) && (-1LL - (long long )casret) - (long long )newTop >= 0LL) && (-1LL - (long long )newTop) - (long long )oldTop >= 0LL) && (-2LL - (long long )casret) - (long long )oldTop >= 0LL) && (1LL + (long long )casret) - (long long )newTop >= 0LL) && (-1LL + (long long )newTop) - (long long )oldTop >= 0LL) && (1LL - (long long )newTop) + (long long )oldTop >= 0LL) && (0LL - (long long )casret) + (long long )oldTop >= 0LL) && (-1LL - (long long )casret) + (long long )newTop >= 0LL) && (2LL + (long long )casret) + (long long )oldTop >= 0LL) && (1LL + (long long )casret) + (long long )newTop >= 0LL) && (1LL + (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:745:5-745:16)
[Info][Witness] unassume invariant: ((((((((newTop != 0 && casret == -1) && oldTop == casret) && -1 == casret) && -1 == oldTop) && (long long )casret - (long long )oldTop >= 0LL) && (-2LL - (long long )casret) - (long long )oldTop >= 0LL) && (0LL - (long long )casret) + (long long )oldTop >= 0LL) && (2LL + (long long )casret) + (long long )oldTop >= 0LL) && 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:745:5-745:16)
[Info][Witness] unassume invariant: ((((((((casret == -1 || casret == 0) && casret != 1) && newTop != 0) && casret <= 127) && casret <= 0) && 1 <= newTop) && -1 <= casret) && -1 <= oldTop) && -128 <= casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:748:3-748:23)
[Info][Witness] unassume invariant: ((((((((casret == -1 || casret == 0) && casret != 1) && newTop != 0) && casret <= 127) && casret <= 0) && 1 <= newTop) && -1 <= casret) && -1 <= oldTop) && -128 <= casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:755:7-755:16)
[Info][Witness] unassume invariant: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:750:4-750:29)
[Info][Witness] unassume invariant: 0 <= oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:751:4-751:16)
[Info][Witness] unassume invariant: (newTop != 0 && 1 <= newTop) && 0 <= oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:752:4-752:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:753:4-753:29)
[Info][Witness] unassume invariant: (newTop != 0 && 1 <= newTop) && 0 <= oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:753:4-753:29)
[Info][Witness] unassume invariant: (((unsigned long )v == (unsigned long )(& top) && 0 <= *v) && 0 <= top) && 0 <= e (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:701:1-715:1)
[Info][Witness] unassume invariant: (((((((-128 <= *r && -1 <= *r) && 0 <= top) && *r <= 0) && *r <= 127) && *r != 1) && (*r == -1 || *r == 0)) || ((0 <= *v && 1 <= u) && u != 0)) && (unsigned long )v == (unsigned long )(& top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:707:5-707:12)
[Info][Witness] unassume invariant: (((((((-128 <= *r && -1 <= *r) && 0 <= top) && *r <= 0) && *r <= 127) && *r != 1) && (*r == -1 || *r == 0)) || ((0 <= *v && 1 <= u) && u != 0)) && (unsigned long )v == (unsigned long )(& top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:709:3-709:17)
[Info][Witness] unassume invariant: (unsigned long )v == (unsigned long )(& top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:709:3-709:17)
[Info][Witness] unassume invariant: ((((((*r == -1 || *r == 0) && *r != 1) && (unsigned long )v == (unsigned long )(& top)) && *r <= 127) && *r <= 0) && -1 <= *r) && -128 <= *r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:707:5-707:12)
[Info][Witness] unassume invariant: (unsigned long )v == (unsigned long )(& top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:713:3-713:9)
[Info][Witness] unassume invariant: ((((casret == 0 || casret == 1) && newTop != 0) && casret <= 1) && 1 <= newTop) && 0 <= casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:754:4-754:53)
[Info][Witness] unassume invariant: ((r == 0 || r == 1) && r <= 1) && 0 <= r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:769:3-769:16)
[Info][Witness] unassume invariant: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:736:1-741:1)
[Info][Witness] unassume invariant: (((((r == -1 || r == 0) || r == 1) && r <= 127) && r <= 1) && -1 <= r) && -128 <= r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:770:5-770:32)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:74:1-78:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:79:1-83:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:84:1-88:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:89:1-93:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:94:1-98:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
  on line 794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:794-794)
[Warning][Deadcode] Function 'push' has dead code:
  on line 760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:760-760)
[Warning][Deadcode] Function 'push_loop' has dead code:
  on line 772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:772-772)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 69
  dead: 8 (5 in uncalled functions)
  total lines: 77
[Warning][Race] Memory location next_alloc_idx (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:717:5-717:23)
  write with region:{next_alloc_idx} (conf. 110)  (exp: & next_alloc_idx) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:728:3-728:22)
  write with [region:{next_alloc_idx}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:793:13-793:43]] (conf. 110)  (exp: & next_alloc_idx) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:728:3-728:22)
  read with region:{next_alloc_idx} (conf. 110)  (exp: & next_alloc_idx) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:723:5-723:35)
  read with [region:{next_alloc_idx}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:793:13-793:43]] (conf. 110)  (exp: & next_alloc_idx) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:723:5-723:35)
  read with region:{next_alloc_idx} (conf. 110)  (exp: & next_alloc_idx) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:727:3-727:34)
  read with [region:{next_alloc_idx}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:793:13-793:43]] (conf. 110)  (exp: & next_alloc_idx) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:727:3-727:34)
  read with region:{next_alloc_idx} (conf. 110)  (exp: & next_alloc_idx) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:728:3-728:22)
  read with [region:{next_alloc_idx}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:793:13-793:43]] (conf. 110)  (exp: & next_alloc_idx) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:728:3-728:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:768:8-768:9)
[Warning][Race] Memory location memory[?] (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:716:5-716:22)
  write with region:{memory[?]} (conf. 110)  (exp: & memory[newTop]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:748:3-748:23)
  write with [region:{memory[?]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:793:13-793:43]] (conf. 110)  (exp: & memory[newTop]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:748:3-748:23)
  write with region:{memory[?]} (conf. 110)  (exp: & memory[newTop + 1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:753:4-753:29)
  write with [region:{memory[?]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:793:13-793:43]] (conf. 110)  (exp: & memory[newTop + 1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:753:4-753:29)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:793:8-793:9)
[Warning][Race] Memory location top (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:719:5-719:8)
  write with [region:{top}, lock:{[__VERIFIER_atomic]}] (conf. 110)  (exp: & *v) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:709:3-709:17)
  write with [region:{top}, lock:{[__VERIFIER_atomic]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:793:13-793:43]] (conf. 110)  (exp: & *v) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:709:3-709:17)
  write with region:{top} (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:734:2-734:9)
  write with [region:{top}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:793:13-793:43]] (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:734:2-734:9)
  read with [region:{top}, lock:{[__VERIFIER_atomic]}] (conf. 110)  (exp: & *v) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:707:5-707:12)
  read with [region:{top}, lock:{[__VERIFIER_atomic]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:793:13-793:43]] (conf. 110)  (exp: & *v) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:707:5-707:12)
  read with [region:{top}, lock:{[__VERIFIER_atomic]}] (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:737:5-737:13)
  read with [region:{top}, lock:{[__VERIFIER_atomic]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:793:13-793:43]] (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:737:5-737:13)
  read with [region:{top}, lock:{[__VERIFIER_atomic]}] (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:751:4-751:16)
  read with [region:{top}, lock:{[__VERIFIER_atomic]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:793:13-793:43]] (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:751:4-751:16)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:17:73-17:74)
[Warning][Race] Memory location state (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:774:5-774:14)
  write with region:{state} (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:782:3-782:12)
  write with [region:{state}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:793:13-793:43]] (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:782:3-782:12)
  read with region:{state} (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:780:2-780:8)
  read with [region:{state}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:793:13-793:43]] (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:780:2-780:8)
  read with region:{state} (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:783:2-783:8)
  read with [region:{state}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:793:13-793:43]] (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:783:2-783:8)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:749:10-749:11)
[Success][Witness] invariant confirmed: 0 <= e (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:707:2)
[Success][Witness] invariant confirmed: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:707:2)
[Success][Witness] invariant confirmed: 0 <= *v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:707:2)
[Success][Witness] invariant confirmed: v == & top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:707:2)
[Success][Witness] invariant confirmed: 0 <= oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:752:4)
[Success][Witness] invariant confirmed: 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:783:2)
[Success][Witness] invariant confirmed: state <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:783:2)
[Success][Witness] invariant confirmed: state == 0 || state == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:783:2)
[Success][Witness] invariant confirmed: 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:728:3)
[Success][Witness] invariant confirmed: 1 <= curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:728:3)
[Warning][Witness] invariant unconfirmed: next_alloc_idx % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:728:3)
[Warning][Witness] invariant unconfirmed: curr_alloc_idx % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:728:3)
[Success][Witness] invariant confirmed: 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:780:2)
[Success][Witness] invariant confirmed: state <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:780:2)
[Success][Witness] invariant confirmed: state == 0 || state == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:780:2)
[Success][Witness] invariant confirmed: 0 <= m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:700:1)
[Success][Witness] invariant confirmed: 0 <= m2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:700:1)
[Success][Witness] invariant confirmed: m <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:700:1)
[Success][Witness] invariant confirmed: m2 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:700:1)
[Success][Witness] invariant confirmed: m == 0 || m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:700:1)
[Success][Witness] invariant confirmed: m2 == 0 || m2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:700:1)
[Success][Witness] invariant confirmed: 0 <= oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:753:4)
[Success][Witness] invariant confirmed: 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:753:4)
[Success][Witness] invariant confirmed: newTop != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:753:4)
[Success][Witness] invariant confirmed: 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:785:3)
[Success][Witness] invariant confirmed: state <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:785:3)
[Success][Witness] invariant confirmed: state == 0 || state == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:785:3)
[Success][Witness] invariant confirmed: (2147483649LL + (long long )arg) + (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:767:2)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )arg) + (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:767:2)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )arg) - (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:767:2)
[Success][Witness] invariant confirmed: (2147483646LL - (long long )arg) - (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:767:2)
[Success][Witness] invariant confirmed: -1 == r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:767:2)
[Success][Witness] invariant confirmed: r == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:767:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

[Warning][Witness] invariant unconfirmed: m == & m2 || m == & m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

[Success][Witness] invariant confirmed: 0 <= oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:754:4)
[Success][Witness] invariant confirmed: 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:754:4)
[Success][Witness] invariant confirmed: newTop != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:754:4)
[Success][Witness] invariant confirmed: v == & top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:709:3)
[Success][Witness] invariant confirmed: ((((((-128 <= *r && -1 <= *r) && 0 <= top) && *r <= 0) && *r <= 127) && *r != 1) && (*r == -1 || *r == 0)) || ((0 <= *v && 1 <= u) && u != 0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:709:3)
[Success][Witness] invariant confirmed: (2LL + (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: (2LL + (long long )casret) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: (2LL + (long long )casret) + (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: (0LL - (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: (0LL - (long long )casret) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: (0LL - (long long )casret) + (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: (-2LL - (long long )newTop) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: (-2LL - (long long )casret) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: (-2LL - (long long )casret) - (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: (long long )newTop - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: (long long )casret - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: (long long )casret - (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: -1 == newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: -1 == casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: oldTop == newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: oldTop == casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: newTop == casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: casret == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:744:2)
[Success][Witness] invariant confirmed: 0 <= r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:770:5)
[Success][Witness] invariant confirmed: r <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:770:5)
[Success][Witness] invariant confirmed: r == 0 || r == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:770:5)
[Success][Witness] invariant confirmed: 0 <= m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698:2)
[Success][Witness] invariant confirmed: 0 <= m2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698:2)
[Success][Witness] invariant confirmed: m <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698:2)
[Success][Witness] invariant confirmed: m2 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698:2)
[Success][Witness] invariant confirmed: m == 0 || m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698:2)
[Success][Witness] invariant confirmed: m2 == 0 || m2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

[Success][Witness] invariant confirmed: 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:729:3)
[Warning][Witness] invariant unconfirmed: next_alloc_idx % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:729:3)
[Success][Witness] invariant confirmed: -1 == curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:725:3)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )arg) + (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:766:2)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )arg) + (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:766:2)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )arg) - (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:766:2)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )arg) - (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:766:2)
[Success][Witness] invariant confirmed: 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:727:3)
[Success][Witness] invariant confirmed: -1 == curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:727:3)
[Warning][Witness] invariant unconfirmed: next_alloc_idx % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:727:3)
[Success][Witness] invariant confirmed: 0 <= curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:731:2)
[Success][Witness] invariant confirmed: 0 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:745:2)
[Success][Witness] invariant confirmed: (2LL + (long long )casret) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:745:2)
[Success][Witness] invariant confirmed: (0LL - (long long )casret) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:745:2)
[Success][Witness] invariant confirmed: (-2LL - (long long )casret) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:745:2)
[Success][Witness] invariant confirmed: (long long )casret - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:745:2)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:745:2)
[Success][Witness] invariant confirmed: -1 == casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:745:2)
[Success][Witness] invariant confirmed: oldTop == casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:745:2)
[Success][Witness] invariant confirmed: 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:723:2)
[Success][Witness] invariant confirmed: -1 == curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:723:2)
[Warning][Witness] invariant unconfirmed: next_alloc_idx % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:723:2)
[Success][Witness] invariant confirmed: 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:784:3)
[Success][Witness] invariant confirmed: state <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:784:3)
[Success][Witness] invariant confirmed: state == 0 || state == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:784:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

[Warning][Witness] invariant unconfirmed: m == & m2 || m == & m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

[Success][Witness] invariant confirmed: 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:748:3)
[Success][Witness] invariant confirmed: (2LL + (long long )casret) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:748:3)
[Success][Witness] invariant confirmed: (0LL - (long long )casret) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:748:3)
[Success][Witness] invariant confirmed: (-2LL - (long long )casret) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:748:3)
[Success][Witness] invariant confirmed: (long long )casret - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:748:3)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:748:3)
[Success][Witness] invariant confirmed: -1 == casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:748:3)
[Success][Witness] invariant confirmed: oldTop == casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:748:3)
[Success][Witness] invariant confirmed: casret == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:748:3)
[Success][Witness] invariant confirmed: newTop != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:748:3)
[Success][Witness] invariant confirmed: -1 == curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:722:2)
[Success][Witness] invariant confirmed: curr_alloc_idx == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:722:2)
[Success][Witness] invariant confirmed: -1 == curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:724:3)
[Success][Witness] invariant confirmed: v == & top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:715:1)
[Success][Witness] invariant confirmed: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:737:2)
[Success][Witness] invariant confirmed: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:735:1)
[Success][Witness] invariant confirmed: 0 <= casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:755:4)
[Success][Witness] invariant confirmed: 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:755:4)
[Success][Witness] invariant confirmed: casret <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:755:4)
[Success][Witness] invariant confirmed: newTop != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:755:4)
[Success][Witness] invariant confirmed: casret == 0 || casret == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:755:4)
[Success][Witness] invariant confirmed: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:751:4)
[Success][Witness] invariant confirmed: 0 <= m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693:2)
[Success][Witness] invariant confirmed: 0 <= m2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693:2)
[Success][Witness] invariant confirmed: m <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693:2)
[Success][Witness] invariant confirmed: m2 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693:2)
[Success][Witness] invariant confirmed: m == 0 || m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693:2)
[Success][Witness] invariant confirmed: m2 == 0 || m2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

[Success][Witness] invariant confirmed: (1LL + (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:746:3)
[Success][Witness] invariant confirmed: (1LL + (long long )casret) + (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:746:3)
[Success][Witness] invariant confirmed: (2LL + (long long )casret) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:746:3)
[Success][Witness] invariant confirmed: (-1LL - (long long )casret) + (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:746:3)
[Success][Witness] invariant confirmed: (0LL - (long long )casret) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:746:3)
[Success][Witness] invariant confirmed: (1LL - (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:746:3)
[Success][Witness] invariant confirmed: (-1LL + (long long )newTop) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:746:3)
[Success][Witness] invariant confirmed: (1LL + (long long )casret) - (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:746:3)
[Success][Witness] invariant confirmed: (-2LL - (long long )casret) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:746:3)
[Success][Witness] invariant confirmed: (-1LL - (long long )newTop) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:746:3)
[Success][Witness] invariant confirmed: (-1LL - (long long )casret) - (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:746:3)
[Success][Witness] invariant confirmed: (long long )casret - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:746:3)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:746:3)
[Success][Witness] invariant confirmed: -1 == casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:746:3)
[Success][Witness] invariant confirmed: oldTop == casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:746:3)
[Success][Witness] invariant confirmed: 0 <= m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:695:1)
[Success][Witness] invariant confirmed: 0 <= m2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:695:1)
[Success][Witness] invariant confirmed: m <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:695:1)
[Success][Witness] invariant confirmed: m2 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:695:1)
[Success][Witness] invariant confirmed: m == 0 || m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:695:1)
[Success][Witness] invariant confirmed: m2 == 0 || m2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:695:1)
[Success][Witness] invariant confirmed: 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:782:3)
[Success][Witness] invariant confirmed: state <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:782:3)
[Success][Witness] invariant confirmed: state == 0 || state == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:782:3)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:743:2)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )casret) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:743:2)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )casret) + (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:743:2)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:743:2)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )casret) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:743:2)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )casret) + (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:743:2)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )newTop) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:743:2)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )casret) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:743:2)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )casret) - (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:743:2)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )newTop) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:743:2)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )casret) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:743:2)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )casret) - (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:743:2)
[Success][Witness] invariant confirmed: -128 <= *r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:713:3)
[Success][Witness] invariant confirmed: -1 <= *r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:713:3)
[Success][Witness] invariant confirmed: *r <= 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:713:3)
[Success][Witness] invariant confirmed: *r <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:713:3)
[Success][Witness] invariant confirmed: v == & top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:713:3)
[Success][Witness] invariant confirmed: *r != 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:713:3)
[Success][Witness] invariant confirmed: *r == -1 || *r == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:713:3)
[Success][Witness] invariant confirmed: -128 <= casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:749:3)
[Success][Witness] invariant confirmed: -1 <= oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:749:3)
[Success][Witness] invariant confirmed: -1 <= casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:749:3)
[Success][Witness] invariant confirmed: 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:749:3)
[Success][Witness] invariant confirmed: casret <= 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:749:3)
[Success][Witness] invariant confirmed: casret <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:749:3)
[Success][Witness] invariant confirmed: newTop != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:749:3)
[Success][Witness] invariant confirmed: casret != 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:749:3)
[Success][Witness] invariant confirmed: casret == -1 || casret == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:749:3)
[Success][Witness] invariant confirmed: -128 <= r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:768:2)
[Success][Witness] invariant confirmed: -1 <= r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:768:2)
[Success][Witness] invariant confirmed: r <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:768:2)
[Success][Witness] invariant confirmed: r <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:768:2)
[Success][Witness] invariant confirmed: (r == -1 || r == 0) || r == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/26_stack_cas_longest-1.i:768:2)
[Info][Witness] witness validation summary:
  confirmed: 171
  unconfirmed: 7
  refuted: 0
  error: 8
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 186
SV-COMP result: ERROR (witness error)
[Info][Race] Memory locations race summary:
  safe: 2
  vulnerable: 0
  unsafe: 4
  total memory locations: 6
