./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/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.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/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.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/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.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___0, key, count, a, tmp, count, i___0, j, i___1, j___0, k, size, r, top, b, a, tmp, tmp___0, x, tmp, x, y, tmp, tmp___0, z, tmp___1
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: (((((((((((4294967294LL - (long long )y) - (long long )z >= 0LL && (4294967294LL - (long long )x) - (long long )z >= 0LL) && (4294967294LL - (long long )x) - (long long )y >= 0LL) && (4294967295LL + (long long )y) - (long long )z >= 0LL) && (4294967295LL + (long long )x) - (long long )z >= 0LL) && (4294967295LL + (long long )x) - (long long )y >= 0LL) && (4294967295LL - (long long )y) + (long long )z >= 0LL) && (4294967295LL - (long long )x) + (long long )z >= 0LL) && (4294967295LL - (long long )x) + (long long )y >= 0LL) && (4294967296LL + (long long )y) + (long long )z >= 0LL) && (4294967296LL + (long long )x) + (long long )z >= 0LL) && (4294967296LL + (long long )x) + (long long )y >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:709:1-729:1)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )y) - (long long )z >= 0LL && (4294967295LL + (long long )y) - (long long )z >= 0LL) && (4294967295LL - (long long )y) + (long long )z >= 0LL) && (4294967296LL + (long long )y) + (long long )z >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:710:7-710:34)
[Info][Witness] unassume invariant: -999 <= g (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:715:5-715:27)
[Info][Witness] unassume invariant: -999 <= x && -1016 <= h (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:716:5-716:10)
[Info][Witness] unassume invariant: -999 <= x && -1016 <= y (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:717:5-717:10)
[Info][Witness] unassume invariant: -999 <= x && -1016 <= y (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:719:5-719:27)
[Info][Witness] unassume invariant: -999 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:721:5-721:29)
[Info][Witness] unassume invariant: (((((1016LL + (long long )a) + (long long )b >= 0LL && (982LL + (long long )a) - (long long )b >= 0LL) && -17 == b) && b == -17) || (31 == b && b == 31)) && -999 <= a (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:751:1-755:1)
[Info][Witness] unassume invariant: (((((1016LL + (long long )a) + (long long )b >= 0LL && (982LL + (long long )a) - (long long )b >= 0LL) && -17 == b) && b == -17) || (31 == b && b == 31)) && -999 <= a (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:752:3-752:54)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:753:3-753:53)
[Info][Witness] unassume invariant: (((((1016LL + (long long )a) + (long long )b >= 0LL && (982LL + (long long )a) - (long long )b >= 0LL) && -17 == b) && b == -17) || (31 == b && b == 31)) && -999 <= a (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:753:3-753:53)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:754:10-754:15)
[Info][Witness] unassume invariant: -968 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:722:5-722:20)
[Info][Witness] unassume invariant: -968 <= z && -999 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:723:5-723:10)
[Info][Witness] unassume invariant: -999 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:725:5-725:29)
[Info][Witness] unassume invariant: -968 <= i && -999 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:737:5-737:11)
[Info][Witness] unassume invariant: -999 <= x && -999 <= g (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:738:5-738:10)
[Info][Witness] unassume invariant: h <= 2147483630 && -1016 <= h (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:739:5-739:22)
[Info][Witness] unassume invariant: -999 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:741:5-741:27)
[Info][Witness] unassume invariant: -999 <= h (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:742:5-742:10)
[Info][Witness] unassume invariant: -968 <= i && -999 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:746:5-746:10)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 47
  dead: 0
  total lines: 47
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:18:73-18:74)
[Warning][Deadcode][CWE-571] condition '(long )a >= (-0x7FFFFFFF-1) - (long )b' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:752:3-752:54)
[Success][Witness] invariant confirmed: -999 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:742:5)
[Success][Witness] invariant confirmed: -999 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:747:5)
[Warning][Witness] invariant unconfirmed: -968 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:747:5)
[Success][Witness] invariant confirmed: -999 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:722:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )y) + (long long )z >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:711:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )y) + (long long )z >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:711:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )y) - (long long )z >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:711:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )y) - (long long )z >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:711:3)
[Success][Witness] invariant confirmed: -999 <= g (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:739:5)
[Success][Witness] invariant confirmed: -999 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:739:5)
[Success][Witness] invariant confirmed: -999 <= a (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:753:3)
[Warning][Witness] invariant unconfirmed: ((((1016LL + (long long )a) + (long long )b >= 0LL && (982LL + (long long )a) - (long long )b >= 0LL) && -17 == b) && b == -17) || (31 == b && b == 31) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:753:3)
[Success][Witness] invariant confirmed: -1016 <= y (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:718:5)
[Success][Witness] invariant confirmed: -999 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:718:5)
[Success][Witness] invariant confirmed: -999 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:724:5)
[Warning][Witness] invariant unconfirmed: -968 <= z (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:724:5)
[Success][Witness] invariant confirmed: -1016 <= h (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:740:5)
[Warning][Witness] invariant unconfirmed: h <= 2147483630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:740:5)
[Warning][Witness] invariant unconfirmed: -968 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:723:5)
[Success][Witness] invariant confirmed: -1016 <= y (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:720:5)
[Success][Witness] invariant confirmed: -999 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:720:5)
[Success][Witness] invariant confirmed: -999 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:738:5)
[Warning][Witness] invariant unconfirmed: -968 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:738:5)
[Success][Witness] invariant confirmed: -999 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:726:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )x) + (long long )y >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:710:3)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )x) + (long long )z >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:710:3)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )y) + (long long )z >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:710:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )x) + (long long )y >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:710:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )x) + (long long )z >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:710:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )y) + (long long )z >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:710:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )x) - (long long )y >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:710:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )x) - (long long )z >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:710:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )y) - (long long )z >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:710:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )x) - (long long )y >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:710:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )x) - (long long )z >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:710:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )y) - (long long )z >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:710:3)
[Success][Witness] invariant confirmed: -999 <= g (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:716:5)
[Success][Witness] invariant confirmed: -999 <= h (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:743:5)
[Success][Witness] invariant confirmed: -999 <= a (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:752:3)
[Warning][Witness] invariant unconfirmed: ((((1016LL + (long long )a) + (long long )b >= 0LL && (982LL + (long long )a) - (long long )b >= 0LL) && -17 == b) && b == -17) || (31 == b && b == 31) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:752:3)
[Success][Witness] invariant confirmed: -999 <= a (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:754:3)
[Warning][Witness] invariant unconfirmed: ((((1016LL + (long long )a) + (long long )b >= 0LL && (982LL + (long long )a) - (long long )b >= 0LL) && -17 == b) && b == -17) || (31 == b && b == 31) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:754:3)
[Success][Witness] invariant confirmed: -1016 <= h (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:717:5)
[Success][Witness] invariant confirmed: -999 <= x (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i:717:5)
[Info][Witness] witness validation summary:
  confirmed: 36
  unconfirmed: 8
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 44
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 3
  vulnerable: 0
  unsafe: 0
  total memory locations: 3
