./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_valid-memsafety/uthash_BER_test1-1.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_valid-memsafety/uthash_BER_test1-1.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/valid-memsafety.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.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
[0;34m[Info] Specification: CHECK( init(main()), LTL(G valid-free) ) -> enabling soundness analyses "base, useAfterFree"[0;0;00m
[0;34m[Info] Specification: CHECK( init(main()), LTL(G valid-deref) ) -> enabling soundness analyses "base, memOutOfBounds"[0;0;00m
[0;34m[Info] Setting "ana.arrayoob" to true[0;0;00m
[0;34m[Info] Setting "cil.addNestedScopeAttr" to true[0;0;00m
[0;34m[Info] Specification: CHECK( init(main()), LTL(G valid-memtrack) ) -> enabling soundness analyses "memLeak"[0;0;00m
[0;34m[Info] Setting "ana.malloc.unique_address_count" to 5[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2670-757:3297 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3360-757:3574 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3631-757:3712 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4976-757:5072 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:5-761:5 with factor 12
[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] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) )
[Info][Witness] couldn't parse entry: find uuid

[Info] runtime: 00:00:10.123
[Info] vars: 426, evals: 26015

[Info] |called|=12

Memory statistics: total=22483.29MB, max=24.04MB, minor=22481.04MB, major=242.44MB, promoted=240.19MB
    minor collections=10743  major collections=47 compactions=0

[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 256 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4945-757:4974)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 416 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4981-757:5059)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4981-757:5059)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4981-757:5059)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5120-757:5184)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (8192) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5120-757:5184)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (16384) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5120-757:5184)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (1024) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5120-757:5184)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (4096) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5120-757:5184)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (2048) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5120-757:5184)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (8192) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5120-757:5184)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 288 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5120-757:5184)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5120-757:5184)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (16384) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5120-757:5184)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (1024) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5120-757:5184)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (4096) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5120-757:5184)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (2048) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5120-757:5184)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5190-757:5226)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 320 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5190-757:5226)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5190-757:5226)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5232-757:5318)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (8192) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5232-757:5318)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 288 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5232-757:5318)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5232-757:5318)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (16384) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5232-757:5318)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (1024) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5232-757:5318)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (4096) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5232-757:5318)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (2048) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5232-757:5318)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5322-757:5347)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (8192) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5322-757:5347)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (16384) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5322-757:5347)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (1024) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5322-757:5347)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (4096) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5322-757:5347)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (2048) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5322-757:5347)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5353-757:5383)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 256 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (8192) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (16384) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (1024) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (4096) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (2048) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5385-757:5423)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (8192) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5429-757:5463)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (16384) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5429-757:5463)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (1024) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5429-757:5463)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (4096) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5429-757:5463)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (2048) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5429-757:5463)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Warning][Unknown] Size of lval dereference expression _he_newbkt->hh_head is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (8192) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (16384) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (1024) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (4096) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (2048) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5467-757:5505)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (8192) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (16384) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (1024) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (4096) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (2048) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5509-757:5538)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4772-757:4846)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4772-757:4846)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4850-757:4910)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]),[5,2147483647],not {} ([-31,31]))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1663-757:1702)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1663-757:1702)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (4) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1663-757:1702)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1663-757:1702)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (3) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1663-757:1702)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (2) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1663-757:1702)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1663-757:1702)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]),[5,2147483647],not {} ([-31,31]))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1712-757:1751)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1712-757:1751)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (4) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1712-757:1751)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1712-757:1751)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (3) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1712-757:1751)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (2) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1712-757:1751)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1712-757:1751)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ((Unknown int([-31,31]),[5,2147483647],not {} ([-31,31]))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1761-757:1799)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1761-757:1799)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (4) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1761-757:1799)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1761-757:1799)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (3) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1761-757:1799)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (2) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1761-757:1799)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array (1) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1761-757:1799)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1809-757:1828)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1837-757:1851)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1853-757:1871)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1903-757:1921)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1923-757:1937)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1939-757:1962)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1964-757:1982)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1984-757:2002)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2004-757:2032)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2034-757:2048)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2050-757:2068)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2070-757:2098)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2100-757:2118)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2120-757:2134)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2136-757:2160)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2162-757:2180)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2182-757:2200)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2202-757:2229)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2231-757:2245)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2247-757:2265)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2267-757:2294)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2296-757:2314)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2316-757:2330)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2332-757:2356)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2358-757:2376)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2378-757:2396)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2398-757:2426)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 480 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2473-757:2502)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2505-757:2544)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 448 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2547-757:2590)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#2)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3327-757:3358)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3366-757:3394)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 128 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 256 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> 0
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> 0
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> 0
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> 0
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3397-757:3484)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 128 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> 0
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> 0
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#2)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> 0
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> 0
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3487-757:3522)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#2)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3525-757:3561)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2609-757:2637)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 128 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2640-757:2668)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2676-757:2737)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2743-757:2758)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2781-757:2830)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2833-757:2868)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2833-757:2868)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2871-757:2903)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2871-757:2903)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 96 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2906-757:2942)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2906-757:2942)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2945-757:3002)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 256 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2945-757:3002)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2945-757:3002)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3005-757:3090)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 416 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3093-757:3131)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3093-757:3131)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3137-757:3161)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3206-757:3278)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3602-757:3629)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 128 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3602-757:3629)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3602-757:3629)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3636-757:3699)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3636-757:3699)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3734-757:3782)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3784-757:3801)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (8192) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3784-757:3801)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (512) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3784-757:3801)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (4096) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3784-757:3801)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (1024) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3784-757:3801)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (2048) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3784-757:3801)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 320 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (8192) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (512) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (4096) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (1024) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (2048) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#2)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3804-757:3845)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 256 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3848-757:3883)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (8192) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3889-757:3921)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (512) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3889-757:3921)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (4096) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3889-757:3921)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (1024) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3889-757:3921)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (2048) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3889-757:3921)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Unknown] Size of lval dereference expression _ha_head->hh_head is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (8192) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (512) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (4096) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (1024) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (2048) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#2)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3925-757:3967)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (8192) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (512) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (4096) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (1024) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (2048) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153(#0)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#2)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL}
                                                       hh_prev -> {NULL, &(alloc@sid:153(#1)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3971-757:4004)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4011-757:4100)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (8192) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4011-757:4100)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (512) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4011-757:4100)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (4096) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4011-757:4100)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (1024) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4011-757:4100)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (2048) (in bytes) with offset by ((Unknown int([-63,63]),[0,68719476720],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4011-757:4100)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4011-757:4100)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4011-757:4100)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4011-757:4100)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4238-757:4352)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4238-757:4352)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4397-757:4497)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4397-757:4497)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 128 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4501-757:4724)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4501-757:4724)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4501-757:4724)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4501-757:4724)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4501-757:4724)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 288 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4501-757:4724)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4501-757:4724)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 128 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4501-757:4724)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 96 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4501-757:4724)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 320 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4728-757:4766)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4728-757:4766)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5566-757:5601)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5605-757:5642)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5605-757:5642)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 96 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5646-757:5684)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5646-757:5684)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#4)).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#0)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#1))}
                                                       prev -> 0
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#1)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#2))}
                                                       prev -> {&(alloc@sid:153(#0)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#2)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#3))}
                                                       prev -> {&(alloc@sid:153(#1)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153(#3)).id}
                                                       keylen -> 4
                                                       next -> {&(alloc@sid:153(#4))}
                                                       prev -> {&(alloc@sid:153(#2)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Info][Unsound] Unknown value in {&(alloc@sid:153(#3)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
                                                       hashv -> ⊤
                                                       hh_next -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       hh_prev -> {NULL, &(alloc@sid:153).hh, &(alloc@sid:153(#3)).hh, &(alloc@sid:153(#2)).hh, &(alloc@sid:153(#1)).hh, &(alloc@sid:153(#0)).hh, &(alloc@sid:153(#4)).hh}
                                                       key -> {&(alloc@sid:153).id}
                                                       keylen -> 4
                                                       next -> {NULL, &(alloc@sid:153)}
                                                       prev -> {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])], &(alloc@sid:153(#4)).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]}
                                                       tbl -> {&(alloc@sid:325(#0))}
                                                     }) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Info][Unsound] Unknown value in {&(alloc@sid:153).hh[def_exc:Unknown int([-31,32]); intervals:[-2147483647,2147483648]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5688-757:5733)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5737-757:5900)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 320 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5737-757:5900)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5737-757:5900)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 128 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5737-757:5900)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 352 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5737-757:5900)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5737-757:5900)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 352 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5737-757:5900)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5737-757:5900)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 352 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5908-757:5946)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5908-757:5946)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 55 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5952-757:5984)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5952-757:5984)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:153(#4)), (alloc@sid:153(#0)), (alloc@sid:153(#1)), (alloc@sid:153(#2)), (alloc@sid:153(#3)), (alloc@sid:648(#1)), (alloc@sid:153), (alloc@sid:325(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:699:64-699:145)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Memory leak detected for heap variables (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:699:64-699:145)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:153(#4)), (alloc@sid:153(#0)), (alloc@sid:153(#1)), (alloc@sid:153(#2)), (alloc@sid:153(#3)), (alloc@sid:648(#4)), (alloc@sid:153), (alloc@sid:325(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:699:64-699:145)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:153(#4)), (alloc@sid:153(#0)), (alloc@sid:153(#1)), (alloc@sid:153(#2)), (alloc@sid:153(#3)), (alloc@sid:648(#0)), (alloc@sid:153), (alloc@sid:325(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:699:64-699:145)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:153(#4)), (alloc@sid:153(#0)), (alloc@sid:153(#1)), (alloc@sid:153(#2)), (alloc@sid:648(#2)), (alloc@sid:153(#3)), (alloc@sid:153), (alloc@sid:325(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:699:64-699:145)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:153(#4)), (alloc@sid:153(#0)), (alloc@sid:153(#1)), (alloc@sid:336(#0)), (alloc@sid:153(#2)), (alloc@sid:153(#3)), (alloc@sid:153), (alloc@sid:325(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:699:64-699:145)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:648(#3)), (alloc@sid:153(#4)), (alloc@sid:153(#0)), (alloc@sid:153(#1)), (alloc@sid:153(#2)), (alloc@sid:153(#3)), (alloc@sid:153), (alloc@sid:325(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:699:64-699:145)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:708:11-708:26)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 63 (in bytes). It is offset by 192 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:648(#3)), (alloc@sid:153(#4)), (alloc@sid:153(#0)), (alloc@sid:153(#1)), (alloc@sid:153(#2)), (alloc@sid:153(#3)), (alloc@sid:153), (alloc@sid:325(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:762:12-762:13)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Memory leak detected for heap variables (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:762:12-762:13)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:153(#4)), (alloc@sid:153(#0)), (alloc@sid:153(#1)), (alloc@sid:336(#0)), (alloc@sid:153(#2)), (alloc@sid:153(#3)), (alloc@sid:153), (alloc@sid:325(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:762:12-762:13)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:153(#4)), (alloc@sid:153(#0)), (alloc@sid:153(#1)), (alloc@sid:153(#2)), (alloc@sid:648(#2)), (alloc@sid:153(#3)), (alloc@sid:153), (alloc@sid:325(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:762:12-762:13)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:153(#4)), (alloc@sid:153(#0)), (alloc@sid:153(#1)), (alloc@sid:153(#2)), (alloc@sid:153(#3)), (alloc@sid:648(#0)), (alloc@sid:153), (alloc@sid:325(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:762:12-762:13)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:153(#4)), (alloc@sid:153(#0)), (alloc@sid:153(#1)), (alloc@sid:153(#2)), (alloc@sid:153(#3)), (alloc@sid:648(#4)), (alloc@sid:153), (alloc@sid:325(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:762:12-762:13)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:153(#4)), (alloc@sid:153(#0)), (alloc@sid:153(#1)), (alloc@sid:153(#2)), (alloc@sid:153(#3)), (alloc@sid:648(#1)), (alloc@sid:153), (alloc@sid:325(#0)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:762:12-762:13)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:282:1-286:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:287:1-291:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:292:1-296:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:297:1-301:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:302:1-306:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:753-753)
[Warning][Deadcode] Function 'reach_error' has dead code:
  on line 700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:700-700)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 40
  dead: 7 (5 in uncalled functions)
  total lines: 47
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:6003-757:6005)
[Warning][Deadcode][CWE-571] condition 'a == 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:722:8-722:48)
[Warning][Deadcode][CWE-570] condition '! (user->hh.tbl)->buckets' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3137-757:3161)
[Warning][Deadcode][CWE-571] condition 'b == 16' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:722:8-722:48)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:6018-757:6020)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:6035-757:6037)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3295-757:3297)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:6050-757:6052)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:6063-757:6065)
[Warning][Deadcode][CWE-570] condition '_hj_k == 11U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1319-757:1326)
[Warning][Deadcode][CWE-570] condition '_hj_k == 10U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1374-757:1381)
[Warning][Deadcode][CWE-570] condition '_hj_k == 9U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1428-757:1434)
[Warning][Deadcode][CWE-571] condition '(unsigned long )user != (unsigned long )((void *)0)' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Deadcode][CWE-570] condition '_hj_k == 8U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1480-757:1486)
[Warning][Deadcode][CWE-570] condition '_hj_k == 7U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1529-757:1535)
[Warning][Deadcode][CWE-570] condition '_hj_k == 6U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1578-757:1584)
[Warning][Deadcode][CWE-571] condition '(unsigned long )user != (unsigned long )((void *)0)' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Deadcode][CWE-570] condition '_hj_k == 5U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1626-757:1632)
[Warning][Deadcode][CWE-571] condition '_hj_k == 4U' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:1655-757:1661)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3710-757:3712)
[Warning][Deadcode][CWE-571] condition '(unsigned long )user != (unsigned long )((void *)0)' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Deadcode][CWE-571] condition '(unsigned long )user != (unsigned long )((void *)0)' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Deadcode][CWE-571] condition '(unsigned long )user != (unsigned long )((void *)0)' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:759:8-759:79)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:699:54-699:55)
[Warning][Deadcode][CWE-570] condition '! _he_new_buckets' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:4358-757:4374)
[Warning][Deadcode][CWE-570] condition '(unsigned long )user == (unsigned long )((void *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:752:13-752:32)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:5070-757:5072)
[Warning][Deadcode][CWE-571] condition 'a == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:710:8-710:47)
[Warning][Deadcode][CWE-571] condition 'b == 0' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:710:8-710:47)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2437-757:2439)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:3572-757:3574)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2450-757:2452)
[Warning][Deadcode][CWE-570] condition '_hj_k >= 12U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:234-757:246)
[Warning][Deadcode][CWE-571] condition 'a == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:713:8-713:47)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2463-757:2465)
[Warning][Deadcode][CWE-571] condition 'b == 1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:713:8-713:47)
[Warning][Deadcode][CWE-571] condition 'a == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:716:8-716:47)
[Warning][Deadcode][CWE-571] condition 'b == 4' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:716:8-716:47)
[Warning][Deadcode][CWE-570] condition '! user->hh.tbl' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:757:2743-757:2758)
[Warning][Deadcode][CWE-571] condition 'a == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:719:8-719:47)
[Warning][Deadcode][CWE-571] condition 'b == 9' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_BER_test1-1.i:719:8-719:47)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
