./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/race-2_2-container_of.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/race-2_2-container_of.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/ldv-races/race-2_2-container_of.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] ldv_assert, __VERIFIER_atomic_begin, i, key, count, a, tmp, count, i, j, i___0, j___0, k, size, r, top, data, ret, tmp, probe_ret, data, res, tmp, data, lb
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: (((4294967294LL - (long long )probe_ret) - (long long )ret >= 0LL && (4294967295LL + (long long )probe_ret) - (long long )ret >= 0LL) && (4294967295LL - (long long )probe_ret) + (long long )ret >= 0LL) && (4294967296LL + (long long )probe_ret) + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3949:1-3967:1)
[Info][Witness] unassume invariant: (((ret == 0 && (2147483647LL - (long long )probe_ret) - (long long )ret >= 0LL) && (2147483648LL + (long long )probe_ret) - (long long )ret >= 0LL) && (2147483647LL - (long long )probe_ret) + (long long )ret >= 0LL) && (2147483648LL + (long long )probe_ret) + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3950:6-3950:25)
[Info][Witness] unassume invariant: (((((((1LL + (long long )probe_ret) + (long long )ret >= 0LL && (-1LL - (long long )probe_ret) + (long long )ret >= 0LL) && (1LL + (long long )probe_ret) - (long long )ret >= 0LL) && (-1LL - (long long )probe_ret) - (long long )ret >= 0LL) && -1 == data.shared.a) && -1 == data.shared.b) && data.shared.a == data.shared.b) || ((((0LL - (long long )probe_ret) + (long long )ret >= 0LL && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret - (long long )ret >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3951:5-3951:11)
[Info][Witness] unassume invariant: (((2147483647LL - (long long )probe_ret) - (long long )ret >= 0LL && (2147483648LL + (long long )probe_ret) - (long long )ret >= 0LL) && (2147483647LL - (long long )probe_ret) + (long long )ret >= 0LL) && (2147483648LL + (long long )probe_ret) + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3951:5-3951:11)
[Info][Witness] unassume invariant: (unsigned long )d == (unsigned long )(& data->dev) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3920:16-3920:31)
[Info][Witness] unassume invariant: (unsigned long )d == (unsigned long )(& data->dev) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3923:2-3923:46)
[Info][Witness] unassume invariant: (data->shared.a == 0 && (unsigned long )d == (unsigned long )(& data->dev)) && 0 == data->shared.a (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3924:2-3924:20)
[Info][Witness] unassume invariant: ((data->shared.a == data->shared.b && (unsigned long )d == (unsigned long )(& data->dev)) && 0 == data->shared.b) && 0 == data->shared.a (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3925:2-3925:20)
[Info][Witness] unassume invariant: (unsigned long )d == (unsigned long )(& data->dev) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3926:6-3926:35)
[Info][Witness] unassume invariant: (unsigned long )d == (unsigned long )(& data->dev) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3927:5-3927:8)
[Info][Witness] unassume invariant: (unsigned long )d == (unsigned long )(& data->dev) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3930:2-3930:58)
[Info][Witness] unassume invariant: (unsigned long )arg == (unsigned long )dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3902:16-3902:42)
[Info][Witness] unassume invariant: ((unsigned long )dev == (unsigned long )__mptr && (unsigned long )arg == (unsigned long )__mptr) && (unsigned long )arg == (unsigned long )dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3904:72-3904:151)
[Info][Witness] unassume invariant: ((unsigned long )dev == (unsigned long )__mptr && (unsigned long )arg == (unsigned long )__mptr) && (unsigned long )arg == (unsigned long )dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3907:5-3907:30)
[Info][Witness] unassume invariant: ((unsigned long )dev == (unsigned long )__mptr && (unsigned long )arg == (unsigned long )__mptr) && (unsigned long )arg == (unsigned long )dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3908:6-3908:24)
[Info][Witness] unassume invariant: ((unsigned long )dev == (unsigned long )__mptr && (unsigned long )arg == (unsigned long )__mptr) && (unsigned long )arg == (unsigned long )dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3909:6-3909:29)
[Info][Witness] unassume invariant: ((unsigned long )dev == (unsigned long )__mptr && (unsigned long )arg == (unsigned long )__mptr) && (unsigned long )arg == (unsigned long )dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3910:6-3910:31)
[Info][Witness] unassume invariant: ((unsigned long )dev == (unsigned long )__mptr && (unsigned long )arg == (unsigned long )__mptr) && (unsigned long )arg == (unsigned long )dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3911:10-3911:29)
[Info][Witness] unassume invariant: ((unsigned long )dev == (unsigned long )__mptr && (unsigned long )arg == (unsigned long )__mptr) && (unsigned long )arg == (unsigned long )dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3912:6-3912:29)
[Info][Witness] unassume invariant: ((unsigned long )dev == (unsigned long )__mptr && (unsigned long )arg == (unsigned long )__mptr) && (unsigned long )arg == (unsigned long )dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3913:6-3913:31)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3914:6-3914:29)
[Info][Witness] unassume invariant: ((unsigned long )dev == (unsigned long )__mptr && (unsigned long )arg == (unsigned long )__mptr) && (unsigned long )arg == (unsigned long )dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3914:6-3914:29)
[Info][Witness] unassume invariant: ((unsigned long )dev == (unsigned long )__mptr && (unsigned long )arg == (unsigned long )__mptr) && (unsigned long )arg == (unsigned long )dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3915:6-3915:29)
[Info][Witness] unassume invariant: (unsigned long )d == (unsigned long )(& data->dev) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3931:2-3931:58)
[Info][Witness] unassume invariant: (data->shared.b == 0 && data->shared.a == 0) && (unsigned long )d == (unsigned long )(& data->dev) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3927:5-3927:8)
[Info][Witness] unassume invariant: (unsigned long )d == (unsigned long )(& data->dev) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3934:2-3934:36)
[Info][Witness] unassume invariant: ((((((1LL + (long long )probe_ret) + (long long )ret >= 0LL && (-1LL - (long long )probe_ret) + (long long )ret >= 0LL) && (1LL + (long long )probe_ret) - (long long )ret >= 0LL) && (-1LL - (long long )probe_ret) - (long long )ret >= 0LL) && probe_ret == -1) && data.shared.b == 0) || (((((0LL - (long long )probe_ret) + (long long )ret >= 0LL && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret - (long long )ret >= 0LL) && probe_ret == 0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3954:3-3954:34)
[Info][Witness] unassume invariant: ((((1LL + (long long )probe_ret) + (long long )ret >= 0LL && (-1LL - (long long )probe_ret) + (long long )ret >= 0LL) && (1LL + (long long )probe_ret) - (long long )ret >= 0LL) && (-1LL - (long long )probe_ret) - (long long )ret >= 0LL) || ((((0LL - (long long )probe_ret) + (long long )ret >= 0LL && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret - (long long )ret >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3955:6-3955:18)
[Info][Witness] unassume invariant: (((long long )probe_ret - (long long )ret >= 0LL && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3955:6-3955:18)
[Info][Witness] unassume invariant: (unsigned long )status == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3939:2-3939:27)
[Info][Unsound] Unknown address in {&status} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3939:2-3939:27)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3939:2-3939:27)
[Info][Witness] unassume invariant: (unsigned long )status == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3940:2-3940:27)
[Info][Witness] unassume invariant: (((long long )probe_ret - (long long )ret >= 0LL && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3956:4-3956:28)
[Info][Witness] unassume invariant: expression == 1 || ((0 <= expression && expression <= 1) && (expression == 0 || expression == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3887:1-3887:96)
[Info][Witness] unassume invariant: (((probe_ret == 0 && (long long )probe_ret - (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3957:4-3957:32)
[Info][Witness] unassume invariant: ((((1LL + (long long )probe_ret) + (long long )ret >= 0LL && (-1LL - (long long )probe_ret) + (long long )ret >= 0LL) && (1LL + (long long )probe_ret) - (long long )ret >= 0LL) && (-1LL - (long long )probe_ret) - (long long )ret >= 0LL) || ((((0LL - (long long )probe_ret) + (long long )ret >= 0LL && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret - (long long )ret >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3958:4-3958:32)
[Info][Witness] unassume invariant: ((((1LL + (long long )probe_ret) + (long long )ret >= 0LL && (-1LL - (long long )probe_ret) + (long long )ret >= 0LL) && (1LL + (long long )probe_ret) - (long long )ret >= 0LL) && (-1LL - (long long )probe_ret) - (long long )ret >= 0LL) || ((((0LL - (long long )probe_ret) + (long long )ret >= 0LL && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret - (long long )ret >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3960:3-3960:19)
[Info][Witness] unassume invariant: ((((((1LL + (long long )probe_ret) + (long long )ret >= 0LL && (-1LL - (long long )probe_ret) + (long long )ret >= 0LL) && (1LL + (long long )probe_ret) - (long long )ret >= 0LL) && (-1LL - (long long )probe_ret) - (long long )ret >= 0LL) && -1 == data.shared.a) && data.shared.a == -1) || ((((0LL - (long long )probe_ret) + (long long )ret >= 0LL && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret - (long long )ret >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3961:3-3961:21)
[Info][Witness] unassume invariant: (((((((((1LL + (long long )probe_ret) + (long long )ret >= 0LL && (-1LL - (long long )probe_ret) + (long long )ret >= 0LL) && (1LL + (long long )probe_ret) - (long long )ret >= 0LL) && (-1LL - (long long )probe_ret) - (long long )ret >= 0LL) && -1 == data.shared.a) && -1 == data.shared.b) && data.shared.a == -1) && data.shared.a == data.shared.b) && data.shared.b == -1) || ((((0LL - (long long )probe_ret) + (long long )ret >= 0LL && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret - (long long )ret >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3962:3-3962:21)
[Info][Witness] unassume invariant: (((((((((1LL + (long long )probe_ret) + (long long )ret >= 0LL && (-1LL - (long long )probe_ret) + (long long )ret >= 0LL) && (1LL + (long long )probe_ret) - (long long )ret >= 0LL) && (-1LL - (long long )probe_ret) - (long long )ret >= 0LL) && -1 == data.shared.a) && -1 == data.shared.b) && data.shared.a == data.shared.b) && data.shared.b == -1) || ((((0LL - (long long )probe_ret) + (long long )ret >= 0LL && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret - (long long )ret >= 0LL)) && ret == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3963:3-3963:32)
[Info][Witness] unassume invariant: (((((((1LL + (long long )probe_ret) + (long long )ret >= 0LL && (-1LL - (long long )probe_ret) + (long long )ret >= 0LL) && (1LL + (long long )probe_ret) - (long long )ret >= 0LL) && (-1LL - (long long )probe_ret) - (long long )ret >= 0LL) && -1 == data.shared.a) && -1 == data.shared.b) && data.shared.a == data.shared.b) || ((((0LL - (long long )probe_ret) + (long long )ret >= 0LL && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret - (long long )ret >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3964:3-3964:32)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 51
  dead: 0
  total lines: 51
[Warning][Race] Memory location data.shared.a (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3953:18-3953:22)
  write with [lock:{[__VERIFIER_atomic]}, thread:[main, my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3930:2-3930:58]] (conf. 110)  (exp: & data->shared.a) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3908:6-3908:24)
  write with [lock:{[__VERIFIER_atomic]}, thread:[main, my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3931:2-3931:58]] (conf. 110)  (exp: & data->shared.a) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3908:6-3908:24)
  write with [mhp:{created={[main, my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3930:2-3930:58], [main, my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3931:2-3931:58]}}, thread:[main]] (conf. 110)  (exp: & data.shared.a) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3961:3-3961:21)
  read with [mhp:{created={[main, my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3930:2-3930:58], [main, my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3931:2-3931:58]}}, thread:[main]] (conf. 110)  (exp: & data.shared.a) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3963:3-3963:32)
[Warning][Race] Memory location data.shared.b (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3953:18-3953:22)
  write with [lock:{[__VERIFIER_atomic]}, thread:[main, my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3930:2-3930:58]] (conf. 110)  (exp: & data->shared.b) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3914:6-3914:29)
  write with [lock:{[__VERIFIER_atomic]}, thread:[main, my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3931:2-3931:58]] (conf. 110)  (exp: & data->shared.b) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3914:6-3914:29)
  write with [mhp:{created={[main, my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3930:2-3930:58], [main, my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3931:2-3931:58]}}, thread:[main]] (conf. 110)  (exp: & data.shared.b) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3962:3-3962:21)
  read with [lock:{[__VERIFIER_atomic]}, thread:[main, my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3930:2-3930:58]] (conf. 110)  (exp: & data->shared.b) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3911:10-3911:29)
  read with [lock:{[__VERIFIER_atomic]}, thread:[main, my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3931:2-3931:58]] (conf. 110)  (exp: & data->shared.b) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3911:10-3911:29)
  read with [mhp:{created={[main, my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3930:2-3930:58], [main, my_callback@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3931:2-3931:58]}}, thread:[main]] (conf. 110)  (exp: & data.shared.b) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3964:3-3964:32)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3883:24-3883:157)
[Warning][Deadcode][CWE-571] condition 'ret == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3951:5-3951:11)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )probe_ret) + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3951:2)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )probe_ret) + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3951:2)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )probe_ret) - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3951:2)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )probe_ret) - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3951:2)
[Success][Witness] invariant confirmed: ret == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3951:2)
[Warning][Witness] invariant unconfirmed: ret == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3964:3)
[Warning][Witness] invariant unconfirmed: ((((((((1LL + (long long )probe_ret) + (long long )ret >= 0LL && (-1LL - (long long )probe_ret) + (long long )ret >= 0LL) && (1LL + (long long )probe_ret) - (long long )ret >= 0LL) && (-1LL - (long long )probe_ret) - (long long )ret >= 0LL) && -1 == data.shared.a) && -1 == data.shared.b) && data.shared.a == data.shared.b) && data.shared.b == -1) || ((((0LL - (long long )probe_ret) + (long long )ret >= 0LL && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret - (long long )ret >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3964:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )probe_ret) + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3954:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )probe_ret) + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3954:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )probe_ret) - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3954:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )probe_ret) - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3954:3)
[Success][Witness] invariant confirmed: arg == dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3915:6)
[Success][Witness] invariant confirmed: arg == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3915:6)
[Success][Witness] invariant confirmed: dev == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3915:6)
[Success][Witness] invariant confirmed: 0 == data->shared.a (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3926:2)
[Success][Witness] invariant confirmed: 0 == data->shared.b (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3926:2)
[Success][Witness] invariant confirmed: d == & data->dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3926:2)
[Success][Witness] invariant confirmed: data->shared.a == data->shared.b (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3926:2)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )probe_ret) + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3956:4)
[Warning][Witness] invariant unconfirmed: (long long )probe_ret + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3956:4)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )probe_ret) - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3956:4)
[Warning][Witness] invariant unconfirmed: (long long )probe_ret - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3956:4)
[Success][Witness] invariant confirmed: arg == dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3911:6)
[Success][Witness] invariant confirmed: arg == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3911:6)
[Success][Witness] invariant confirmed: dev == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3911:6)
[Success][Witness] invariant confirmed: d == & data->dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3935:2)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )probe_ret) + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3958:4)
[Warning][Witness] invariant unconfirmed: (long long )probe_ret + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3958:4)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )probe_ret) - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3958:4)
[Warning][Witness] invariant unconfirmed: (long long )probe_ret - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3958:4)
[Success][Witness] invariant confirmed: probe_ret == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3958:4)
[Success][Witness] invariant confirmed: d == & data->dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3931:2)
[Success][Witness] invariant confirmed: arg == dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3917:2)
[Success][Witness] invariant confirmed: arg == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3917:2)
[Success][Witness] invariant confirmed: dev == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3917:2)
[Success][Witness] invariant confirmed: arg == dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3907:5)
[Success][Witness] invariant confirmed: arg == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3907:5)
[Success][Witness] invariant confirmed: dev == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3907:5)
[Success][Witness] invariant confirmed: arg == dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3913:6)
[Success][Witness] invariant confirmed: arg == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3913:6)
[Success][Witness] invariant confirmed: dev == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3913:6)
[Warning][Witness] invariant unconfirmed: ((((((1LL + (long long )probe_ret) + (long long )ret >= 0LL && (-1LL - (long long )probe_ret) + (long long )ret >= 0LL) && (1LL + (long long )probe_ret) - (long long )ret >= 0LL) && (-1LL - (long long )probe_ret) - (long long )ret >= 0LL) && probe_ret == -1) && data.shared.b == 0) || (((((0LL - (long long )probe_ret) + (long long )ret >= 0LL && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret - (long long )ret >= 0LL) && probe_ret == 0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3955:3)
[Warning][Witness] invariant unconfirmed: ((((1LL + (long long )probe_ret) + (long long )ret >= 0LL && (-1LL - (long long )probe_ret) + (long long )ret >= 0LL) && (1LL + (long long )probe_ret) - (long long )ret >= 0LL) && (-1LL - (long long )probe_ret) - (long long )ret >= 0LL) || ((((0LL - (long long )probe_ret) + (long long )ret >= 0LL && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret - (long long )ret >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3960:3)
[Success][Witness] invariant confirmed: d == & data->dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3932:2)
[Success][Witness] invariant confirmed: d == & data->dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3934:2)
[Success][Witness] invariant confirmed: data->shared.a == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3934:2)
[Success][Witness] invariant confirmed: data->shared.b == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3934:2)
[Warning][Witness] invariant unconfirmed: (((((((((1LL + (long long )probe_ret) + (long long )ret >= 0LL && (-1LL - (long long )probe_ret) + (long long )ret >= 0LL) && (1LL + (long long )probe_ret) - (long long )ret >= 0LL) && (-1LL - (long long )probe_ret) - (long long )ret >= 0LL) && -1 == data.shared.a) && -1 == data.shared.b) && data.shared.a == -1) && data.shared.a == data.shared.b) && data.shared.b == -1) || ((((0LL - (long long )probe_ret) + (long long )ret >= 0LL && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret - (long long )ret >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3963:3)
[Success][Witness] invariant confirmed: d == & data->dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3923:2)
[Success][Witness] invariant confirmed: d == & data->dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3927:2)
[Success][Witness] invariant confirmed: d == & data->dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3930:2)
[Success][Witness] invariant confirmed: expression == 1 || ((0 <= expression && expression <= 1) && (expression == 0 || expression == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3887:35)
[Warning][Witness] invariant unconfirmed: (unsigned long )status == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3941:2)
[Success][Witness] invariant confirmed: arg == dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3912:6)
[Success][Witness] invariant confirmed: arg == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3912:6)
[Success][Witness] invariant confirmed: dev == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3912:6)
[Success][Witness] invariant confirmed: 0 == data->shared.a (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3925:2)
[Success][Witness] invariant confirmed: d == & data->dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3925:2)
[Success][Witness] invariant confirmed: data->shared.a == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3925:2)
[Success][Witness] invariant confirmed: d == & data->dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3924:2)
[Success][Witness] invariant confirmed: arg == dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3914:6)
[Success][Witness] invariant confirmed: arg == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3914:6)
[Success][Witness] invariant confirmed: dev == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3914:6)
[Warning][Witness] invariant unconfirmed: (unsigned long )status == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3940:2)
[Success][Witness] invariant confirmed: arg == dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3909:6)
[Success][Witness] invariant confirmed: arg == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3909:6)
[Success][Witness] invariant confirmed: dev == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3909:6)
[Success][Witness] invariant confirmed: arg == dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3904:12)
[Warning][Witness] invariant unconfirmed: ((((1LL + (long long )probe_ret) + (long long )ret >= 0LL && (-1LL - (long long )probe_ret) + (long long )ret >= 0LL) && (1LL + (long long )probe_ret) - (long long )ret >= 0LL) && (-1LL - (long long )probe_ret) - (long long )ret >= 0LL) || ((((0LL - (long long )probe_ret) + (long long )ret >= 0LL && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret - (long long )ret >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3961:3)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )probe_ret) + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3950:2)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )probe_ret) + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3950:2)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )probe_ret) - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3950:2)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )probe_ret) - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3950:2)
[Warning][Witness] invariant unconfirmed: (((((((1LL + (long long )probe_ret) + (long long )ret >= 0LL && (-1LL - (long long )probe_ret) + (long long )ret >= 0LL) && (1LL + (long long )probe_ret) - (long long )ret >= 0LL) && (-1LL - (long long )probe_ret) - (long long )ret >= 0LL) && -1 == data.shared.a) && -1 == data.shared.b) && data.shared.a == data.shared.b) || ((((0LL - (long long )probe_ret) + (long long )ret >= 0LL && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret - (long long )ret >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3966:2)
[Warning][Witness] invariant unconfirmed: ((((((1LL + (long long )probe_ret) + (long long )ret >= 0LL && (-1LL - (long long )probe_ret) + (long long )ret >= 0LL) && (1LL + (long long )probe_ret) - (long long )ret >= 0LL) && (-1LL - (long long )probe_ret) - (long long )ret >= 0LL) && -1 == data.shared.a) && data.shared.a == -1) || ((((0LL - (long long )probe_ret) + (long long )ret >= 0LL && (long long )probe_ret + (long long )ret >= 0LL) && (0LL - (long long )probe_ret) - (long long )ret >= 0LL) && (long long )probe_ret - (long long )ret >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3962:3)
[Success][Witness] invariant confirmed: arg == dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3908:6)
[Success][Witness] invariant confirmed: arg == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3908:6)
[Success][Witness] invariant confirmed: dev == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3908:6)
[Success][Witness] invariant confirmed: arg == dev (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3910:6)
[Success][Witness] invariant confirmed: arg == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3910:6)
[Success][Witness] invariant confirmed: dev == __mptr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3910:6)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )probe_ret) + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3957:4)
[Warning][Witness] invariant unconfirmed: (long long )probe_ret + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3957:4)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )probe_ret) - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3957:4)
[Warning][Witness] invariant unconfirmed: (long long )probe_ret - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_2-container_of.i:3957:4)
[Info][Witness] witness validation summary:
  confirmed: 63
  unconfirmed: 22
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 85
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 2
  vulnerable: 0
  unsafe: 2
  total memory locations: 4
