./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/printf-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/printf-2.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/printf-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/busybox-1.22.0/printf-2.i:2419:3-2442:25 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:2447:5-2457:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:2696:3-2707:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:2796:5-2804:20 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:3006:3-3024:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:3088:9-3094:9 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:3111:11-3117:11 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:3119:7-3130:7 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:3220:3-3231:35 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:3243:3-3251:35 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:3271:5-3294:5 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:3342:3-3343:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:3344:3-3345:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:3396:3-3397:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:3403:3-3409:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:3423:3-3424:34 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:3438:5-3439:42 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:3433:3-3440:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/printf-2.i:3442:3-3443: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] 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.267
[Info] vars: 23645, evals: 26088

[Info] |called|=307

Memory statistics: total=19282.60MB, max=133.72MB, minor=19274.26MB, major=257.43MB, promoted=249.08MB
    minor collections=9199  major collections=18 compactions=0


[Info] runtime: 00:00:20.372
[Info] vars: 44121, evals: 50953

[Info] |called|=219

Memory statistics: total=38670.44MB, max=309.31MB, minor=38658.04MB, major=511.35MB, promoted=498.95MB
    minor collections=18444  major collections=22 compactions=0


[Info] runtime: 00:00:30.468
[Info] vars: 66023, evals: 74140

[Info] |called|=311

Memory statistics: total=57659.97MB, max=409.07MB, minor=57641.13MB, major=734.58MB, promoted=715.75MB
    minor collections=27497  major collections=24 compactions=0


[Info] runtime: 00:00:40.566
[Info] vars: 88683, evals: 99269

[Info] |called|=302

Memory statistics: total=76598.71MB, max=541.00MB, minor=76575.09MB, major=969.66MB, promoted=946.04MB
    minor collections=36526  major collections=25 compactions=0


[Info] runtime: 00:00:50.655
[Info] vars: 109191, evals: 122051

[Info] |called|=298

Memory statistics: total=94577.33MB, max=715.47MB, minor=94550.42MB, major=1196.92MB, promoted=1170.01MB
    minor collections=45098  major collections=26 compactions=0


[Info] runtime: 00:01:00.765
[Info] vars: 128984, evals: 144263

[Info] |called|=299

Memory statistics: total=112490.88MB, max=822.80MB, minor=112460.72MB, major=1414.93MB, promoted=1384.76MB
    minor collections=53639  major collections=27 compactions=0

