./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/25_stack.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/25_stack.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/25_stack.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_release, abort, i, key, count, a, tmp, count, i, j, i___0, j___0, k, size, r, top___0, r, arg, tmp, tmp, newTop, d, oldTop, curr_alloc_idx, 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/25_stack.i:699:2)
[Info][Witness] invariant has undefined variables or side effects: 0 <= *m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:699:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.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/25_stack.i:699:2)
[Info][Witness] invariant has undefined variables or side effects: *m <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:699:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.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/25_stack.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/25_stack.i:699:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.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/25_stack.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/25_stack.i:693:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

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

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

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

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

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

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

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

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

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

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

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:693: 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/25_stack.i:694:2)
[Info][Witness] invariant has undefined variables or side effects: 0 <= *m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:694:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.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/25_stack.i:694:2)
[Info][Witness] invariant has undefined variables or side effects: *m <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:694:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.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/25_stack.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/25_stack.i:694:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.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/25_stack.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/25_stack.i:698:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

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

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

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

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

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

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

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

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

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

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

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:698: 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/25_stack.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/25_stack.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/25_stack.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/25_stack.i:763:2-763:32)
[Info][Witness] unassume invariant: ((state == 0 || state == 1) && state <= 1) && 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:766:2-766:8)
[Info][Witness] unassume invariant: ((state == 0 || state == 1) && state <= 1) && 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:769:2-769:8)
[Info][Witness] unassume invariant: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:719:2-719:9)
[Info][Witness] unassume invariant: ((state == 0 || state == 1) && state <= 1) && 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:767:3-767:17)
[Info][Witness] unassume invariant: ((state == 0 || state == 1) && state <= 1) && 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:768:3-768: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/25_stack.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/25_stack.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/25_stack.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/25_stack.i:770:3-770: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/25_stack.i:751:1-758: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/25_stack.i:752:6-752: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/25_stack.i:753:6-753:35)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )newTop) - (long long )oldTop >= 0LL && (4294967295LL + (long long )newTop) - (long long )oldTop >= 0LL) && (4294967295LL - (long long )newTop) + (long long )oldTop >= 0LL) && (4294967296LL + (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:727:1-743:1)
[Info][Witness] unassume invariant: ((((((newTop == -1 && oldTop == newTop) && -1 == newTop) && -1 == oldTop) && (long long )newTop - (long long )oldTop >= 0LL) && (-2LL - (long long )newTop) - (long long )oldTop >= 0LL) && (0LL - (long long )newTop) + (long long )oldTop >= 0LL) && (2LL + (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:728:19-728:30)
[Info][Witness] unassume invariant: curr_alloc_idx == -1 && -1 == curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:706:6-706: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/25_stack.i:707:2-707:31)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:708:5-708:34)
[Info][Witness] unassume invariant: -1 == curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:708:5-708:34)
[Info][Witness] unassume invariant: -1 == curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:709:3-709:32)
[Info][Witness] unassume invariant: 0 <= curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:710:3-710: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/25_stack.i:708:5-708:34)
[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/25_stack.i:712:3-712:34)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:713:3-713:22)
[Info][Witness] unassume invariant: next_alloc_idx % 2 == 1 && 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:713:3-713:22)
[Info][Witness] unassume invariant: 0 <= curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:714:3-714:32)
[Info][Witness] unassume invariant: -1 == oldTop && 0 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:729:2-729:25)
[Info][Witness] unassume invariant: (((-1 == oldTop && (-1LL - (long long )newTop) - (long long )oldTop >= 0LL) && (-1LL + (long long )newTop) - (long long )oldTop >= 0LL) && (1LL - (long long )newTop) + (long long )oldTop >= 0LL) && (1LL + (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:730:5-730:16)
[Info][Witness] unassume invariant: (newTop != 0 && -1 == oldTop) && 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:730:5-730:16)
[Info][Witness] unassume invariant: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:733:3-733:23)
[Info][Witness] unassume invariant: -1 == oldTop && 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:734:3-734:32)
[Info][Witness] unassume invariant: (newTop != 0 && 1 <= newTop) && 0 <= oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:735:3-735:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:736:3-736:28)
[Info][Witness] unassume invariant: newTop != 0 && 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:737:3-737:28)
[Info][Witness] unassume invariant: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:738:3-738:15)
[Info][Witness] unassume invariant: ((r == 0 || r == 1) && r <= 1) && 0 <= r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:755:3-755:16)
[Info][Witness] unassume invariant: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:721:1-726: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/25_stack.i:756:5-756:32)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:74:1-78:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:79:1-83:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:84:1-88:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:89:1-93:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:94:1-98:1)
[Warning][Deadcode] Function 'init' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:744:1-746:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
  on line 780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:780-780)
