./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/benchexec/results/247-all-validate-pr-1709-before/goblint.2025-03-13_10-21-57.files/SV-COMP25_unreach-call/tdh_sys_key_config__cover__success_havoc_object.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/benchexec/results/247-all-validate-pr-1709-before/goblint.2025-03-13_10-21-57.files/SV-COMP25_unreach-call/tdh_sys_key_config__cover__success_havoc_object.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.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
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2011:5-2014:5 with factor 16
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2017:5-2019:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2028:5-2030:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2044:5-2046:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2049:5-2051:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2054:5-2056:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2124:5-2126:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2129:5-2131:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2218:5-2223:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2255:5-2258:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2265:5-2269:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2281:9-2284:9 with factor 16
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2272:5-2286:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2340:5-2343:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2372:5-2375:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2384:5-2387:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2430:9-2433:9 with factor 16
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2421:5-2434:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2633:5-2635:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2666:5-2668:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2682:5-2684:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2748:5-2750:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2756:5-2765:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2776:5-2778:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2849:5-2858:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2889:5-2892:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/intel-tdx-module/tdh_sys_key_config__cover__success_havoc_object.i:2963:5-2965:5 with factor 4
[Info] no thread creation -> disabling analyses: "race, symb_locks, region, deadlock, maylocks, thread, threadid, threadJoins, threadreturn, mhp, pthreadMutexType"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )

[Info] runtime: 00:00:59.842
[Info] vars: 804, evals: 582

[Info] |called|=121

Memory statistics: total=28139.53MB, max=269.46MB, minor=25643.03MB, major=10269.96MB, promoted=7773.46MB
    minor collections=13946  major collections=300 compactions=0


[Info] runtime: 00:01:09.858
[Info] vars: 1147, evals: 848

[Info] |called|=96

Memory statistics: total=33476.25MB, max=269.46MB, minor=30978.58MB, major=11516.75MB, promoted=9019.08MB
    minor collections=16500  major collections=319 compactions=0


[Info] runtime: 00:01:19.872
[Info] vars: 1345, evals: 1005

[Info] |called|=95

Memory statistics: total=38271.10MB, max=269.46MB, minor=35772.35MB, major=12714.16MB, promoted=10215.40MB
    minor collections=18795  major collections=336 compactions=0


[Info] runtime: 00:01:29.902
[Info] vars: 1439, evals: 1081

[Info] |called|=95

Memory statistics: total=42667.37MB, max=309.88MB, minor=40167.59MB, major=13868.83MB, promoted=11369.05MB
    minor collections=20898  major collections=351 compactions=0


[Info] runtime: 00:01:39.923
[Info] vars: 1512, evals: 1141

[Info] |called|=95

Memory statistics: total=47101.05MB, max=309.88MB, minor=44600.31MB, major=15039.21MB, promoted=12538.47MB
    minor collections=23020  major collections=367 compactions=0


[Info] runtime: 00:01:49.937
[Info] vars: 1596, evals: 1211

[Info] |called|=95

Memory statistics: total=51505.64MB, max=309.88MB, minor=49003.88MB, major=16193.99MB, promoted=13692.24MB
    minor collections=25126  major collections=381 compactions=0


[Info] runtime: 00:01:59.950
[Info] vars: 1679, evals: 1283

[Info] |called|=95

Memory statistics: total=56078.04MB, max=309.88MB, minor=53575.29MB, major=17397.03MB, promoted=14894.28MB
    minor collections=27314  major collections=396 compactions=0


[Info] runtime: 00:02:09.964
[Info] vars: 1798, evals: 1477

[Info] |called|=139

Memory statistics: total=60530.40MB, max=309.88MB, minor=58026.61MB, major=18563.80MB, promoted=16060.01MB
    minor collections=29444  major collections=411 compactions=0


[Info] runtime: 00:02:19.979
[Info] vars: 2116, evals: 1668

[Info] |called|=92

Memory statistics: total=65004.80MB, max=309.88MB, minor=62499.94MB, major=19703.67MB, promoted=17198.81MB
    minor collections=31584  major collections=425 compactions=0


[Info] runtime: 00:02:29.994
[Info] vars: 2859, evals: 2160

[Info] |called|=56

Memory statistics: total=70833.65MB, max=309.88MB, minor=68327.47MB, major=20966.68MB, promoted=18460.49MB
    minor collections=34372  major collections