./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/tree_del_iter_incorrect.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/tree_del_iter_incorrect.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/tree_del_iter_incorrect.c


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/tree_del_iter_incorrect.c:56:9-58:9 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/tree_del_iter_incorrect.c:100:5-101:42 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] function nondet_tree is recursive, disable interval and interval_set contexts
[Info] function min is recursive, disable interval and interval_set contexts
[Info] function tree_inorder is recursive, disable interval and interval_set contexts
[Info] function size 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] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] __VERIFIER_assert, tree_inorder, i, count, tmp, key, a, count, j, k, size___0, i, i___0, j___0, a, top, expression, tmp, i, m, n, a, b, t, tmp, tmp___0, t, tmp, tmp___0, i, a, t, tt, p, t, min___0, m, pp, a, b, n, tmp, tmp___0, n, tmp___0, cond, cond
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence

[Info] runtime: 00:00:10.231
[Info] vars: 20083, evals: 27333

[Info] |called|=3633

Memory statistics: total=12137.25MB, max=158.61MB, minor=12132.57MB, major=179.41MB, promoted=174.73MB
    minor collections=5792  major collections=14 compactions=0


[Info] runtime: 00:00:20.355
[Info] vars: 29357, evals: 39979

[Info] |called|=5313

Memory statistics: total=24348.33MB, max=277.41MB, minor=24343.28MB, major=320.97MB, promoted=315.92MB
    minor collections=11615  major collections=15 compactions=0


[Info] runtime: 00:00:30.498
[Info] vars: 35561, evals: 48444

[Info] |called|=6443

Memory statistics: total=35990.30MB, max=366.89MB, minor=35983.50MB, major=441.38MB, promoted=434.58MB
    minor collections=17166  major collections=16 compactions=0


[Info] runtime: 00:00:40.619
[Info] vars: 40071, evals: 54588

[Info] |called|=7261

Memory statistics: total=46556.46MB, max=485.21MB, minor=46549.52MB, major=539.03MB, promoted=532.09MB
    minor collections=22205  major collections=17 compactions=0


[Info] runtime: 00:00:50.735
[Info] vars: 44130, evals: 60129

[Info] |called|=8002

Memory statistics: total=57658.80MB, max=557.99MB, minor=57651.19MB, major=636.74MB, promoted=629.14MB
    minor collections=27499  major collections=17 compactions=0


[Info] runtime: 00:01:00.846
[Info] vars: 47738, evals: 65049

[Info] |called|=8658

Memory statistics: total=68753.36MB, max=641.70MB, minor=68745.37MB, major=729.91MB, promoted=721.92MB
    minor collections=32789  major collections=18 compactions=0