[Warning][Deadcode] Function 'push_loop' has dead code:
  on line 758 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:758-758)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 64
  dead: 9 (7 in uncalled functions)
  total lines: 73
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:754:8-754:9)
[Warning][Race] Memory location memory[?] (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:701:5-701:21)
  write with region:{memory[?]} (conf. 110)  (exp: & memory[newTop]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:733:3-733:23)
  write with [region:{memory[?]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:779:13-779:43]] (conf. 110)  (exp: & memory[newTop]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:733:3-733:23)
  write with region:{memory[?]} (conf. 110)  (exp: & memory[newTop + 1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:736:3-736:28)
  write with [region:{memory[?]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:779:13-779:43]] (conf. 110)  (exp: & memory[newTop + 1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:736:3-736:28)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:779:8-779:9)
[Warning][Race] Memory location top (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:704:5-704:8)
  write with region:{top} (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:719:2-719:9)
  write with [region:{top}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:779:13-779:43]] (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:719:2-719:9)
  write with [region:{top}, lock:{[__VERIFIER_atomic]}] (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:738:3-738:15)
  write with [region:{top}, lock:{[__VERIFIER_atomic]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:779:13-779:43]] (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:738:3-738:15)
  read with [region:{top}, lock:{[__VERIFIER_atomic]}] (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:722:5-722:13)
  read with [region:{top}, lock:{[__VERIFIER_atomic]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:779:13-779:43]] (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:722:5-722:13)
  read with region:{top} (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:735:3-735:15)
  read with [region:{top}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:779:13-779:43]] (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:735:3-735:15)
[Warning][Race] Memory location state (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:760:5-760:14)
  write with region:{state} (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:768:3-768:12)
  write with [region:{state}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:779:13-779:43]] (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:768:3-768:12)
  read with region:{state} (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:766:2-766:8)
  read with [region:{state}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:779:13-779:43]] (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:766:2-766:8)
  read with region:{state} (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:769:2-769:8)
  read with [region:{state}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:779:13-779:43]] (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:769:2-769:8)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:17:73-17:74)
[Warning][Race] Memory location next_alloc_idx (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:702:5-702:23)
  write with region:{next_alloc_idx} (conf. 110)  (exp: & next_alloc_idx) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:713:3-713:22)
  write with [region:{next_alloc_idx}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:779:13-779:43]] (conf. 110)  (exp: & next_alloc_idx) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:713:3-713:22)
  read with region:{next_alloc_idx} (conf. 110)  (exp: & next_alloc_idx) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:708:5-708:34)
  read with [region:{next_alloc_idx}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:779:13-779:43]] (conf. 110)  (exp: & next_alloc_idx) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:708:5-708:34)
  read with region:{next_alloc_idx} (conf. 110)  (exp: & next_alloc_idx) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:712:3-712:34)
  read with [region:{next_alloc_idx}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:779:13-779:43]] (conf. 110)  (exp: & next_alloc_idx) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:712:3-712:34)
  read with region:{next_alloc_idx} (conf. 110)  (exp: & next_alloc_idx) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:713:3-713:22)
  read with [region:{next_alloc_idx}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:779:13-779:43]] (conf. 110)  (exp: & next_alloc_idx) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:713:3-713:22)
