./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_OAT_test5-2.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_OAT_test5-2.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_OAT_test5-2.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_OAT_test5-2.i:743:2670-743:3297 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_test5-2.i:743:3360-743:3574 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_test5-2.i:743:3631-743:3712 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_test5-2.i:743:4976-743:5072 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_test5-2.i:744:2691-744:3346 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_test5-2.i:744:3419-744:3659 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_test5-2.i:744:3721-744:3807 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_test5-2.i:744:5106-744:5204 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_test5-2.i:748:2516-748:2602 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_test5-2.i:748:2698-748:2845 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_test5-2.i:748:3093-748:3209 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_test5-2.i:757:546-757:609 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_test5-2.i:757:757-757:846 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_test5-2.i:757:848-757:1208 with factor 5
[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.230
[Info] vars: 828, evals: 31814

[Info] |called|=181

Memory statistics: total=19271.15MB, max=30.86MB, minor=19268.39MB, major=201.52MB, promoted=198.76MB
    minor collections=9205  major collections=34 compactions=0


[Info] runtime: 00:00:20.258
[Info] vars: 831, evals: 36869

[Info] |called|=31

Memory statistics: total=39604.03MB, max=46.93MB, minor=39601.26MB, major=455.51MB, promoted=452.74MB
    minor collections=18912  major collections=57 compactions=0


[Info] runtime: 00:00:30.289
[Info] vars: 832, evals: 39964

[Info] |called|=202

Memory statistics: total=60036.90MB, max=62.07MB, minor=60034.13MB, major=739.50MB, promoted=736.73MB
    minor collections=28664  major collections=75 compactions=0


[Info] runtime: 00:00:40.321
[Info] vars: 833, evals: 42025

[Info] |called|=25

Memory statistics: total=80352.42MB, max=71.38MB, minor=80349.65MB, major=1013.84MB, promoted=1011.06MB
    minor collections=38359  major collections=90 compactions=0


[Info] runtime: 00:00:50.340
[Info] vars: 834, evals: 44234

[Info] |called|=201

Memory statistics: total=100912.92MB, max=82.09MB, minor=100910.14MB, major=1274.52MB, promoted=1271.74MB
    minor collections=48169  major collections=102 compactions=0


[Info] runtime: 00:01:00.379
[Info] vars: 834, evals: 45698

[Info] |called|=207

Memory statistics: total=120536.58MB, max=94.40MB, minor=120533.80MB, major=1554.39MB, promoted=1551.61MB
    minor collections=57532  major collections=113 compactions=0

