./goblint --conf conf/svcomp24-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/benchexec/results/167-concurrency-witness-0.1-for/goblint.2024-04-25_07-32-24.files/SV-COMP24_unreach-call/popl20-bad-commit-2.wvr-bad.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/benchexec/results/167-concurrency-witness-0.1-for/goblint.2024-04-25_07-32-24.files/SV-COMP24_unreach-call/popl20-bad-commit-2.wvr-bad.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/weaver/popl20-bad-commit-2.wvr-bad.c


--------------------------------------------------------------------------------


[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] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:52:3-96:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:102:3-118:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:124:3-140:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:146:3-162:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:216:3-218:3 with factor 8
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || (__VERIFIER_atomic_locked || ((0 <= manager_state && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state == 5))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || (__VERIFIER_atomic_locked || ((0 <= manager_state && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state == 5))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197: Error: Cannot resolve variable __VERIFIER_atomic_locked.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || (__VERIFIER_atomic_locked || ((0 <= manager_state && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state == 5))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || (__VERIFIER_atomic_locked || ((0 <= manager_state && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state == 5))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198: Error: Cannot resolve variable __VERIFIER_atomic_locked.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || (__VERIFIER_atomic_locked || ((0 <= manager_state && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state == 5))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || (__VERIFIER_atomic_locked || ((0 <= manager_state && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state == 5))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199: Error: Cannot resolve variable __VERIFIER_atomic_locked.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || (__VERIFIER_atomic_locked || ((0 <= manager_state && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state == 5))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || (__VERIFIER_atomic_locked || ((0 <= manager_state && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state == 5))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200: Error: Cannot resolve variable __VERIFIER_atomic_locked.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || ((0 <= node2_state && node2_state <= 1) && (node2_state == 0 || node2_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || ((0 <= node2_state && node2_state <= 1) && (node2_state == 0 || node2_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || ((0 <= node2_state && node2_state <= 1) && (node2_state == 0 || node2_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || ((0 <= node2_state && node2_state <= 1) && (node2_state == 0 || node2_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || ((0 <= node2_state && node2_state <= 1) && (node2_state == 0 || node2_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || ((0 <= node2_state && node2_state <= 1) && (node2_state == 0 || node2_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || ((0 <= node2_state && node2_state <= 1) && (node2_state == 0 || node2_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || ((0 <= node2_state && node2_state <= 1) && (node2_state == 0 || node2_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || (((0 <= manager_state && manager_state <= 5) && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state == 5)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || (((0 <= manager_state && manager_state <= 5) && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state == 5)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || (((0 <= manager_state && manager_state <= 5) && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state == 5)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || (((0 <= manager_state && manager_state <= 5) && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state == 5)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || (((0 <= manager_state && manager_state <= 5) && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state == 5)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || (((0 <= manager_state && manager_state <= 5) && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state == 5)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || (((0 <= manager_state && manager_state <= 5) && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state == 5)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || (((0 <= manager_state && manager_state <= 5) && manager_state <= 127) && (((((manager_state == 0 || manager_state == 1) || manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state == 5)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || ((0 <= client_state && client_state <= 1) && (client_state == 0 || client_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || ((0 <= client_state && client_state <= 1) && (client_state == 0 || client_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || ((0 <= client_state && client_state <= 1) && (client_state == 0 || client_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || ((0 <= client_state && client_state <= 1) && (client_state == 0 || client_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || ((0 <= client_state && client_state <= 1) && (client_state == 0 || client_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || ((0 <= client_state && client_state <= 1) && (client_state == 0 || client_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || ((0 <= client_state && client_state <= 1) && (client_state == 0 || client_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || ((0 <= client_state && client_state <= 1) && (client_state == 0 || client_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || (safe == (_Bool)0 || safe == (_Bool)1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || (safe == (_Bool)0 || safe == (_Bool)1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || (safe == (_Bool)0 || safe == (_Bool)1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || (safe == (_Bool)0 || safe == (_Bool)1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || (safe == (_Bool)0 || safe == (_Bool)1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || (safe == (_Bool)0 || safe == (_Bool)1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || (safe == (_Bool)0 || safe == (_Bool)1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || (safe == (_Bool)0 || safe == (_Bool)1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || ((0 <= node1_state && node1_state <= 1) && (node1_state == 0 || node1_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || ((0 <= node1_state && node1_state <= 1) && (node1_state == 0 || node1_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || ((0 <= node1_state && node1_state <= 1) && (node1_state == 0 || node1_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || ((0 <= node1_state && node1_state <= 1) && (node1_state == 0 || node1_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || ((0 <= node1_state && node1_state <= 1) && (node1_state == 0 || node1_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || ((0 <= node1_state && node1_state <= 1) && (node1_state == 0 || node1_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199:3)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199: Error: Cannot resolve variable multithreaded.
[Error][Witness] CIL couldn't parse invariant: ! multithreaded || ((0 <= node1_state && node1_state <= 1) && (node1_state == 0 || node1_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200:3)
[Info][Witness] invariant has undefined variables or side effects: ! multithreaded || ((0 <= node1_state && node1_state <= 1) && (node1_state == 0 || node1_state == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200:3)
[Warning][Witness] cannot unassume entry of type ghost_variable
[Warning][Witness] cannot unassume entry of type ghost_update
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:213:3-213:69)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:215:6-215:54)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:215:6-215:54)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:57:7-57:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:64:7-64:19)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:71:7-71:19)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:78:7-78:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:85:7-85:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:92:7-92:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:92:7-92:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:85:7-85:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:78:7-78:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:71:7-71:19)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:64:7-64:19)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:57:7-57:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:107:7-107:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:114:7-114:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:107:7-107:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:114:7-114:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:114:7-114:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:107:7-107:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:129:7-129:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:136:7-136:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:129:7-129:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:136:7-136:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:136:7-136:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:129:7-129:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:151:7-151:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:158:7-158:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:151:7-151:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:158:7-158:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:158:7-158:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:151:7-151:21)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
  on line 208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:208-208)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 139
  dead: 1
  total lines: 140
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197: Error: Cannot resolve variable __VERIFIER_atomic_locked.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198: Error: Cannot resolve variable __VERIFIER_atomic_locked.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199: Error: Cannot resolve variable __VERIFIER_atomic_locked.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200: Error: Cannot resolve variable __VERIFIER_atomic_locked.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:197: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:198: Error: Cannot resolve variable multithreaded.
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:199: Error: Cannot resolve variable multithreaded.
[Warning][Witness] cannot validate entry of type ghost_variable
[Warning][Witness] cannot validate entry of type ghost_update
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 24
  unchecked: 0
  unsupported: 27
  disabled: 0
  total validation entries: 51
SV-COMP result: ERROR (witness error)
[Info][Race] Memory locations race summary:
  safe: 24
  vulnerable: 0
  unsafe: 0
  total memory locations: 24
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c:200: Error: Cannot resolve variable multithreaded.