[Success][Witness] invariant confirmed: 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:712:3)
[Success][Witness] invariant confirmed: -1 == curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:712:3)
[Warning][Witness] invariant unconfirmed: next_alloc_idx % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:712:3)
[Success][Witness] invariant confirmed: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:739:3)
[Success][Witness] invariant confirmed: 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:733:3)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:733:3)
[Success][Witness] invariant confirmed: newTop != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:733:3)
[Success][Witness] invariant confirmed: 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:738:3)
[Success][Witness] invariant confirmed: newTop != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:738:3)
[Success][Witness] invariant confirmed: 0 <= m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:695:1)
[Success][Witness] invariant confirmed: 0 <= m2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:695:1)
[Success][Witness] invariant confirmed: m <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:695:1)
[Success][Witness] invariant confirmed: m2 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:695:1)
[Success][Witness] invariant confirmed: m == 0 || m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:695:1)
[Success][Witness] invariant confirmed: m2 == 0 || m2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:695:1)
[Success][Witness] invariant confirmed: 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:766:2)
[Success][Witness] invariant confirmed: state <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:766:2)
[Success][Witness] invariant confirmed: state == 0 || state == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:766:2)
[Success][Witness] invariant confirmed: 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:768:3)
[Success][Witness] invariant confirmed: state <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:768:3)
[Success][Witness] invariant confirmed: state == 0 || state == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:768:3)
[Success][Witness] invariant confirmed: 0 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:730:2)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:730:2)
[Success][Witness] invariant confirmed: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:720:1)
[Success][Witness] invariant confirmed: 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:713:3)
[Success][Witness] invariant confirmed: 1 <= curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:713:3)
[Warning][Witness] invariant unconfirmed: next_alloc_idx % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:713:3)
[Warning][Witness] invariant unconfirmed: curr_alloc_idx % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:713:3)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )arg) + (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:752:2)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )arg) + (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:752:2)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )arg) - (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:752:2)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )arg) - (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:752:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

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

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

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

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

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

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

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

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

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

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

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.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/25_stack.i:699:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:699: Error: Expecting a pointer type in *. Got TInt(int,
)

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

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

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

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

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

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

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

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

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

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

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

[Success][Witness] invariant confirmed: -1 == curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:707:2)
[Success][Witness] invariant confirmed: curr_alloc_idx == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:707:2)
[Success][Witness] invariant confirmed: 0 <= curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:716:2)
[Success][Witness] invariant confirmed: 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:714:3)
[Warning][Witness] invariant unconfirmed: next_alloc_idx % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:714:3)
[Success][Witness] invariant confirmed: (2LL + (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:729:2)
[Success][Witness] invariant confirmed: (0LL - (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:729:2)
[Success][Witness] invariant confirmed: (-2LL - (long long )newTop) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:729:2)
[Success][Witness] invariant confirmed: (long long )newTop - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:729:2)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:729:2)
[Success][Witness] invariant confirmed: -1 == newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:729:2)
[Success][Witness] invariant confirmed: oldTop == newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:729:2)
[Success][Witness] invariant confirmed: newTop == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:729:2)
[Success][Witness] invariant confirmed: 0 <= m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:693:2)
[Success][Witness] invariant confirmed: 0 <= m2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:693:2)
[Success][Witness] invariant confirmed: m <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:693:2)
[Success][Witness] invariant confirmed: m2 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:693:2)
[Success][Witness] invariant confirmed: m == 0 || m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:693:2)
[Success][Witness] invariant confirmed: m2 == 0 || m2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:693:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:693: Error: Expecting a pointer type in *. Got TInt(int,
)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

[Success][Witness] invariant confirmed: 0 <= r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:756:5)
[Success][Witness] invariant confirmed: r <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:756:5)
[Success][Witness] invariant confirmed: r == 0 || r == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:756:5)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

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

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

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

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

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

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

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

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

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

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

