# . * SAT 0 * UNSAT 979 * TIMEOUT 29 * UNKNOWN 0 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/UFDTNIA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-UFDTNIA.tar.zst-do
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 459629c662eb7abf25a010b7383431a9f729d234
Z3 branch: master
Z3 options: "-T:20 model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/UFDTNIA.tar.zst?download=1
Z3 commit message: bugfixes to ho_matcher

Signed-off-by: Nikolaj Bjorner
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.mult_leq_mono2._01.smt2 | 0.031s | 19.892MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.19.smt2 | 0.033s | 19.976MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-constants.6.smt2 | 0.033s | 20.68MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.17.smt2 | 0.036s | 20.396MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extra.1.smt2 | 0.036s | 19.868MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__math_v.smt2 | 0.037s | 20.936MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.39.smt2 | 0.039s | 19.928MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.27.smt2 | 0.039s | 20.484MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_t.25.smt2 | 0.043s | 20.156MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-spec_t__hardware.1.smt2 | 0.043s | 20.052MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout__align_downlib_layout.align_down._02.smt2 | 0.045s | 21.008MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.29.smt2 | 0.047s | 19.904MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.27.smt2 | 0.047s | 20.364MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.36.smt2 | 0.047s | 20.316MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_alloc.6.smt2 | 0.047s | 20.576MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-constants.3.smt2 | 0.048s | 19.636MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.37.smt2 | 0.050s | 20.108MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.22.smt2 | 0.052s | 20.032MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.22.smt2 | 0.054s | 20.344MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.16.smt2 | 0.055s | 19.976MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.9.smt2 | 0.055s | 21.316MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/lock__spincell_e.6.smt2 | 0.056s | 21.396MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.20.smt2 | 0.060s | 19.948MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__indexinglib_impl_u.indexing.lemma_entry_base_from_index_support._02.smt2 | 0.060s | 21.108MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.23.smt2 | 0.061s | 21.356MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-spec_t__hardware.17.smt2 | 0.061s | 19.944MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l0.6.smt2 | 0.062s | 19.944MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_small_mod._01.smt2 | 0.063s | 20.88MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl__PT.5.smt2 | 0.065s | 20.548MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__math_vlib_marshalling.math_v.distribute_left._01.smt2 | 0.066s | 21.176MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.5.smt2 | 0.067s | 20.996MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extra.3.smt2 | 0.067s | 21.528MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_is_distributive_sub_other_way._01.smt2 | 0.067s | 20.98MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__layout_v.30.smt2 | 0.068s | 22.596MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_t.15.smt2 | 0.069s | 21.716MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-spec_t__hardware.6.smt2 | 0.069s | 20.092MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.18.smt2 | 0.069s | 20.16MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__pow_p.1.smt2 | 0.070s | 20.636MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.10.smt2 | 0.070s | 21.98MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l0.14.smt2 | 0.070s | 19.86MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.28.smt2 | 0.070s | 23.492MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__math_v.smt2 | 0.070s | 20.94MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.43.smt2 | 0.071s | 21.652MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__setlib.11.smt2 | 0.071s | 22.312MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_t.18.smt2 | 0.071s | 20.096MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__UniformSizedSeq_v.2.smt2 | 0.071s | 22.516MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_is_distributive_add._01.smt2 | 0.075s | 21.028MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.lemma_aligned_iff_eq_mul_div._02.smt2 | 0.075s | 21.348MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_fundamental_div_mod_converse_helper_1._01.smt2 | 0.075s | 20.652MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_fundamental_div_mod_converse_helper_2._01.smt2 | 0.075s | 20.856MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-spec_t__hardware.2.smt2 | 0.076s | 19.956MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.10.smt2 | 0.076s | 21.092MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.32.smt2 | 0.076s | 20.372MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__indexinglib_impl_u.indexing.lemma_entry_base_from_index._01.smt2 | 0.077s | 21.132MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__indexinglib_impl_u.indexing.lemma_index_from_base_and_addr._01.smt2 | 0.077s | 21.628MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_u.1.smt2 | 0.077s | 20.156MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.mod_less_eq._01.smt2 | 0.077s | 21.32MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/util__page_ptr_util_u.13.smt2 | 0.078s | 20.072MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__pgtable__memmap_p.3.smt2 | 0.078s | 24.472MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.28.smt2 | 0.078s | 22.888MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.lemma_aligned_iff_eq_mul_div._01.smt2 | 0.078s | 21.492MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extra.7.smt2 | 0.079s | 21.132MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__indexinglib_impl_u.indexing.lemma_entry_base_from_index._05.smt2 | 0.079s | 21.396MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.aligned_transitive._02.smt2 | 0.079s | 21.712MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.23.smt2 | 0.081s | 19.956MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-spec_t__hardware.4.smt2 | 0.082s | 20.14MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizeslib_bin_sizes.mod8._01.smt2 | 0.082s | 21.836MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l0.15.smt2 | 0.082s | 22.064MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.32.smt2 | 0.082s | 21.396MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.mod_mult_zero_implies_mod_zero._01.smt2 | 0.083s | 21.6MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout__two_mul_with_bit1.smt2 | 0.083s | 20.912MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.22.smt2 | 0.084s | 21.36MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.2.smt2 | 0.084s | 21.324MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl.1.smt2 | 0.084s | 22.192MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.38.smt2 | 0.084s | 20.276MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.44.smt2 | 0.086s | 21.66MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/ironkv-smt-verus_extra__seq_lib_vlib_verus_extra.seq_lib_v.lemma_seq_fold_left_sum_le._01.smt2 | 0.086s | 21.544MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/lemma__lemma_u.1.smt2 | 0.087s | 21.708MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.21.smt2 | 0.087s | 20.396MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl__PT.1.smt2 | 0.087s | 20.472MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__bits_p.7.smt2 | 0.088s | 24.208MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__KVPairFormat_v.1.smt2 | 0.089s | 22.4MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.3.smt2 | 0.089s | 22.16MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__pgtable__memmap_p.5.smt2 | 0.090s | 22.076MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.mul_commute._01.smt2 | 0.090s | 21.252MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_one_to_one._01.smt2 | 0.090s | 21.524MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.16.smt2 | 0.090s | 21.088MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__align_sverismo_tspec.math.align_s.proof_align_down._01.smt2 | 0.091s | 21.38MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_t.13.smt2 | 0.091s | 21.72MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l0.24.smt2 | 0.091s | 22.404MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.18.smt2 | 0.092s | 21.284MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__UniformSizedSeq_v.5.smt2 | 0.092s | 22.612MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.7.smt2 | 0.092s | 22.016MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_ulib_definitions_u.impl_%2.index_for_vaddr._01.smt2 | 0.092s | 22.088MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.5.smt2 | 0.095s | 21.356MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.2.smt2 | 0.095s | 21.584MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__math_vlib_marshalling.math_v.distribute_left._01.smt2 | 0.095s | 21.16MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.1.smt2 | 0.095s | 24.164MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_ulib_definitions_u.impl_%3.lemma_entry_sizes_increase._01.smt2 | 0.096s | 23.068MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_t.22.smt2 | 0.097s | 21.82MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.40.smt2 | 0.097s | 22.128MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.33.smt2 | 0.098s | 21.716MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__KVPairFormat_v.7.smt2 | 0.098s | 22.044MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l0.5.smt2 | 0.098s | 21.552MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.7.smt2 | 0.098s | 22.632MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_t.20.smt2 | 0.098s | 20.124MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.31.smt2 | 0.100s | 21.388MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.33.smt2 | 0.100s | 22.972MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l0.19.smt2 | 0.101s | 23.512MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-alloc_generic.2.smt2 | 0.101s | 21.48MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_ulib_definitions_u.overflow_bounds._02.smt2 | 0.101s | 22.56MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.13.smt2 | 0.102s | 21.244MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl.14.smt2 | 0.103s | 21.708MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.20.smt2 | 0.103s | 21.24MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.15.smt2 | 0.103s | 21.86MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.27.smt2 | 0.104s | 21.26MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.4.smt2 | 0.104s | 21.096MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_alloc.3.smt2 | 0.104s | 23.184MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_is_distributive._01.smt2 | 0.106s | 21.584MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__rmp__rmp_t.7.smt2 | 0.107s | 22.32MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.12.smt2 | 0.107s | 22.148MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.15.smt2 | 0.108s | 23.64MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.15.smt2 | 0.108s | 22.752MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.4.smt2 | 0.109s | 23.816MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.10.smt2 | 0.110s | 21.172MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_ulib_definitions_u.impl_%2.next_entry_base._02.smt2 | 0.110s | 21.9MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.6.smt2 | 0.110s | 24.296MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.1.smt2 | 0.111s | 22.896MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.3.smt2 | 0.111s | 21.192MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__UniformSizedSeq_v.5.smt2 | 0.111s | 22.832MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.25.smt2 | 0.112s | 21.388MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__bit_p.smt2 | 0.112s | 23.404MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-spec_t__hardware.21.smt2 | 0.112s | 22.616MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__UniformSizedSeq_v.1.smt2 | 0.112s | 22.428MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.2.smt2 | 0.113s | 20.652MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizeslib_bin_sizes.lemma_div_is_ordered._01.smt2 | 0.113s | 22.292MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__addr_s__def_s.3.smt2 | 0.114s | 20.576MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.1.smt2 | 0.114s | 21.16MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__UniformSizedSeq_v.2.smt2 | 0.115s | 22.608MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.13.smt2 | 0.115s | 24.204MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.24.smt2 | 0.115s | 20.364MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.27.smt2 | 0.117s | 24.432MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.10.smt2 | 0.117s | 22.212MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-root.smt2 | 0.117s | 23.828MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extra.8.smt2 | 0.117s | 21.336MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.2.smt2 | 0.118s | 20.92MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__layout_v.31.smt2 | 0.118s | 24.768MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_is_associative._01.smt2 | 0.118s | 21.284MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__ResizableUniformSizedSeq_v.4.smt2 | 0.119s | 23.32MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.mult_less_mono_both2._01.smt2 | 0.120s | 21.768MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-init.1.smt2 | 0.120s | 22.008MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.12.smt2 | 0.120s | 24.532MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl.5.smt2 | 0.121s | 23.036MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/va_range.2.smt2 | 0.122s | 22.468MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.26.smt2 | 0.122s | 21.376MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__rmp__rmp_t.8.smt2 | 0.123s | 22.34MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.13.smt2 | 0.123s | 22.344MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.38.smt2 | 0.124s | 23.2MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl__PT.8.smt2 | 0.124s | 25.024MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-pmem__pmcopy_t.3.smt2 | 0.124s | 22.284MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__rmp__rmp_t.6.smt2 | 0.127s | 22.404MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.5.smt2 | 0.127s | 22.888MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.22.smt2 | 0.127s | 24.044MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.20.smt2 | 0.128s | 22.632MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.1.smt2 | 0.128s | 22.844MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-init.10.smt2 | 0.129s | 21.78MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__bits_p.4.smt2 | 0.130s | 19.852MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/util__page_ptr_util_u.8.smt2 | 0.131s | 22.204MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__setlib.12.smt2 | 0.131s | 22.156MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_ulib_definitions_u.impl_%2.entry_base._01.smt2 | 0.131s | 23.252MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_t.24.smt2 | 0.131s | 21.772MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__rmp__rmp_t.2.smt2 | 0.132s | 22.408MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/vcell__vcell.smt2 | 0.132s | 20.656MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.42.smt2 | 0.132s | 22.88MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.34.smt2 | 0.133s | 23.792MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__addr_s__page.1.smt2 | 0.134s | 22.196MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page.15.smt2 | 0.134s | 21.68MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_div_equal._01.smt2 | 0.134s | 21.672MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-spec_t__hardware.7.smt2 | 0.134s | 20.036MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-constants.8.smt2 | 0.135s | 20.864MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.10.smt2 | 0.138s | 22.136MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.24.smt2 | 0.138s | 22.72MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_alloc.8.smt2 | 0.138s | 20.46MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.11.smt2 | 0.139s | 22.956MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_left_inequality._01.smt2 | 0.139s | 21.42MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layoutlib_layout.calculate_page_block_at._02.smt2 | 0.139s | 23.92MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-main_t.7.smt2 | 0.140s | 22.772MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.31.smt2 | 0.140s | 23.772MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.14.smt2 | 0.140s | 23.676MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_ulib_definitions_u.impl_%2.next_entry_base._01.smt2 | 0.141s | 23.016MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__bits_p.9.smt2 | 0.142s | 30.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.23.smt2 | 0.142s | 23.136MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.2.smt2 | 0.143s | 22.18MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.15.smt2 | 0.144s | 22.88MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__layout_v.26.smt2 | 0.144s | 22.36MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__cast.2.smt2 | 0.145s | 25.24MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpuid.13.smt2 | 0.146s | 22.92MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l0.23.smt2 | 0.146s | 24.236MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.26.smt2 | 0.148s | 23.82MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__idt__def.3.smt2 | 0.149s | 22.292MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layoutlib_layout.bitand_with_mask_gives_rounding._09.smt2 | 0.149s | 24.592MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer.5.smt2 | 0.149s | 23.172MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/util__page_ptr_util_u.14.smt2 | 0.150s | 22.424MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.mult_leq_mono_both._01.smt2 | 0.151s | 21.676MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.27.smt2 | 0.152s | 22.804MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/ironkv-smt-verus_extra__seq_lib_v.15.smt2 | 0.153s | 22.392MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout__two_mul_with_bit1lib_layout.two_mul_with_bit1._01.smt2 | 0.155s | 21.392MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.6.smt2 | 0.156s | 21.984MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_u.11.smt2 | 0.156s | 22.704MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.5.smt2 | 0.157s | 24.56MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.12.smt2 | 0.157s | 24.3MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/memory_manager__spec_impl.2.smt2 | 0.158s | 25.456MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpuid.5.smt2 | 0.158s | 22.668MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1lib_impl_u.l1.impl_%1.lemma_ranges_disjoint_interp_aux_interp_of_entry._01.smt2 | 0.158s | 23.984MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.2.smt2 | 0.159s | 22.728MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.16.smt2 | 0.160s | 25.46MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.14.smt2 | 0.161s | 22.912MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.24.smt2 | 0.161s | 21.392MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/memory_manager__spec_impl.8.smt2 | 0.162s | 25.84MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__size_s.4.smt2 | 0.164s | 26.156MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.7.smt2 | 0.166s | 22.9MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer.4.smt2 | 0.168s | 23.216MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.6.smt2 | 0.169s | 23.036MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_t.11.smt2 | 0.169s | 21.684MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-alloc_generic__page_free_list_extendlib_alloc_generic.page_free_list_extend._07.smt2 | 0.170s | 26.42MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__integer.2.smt2 | 0.171s | 25.316MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/trusted_hacl__stub.7.smt2 | 0.171s | 22.124MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/lemma__lemma_u.2.smt2 | 0.173s | 24.208MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__replica.1.smt2 | 0.173s | 26.212MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-spec_t__hardware.19.smt2 | 0.173s | 22.636MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.35.smt2 | 0.173s | 25.772MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-alloc_generic__page_free_list_extendlib_alloc_generic.page_free_list_extend._04.smt2 | 0.174s | 26.524MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__layout_v.27.smt2 | 0.174s | 22.564MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-main_t.4.smt2 | 0.174s | 25.464MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__ptram__ptram_u.smt2 | 0.175s | 25.708MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__pgtable__entry_p.3.smt2 | 0.175s | 25.224MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.42.smt2 | 0.175s | 25.008MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__bits_p.8.smt2 | 0.176s | 27.624MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_listlib_linked_list.impl_%2.prepend_contiguous_blocks._05.smt2 | 0.179s | 26.404MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpuid.11.smt2 | 0.181s | 22.844MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.22.smt2 | 0.181s | 24.692MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__stream__basic.1.smt2 | 0.184s | 21.08MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/registers__msr_t.11.smt2 | 0.187s | 26.86MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.45.smt2 | 0.187s | 25.896MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.3.smt2 | 0.188s | 26.668MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__log.7.smt2 | 0.188s | 26.304MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.4.smt2 | 0.189s | 24.68MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-init.11.smt2 | 0.190s | 29.436MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__stream__basic.2.smt2 | 0.192s | 21.66MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/primitives_e__seq.2.smt2 | 0.193s | 25.412MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/registers__msr_t.3.smt2 | 0.194s | 26.776MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/registers__msr_t.2.smt2 | 0.194s | 26.72MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec.4.smt2 | 0.195s | 26.952MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_listlib_linked_list.impl_%2.prepend_contiguous_blocks._03.smt2 | 0.195s | 26.252MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.39.smt2 | 0.196s | 26.392MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_listlib_linked_list.impl_%2.prepend_contiguous_blocks._08.smt2 | 0.197s | 26.44MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.36.smt2 | 0.199s | 27.452MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.51.smt2 | 0.199s | 24.768MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__addr_interface.11.smt2 | 0.200s | 29.516MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layoutlib_layout.calculate_slice_page_ptr_from_block._01.smt2 | 0.200s | 23.796MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.13.smt2 | 0.202s | 25.028MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_listlib_linked_list.impl_%2.prepend_contiguous_blocks._09.smt2 | 0.203s | 26.28MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.23.smt2 | 0.203s | 24.66MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.3.smt2 | 0.204s | 21.636MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.12.smt2 | 0.204s | 26.348MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__snp_u.8.smt2 | 0.205s | 28.348MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-alloc_generic__page_free_list_extendlib_alloc_generic.page_free_list_extend._09.smt2 | 0.205s | 27.848MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__pgtable__entry_p.7.smt2 | 0.206s | 23.692MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.11.smt2 | 0.206s | 30.552MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.17.smt2 | 0.207s | 23.22MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__UniformSizedSeq_v.4.smt2 | 0.207s | 23.184MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.1.smt2 | 0.208s | 32.928MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.3.smt2 | 0.208s | 22.188MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec_e__size_e.smt2 | 0.209s | 27.236MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.17.smt2 | 0.211s | 23.024MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.6.smt2 | 0.211s | 24.68MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.42.smt2 | 0.211s | 27.956MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.11.smt2 | 0.212s | 25.484MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_utillib_os_mem_util.preserves_mem_chunk_good_except._01.smt2 | 0.212s | 28.292MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__addr_interface.13.smt2 | 0.214s | 29.512MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.5.smt2 | 0.214s | 25.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.35.smt2 | 0.214s | 25.992MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.42.smt2 | 0.214s | 27.244MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__cast.5.smt2 | 0.215s | 27.024MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__ResizableUniformSizedSeq_v.3.smt2 | 0.215s | 24.236MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.60.smt2 | 0.216s | 29.916MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.3.smt2 | 0.218s | 25.868MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.17.smt2 | 0.218s | 26.104MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.10.smt2 | 0.220s | 21.608MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__params.8.smt2 | 0.221s | 23.788MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.61.smt2 | 0.222s | 27.844MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.33.smt2 | 0.223s | 27.496MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.20.smt2 | 0.224s | 27.036MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbufferlib_spec.cyclicbuffer.log_entry_alive_value_wrap_around._01.smt2 | 0.224s | 23.732MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.19.smt2 | 0.225s | 25.3MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1lib_impl_u.l1.impl_%1.lemma_interp_of_entries_disjoint._04.smt2 | 0.226s | 25.884MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__params.5.smt2 | 0.227s | 23.904MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.9.smt2 | 0.228s | 22.144MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.26.smt2 | 0.228s | 26.78MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.23.smt2 | 0.228s | 27.172MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.41.smt2 | 0.228s | 23.52MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.3.smt2 | 0.228s | 25.4MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__ptram__ptram_s.smt2 | 0.230s | 25.468MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__layout_v.32.smt2 | 0.230s | 25.712MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__addr_s__def_s.8.smt2 | 0.231s | 26.244MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.21.smt2 | 0.231s | 29.132MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__multilogimpl_v.1.smt2 | 0.231s | 24.792MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout__align_down.smt2 | 0.231s | 21.944MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.1.smt2 | 0.233s | 24.82MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-alloc_fast.4.smt2 | 0.234s | 26.66MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.32.smt2 | 0.235s | 25.956MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.98.smt2 | 0.236s | 29.8MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.3.smt2 | 0.236s | 29.264MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.30.smt2 | 0.236s | 24.856MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.12.smt2 | 0.237s | 26.792MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.19.smt2 | 0.237s | 24.752MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.51.smt2 | 0.238s | 29.044MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__replica.19.smt2 | 0.238s | 26.808MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.11.smt2 | 0.238s | 29.048MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.5.smt2 | 0.240s | 25.892MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.19.smt2 | 0.241s | 33.176MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.49.smt2 | 0.241s | 28.804MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.2.smt2 | 0.241s | 26.536MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__ResizableUniformSizedSeq_v.9.smt2 | 0.241s | 25.508MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype_test.1.smt2 | 0.242s | 29.62MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/memory_manager__spec_impl.9.smt2 | 0.243s | 25.932MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/primitives_e__vec.2.smt2 | 0.243s | 27.256MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.140.smt2 | 0.244s | 30.516MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpuid.2.smt2 | 0.245s | 22.88MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/primitives_e__vec.1.smt2 | 0.246s | 27.392MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_listlib_linked_list.impl_%2.prepend_contiguous_blocks._06.smt2 | 0.246s | 26.452MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__rmp__rmp_t.5.smt2 | 0.247s | 22.408MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.9.smt2 | 0.249s | 26.704MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-root.5.smt2 | 0.249s | 26.14MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__replica.6.smt2 | 0.250s | 27.884MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.6.smt2 | 0.253s | 32.324MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.130.smt2 | 0.253s | 30.328MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.32.smt2 | 0.253s | 25.792MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.18.smt2 | 0.253s | 31.432MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.30.smt2 | 0.254s | 25.784MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__log.3.smt2 | 0.254s | 26.856MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.7.smt2 | 0.255s | 28.708MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-pagelib_page.page_init._02.smt2 | 0.256s | 29.112MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-alloc_generic__page_free_list_extendlib_alloc_generic.page_free_list_extend._05.smt2 | 0.256s | 27.752MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.16.smt2 | 0.256s | 25.516MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.14.smt2 | 0.257s | 36.272MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__ResizableUniformSizedSeq_v.9.smt2 | 0.258s | 25.296MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.6.smt2 | 0.259s | 30.284MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.26.smt2 | 0.260s | 28.968MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.2.smt2 | 0.261s | 33.664MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.51.smt2 | 0.264s | 30.412MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.6.smt2 | 0.265s | 27.208MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.34.smt2 | 0.266s | 28.9MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.48.smt2 | 0.267s | 30.588MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-alloc_generic__page_free_list_extendlib_alloc_generic.page_free_list_extend._06.smt2 | 0.267s | 28.716MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.97.smt2 | 0.268s | 30.984MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.165.smt2 | 0.268s | 30.776MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.15.smt2 | 0.268s | 28.844MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.32.smt2 | 0.269s | 30.508MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__addr_interface.10.smt2 | 0.270s | 29.484MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.32.smt2 | 0.271s | 26.472MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_refinement.1.smt2 | 0.271s | 27.9MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.56.smt2 | 0.273s | 30.688MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__log.20.smt2 | 0.274s | 27.196MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.8.smt2 | 0.275s | 34.02MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__addr_s__page.6.smt2 | 0.275s | 23.668MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__replica.4.smt2 | 0.275s | 28.288MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page.8.smt2 | 0.275s | 32.988MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.22.smt2 | 0.275s | 26.484MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.64.smt2 | 0.277s | 28.02MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__snp_u.13.smt2 | 0.278s | 30.668MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.17.smt2 | 0.278s | 28.212MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__addr_interface.3.smt2 | 0.279s | 29.024MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.11.smt2 | 0.280s | 28.784MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.20.smt2 | 0.281s | 33.244MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__addr_interface.16.smt2 | 0.281s | 29.36MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.26.smt2 | 0.281s | 29.9MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.8.smt2 | 0.281s | 26.584MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.40.smt2 | 0.282s | 30.648MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/pagetable__pagetable_spec_impl.10.smt2 | 0.283s | 33.9MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__range_interface.13.smt2 | 0.283s | 32.224MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.34.smt2 | 0.283s | 29.732MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.50.smt2 | 0.284s | 30.644MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/registers__msr_t.7.smt2 | 0.284s | 26.648MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec_e__math__bits_e.1.smt2 | 0.286s | 33.2MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-segment.5.smt2 | 0.288s | 30.796MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.17.smt2 | 0.289s | 25.28MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__log.1.smt2 | 0.291s | 27.176MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.13.smt2 | 0.293s | 27.16MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.24.smt2 | 0.294s | 28.024MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.54.smt2 | 0.294s | 30.272MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.53.smt2 | 0.295s | 30.212MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.43.smt2 | 0.296s | 28.58MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_utillib_os_mem_util.preserves_mem_chunk_good_on_transfer_to_capacity._02.smt2 | 0.296s | 28.316MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.35.smt2 | 0.297s | 27.368MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.4.smt2 | 0.299s | 26.708MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__ResizableUniformSizedSeq_v.10.smt2 | 0.300s | 24.828MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__log.16.smt2 | 0.300s | 26.5MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.53.smt2 | 0.300s | 30.952MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.45.smt2 | 0.301s | 29.124MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.239.smt2 | 0.301s | 31.336MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec.3.smt2 | 0.301s | 28.296MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.3.smt2 | 0.302s | 35.884MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec_e__math__bits_e.8.smt2 | 0.303s | 31.608MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.12.smt2 | 0.304s | 29.728MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/pagetable__pagetable_spec_impl.11.smt2 | 0.305s | 34.932MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__snp_u.2.smt2 | 0.306s | 27.664MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.38.smt2 | 0.307s | 28.628MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.199.smt2 | 0.308s | 30.816MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__def_s.2.smt2 | 0.308s | 26.472MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.27.smt2 | 0.308s | 34.268MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.35.smt2 | 0.311s | 25.784MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__range_interface.5.smt2 | 0.312s | 27.988MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.115.smt2 | 0.313s | 31.812MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.81.smt2 | 0.314s | 30.792MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.19.smt2 | 0.315s | 29.02MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__range_interface.7.smt2 | 0.316s | 28.7MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.119.smt2 | 0.316s | 31.768MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.71.smt2 | 0.319s | 28.472MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-alloc_generic__page_free_list_extendlib_alloc_generic.page_free_list_extend._03.smt2 | 0.322s | 28.396MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.40.smt2 | 0.323s | 33.144MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.122.smt2 | 0.327s | 33.244MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.28.smt2 | 0.329s | 25.872MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.32.smt2 | 0.329s | 29.924MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.209.smt2 | 0.330s | 31.208MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.41.smt2 | 0.330s | 29.112MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.8.smt2 | 0.331s | 30.308MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.102.smt2 | 0.333s | 29.788MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.24.smt2 | 0.334s | 32.692MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.66.smt2 | 0.334s | 29.216MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__cast.6.smt2 | 0.335s | 28.02MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.41.smt2 | 0.335s | 28.66MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.186.smt2 | 0.337s | 32.52MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.47.smt2 | 0.338s | 31.028MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.175.smt2 | 0.339s | 33.748MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.108.smt2 | 0.339s | 31.008MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__cast.7.smt2 | 0.339s | 28.192MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.40.smt2 | 0.340s | 27.328MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.109.smt2 | 0.341s | 33.088MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.99.smt2 | 0.343s | 29.816MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.15.smt2 | 0.343s | 29.572MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.5.smt2 | 0.345s | 29.992MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.72.smt2 | 0.347s | 30.72MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__exe.1.smt2 | 0.347s | 31.632MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-alloc_generic.9.smt2 | 0.347s | 35.252MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.7.smt2 | 0.348s | 32.12MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec.1.smt2 | 0.348s | 26.844MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.33.smt2 | 0.348s | 26.216MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.216.smt2 | 0.350s | 33.032MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.9.smt2 | 0.351s | 31.044MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.16.smt2 | 0.351s | 28.292MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.47.smt2 | 0.351s | 26.068MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/lock__spincell_e.1.smt2 | 0.352s | 38.232MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.44.smt2 | 0.352s | 33.012MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.30.smt2 | 0.352s | 32.844MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_ulib_definitions_u.x86_arch_inv._01.smt2 | 0.352s | 24.024MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.31.smt2 | 0.352s | 32.236MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.19.smt2 | 0.353s | 29.98MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__snp_u.15.smt2 | 0.356s | 32.788MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.413.smt2 | 0.357s | 33.04MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.178.smt2 | 0.359s | 31.58MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.10.smt2 | 0.360s | 26.688MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__multilogimpl_v.12.smt2 | 0.360s | 31.072MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.21.smt2 | 0.361s | 34.296MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-segment__segment_alloclib_segment.segment_alloc._02.smt2 | 0.361s | 28.596MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.21.smt2 | 0.361s | 33.692MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.21.smt2 | 0.362s | 34.736MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.172.smt2 | 0.362s | 33.804MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_e.12.smt2 | 0.362s | 34.84MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.297.smt2 | 0.364s | 32.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.155.smt2 | 0.364s | 30.72MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-init.12.smt2 | 0.365s | 29.736MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__log.8.smt2 | 0.365s | 27.892MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.11.smt2 | 0.366s | 35.368MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.151.smt2 | 0.369s | 34.152MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__replica.12.smt2 | 0.372s | 28.044MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.55.smt2 | 0.374s | 32.104MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.91.smt2 | 0.376s | 33.1MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.13.smt2 | 0.379s | 35.316MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.19.smt2 | 0.379s | 35.588MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.403.smt2 | 0.379s | 32.932MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.24.smt2 | 0.380s | 27.12MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.56.smt2 | 0.380s | 28.272MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.11.smt2 | 0.380s | 30.672MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__log.14.smt2 | 0.383s | 27.788MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.45.smt2 | 0.384s | 32.624MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.193.smt2 | 0.387s | 35.452MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.213.smt2 | 0.387s | 35.78MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.28.smt2 | 0.388s | 27.996MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__ResizableUniformSizedSeq_v.7.smt2 | 0.389s | 25.704MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__UniformSizedSeq_v.6.smt2 | 0.391s | 24.82MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.49.smt2 | 0.392s | 32.872MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.220.smt2 | 0.394s | 34.676MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.95.smt2 | 0.394s | 30.688MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.57.smt2 | 0.395s | 30.292MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.32.smt2 | 0.397s | 29.876MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec_e__math__bits_e.3.smt2 | 0.398s | 32.364MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.366.smt2 | 0.399s | 32.612MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.336.smt2 | 0.399s | 32.256MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.184.smt2 | 0.399s | 32.348MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/pagetable__pagetable_spec_impl.6.smt2 | 0.401s | 35.296MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.281.smt2 | 0.401s | 36.256MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.39.smt2 | 0.401s | 29.056MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.51.smt2 | 0.401s | 31.28MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.44.smt2 | 0.404s | 31.936MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.350.smt2 | 0.408s | 34.268MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.85.smt2 | 0.409s | 30.768MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.68.smt2 | 0.410s | 29.876MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-segment__segments_page_find_and_allocate.3.smt2 | 0.412s | 33.58MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__os_refinement.1.smt2 | 0.412s | 30.48MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.7.smt2 | 0.413s | 23.476MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__range_interface.10.smt2 | 0.415s | 31.448MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.26.smt2 | 0.415s | 33.4MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.364.smt2 | 0.416s | 35.984MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.168.smt2 | 0.417s | 34.044MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.19.smt2 | 0.417s | 28.268MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.5.smt2 | 0.420s | 31.376MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.380.smt2 | 0.424s | 33.456MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.52.smt2 | 0.425s | 30.64MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.196.smt2 | 0.426s | 34.308MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/memory_manager__spec_impl.12.smt2 | 0.427s | 25.712MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__mshyper__param_e.5.smt2 | 0.427s | 32.052MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.2.smt2 | 0.429s | 36.08MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.86.smt2 | 0.432s | 33.168MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.26.smt2 | 0.434s | 34.412MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.11.smt2 | 0.435s | 33.288MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl__PT.10.smt2 | 0.435s | 29.36MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.77.smt2 | 0.437s | 32.944MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__params.23.smt2 | 0.437s | 39.676MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.371.smt2 | 0.441s | 33.404MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.27.smt2 | 0.443s | 30.312MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype_test.8.smt2 | 0.449s | 29.548MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.201.smt2 | 0.451s | 34.192MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__addr_interface.2.smt2 | 0.451s | 28.656MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.23.smt2 | 0.451s | 27.528MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.162.smt2 | 0.452s | 31.504MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.78.smt2 | 0.453s | 30.028MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__pgtable__entry_p.4.smt2 | 0.454s | 26.74MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_e.13.smt2 | 0.454s | 34.9MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.418.smt2 | 0.455s | 33.128MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__snp_u.16.smt2 | 0.458s | 34.868MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.20.smt2 | 0.458s | 29.764MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.28.smt2 | 0.458s | 33.5MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__integer.8.smt2 | 0.459s | 24.076MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.4.smt2 | 0.460s | 31.872MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.198.smt2 | 0.461s | 35.46MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.286.smt2 | 0.462s | 36.168MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.58.smt2 | 0.462s | 32.248MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.17.smt2 | 0.462s | 31.04MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.329.smt2 | 0.464s | 36.552MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.53.smt2 | 0.464s | 28.088MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__cast.4.smt2 | 0.468s | 27.748MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.148.smt2 | 0.469s | 33.772MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.18.smt2 | 0.469s | 23.08MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.393.smt2 | 0.472s | 33.056MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.415.smt2 | 0.473s | 36.408MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.341.smt2 | 0.475s | 35.792MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.34.smt2 | 0.475s | 51.496MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.6.smt2 | 0.476s | 33.304MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.18.smt2 | 0.476s | 22.196MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.265.smt2 | 0.477s | 35.124MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.408.smt2 | 0.477s | 33.084MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpuid.16.smt2 | 0.477s | 42.368MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.42.smt2 | 0.478s | 31.824MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.88.smt2 | 0.478s | 29.86MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-segment__segment_span_allocate.1.smt2 | 0.480s | 34.12MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec_e__math__bits_e.5.smt2 | 0.483s | 33.384MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__idt__dummy.2.smt2 | 0.488s | 33.884MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.69.smt2 | 0.488s | 31.816MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.152.smt2 | 0.489s | 33.776MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec_e__math__align_e.1.smt2 | 0.491s | 32.824MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.6.smt2 | 0.493s | 34.772MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__range_interface.15.smt2 | 0.494s | 32.8MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.176.smt2 | 0.495s | 33.816MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.423.smt2 | 0.496s | 33.076MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.21.smt2 | 0.497s | 24.596MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.237.smt2 | 0.500s | 34.596MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.240.smt2 | 0.504s | 35.216MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.83.smt2 | 0.505s | 29.408MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.73.smt2 | 0.507s | 33.024MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-alloc_fast.3.smt2 | 0.510s | 36.088MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/ironkv-smt-verus_extra__seq_lib_v.5.smt2 | 0.511s | 22.512MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.22.smt2 | 0.513s | 33.74MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.121.smt2 | 0.514s | 33.216MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/allocator__page_allocator_spec_impl.7.smt2 | 0.515s | 30.496MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.12.smt2 | 0.515s | 37.656MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.46.smt2 | 0.515s | 32.716MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.19.smt2 | 0.515s | 30.588MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.26.smt2 | 0.516s | 40.836MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.370.smt2 | 0.516s | 33.348MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.2.smt2 | 0.518s | 39.196MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__pcr.8.smt2 | 0.520s | 51.112MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__log.10.smt2 | 0.520s | 30.24MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.3.smt2 | 0.520s | 28.144MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.3.smt2 | 0.521s | 32.276MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.381.smt2 | 0.522s | 34.288MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.282.smt2 | 0.525s | 31.956MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.22.smt2 | 0.526s | 29.26MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.21.smt2 | 0.527s | 34.82MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.39.smt2 | 0.529s | 34.144MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__ptram__ptram_p.6.smt2 | 0.530s | 33.324MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.18.smt2 | 0.530s | 35.584MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.391.smt2 | 0.538s | 32.732MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.395.smt2 | 0.538s | 36.024MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.363.smt2 | 0.539s | 32.504MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.29.smt2 | 0.540s | 40.672MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.256.smt2 | 0.540s | 34.416MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.9.smt2 | 0.541s | 33.388MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.5.smt2 | 0.542s | 29.984MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.388.smt2 | 0.545s | 32.712MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.149.smt2 | 0.552s | 35.004MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.18.smt2 | 0.554s | 37.424MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.233.smt2 | 0.555s | 35.7MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.274.smt2 | 0.556s | 35.008MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__mshyper__param_e.1.smt2 | 0.558s | 35.428MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.41.smt2 | 0.561s | 27.748MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/pagetable__pagetable_spec_impl.7.smt2 | 0.563s | 37.056MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.225.smt2 | 0.563s | 34.684MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_e.15.smt2 | 0.566s | 34.284MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.283.smt2 | 0.569s | 35.556MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.208.smt2 | 0.571s | 35.84MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.38.smt2 | 0.571s | 33.244MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.226.smt2 | 0.573s | 34.476MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.7.smt2 | 0.576s | 27.952MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.324.smt2 | 0.578s | 34.924MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.124.smt2 | 0.580s | 34.872MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.372.smt2 | 0.581s | 35.844MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.338.smt2 | 0.581s | 32.26MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.9.smt2 | 0.584s | 41.968MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.306.smt2 | 0.586s | 36.464MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.342.smt2 | 0.586s | 36.88MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.67.smt2 | 0.586s | 30.852MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_e.2.smt2 | 0.590s | 40.44MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.40.smt2 | 0.590s | 51.504MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_commit.2.smt2 | 0.590s | 25.732MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.30.smt2 | 0.591s | 33.12MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_e.20.smt2 | 0.591s | 35.244MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.27.smt2 | 0.592s | 31.104MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl__PT.15.smt2 | 0.593s | 33.32MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.307.smt2 | 0.602s | 32.164MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.106.smt2 | 0.602s | 33.344MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.231.smt2 | 0.604s | 34.336MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.346.smt2 | 0.605s | 35.672MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.51.smt2 | 0.606s | 32.612MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.3.smt2 | 0.608s | 36.604MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__idt__dummy.3.smt2 | 0.611s | 42.372MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.398.smt2 | 0.611s | 33.024MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.261.smt2 | 0.614s | 34.712MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.368.smt2 | 0.614s | 35.82MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpuid.14.smt2 | 0.623s | 40.852MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.348.smt2 | 0.625s | 32.32MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.37.smt2 | 0.625s | 35.408MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.206.smt2 | 0.626s | 34.268MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.10.smt2 | 0.626s | 32.596MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.20.smt2 | 0.628s | 33.076MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.144.smt2 | 0.628s | 35.124MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.309.smt2 | 0.628s | 35.096MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.328.smt2 | 0.631s | 35.34MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.221.smt2 | 0.633s | 34.292MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__init__mshv_fmt.1.smt2 | 0.633s | 47.036MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.6.smt2 | 0.635s | 32.828MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__KVPairFormat_v.3.smt2 | 0.636s | 27.252MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.202.smt2 | 0.639s | 34.332MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__replica.13.smt2 | 0.641s | 30.992MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.14.smt2 | 0.646s | 31.584MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.10.smt2 | 0.648s | 27.908MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.6.smt2 | 0.648s | 27.976MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.10.smt2 | 0.651s | 37.752MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.25.smt2 | 0.653s | 30.12MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.9.smt2 | 0.653s | 31.42MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype_test.5.smt2 | 0.656s | 31.296MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__linkedlist.3.smt2 | 0.658s | 33.728MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.308.smt2 | 0.660s | 35.32MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.235.smt2 | 0.663s | 35.212MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/allocator__page_allocator_spec_impl.4.smt2 | 0.664s | 29.364MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__monitor_params.smt2 | 0.665s | 39.288MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.417.smt2 | 0.665s | 37.504MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.2.smt2 | 0.668s | 27.644MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.362.smt2 | 0.669s | 36.776MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.27.smt2 | 0.672s | 65.02MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.14.smt2 | 0.676s | 65.912MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.325.smt2 | 0.679s | 35.272MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.25.smt2 | 0.679s | 51.292MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__create_and_map_pages.1.smt2 | 0.681s | 37.544MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__ptram__ptram_p.10.smt2 | 0.681s | 35.512MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.2.smt2 | 0.685s | 32.536MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.321.smt2 | 0.690s | 35.148MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.414.smt2 | 0.693s | 36.772MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.7.smt2 | 0.693s | 42.012MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__replica.11.smt2 | 0.701s | 30.348MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.16.smt2 | 0.701s | 29.852MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-pagelib_page.page_init._01.smt2 | 0.702s | 30.356MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.28.smt2 | 0.708s | 56.928MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.138.smt2 | 0.710s | 33.976MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__secret.1.smt2 | 0.713s | 51.448MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/memory_manager__spec_impl.5.smt2 | 0.716s | 29.744MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.27.smt2 | 0.720s | 57.812MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.16.smt2 | 0.721s | 30.036MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__multilogimpl_v.9.smt2 | 0.725s | 33.444MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__snp_s.smt2 | 0.728s | 37.348MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.390.smt2 | 0.736s | 36.216MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/allocator__page_allocator_spec_impl.8.smt2 | 0.737s | 30.48MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_refinement.5.smt2 | 0.737s | 30.316MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.45.smt2 | 0.740s | 29.732MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.29.smt2 | 0.740s | 31.96MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__linkedlist.11.smt2 | 0.745s | 40.76MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper__wakeup.1.smt2 | 0.746s | 51.076MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.34.smt2 | 0.748s | 51.84MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.389.smt2 | 0.748s | 36.316MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.183.smt2 | 0.751s | 34.008MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.63.smt2 | 0.754s | 31.42MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.22.smt2 | 0.754s | 36.492MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.56.smt2 | 0.761s | 34.488MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.10.smt2 | 0.765s | 39.636MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.392.smt2 | 0.767s | 36.544MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.1.smt2 | 0.767s | 27.336MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.7.smt2 | 0.767s | 29.808MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.31.smt2 | 0.768s | 60.78MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.17.smt2 | 0.772s | 30.344MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__mem_util.2.smt2 | 0.775s | 37.924MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__slice_print.3.smt2 | 0.775s | 48.884MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.222.smt2 | 0.778s | 34.452MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.2.smt2 | 0.781s | 65.92MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.8.smt2 | 0.787s | 41.82MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.412.smt2 | 0.792s | 37.512MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__params.12.smt2 | 0.792s | 49.972MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.16.smt2 | 0.795s | 43.272MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__params.14.smt2 | 0.801s | 45.26MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.35.smt2 | 0.805s | 56.56MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__init__init_e.2.smt2 | 0.809s | 61.74MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.11.smt2 | 0.814s | 60.028MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.48.smt2 | 0.818s | 31.552MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.11.smt2 | 0.818s | 59.652MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.127.smt2 | 0.826s | 70.376MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_segment.6.smt2 | 0.830s | 35.776MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.36.smt2 | 0.831s | 51.344MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.33.smt2 | 0.834s | 29.552MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.10.smt2 | 0.842s | 65.912MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__range_interface.14.smt2 | 0.844s | 36.388MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.5.smt2 | 0.846s | 30.908MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.64.smt2 | 0.848s | 56.896MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page.16.smt2 | 0.852s | 36.488MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.7.smt2 | 0.860s | 59.056MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.117.smt2 | 0.861s | 57.432MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper__hypercall.2.smt2 | 0.862s | 51.38MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-queues.3.smt2 | 0.862s | 34.26MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__idt__dummy.5.smt2 | 0.867s | 43.352MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.44.smt2 | 0.871s | 52.056MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.121.smt2 | 0.872s | 52.048MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.18.smt2 | 0.872s | 65.908MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.20.smt2 | 0.872s | 60.092MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.16.smt2 | 0.877s | 40.484MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.126.smt2 | 0.877s | 70.648MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.94.smt2 | 0.877s | 35.044MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__raw_ptr_s.1.smt2 | 0.880s | 44.584MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.3.smt2 | 0.881s | 32.736MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.394.smt2 | 0.885s | 36.48MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.19.smt2 | 0.886s | 65.036MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.5.smt2 | 0.889s | 58.684MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.26.smt2 | 0.889s | 67.016MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.89.smt2 | 0.893s | 63.948MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.58.smt2 | 0.895s | 56.844MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.28.smt2 | 0.897s | 37.312MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.38.smt2 | 0.900s | 70.496MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.1.smt2 | 0.900s | 37.216MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.20.smt2 | 0.911s | 39.032MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.1.smt2 | 0.920s | 30.656MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.23.smt2 | 0.924s | 67.152MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__mem__mem_p.16.smt2 | 0.924s | 38.996MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.49.smt2 | 0.931s | 51.268MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.17.smt2 | 0.939s | 56.12MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.14.smt2 | 0.941s | 62.22MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.12.smt2 | 0.942s | 62.308MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.39.smt2 | 0.945s | 32.328MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.25.smt2 | 0.947s | 67.28MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.16.smt2 | 0.949s | 35.176MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.4.smt2 | 0.954s | 65.912MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__secret.9.smt2 | 0.954s | 64.78MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.7.smt2 | 0.975s | 34.908MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.28.smt2 | 0.976s | 60.852MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__secret.17.smt2 | 0.979s | 50.784MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.22.smt2 | 0.984s | 62.584MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.39.smt2 | 0.988s | 38.944MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.13.smt2 | 0.991s | 58.796MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.30.smt2 | 0.993s | 62.396MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.7.smt2 | 1.004s | 63.092MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.7.smt2 | 1.006s | 39.952MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.1.smt2 | 1.007s | 59.548MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.4.smt2 | 1.009s | 63.096MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.138.smt2 | 1.011s | 56.8MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__mem__mem_p.11.smt2 | 1.011s | 37.188MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.71.smt2 | 1.012s | 64.516MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.37.smt2 | 1.014s | 56.34MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.6.smt2 | 1.015s | 66.412MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.15.smt2 | 1.017s | 38.164MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.30.smt2 | 1.022s | 65.864MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__pcr.2.smt2 | 1.027s | 59.028MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.88.smt2 | 1.028s | 65.14MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.11.smt2 | 1.036s | 60.136MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.4.smt2 | 1.038s | 63.584MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.43.smt2 | 1.038s | 61.664MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.73.smt2 | 1.048s | 66.008MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.5.smt2 | 1.056s | 59.348MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__layout_v.30.smt2 | 1.058s | 31.6MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.26.smt2 | 1.064s | 65.936MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.6.smt2 | 1.086s | 63.904MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.8.smt2 | 1.092s | 63.872MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__create_and_share_pages.4.smt2 | 1.096s | 70.248MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.69.smt2 | 1.099s | 65.884MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.8.smt2 | 1.103s | 65.92MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__params.16.smt2 | 1.119s | 65.66MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.35.smt2 | 1.120s | 35.548MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__secret.6.smt2 | 1.125s | 65.42MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.67.smt2 | 1.131s | 69.86MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.20.smt2 | 1.134s | 67.056MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.91.smt2 | 1.139s | 65.444MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.16.smt2 | 1.142s | 65.912MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.28.smt2 | 1.142s | 60.88MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.31.smt2 | 1.143s | 64.936MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.13.smt2 | 1.147s | 38.752MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.50.smt2 | 1.161s | 65.636MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__create_and_map_pages.6.smt2 | 1.167s | 49.692MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.83.smt2 | 1.172s | 66.584MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.10.smt2 | 1.174s | 62.7MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.14.smt2 | 1.180s | 37.916MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.45.smt2 | 1.180s | 39.16MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__trackedcore__snpmulticore.1.smt2 | 1.188s | 68.412MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1__impl_%1__lemma_resolve_refines.smt2 | 1.189s | 36.448MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.37.smt2 | 1.198s | 60.356MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.26.smt2 | 1.202s | 39.452MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__init__mshv_alloc.3.smt2 | 1.203s | 64.532MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.21.smt2 | 1.207s | 65.628MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.98.smt2 | 1.215s | 64.792MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.11.smt2 | 1.215s | 43.308MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.93.smt2 | 1.219s | 58.672MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.44.smt2 | 1.220s | 64.416MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__secret.22.smt2 | 1.230s | 62.224MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__linkedlist.13.smt2 | 1.236s | 48.384MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__secret.24.smt2 | 1.238s | 63.744MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.45.smt2 | 1.239s | 39.36MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.104.smt2 | 1.241s | 64.748MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.25.smt2 | 1.249s | 65.744MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.103.smt2 | 1.255s | 65.404MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.107.smt2 | 1.259s | 66.44MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.36.smt2 | 1.285s | 38.672MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.102.smt2 | 1.286s | 65.692MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_e.19.smt2 | 1.295s | 67.804MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.48.smt2 | 1.299s | 65.76MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-init.13.smt2 | 1.300s | 40.172MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__schedule_idle_cpu.smt2 | 1.308s | 45.964MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl.10.smt2 | 1.319s | 29.46MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.10.smt2 | 1.322s | 68.032MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.63.smt2 | 1.324s | 71.028MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.94.smt2 | 1.331s | 65.708MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/pagetable__pagetable_spec_impl.5.smt2 | 1.338s | 37.36MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.42.smt2 | 1.343s | 64.696MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__ptr_e.9.smt2 | 1.348s | 40.592MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.70.smt2 | 1.349s | 65.628MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.17.smt2 | 1.350s | 33.564MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.110.smt2 | 1.357s | 66.288MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.26.smt2 | 1.361s | 66.292MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.112.smt2 | 1.367s | 67.28MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.85.smt2 | 1.379s | 66.9MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-free.6.smt2 | 1.389s | 64.208MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.25.smt2 | 1.391s | 64.504MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__raw_ptr_s.3.smt2 | 1.421s | 44.472MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.18.smt2 | 1.422s | 60.96MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.39.smt2 | 1.431s | 38.372MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.13.smt2 | 1.436s | 64.44MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.41.smt2 | 1.439s | 74.736MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.68.smt2 | 1.455s | 66.288MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.81.smt2 | 1.455s | 66.664MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.45.smt2 | 1.462s | 66.352MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.2.smt2 | 1.481s | 39.184MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.38.smt2 | 1.533s | 64.344MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.96.smt2 | 1.537s | 64.564MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.12.smt2 | 1.554s | 34.42MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.9.smt2 | 1.573s | 68.948MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.33.smt2 | 1.599s | 69.928MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.22.smt2 | 1.601s | 68.636MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__secret.18.smt2 | 1.607s | 67.084MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__range_interface.17.smt2 | 1.643s | 40.868MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.42.smt2 | 1.649s | 31.8MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.26.smt2 | 1.654s | 67.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.31.smt2 | 1.688s | 38.256MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.65.smt2 | 1.708s | 37.276MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.20.smt2 | 1.717s | 66.824MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1__impl_%1__lemma_interp_of_entry_contains_mapping_implies_interp_aux_contains_mapping.smt2 | 1.730s | 41.06MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__syscall_receive_empty.2.smt2 | 1.745s | 67.212MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.40.smt2 | 1.753s | 31.636MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.44.smt2 | 1.780s | 63.98MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-alloc_generic.5.smt2 | 1.780s | 46.1MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.66.smt2 | 1.788s | 81.708MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.32.smt2 | 1.789s | 64.352MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.50.smt2 | 1.815s | 66.188MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__align_s.5.smt2 | 1.849s | 32.972MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.32.smt2 | 1.862s | 75.22MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-free.3.smt2 | 1.867s | 64.996MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__mem__mem_p.13.smt2 | 1.878s | 43.044MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.17.smt2 | 1.886s | 68.208MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.10.smt2 | 1.888s | 73.436MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.25.smt2 | 1.915s | 43.52MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.79.smt2 | 2.006s | 39.108MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-root.smt2 | 2.087s | 70.492MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.16.smt2 | 2.088s | 38.048MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/lock__spincell_e.5.smt2 | 2.116s | 72.924MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__start_v.2.smt2 | 2.120s | 36.616MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.27.smt2 | 2.121s | 67.372MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.13.smt2 | 2.206s | 85.66MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper__wakeup.5.smt2 | 2.222s | 149.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.19.smt2 | 2.244s | 32.176MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layoutlib_layout.align_up._02.smt2 | 2.255s | 26.692MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.49.smt2 | 2.263s | 64.136MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.15.smt2 | 2.325s | 38.48MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.4.smt2 | 2.585s | 82.728MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_segment.1.smt2 | 2.612s | 33.304MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.18.smt2 | 2.626s | 36.388MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.34.smt2 | 2.696s | 37.504MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.60.smt2 | 2.702s | 39.728MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__def_s.smt2 | 2.709s | 94.076MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.12.smt2 | 2.780s | 76.428MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.134.smt2 | 2.808s | 77.784MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__create_and_share_pages.3.smt2 | 2.891s | 69.38MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__x64__x64_p.2.smt2 | 2.950s | 47.356MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/vbox__vbox.6.smt2 | 3.267s | 141.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.5.smt2 | 3.392s | 78.084MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__mem__mem_p.4.smt2 | 3.448s | 48.908MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.9.smt2 | 3.484s | 41.028MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.11.smt2 | 3.546s | 31.784MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.7.smt2 | 3.560s | 81.292MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.17.smt2 | 3.624s | 74.968MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout__block_ptr_aligned_to_word.smt2 | 3.886s | 26.284MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__syscall_send_endpoint.smt2 | 4.107s | 121.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/vbox__vbox.2.smt2 | 4.193s | 129.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.4.smt2 | 4.219s | 44.36MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__locked.1.smt2 | 4.349s | 100.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/lock__spin_perm_s.3.smt2 | 4.452s | 87.476MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_e.18.smt2 | 4.463s | 74.652MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.7.smt2 | 4.471s | 78.908MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.47.smt2 | 4.622s | 48.044MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/allocator__page_allocator_spec_impl.20.smt2 | 4.801s | 46.252MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__init__init_s.smt2 | 4.837s | 145.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__rmp__rmp_e.7.smt2 | 4.910s | 77.08MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/allocator__page_allocator_spec_impl.10.smt2 | 5.363s | 48.792MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.37.smt2 | 5.501s | 136.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl__internal.2.smt2 | 5.844s | 130.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__rmp__rmp_e.5.smt2 | 6.205s | 96.044MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.15.smt2 | 6.311s | 167.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.38.smt2 | 6.432s | 264.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.15.smt2 | 6.892s | 48.476MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__linkedlist.6.smt2 | 7.061s | 95.18MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.23.smt2 | 7.415s | 145.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.9.smt2 | 7.783s | 76.724MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.9.smt2 | 7.885s | 80.132MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.140.smt2 | 7.995s | 182.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__linkedlist.10.smt2 | 8.526s | 72.808MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__syscall_send_pages.smt2 | 8.666s | 122.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/allocator__page_allocator_spec_impl.15.smt2 | 9.322s | 70.396MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.50.smt2 | 9.323s | 50.908MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/vbox__vbox.7.smt2 | 9.421s | 129.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/vbox__vbox.3.smt2 | 9.581s | 191.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.1.smt2 | 9.601s | 187.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/allocator__page_allocator_spec_impl.23.smt2 | 9.986s | 72.832MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout__align_downlib_layout.align_down._03.smt2 | 10.015s | 23.888MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.22.smt2 | 10.691s | 267.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.13.smt2 | 10.971s | 93.992MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.8.smt2 | 10.986s | 62.084MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.37.smt2 | 11.486s | 58.632MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__rmp__rmp_e.3.smt2 | 12.123s | 135.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper__wakeup.7.smt2 | 13.297s | 263.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.9.smt2 | 13.450s | 66.552MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.12.smt2 | 13.664s | 137.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.19.smt2 | 14.468s | 198.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__pcr.5.smt2 | 15.002s | 286.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.15.smt2 | 16.553s | 93.608MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.11.smt2 | 16.709s | 50.852MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__syscall_new_proc.smt2 | 17.292s | 121.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__os_refinement.10.smt2 | 18.960s | 94.48MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.4.smt2 | 20.001s | 143.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-segment__segment_slice_split.smt2 | 20.027s | 94.884MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.24.smt2 | 20.030s | 159.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.15.smt2 | 20.032s | 201.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.13.smt2 | 20.032s | 150.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl__PT.28.smt2 | 20.032s | 83.708MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__multilogimpl_v.5.smt2 | 20.033s | 84.42MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20230314-Jaroslav-Bendik-Certora/52759_b3ecd2335fd16ec2eee2_9_UFDTNIA.smt2 | 20.038s | 42.272MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-segment__segment_span_free_coalesce_before.smt2 | 20.040s | 121.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1__impl_%1__lemma_no_mapping_in_interp_of_entry_implies_no_mapping_in_interp.smt2 | 20.043s | 66.252MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_refinement.4.smt2 | 20.045s | 76.252MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.14.smt2 | 20.048s | 180.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-segment__segment_page_clear.smt2 | 20.053s | 120.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.16.smt2 | 20.062s | 180.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/pagetable__pagetable_spec_impl.1.smt2 | 20.066s | 332.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__append_v.2.smt2 | 20.066s | 93.852MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_refinement.3.smt2 | 20.070s | 96.332MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.6.smt2 | 20.075s | 137.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.2.smt2 | 20.076s | 529.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_ulib_definitions_u.impl_%3.lemma_entry_sizes_aligned._02.smt2 | 20.079s | 28.12MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__secret.13.smt2 | 20.082s | 273.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl__PT.18.smt2 | 20.086s | 99.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-queues__page_queue_push.smt2 | 20.098s | 119.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-queues__page_queue_push_back.smt2 | 20.101s | 124.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__idt__def.4.smt2 | 20.114s | 309.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.31.smt2 | 20.117s | 750.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__setup_v.6.smt2 | 20.150s | 810.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.12.smt2 | 20.163s | 280.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.10.smt2 | 20.165s | 175.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/2019-Gleiss/non-interference/10-ni-rsa-exponentiation.spec.smt2 | 20.271s | 2166.0MiB| timeout | 0 | | |