./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/split_list_test05-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/split_list_test05-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/memsafety-ext2/split_list_test05-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/memsafety-ext2/split_list_test05-1.i:580:5-582:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memsafety-ext2/split_list_test05-1.i:592:5-594:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memsafety-ext2/split_list_test05-1.i:605:5-607:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memsafety-ext2/split_list_test05-1.i:612:3-619:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memsafety-ext2/split_list_test05-1.i:621:3-625:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memsafety-ext2/split_list_test05-1.i:626:3-630:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memsafety-ext2/split_list_test05-1.i:631:3-635:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memsafety-ext2/split_list_test05-1.i:636:3-640:3 with factor 8
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] malloc wrapper: append
[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.164
[Info] vars: 10957, evals: 9514

[Info] |called|=18

Memory statistics: total=23133.69MB, max=87.49MB, minor=23130.21MB, major=395.38MB, promoted=391.90MB
    minor collections=11047  major collections=35 compactions=0


[Info] runtime: 00:00:20.202
[Info] vars: 14055, evals: 11965

[Info] |called|=51

Memory statistics: total=46477.10MB, max=115.70MB, minor=46473.55MB, major=759.29MB, promoted=755.75MB
    minor collections=22184  major collections=47 compactions=0


[Info] runtime: 00:00:30.250
[Info] vars: 20044, evals: 19077

[Info] |called|=20

Memory statistics: total=69821.62MB, max=133.06MB, minor=69817.17MB, major=1102.49MB, promoted=1098.04MB
    minor collections=33320  major collections=56 compactions=0


[Info] runtime: 00:00:40.315
[Info] vars: 22645, evals: 23714

[Info] |called|=17

Memory statistics: total=92802.20MB, max=153.02MB, minor=92797.44MB, major=1433.48MB, promoted=1428.73MB
    minor collections=44282  major collections=64 compactions=0


[Info] runtime: 00:00:50.373
[Info] vars: 27847, evals: 32868

[Info] |called|=53

Memory statistics: total=115077.68MB, max=153.02MB, minor=115072.85MB, major=1736.46MB, promoted=1731.63MB
    minor collections=54907  major collections=71 compactions=0


[Info] runtime: 00:01:00.421
[Info] vars: 32941, evals: 38474

[Info] |called|=6

Memory statistics: total=138238.71MB, max=175.98MB, minor=138232.77MB, major=2041.93MB, promoted=2035.99MB
    minor collections=65954  major collections=77 compactions=0