/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.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/25_stack.i:694:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:694: Error: Expecting a pointer type in *. Got TInt(int,
)

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

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

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

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

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

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

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

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

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

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

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

[Success][Witness] invariant confirmed: (2147483649LL + (long long )arg) + (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:753:2)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )arg) + (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:753:2)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )arg) - (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:753:2)
[Success][Witness] invariant confirmed: (2147483646LL - (long long )arg) - (long long )r >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:753:2)
[Success][Witness] invariant confirmed: -1 == r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:753:2)
[Success][Witness] invariant confirmed: r == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:753:2)
[Success][Witness] invariant confirmed: 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:769:2)
[Success][Witness] invariant confirmed: state <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:769:2)
[Success][Witness] invariant confirmed: state == 0 || state == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:769:2)
[Success][Witness] invariant confirmed: 0 <= m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:698:2)
[Success][Witness] invariant confirmed: 0 <= m2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:698:2)
[Success][Witness] invariant confirmed: m <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:698:2)
[Success][Witness] invariant confirmed: m2 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:698:2)
[Success][Witness] invariant confirmed: m == 0 || m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:698:2)
[Success][Witness] invariant confirmed: m2 == 0 || m2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:698:2)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:698: Error: Expecting a pointer type in *. Got TInt(int,
)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

[Success][Witness] invariant confirmed: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:735:3)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:735:3)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:734:3)
[Success][Witness] invariant confirmed: (1LL + (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:731:3)
[Success][Witness] invariant confirmed: (1LL - (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:731:3)
[Success][Witness] invariant confirmed: (-1LL + (long long )newTop) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:731:3)
[Success][Witness] invariant confirmed: (-1LL - (long long )newTop) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:731:3)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:731:3)
[Success][Witness] invariant confirmed: 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:708:2)
[Success][Witness] invariant confirmed: -1 == curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:708:2)
[Warning][Witness] invariant unconfirmed: next_alloc_idx % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:708:2)
[Success][Witness] invariant confirmed: -1 == curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:710:3)
[Success][Witness] invariant confirmed: 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:770:3)
[Success][Witness] invariant confirmed: state <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:770:3)
[Success][Witness] invariant confirmed: state == 0 || state == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:770:3)
[Success][Witness] invariant confirmed: 0 <= m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:700:1)
[Success][Witness] invariant confirmed: 0 <= m2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:700:1)
[Success][Witness] invariant confirmed: m <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:700:1)
[Success][Witness] invariant confirmed: m2 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:700:1)
[Success][Witness] invariant confirmed: m == 0 || m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:700:1)
[Success][Witness] invariant confirmed: m2 == 0 || m2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:700:1)
[Success][Witness] invariant confirmed: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:722:2)
[Success][Witness] invariant confirmed: 0 <= state (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:771:3)
[Success][Witness] invariant confirmed: state <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:771:3)
[Success][Witness] invariant confirmed: state == 0 || state == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:771:3)
[Success][Witness] invariant confirmed: 0 <= oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:736:3)
[Success][Witness] invariant confirmed: 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:736:3)
[Success][Witness] invariant confirmed: newTop != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:736:3)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:728:2)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:728:2)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )newTop) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:728:2)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )newTop) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:728:2)
[Success][Witness] invariant confirmed: -1 == curr_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:709:3)
[Success][Witness] invariant confirmed: -128 <= r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:754:2)
[Success][Witness] invariant confirmed: -1 <= r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:754:2)
[Success][Witness] invariant confirmed: r <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:754:2)
[Success][Witness] invariant confirmed: r <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:754:2)
[Success][Witness] invariant confirmed: (r == -1 || r == 0) || r == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack.i:754:2)
[Info][Witness] witness validation summary:
  confirmed: 102
  unconfirmed: 7
  refuted: 0
  error: 8
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 117
SV-COMP result: ERROR (witness error)
[Info][Race] Memory locations race summary:
  safe: 2
  vulnerable: 0
  unsafe: 4
  total memory locations: 6
