./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/28-race_reach_78-equ_racing.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/28-race_reach_78-equ_racing.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/goblint-regression/28-race_reach_78-equ_racing.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] pthread_mutex_lock, pthread_mutex_unlock, i, key, count, a, tmp, count, i, j, i___0, j___0, k, size, r, top, x, d, m, i, i___0, tmp, t_ids, tmp___0, tmp, __x, __x, __x
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: (((((((((unsigned long )s == (unsigned long )(& B) && (s->inside.x == 0 && s->inside.y == 0)) || ((unsigned long )s == (unsigned long )(& A) && (s->inside.x == 0 && s->inside.y == 0))) && ((unsigned long )m == (unsigned long )(& A.mutex) || (unsigned long )m == (unsigned long )(& B.mutex))) && ((unsigned long )d == (unsigned long )(& B.datum) || (unsigned long )d == (unsigned long )(& A.datum))) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum)) && -2147483647 <= x) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:378-1038:380)
[Info][Witness] unassume invariant: x != 2147483647 && x <= 2147483646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1021:7-1021:22)
[Info][Witness] unassume invariant: (((((x != 2147483647 && x != 0) && s->inside.y == 0) && s->inside.x == 0) && s->datum == 0) && (unsigned long )s == (unsigned long )(& A)) && x <= 2147483646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1028:4-1028:10)
[Info][Witness] unassume invariant: (((unsigned long )s == (unsigned long )(& B) && (s->datum == 0 && (s->inside.x == 0 && s->inside.y == 0))) || ((unsigned long )s == (unsigned long )(& A) && (s->datum == 0 && (s->inside.x == 0 && s->inside.y == 0)))) && -2147483647 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1029:4-1029:7)
[Info][Witness] unassume invariant: (((s->inside.y == 0 && s->inside.x == 0) && s->datum == 0) && (unsigned long )s == (unsigned long )(& B)) && x == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1031:4-1031:10)
[Info][Witness] unassume invariant: (((unsigned long )s == (unsigned long )(& B) && (s->datum == 0 && (s->inside.x == 0 && s->inside.y == 0))) || ((unsigned long )s == (unsigned long )(& A) && (s->datum == 0 && (s->inside.x == 0 && s->inside.y == 0)))) && -2147483647 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1032:4-1032:7)
[Info][Witness] unassume invariant: ((((unsigned long )s == (unsigned long )(& B) && (s->datum == 0 && (s->inside.x == 0 && s->inside.y == 0))) || ((unsigned long )s == (unsigned long )(& A) && (s->datum == 0 && (s->inside.x == 0 && s->inside.y == 0)))) && ((unsigned long )m == (unsigned long )(& B.mutex) || (unsigned long )m == (unsigned long )(& A.mutex))) && (unsigned long )m == (unsigned long )(& s->mutex) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1034:3-1034:16)
[Info][Witness] unassume invariant: ((((unsigned long )d == (unsigned long )(& B.datum) && *d == 0) || ((unsigned long )d == (unsigned long )(& A.datum) && *d == 0)) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1035:3-1035:16)
[Info][Witness] unassume invariant: (((((((((((A.datum == 0 && A.inside.x == 0) && A.inside.y == 0) && B.datum == 0) && B.inside.x == 0) && B.inside.y == 0) && (((unsigned long )s == (unsigned long )(& B) && (s->datum == 0 && (s->inside.x == 0 && s->inside.y == 0))) || ((unsigned long )s == (unsigned long )(& A) && (s->datum == 0 && (s->inside.x == 0 && s->inside.y == 0))))) && (((unsigned long )d == (unsigned long )(& B.datum) && *d == 0) || ((unsigned long )d == (unsigned long )(& A.datum) && *d == 0))) || (((unsigned long )d == (unsigned long )(& B.datum) || (unsigned long )d == (unsigned long )(& A.datum)) && (((unsigned long )s == (unsigned long )(& B) && (s->inside.x == 0 && s->inside.y == 0)) || ((unsigned long )s == (unsigned long )(& A) && (s->inside.x == 0 && s->inside.y == 0))))) && ((unsigned long )m == (unsigned long )(& B.mutex) || (unsigned long )m == (unsigned long )(& A.mutex))) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum)) && -2147483647 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1036:36-1036:39)
[Info][Witness] unassume invariant: (unsigned long )m == (unsigned long )(& s->mutex) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1036:31-1036:53)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:393-1013:395)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1012:3-1012:31)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:406-1013:408)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:12-1013:35)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:248-1013:250)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:261-1013:263)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:143-1013:145)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:84-1013:94)
[Info][Witness] unassume invariant: -2147483647 <= B.datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:84-1013:94)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:189-1013:199)
[Info][Witness] unassume invariant: B.datum <= 2147483646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:189-1013:199)
[Info][Witness] unassume invariant: (((((((((((A.datum == 0 && A.inside.x == 0) && A.inside.y == 0) && B.datum == 0) && B.inside.x == 0) && B.inside.y == 0) && (((unsigned long )s == (unsigned long )(& B) && (s->datum == 0 && (s->inside.x == 0 && s->inside.y == 0))) || ((unsigned long )s == (unsigned long )(& A) && (s->datum == 0 && (s->inside.x == 0 && s->inside.y == 0))))) && (((unsigned long )d == (unsigned long )(& B.datum) && *d == 0) || ((unsigned long )d == (unsigned long )(& A.datum) && *d == 0))) || (((unsigned long )d == (unsigned long )(& B.datum) || (unsigned long )d == (unsigned long )(& A.datum)) && (((unsigned long )s == (unsigned long )(& B) && (s->inside.x == 0 && s->inside.y == 0)) || ((unsigned long )s == (unsigned long )(& A) && (s->inside.x == 0 && s->inside.y == 0))))) && ((unsigned long )m == (unsigned long )(& B.mutex) || (unsigned long )m == (unsigned long )(& A.mutex))) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum)) && -2147483647 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1036:36-1036:39)
[Info][Witness] unassume invariant: (((unsigned long )m == (unsigned long )(& B.mutex) || (unsigned long )m == (unsigned long )(& A.mutex)) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1036:31-1036:53)
[Info][Witness] unassume invariant: (((((((((unsigned long )s == (unsigned long )(& B) && (s->inside.x == 0 && s->inside.y == 0)) || ((unsigned long )s == (unsigned long )(& A) && (s->inside.x == 0 && s->inside.y == 0))) && ((unsigned long )m == (unsigned long )(& A.mutex) || (unsigned long )m == (unsigned long )(& B.mutex))) && ((unsigned long )d == (unsigned long )(& B.datum) || (unsigned long )d == (unsigned long )(& A.datum))) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum)) && -2147483647 <= x) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1037:3-1037:24)
[Info][Witness] unassume invariant: (((((((((unsigned long )s == (unsigned long )(& B) && (s->inside.x == 0 && s->inside.y == 0)) || ((unsigned long )s == (unsigned long )(& A) && (s->inside.x == 0 && s->inside.y == 0))) && ((unsigned long )m == (unsigned long )(& A.mutex) || (unsigned long )m == (unsigned long )(& B.mutex))) && ((unsigned long )d == (unsigned long )(& B.datum) || (unsigned long )d == (unsigned long )(& A.datum))) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum)) && -2147483647 <= x) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:391-1038:393)
[Info][Witness] unassume invariant: (unsigned long )m == (unsigned long )(& s->mutex) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:12-1038:35)
[Info][Witness] unassume invariant: (((((((((unsigned long )s == (unsigned long )(& B) && (s->inside.x == 0 && s->inside.y == 0)) || ((unsigned long )s == (unsigned long )(& A) && (s->inside.x == 0 && s->inside.y == 0))) && ((unsigned long )m == (unsigned long )(& A.mutex) || (unsigned long )m == (unsigned long )(& B.mutex))) && ((unsigned long )d == (unsigned long )(& B.datum) || (unsigned long )d == (unsigned long )(& A.datum))) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum)) && -2147483647 <= x) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:12-1038:35)
[Info][Witness] unassume invariant: (((unsigned long )d == (unsigned long )(& B.datum) || (unsigned long )d == (unsigned long )(& A.datum)) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:265-1038:299)
[Info][Witness] unassume invariant: (unsigned long )m == (unsigned long )(& s->mutex) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:301-1038:329)
[Info][Witness] unassume invariant: (((((((((unsigned long )s == (unsigned long )(& B) && (s->inside.x == 0 && s->inside.y == 0)) || ((unsigned long )s == (unsigned long )(& A) && (s->inside.x == 0 && s->inside.y == 0))) && ((unsigned long )m == (unsigned long )(& A.mutex) || (unsigned long )m == (unsigned long )(& B.mutex))) && ((unsigned long )d == (unsigned long )(& B.datum) || (unsigned long )d == (unsigned long )(& A.datum))) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum)) && -2147483647 <= x) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:238-1038:240)
[Info][Witness] unassume invariant: (((((((((unsigned long )s == (unsigned long )(& B) && (s->inside.x == 0 && s->inside.y == 0)) || ((unsigned long )s == (unsigned long )(& A) && (s->inside.x == 0 && s->inside.y == 0))) && ((unsigned long )m == (unsigned long )(& A.mutex) || (unsigned long )m == (unsigned long )(& B.mutex))) && ((unsigned long )d == (unsigned long )(& B.datum) || (unsigned long )d == (unsigned long )(& A.datum))) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum)) && -2147483647 <= x) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:251-1038:253)
[Info][Witness] unassume invariant: (((((((((unsigned long )s == (unsigned long )(& B) && (s->inside.x == 0 && s->inside.y == 0)) || ((unsigned long )s == (unsigned long )(& A) && (s->inside.x == 0 && s->inside.y == 0))) && ((unsigned long )m == (unsigned long )(& A.mutex) || (unsigned long )m == (unsigned long )(& B.mutex))) && ((unsigned long )d == (unsigned long )(& B.datum) || (unsigned long )d == (unsigned long )(& A.datum))) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum)) && -2147483647 <= x) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:138-1038:140)
[Info][Witness] unassume invariant: (((unsigned long )d == (unsigned long )(& B.datum) || (unsigned long )d == (unsigned long )(& A.datum)) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:47-1038:81)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:84-1038:89)
[Info][Witness] unassume invariant: (((unsigned long )m == (unsigned long )(& s->mutex) && (unsigned long )d == (unsigned long )(& s->datum)) && -2147483647 <= B.datum) && -2147483647 <= A.datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:84-1038:89)
[Info][Witness] unassume invariant: (((unsigned long )d == (unsigned long )(& B.datum) || (unsigned long )d == (unsigned long )(& A.datum)) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:147-1038:181)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:184-1038:189)
[Info][Witness] unassume invariant: (((unsigned long )m == (unsigned long )(& s->mutex) && (unsigned long )d == (unsigned long )(& s->datum)) && B.datum <= 2147483646) && A.datum <= 2147483646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:184-1038:189)
[Info][Witness] unassume invariant: (unsigned long )m == (unsigned long )(& s->mutex) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:391-1038:393)
[Info][Witness] unassume invariant: (unsigned long )m == (unsigned long )(& s->mutex) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1039:3-1039:26)
[Warning][Unknown] unlocking mutex (B.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1039:3-1039:26)
[Warning][Unknown] unlocking mutex (A.mutex) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1039:3-1039:26)
[Info][Witness] unassume invariant: (((((((unsigned long )s == (unsigned long )(& B) && (s->inside.x == 0 && s->inside.y == 0)) || ((unsigned long )s == (unsigned long )(& A) && (s->inside.x == 0 && s->inside.y == 0))) && ((unsigned long )m == (unsigned long )(& B.mutex) || (unsigned long )m == (unsigned long )(& A.mutex))) && ((unsigned long )d == (unsigned long )(& B.datum) || (unsigned long )d == (unsigned long )(& A.datum))) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum)) && -2147483647 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1040:12-1040:15)
[Info][Witness] unassume invariant: (unsigned long )m == (unsigned long )(& s->mutex) && (unsigned long )d == (unsigned long )(& s->datum) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1040:7-1040:31)
[Info][Witness] unassume invariant: (((((((unsigned long )s == (unsigned long )(& B) && (s->inside.x == 0 && s->inside.y == 0)) || ((unsigned long )s == (unsigned long )(& A) && (s->inside.x == 0 && s->inside.y == 0))) && ((unsigned long )m == (unsigned long )(& B.mutex) || (unsigned long )m == (unsigned long )(& A.mutex))) && ((unsigned long )d == (unsigned long )(& B.datum) || (unsigned long )d == (unsigned long )(& A.datum))) && (unsigned long )m == (unsigned long )(& s->mutex)) && (unsigned long )d == (unsigned long )(& s->datum)) && -2147483647 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1040:12-1040:15)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:62:1-66:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:67:1-71:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:72:1-76:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:77:1-81:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:82:1-86:1)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1001:1-1003:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 27
  dead: 7 (7 in uncalled functions)
  total lines: 34
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:138-1038:140)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:238-1038:240)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:251-1038:253)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:998:73-998:74)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:378-1038:380)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:391-1038:393)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:143-1013:145)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:248-1013:250)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:261-1013:263)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:393-1013:395)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:406-1013:408)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1036:55)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1036:55)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:265)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:265)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1041:3)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1041:3)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1036:32)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1036:32)
[Warning][Witness] invariant unconfirmed: (d == & B.datum && *d == 0) || (d == & A.datum && *d == 0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1036:32)
[Success][Witness] invariant confirmed: -2147483647 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1034:3)
[Warning][Witness] invariant unconfirmed: (s == & B && (s->datum == 0 && (s->inside.x == 0 && s->inside.y == 0))) || (s == & A && (s->datum == 0 && (s->inside.x == 0 && s->inside.y == 0))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1034:3)
[Success][Witness] invariant confirmed: -2147483647 <= A.datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:91)
[Success][Witness] invariant confirmed: -2147483647 <= B.datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:91)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:91)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:91)
[Success][Witness] invariant confirmed: x <= 2147483646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1029:4)
[Success][Witness] invariant confirmed: s == & A (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1029:4)
[Success][Witness] invariant confirmed: s->datum == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1029:4)
[Success][Witness] invariant confirmed: s->inside.x == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1029:4)
[Success][Witness] invariant confirmed: s->inside.y == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1029:4)
[Success][Witness] invariant confirmed: x != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1029:4)
[Success][Witness] invariant confirmed: x != 2147483647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1029:4)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1040:8)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1040:8)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:147)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:147)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1037:3)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1037:3)
[Success][Witness] invariant confirmed: m == & B.mutex || m == & A.mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1037:3)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1039:3)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1039:3)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:331)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:331)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1040:33)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1040:33)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:84)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:84)
[Success][Witness] invariant confirmed: d == & B.datum || d == & A.datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:84)
[Success][Witness] invariant confirmed: x <= 2147483646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1027:3)
[Success][Witness] invariant confirmed: x != 2147483647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1027:3)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1035:3)
[Success][Witness] invariant confirmed: m == & B.mutex || m == & A.mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1035:3)
[Warning][Witness] invariant unconfirmed: (s == & B && (s->datum == 0 && (s->inside.x == 0 && s->inside.y == 0))) || (s == & A && (s->datum == 0 && (s->inside.x == 0 && s->inside.y == 0))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1035:3)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:301)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:301)
[Success][Witness] invariant confirmed: d == & B.datum || d == & A.datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:301)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:47)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:47)
[Success][Witness] invariant confirmed: -2147483647 <= B.datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:96)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:184)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:184)
[Success][Witness] invariant confirmed: d == & B.datum || d == & A.datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:184)
[Success][Witness] invariant confirmed: A.datum <= 2147483646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:191)
[Success][Witness] invariant confirmed: B.datum <= 2147483646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:191)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:191)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:191)
[Success][Witness] invariant confirmed: B.datum <= 2147483646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:201)
[Success][Witness] invariant confirmed: x == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1032:4)
[Success][Witness] invariant confirmed: s == & B (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1032:4)
[Success][Witness] invariant confirmed: s->datum == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1032:4)
[Success][Witness] invariant confirmed: s->inside.x == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1032:4)
[Success][Witness] invariant confirmed: s->inside.y == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1032:4)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:8)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:8)
[Success][Witness] invariant confirmed: -2147483647 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:260)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:260)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:260)
[Success][Witness] invariant confirmed: d == & B.datum || d == & A.datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:260)
[Success][Witness] invariant confirmed: m == & A.mutex || m == & B.mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:260)
[Warning][Witness] invariant unconfirmed: (s == & B && (s->inside.x == 0 && s->inside.y == 0)) || (s == & A && (s->inside.x == 0 && s->inside.y == 0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:260)
[Success][Witness] invariant confirmed: -2147483647 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1040:3)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1040:3)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1040:3)
[Success][Witness] invariant confirmed: d == & B.datum || d == & A.datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1040:3)
[Success][Witness] invariant confirmed: m == & B.mutex || m == & A.mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1040:3)
[Warning][Witness] invariant unconfirmed: (s == & B && (s->inside.x == 0 && s->inside.y == 0)) || (s == & A && (s->inside.x == 0 && s->inside.y == 0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1040:3)
[Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:3)
[Success][Witness] invariant confirmed: -2147483647 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1036:27)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1036:27)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1036:27)
[Success][Witness] invariant confirmed: m == & B.mutex || m == & A.mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1036:27)
[Warning][Witness] invariant unconfirmed: (((((((A.datum == 0 && A.inside.x == 0) && A.inside.y == 0) && B.datum == 0) && B.inside.x == 0) && B.inside.y == 0) && ((s == & B && (s->datum == 0 && (s->inside.x == 0 && s->inside.y == 0))) || (s == & A && (s->datum == 0 && (s->inside.x == 0 && s->inside.y == 0))))) && ((d == & B.datum && *d == 0) || (d == & A.datum && *d == 0))) || ((d == & B.datum || d == & A.datum) && ((s == & B && (s->inside.x == 0 && s->inside.y == 0)) || (s == & A && (s->inside.x == 0 && s->inside.y == 0)))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1036:27)
[Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:42)
[Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:147)
[Success][Witness] invariant confirmed: -2147483647 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:42)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:42)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:42)
[Success][Witness] invariant confirmed: d == & B.datum || d == & A.datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:42)
[Success][Witness] invariant confirmed: m == & A.mutex || m == & B.mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:42)
[Warning][Witness] invariant unconfirmed: (s == & B && (s->inside.x == 0 && s->inside.y == 0)) || (s == & A && (s->inside.x == 0 && s->inside.y == 0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:42)
[Success][Witness] invariant confirmed: -2147483647 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:3)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:3)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:3)
[Success][Witness] invariant confirmed: d == & B.datum || d == & A.datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:3)
[Success][Witness] invariant confirmed: m == & A.mutex || m == & B.mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:3)
[Warning][Witness] invariant unconfirmed: (s == & B && (s->inside.x == 0 && s->inside.y == 0)) || (s == & A && (s->inside.x == 0 && s->inside.y == 0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:3)
[Success][Witness] invariant confirmed: -2147483647 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:142)
[Warning][Witness] invariant unconfirmed: d == & s->datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:142)
[Warning][Witness] invariant unconfirmed: m == & s->mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:142)
[Success][Witness] invariant confirmed: d == & B.datum || d == & A.datum (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:142)
[Success][Witness] invariant confirmed: m == & A.mutex || m == & B.mutex (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:142)
[Warning][Witness] invariant unconfirmed: (s == & B && (s->inside.x == 0 && s->inside.y == 0)) || (s == & A && (s->inside.x == 0 && s->inside.y == 0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1038:142)
[Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_78-equ_racing.i:1013:270)
[Info][Witness] witness validation summary:
  confirmed: 47
  unconfirmed: 56
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 103
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 2
  vulnerable: 0
  unsafe: 0
  total memory locations: 2
