./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/test-incomplete-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/test-incomplete-1.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/valid-memsafety.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-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/busybox-1.22.0/test-incomplete-1.i:2850:3-2861:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2889:3-2902:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2909:3-2918:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2939:3-2946:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3073:3-3081:35 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:3-3092:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3232:3-3238:18 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3264:3-3270:18 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3326:3-3327:39 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3394:3-3395:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3396:3-3397:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3448:3-3449:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3455:3-3461:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3475:3-3476:34 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:5-3491:42 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3485:3-3492:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3494:3-3495:23 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] longjmp -> enabling longjmp analyses "activeLongjmp, activeSetjmp, taintPartialContexts, modifiedSinceSetjmp, poisonVariables, expsplit, vla"
[Info] function aexpr is recursive, disable interval and interval_set contexts
[Info] function nexpr is recursive, disable interval and interval_set contexts
[Info] function oexpr is recursive, disable interval and interval_set contexts
[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.242
[Info] vars: 21402, evals: 21679

[Info] |called|=150

Memory statistics: total=19983.54MB, max=132.00MB, minor=19974.41MB, major=237.41MB, promoted=228.27MB
    minor collections=9533  major collections=18 compactions=0


[Info] runtime: 00:00:20.328
[Info] vars: 42012, evals: 43042

[Info] |called|=95

Memory statistics: total=39261.29MB, max=230.87MB, minor=39246.01MB, major=434.10MB, promoted=418.83MB
    minor collections=18724  major collections=21 compactions=0


[Info] runtime: 00:00:30.395
[Info] vars: 62199, evals: 63758

[Info] |called|=113

Memory statistics: total=58467.08MB, max=305.32MB, minor=58447.71MB, major=627.58MB, promoted=608.21MB
    minor collections=27881  major collections=23 compactions=0


[Info] runtime: 00:00:40.493
[Info] vars: 81502, evals: 83362

[Info] |called|=110

Memory statistics: total=77203.86MB, max=403.80MB, minor=77176.20MB, major=818.58MB, promoted=790.92MB
    minor collections=36813  major collections=25 compactions=0


[Info] runtime: 00:00:50.619
[Info] vars: 100007, evals: 102633

[Info] |called|=73

Memory statistics: total=96073.71MB, max=534.03MB, minor=96042.18MB, major=999.75MB, promoted=968.22MB
    minor collections=45810  major collections=26 compactions=0


[Info] runtime: 00:01:00.734
[Info] vars: 119482, evals: 122083

[Info] |called|=109

Memory statistics: total=114929.62MB, max=614.13MB, minor=114893.85MB, major=1186.68MB, promoted=1150.92MB
    minor collections=54800  major collections=27 compactions=0

