# . * SAT 0 * UNSAT 980 * TIMEOUT 28 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: UFDTNIA.tar.zst
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: bc6c38e7d3424b88a505cacba4b268d0774d4547
Z3 branch: master
Z3 options: "-T:20"
Z3 inputs: https://zenodo.org/records/16740866/files/UFDTNIA.tar.zst?download=1
Z3 commit message: [code-simplifier] Simplify `api_ast.cpp` by removing unreachable branch and stray comment (#9570)

This change simplifies recently touched API code in
`src/api/api_ast.cpp` without altering semantics. It removes an
unreachable error path in `Z3_get_index_value` and deletes an empty
comment in `Z3_mk_rec_func_decl`.

- **`Z3_get_index_value`: remove dead branch**
- After validating `a` is non-null and of kind `AST_VAR`, the conversion
to `var*` is already guaranteed by existing AST casting invariants.
- The redundant null-check/error-return branch was removed, leaving a
direct index return.

- **`Z3_mk_rec_func_decl`: remove noise**
  - Deleted a stray empty `//` line.

```cpp
// before
var* va = to_var(_a);
if (va) {
    return va->get_idx();
}
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return 0;

// after
var* va = to_var(_a);
return va->get_idx();
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-constants.3.smt2 | 0.037s | 19.624MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__bits_p.4.smt2 | 0.041s | 19.856MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.29.smt2 | 0.043s | 19.888MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__align_sverismo_tspec.math.align_s.proof_align_down._01.smt2 | 0.044s | 21.244MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.27.smt2 | 0.044s | 20.188MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__pow_p.1.smt2 | 0.047s | 20.54MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.19.smt2 | 0.051s | 19.796MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.22.smt2 | 0.051s | 20.28MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extra.1.smt2 | 0.052s | 19.692MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout__two_mul_with_bit1.smt2 | 0.053s | 20.992MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-spec_t__hardware.6.smt2 | 0.053s | 20.044MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extra.3.smt2 | 0.055s | 21.516MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.17.smt2 | 0.056s | 20.24MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.16.smt2 | 0.057s | 19.852MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__math_v.smt2 | 0.057s | 20.828MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__math_v.smt2 | 0.057s | 20.828MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_alloc.6.smt2 | 0.058s | 20.48MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.36.smt2 | 0.061s | 20.34MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout__align_downlib_layout.align_down._02.smt2 | 0.063s | 20.948MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-spec_t__hardware.17.smt2 | 0.064s | 20.116MiB| 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.065s | 20.984MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_small_mod._01.smt2 | 0.067s | 20.912MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-spec_t__hardware.2.smt2 | 0.068s | 20.024MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.23.smt2 | 0.070s | 21.176MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.2.smt2 | 0.070s | 20.788MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-spec_t__hardware.1.smt2 | 0.070s | 20.116MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.27.smt2 | 0.070s | 20.356MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_t.25.smt2 | 0.071s | 19.944MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.2.smt2 | 0.072s | 21.072MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__math_vlib_marshalling.math_v.distribute_left._01.smt2 | 0.073s | 21.384MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.24.smt2 | 0.073s | 20.396MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__layout_v.30.smt2 | 0.075s | 22.588MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.lemma_aligned_iff_eq_mul_div._02.smt2 | 0.075s | 21.432MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_t.18.smt2 | 0.075s | 19.936MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.32.smt2 | 0.075s | 20.208MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_div_equal._01.smt2 | 0.076s | 21.588MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/util__page_ptr_util_u.13.smt2 | 0.078s | 20.004MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.3.smt2 | 0.078s | 21.36MiB| 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.078s | 21.052MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l0.6.smt2 | 0.078s | 20.144MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.42.smt2 | 0.078s | 22.816MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.28.smt2 | 0.079s | 22.892MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__stream__basic.1.smt2 | 0.080s | 21.136MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.mul_commute._01.smt2 | 0.080s | 21.276MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-spec_t__hardware.4.smt2 | 0.080s | 20.144MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-constants.6.smt2 | 0.080s | 20.712MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.18.smt2 | 0.080s | 20.32MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.31.smt2 | 0.081s | 21.372MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.18.smt2 | 0.081s | 21.236MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl.1.smt2 | 0.081s | 22.228MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__bits_p.7.smt2 | 0.082s | 24.14MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.21.smt2 | 0.082s | 20.304MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.22.smt2 | 0.083s | 20.176MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__rmp__rmp_t.2.smt2 | 0.083s | 22.34MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.25.smt2 | 0.083s | 21.304MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.22.smt2 | 0.083s | 21.212MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_t.13.smt2 | 0.083s | 21.584MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_t.24.smt2 | 0.085s | 21.764MiB| 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.085s | 21.648MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-spec_t__hardware.7.smt2 | 0.085s | 20.124MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__KVPairFormat_v.7.smt2 | 0.086s | 22.016MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_t.20.smt2 | 0.086s | 20.268MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.9.smt2 | 0.087s | 22.156MiB| 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.087s | 21.124MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.mod_mult_zero_implies_mod_zero._01.smt2 | 0.087s | 21.544MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l0.24.smt2 | 0.087s | 22.312MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.17.smt2 | 0.088s | 22.9MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.5.smt2 | 0.088s | 21.328MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.38.smt2 | 0.088s | 20.296MiB| 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.088s | 20.676MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.23.smt2 | 0.089s | 20.008MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.20.smt2 | 0.089s | 19.924MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.4.smt2 | 0.089s | 21.004MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/lock__spincell_e.6.smt2 | 0.089s | 21.608MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__bits_p.9.smt2 | 0.089s | 29.868MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.lemma_aligned_iff_eq_mul_div._01.smt2 | 0.089s | 21.32MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__setlib.12.smt2 | 0.090s | 22.14MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.24.smt2 | 0.091s | 21.172MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.10.smt2 | 0.091s | 21.572MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_is_associative._01.smt2 | 0.091s | 21.164MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.mult_leq_mono2._01.smt2 | 0.091s | 19.904MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.1.smt2 | 0.092s | 21.128MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.16.smt2 | 0.092s | 21.156MiB| 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.093s | 21.404MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_ulib_definitions_u.impl_%2.index_for_vaddr._01.smt2 | 0.094s | 21.928MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.20.smt2 | 0.094s | 22.536MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.27.smt2 | 0.095s | 21.176MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/vcell__vcell.smt2 | 0.095s | 20.868MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.9.smt2 | 0.095s | 21.252MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.2.smt2 | 0.095s | 21.42MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.mod_less_eq._01.smt2 | 0.095s | 21.46MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__math_vlib_marshalling.math_v.distribute_left._01.smt2 | 0.095s | 21.356MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.33.smt2 | 0.096s | 21.656MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__pgtable__memmap_p.5.smt2 | 0.096s | 22.024MiB| 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.096s | 21.54MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__integer.2.smt2 | 0.098s | 25.232MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.10.smt2 | 0.098s | 22.064MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_t.15.smt2 | 0.098s | 21.66MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-constants.8.smt2 | 0.099s | 20.64MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_t.11.smt2 | 0.099s | 21.776MiB| 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.099s | 21.488MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__ResizableUniformSizedSeq_v.4.smt2 | 0.099s | 23.332MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__bit_p.smt2 | 0.100s | 23.216MiB| 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.100s | 20.684MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizeslib_bin_sizes.lemma_div_is_ordered._01.smt2 | 0.100s | 22.168MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l0.19.smt2 | 0.101s | 23.648MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.40.smt2 | 0.101s | 22.132MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.43.smt2 | 0.102s | 21.772MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__addr_s__page.1.smt2 | 0.102s | 22.148MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.27.smt2 | 0.102s | 22.528MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-init.1.smt2 | 0.102s | 21.792MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__UniformSizedSeq_v.1.smt2 | 0.102s | 22.668MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_u.1.smt2 | 0.103s | 19.944MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.15.smt2 | 0.103s | 22.86MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.10.smt2 | 0.103s | 21.928MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.13.smt2 | 0.104s | 21.196MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l0.5.smt2 | 0.105s | 21.548MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.mult_less_mono_both2._01.smt2 | 0.105s | 21.764MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.15.smt2 | 0.105s | 21.956MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.aligned_transitive._02.smt2 | 0.106s | 21.692MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page.15.smt2 | 0.107s | 21.668MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-alloc_generic.2.smt2 | 0.107s | 21.44MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.12.smt2 | 0.107s | 24.54MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extra.7.smt2 | 0.108s | 21.188MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.32.smt2 | 0.108s | 21.328MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__rmp__rmp_t.8.smt2 | 0.109s | 22.456MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.2.smt2 | 0.109s | 21.248MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__UniformSizedSeq_v.5.smt2 | 0.109s | 22.76MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_alloc.8.smt2 | 0.109s | 20.508MiB| 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.109s | 21.128MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__rmp__rmp_t.7.smt2 | 0.110s | 22.268MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.2.smt2 | 0.110s | 22.784MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.39.smt2 | 0.111s | 20.088MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__rmp__rmp_t.5.smt2 | 0.111s | 22.252MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.5.smt2 | 0.111s | 21.1MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.7.smt2 | 0.111s | 22.736MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l0.15.smt2 | 0.111s | 21.956MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__UniformSizedSeq_v.2.smt2 | 0.112s | 22.576MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizeslib_bin_sizes.mod8._01.smt2 | 0.113s | 21.648MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.20.smt2 | 0.113s | 21.088MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.13.smt2 | 0.113s | 22.168MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.26.smt2 | 0.116s | 21.364MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_is_distributive._01.smt2 | 0.116s | 21.436MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/util__page_ptr_util_u.14.smt2 | 0.117s | 22.404MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.1.smt2 | 0.117s | 22.756MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-spec_t__hardware.19.smt2 | 0.117s | 22.584MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.28.smt2 | 0.118s | 23.448MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.37.smt2 | 0.119s | 19.936MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/util__page_ptr_util_u.8.smt2 | 0.119s | 22.168MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__rmp__rmp_t.6.smt2 | 0.119s | 22.42MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__idt__def.3.smt2 | 0.120s | 22.24MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__addr_s__def_s.3.smt2 | 0.120s | 20.36MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__KVPairFormat_v.1.smt2 | 0.120s | 22.496MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl.14.smt2 | 0.120s | 21.7MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l0.14.smt2 | 0.121s | 19.956MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-config.23.smt2 | 0.121s | 23.12MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout__two_mul_with_bit1lib_layout.two_mul_with_bit1._01.smt2 | 0.122s | 21.252MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_t.22.smt2 | 0.122s | 21.968MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.4.smt2 | 0.123s | 23.876MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__size_s.4.smt2 | 0.124s | 26.268MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpuid.5.smt2 | 0.124s | 22.828MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/trusted_hacl__stub.7.smt2 | 0.125s | 21.936MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.10.smt2 | 0.125s | 21.18MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extra.8.smt2 | 0.125s | 21.276MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpuid.13.smt2 | 0.126s | 22.656MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-pmem__pmcopy_t.3.smt2 | 0.126s | 22.384MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl__PT.1.smt2 | 0.126s | 20.364MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__UniformSizedSeq_v.5.smt2 | 0.127s | 22.668MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__UniformSizedSeq_v.2.smt2 | 0.128s | 22.408MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.6.smt2 | 0.128s | 24.496MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_left_inequality._01.smt2 | 0.128s | 21.66MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__bits_p.8.smt2 | 0.129s | 27.58MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_ulib_definitions_u.impl_%2.next_entry_base._01.smt2 | 0.129s | 23.04MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.7.smt2 | 0.130s | 23.012MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/va_range.2.smt2 | 0.131s | 22.348MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/lemma__lemma_u.1.smt2 | 0.131s | 21.628MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.23.smt2 | 0.131s | 24.536MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl__PT.5.smt2 | 0.132s | 20.376MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_u.11.smt2 | 0.132s | 22.708MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.12.smt2 | 0.133s | 22.084MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.6.smt2 | 0.134s | 22.148MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.34.smt2 | 0.134s | 23.692MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layoutlib_layout.bitand_with_mask_gives_rounding._09.smt2 | 0.135s | 24.54MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-init.10.smt2 | 0.136s | 21.772MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-extralib_extra.mult_leq_mono_both._01.smt2 | 0.137s | 21.648MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__pgtable__memmap_p.3.smt2 | 0.138s | 24.204MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.24.smt2 | 0.138s | 22.752MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_ulib_definitions_u.impl_%2.entry_base._01.smt2 | 0.138s | 23.452MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__layout_v.27.smt2 | 0.138s | 22.488MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/define.44.smt2 | 0.139s | 21.848MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.11.smt2 | 0.140s | 23.056MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layoutlib_layout.calculate_page_block_at._02.smt2 | 0.140s | 23.908MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_ulib_definitions_u.overflow_bounds._02.smt2 | 0.140s | 22.676MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.1.smt2 | 0.142s | 23.028MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__pgtable__entry_p.3.smt2 | 0.143s | 25.224MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-main_t.7.smt2 | 0.143s | 22.896MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.22.smt2 | 0.144s | 23.96MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer.4.smt2 | 0.147s | 23.172MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.14.smt2 | 0.148s | 23.028MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__stream__basic.2.smt2 | 0.148s | 21.392MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpuid.11.smt2 | 0.148s | 22.668MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.7.smt2 | 0.148s | 21.928MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.5.smt2 | 0.149s | 22.928MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_ulib_definitions_u.impl_%2.next_entry_base._02.smt2 | 0.149s | 21.9MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.33.smt2 | 0.149s | 22.916MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layoutlib_layout.calculate_slice_page_ptr_from_block._01.smt2 | 0.149s | 23.712MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.27.smt2 | 0.150s | 24.54MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.22.smt2 | 0.150s | 24.584MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.2.smt2 | 0.151s | 22.208MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_alloc.3.smt2 | 0.152s | 23.076MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__layout_v.26.smt2 | 0.152s | 22.236MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__params.8.smt2 | 0.153s | 23.724MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.6.smt2 | 0.154s | 23.004MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.15.smt2 | 0.155s | 23.684MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_utillib_os_mem_util.preserves_mem_chunk_good_except._01.smt2 | 0.157s | 28.2MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/lemma__lemma_u.2.smt2 | 0.158s | 24.396MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/registers__msr_t.3.smt2 | 0.158s | 26.652MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.3.smt2 | 0.158s | 22.132MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.3.smt2 | 0.158s | 21.644MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.3.smt2 | 0.158s | 21.94MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__setlib.11.smt2 | 0.159s | 22.424MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.26.smt2 | 0.159s | 28.976MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.26.smt2 | 0.159s | 23.94MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.13.smt2 | 0.159s | 24.888MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.10.smt2 | 0.160s | 22.156MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl.5.smt2 | 0.160s | 23.152MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_listlib_linked_list.impl_%2.prepend_contiguous_blocks._08.smt2 | 0.160s | 26.232MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.5.smt2 | 0.163s | 24.336MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.1.smt2 | 0.164s | 24.32MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__layout_v.31.smt2 | 0.164s | 24.592MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.13.smt2 | 0.165s | 24.156MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l0.23.smt2 | 0.166s | 24.344MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__params.5.smt2 | 0.168s | 24.192MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-spec_t__hardware.21.smt2 | 0.168s | 22.58MiB| 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.169s | 24.064MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.4.smt2 | 0.169s | 26.752MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-main_t.4.smt2 | 0.169s | 25.668MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.12.smt2 | 0.169s | 24.348MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.17.smt2 | 0.170s | 26.228MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-root.smt2 | 0.172s | 23.94MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_ulib_definitions_u.impl_%3.lemma_entry_sizes_increase._01.smt2 | 0.173s | 23.004MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.45.smt2 | 0.173s | 25.836MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.14.smt2 | 0.173s | 23.68MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.16.smt2 | 0.174s | 25.56MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/registers__msr_t.11.smt2 | 0.175s | 26.856MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/ironkv-smt-verus_extra__seq_lib_v.15.smt2 | 0.176s | 22.528MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__ResizableUniformSizedSeq_v.9.smt2 | 0.176s | 25.388MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__def_s.2.smt2 | 0.177s | 26.492MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer.5.smt2 | 0.179s | 22.984MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.6.smt2 | 0.180s | 24.168MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__ResizableUniformSizedSeq_v.9.smt2 | 0.182s | 25.392MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.31.smt2 | 0.184s | 23.932MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.11.smt2 | 0.186s | 25.408MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/registers__msr_t.7.smt2 | 0.190s | 26.776MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__cast.2.smt2 | 0.191s | 25.2MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.32.smt2 | 0.191s | 30.52MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_listlib_linked_list.impl_%2.prepend_contiguous_blocks._09.smt2 | 0.191s | 26.24MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.30.smt2 | 0.192s | 25.64MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.1.smt2 | 0.193s | 24.776MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.26.smt2 | 0.193s | 26.704MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_listlib_linked_list.impl_%2.prepend_contiguous_blocks._05.smt2 | 0.194s | 26.444MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.61.smt2 | 0.195s | 27.904MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__ptram__ptram_s.smt2 | 0.195s | 25.588MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.17.smt2 | 0.195s | 23.2MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.51.smt2 | 0.195s | 24.76MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.60.smt2 | 0.196s | 29.836MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__ResizableUniformSizedSeq_v.3.smt2 | 0.196s | 24.284MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__replica.19.smt2 | 0.196s | 26.692MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__log.7.smt2 | 0.197s | 26.48MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__addr_interface.11.smt2 | 0.198s | 29.464MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.39.smt2 | 0.198s | 26.36MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.15.smt2 | 0.199s | 22.924MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__log.16.smt2 | 0.199s | 26.48MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.38.smt2 | 0.200s | 23.144MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.4.smt2 | 0.201s | 24.86MiB| 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.202s | 26.448MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.43.smt2 | 0.203s | 28.58MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.5.smt2 | 0.203s | 24.804MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.19.smt2 | 0.204s | 24.848MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.32.smt2 | 0.204s | 25.824MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec_e__size_e.smt2 | 0.206s | 27.248MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__pgtable__entry_p.7.smt2 | 0.207s | 23.84MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__ptram__ptram_u.smt2 | 0.207s | 25.764MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.35.smt2 | 0.208s | 25.532MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.17.smt2 | 0.209s | 28.312MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_listlib_linked_list.impl_%2.prepend_contiguous_blocks._03.smt2 | 0.209s | 26.212MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.42.smt2 | 0.212s | 25.008MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__addr_interface.13.smt2 | 0.213s | 29.42MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__log.20.smt2 | 0.213s | 27.328MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout__align_down.smt2 | 0.217s | 22.06MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.48.smt2 | 0.218s | 30.492MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-alloc_fast.4.smt2 | 0.219s | 26.632MiB| 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.219s | 27.7MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.3.smt2 | 0.220s | 25.976MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.8.smt2 | 0.221s | 26.64MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/memory_manager__spec_impl.9.smt2 | 0.222s | 25.808MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__range_interface.7.smt2 | 0.222s | 28.664MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpuid.2.smt2 | 0.222s | 22.656MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl__PT.8.smt2 | 0.222s | 24.98MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__UniformSizedSeq_v.4.smt2 | 0.222s | 23.06MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/memory_manager__spec_impl.8.smt2 | 0.223s | 25.928MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__replica.1.smt2 | 0.223s | 26.212MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/registers__msr_t.2.smt2 | 0.224s | 26.612MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec.4.smt2 | 0.224s | 26.872MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.12.smt2 | 0.224s | 26.388MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.41.smt2 | 0.224s | 23.472MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.13.smt2 | 0.225s | 27.16MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.5.smt2 | 0.225s | 25.776MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.98.smt2 | 0.227s | 29.808MiB| 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.228s | 26.312MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.22.smt2 | 0.228s | 26.548MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.30.smt2 | 0.228s | 24.86MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.66.smt2 | 0.229s | 29.256MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.23.smt2 | 0.229s | 27.208MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.10.smt2 | 0.230s | 21.636MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-pagelib_page.page_init._02.smt2 | 0.234s | 29.06MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.9.smt2 | 0.235s | 26.544MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__ResizableUniformSizedSeq_v.7.smt2 | 0.235s | 25.68MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.2.smt2 | 0.236s | 33.708MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__multilogimpl_v.1.smt2 | 0.236s | 24.844MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__layout_v.32.smt2 | 0.239s | 25.536MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec_e__math__bits_e.1.smt2 | 0.240s | 33.028MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__addr_interface.10.smt2 | 0.240s | 29.348MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.20.smt2 | 0.242s | 27.028MiB| 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.242s | 28.4MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/primitives_e__vec.2.smt2 | 0.243s | 27.42MiB| 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.243s | 27.76MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.51.smt2 | 0.243s | 28.952MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__cast.4.smt2 | 0.244s | 27.772MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.6.smt2 | 0.244s | 27.08MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.24.smt2 | 0.244s | 27.184MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype_test.1.smt2 | 0.245s | 29.456MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/primitives_e__vec.1.smt2 | 0.247s | 27.164MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.19.smt2 | 0.247s | 25.32MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__addr_s__def_s.8.smt2 | 0.248s | 26.296MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.130.smt2 | 0.249s | 30.34MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.24.smt2 | 0.249s | 28.1MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.28.smt2 | 0.250s | 25.844MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__log.8.smt2 | 0.250s | 27.908MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.20.smt2 | 0.251s | 29.68MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.33.smt2 | 0.251s | 27.596MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__log.1.smt2 | 0.251s | 27.196MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype_test.8.smt2 | 0.252s | 29.448MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.109.smt2 | 0.254s | 33.144MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.2.smt2 | 0.256s | 26.6MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.42.smt2 | 0.256s | 27.148MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-init.11.smt2 | 0.257s | 29.468MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/memory_manager__spec_impl.2.smt2 | 0.258s | 25.32MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.72.smt2 | 0.258s | 30.616MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.3.smt2 | 0.258s | 25.424MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-root.5.smt2 | 0.259s | 26.004MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.45.smt2 | 0.260s | 29.016MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-segment__segments_page_find_and_allocate.3.smt2 | 0.260s | 33.5MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__cast.6.smt2 | 0.261s | 28.1MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__cast.5.smt2 | 0.261s | 26.912MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/primitives_e__seq.2.smt2 | 0.262s | 25.612MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.42.smt2 | 0.262s | 31.688MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbufferlib_spec.cyclicbuffer.log_entry_alive_value_wrap_around._01.smt2 | 0.262s | 23.624MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_listlib_linked_list.impl_%2.prepend_contiguous_blocks._06.smt2 | 0.262s | 26.464MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.11.smt2 | 0.262s | 28.964MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.108.smt2 | 0.263s | 30.9MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.15.smt2 | 0.263s | 28.936MiB| 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.263s | 28.476MiB| 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.263s | 25.812MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.5.smt2 | 0.263s | 29.796MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.11.smt2 | 0.263s | 30.496MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.27.smt2 | 0.268s | 30.42MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.26.smt2 | 0.269s | 29.732MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.97.smt2 | 0.270s | 30.864MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.35.smt2 | 0.270s | 27.296MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__snp_u.2.smt2 | 0.271s | 27.64MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.19.smt2 | 0.271s | 28.908MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__replica.12.smt2 | 0.271s | 28.228MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.3.smt2 | 0.272s | 29.216MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.3.smt2 | 0.273s | 26.636MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.115.smt2 | 0.274s | 31.816MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.11.smt2 | 0.274s | 28.936MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.40.smt2 | 0.275s | 27.512MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-init.12.smt2 | 0.275s | 29.564MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.9.smt2 | 0.276s | 30.928MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__replica.4.smt2 | 0.277s | 28.408MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.40.smt2 | 0.278s | 33.184MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__integer.8.smt2 | 0.279s | 23.912MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.12.smt2 | 0.281s | 26.936MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.17.smt2 | 0.281s | 25.392MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec.3.smt2 | 0.282s | 28.392MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.32.smt2 | 0.282s | 26.56MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.51.smt2 | 0.284s | 32.7MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec.1.smt2 | 0.284s | 26.748MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.18.smt2 | 0.285s | 31.38MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__cast.7.smt2 | 0.286s | 28.104MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.39.smt2 | 0.288s | 34.144MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_s.41.smt2 | 0.289s | 28.684MiB| 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.289s | 28.644MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.42.smt2 | 0.289s | 27.804MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__log.14.smt2 | 0.292s | 27.744MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.6.smt2 | 0.293s | 32.34MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.50.smt2 | 0.294s | 30.552MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.27.smt2 | 0.294s | 34.464MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/pagetable__pagetable_spec_impl.10.smt2 | 0.296s | 33.888MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_refinement.1.smt2 | 0.296s | 27.732MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__replica.6.smt2 | 0.297s | 27.664MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.41.smt2 | 0.298s | 28.992MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page.8.smt2 | 0.298s | 32.936MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.7.smt2 | 0.300s | 32.268MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.413.smt2 | 0.303s | 33.144MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__log.3.smt2 | 0.303s | 27.028MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.165.smt2 | 0.304s | 30.692MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.51.smt2 | 0.304s | 30.348MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.307.smt2 | 0.305s | 32.004MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__snp_u.15.smt2 | 0.305s | 32.716MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.7.smt2 | 0.306s | 23.464MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.35.smt2 | 0.306s | 25.88MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.53.smt2 | 0.308s | 30.06MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.21.smt2 | 0.309s | 34.776MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.297.smt2 | 0.311s | 31.996MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.7.smt2 | 0.312s | 28.604MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__ResizableUniformSizedSeq_v.10.smt2 | 0.312s | 24.776MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.15.smt2 | 0.312s | 29.692MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.403.smt2 | 0.313s | 32.88MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-segment__segment_alloclib_segment.segment_alloc._02.smt2 | 0.313s | 28.42MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.21.smt2 | 0.315s | 29.036MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.6.smt2 | 0.315s | 30.136MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.38.smt2 | 0.316s | 28.704MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__idt__dummy.2.smt2 | 0.316s | 33.972MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.102.smt2 | 0.317s | 29.824MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.16.smt2 | 0.317s | 25.652MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.31.smt2 | 0.317s | 32.12MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.49.smt2 | 0.321s | 28.968MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.28.smt2 | 0.322s | 27.856MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.24.smt2 | 0.323s | 32.72MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.14.smt2 | 0.325s | 36.276MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.36.smt2 | 0.326s | 27.424MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.35.smt2 | 0.326s | 25.964MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/pagetable__pagetable_spec_impl.11.smt2 | 0.328s | 34.88MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.57.smt2 | 0.328s | 30.216MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.151.smt2 | 0.328s | 34.272MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__addr_interface.3.smt2 | 0.328s | 29.032MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.13.smt2 | 0.330s | 35.464MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__snp_u.13.smt2 | 0.330s | 30.56MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.193.smt2 | 0.330s | 35.352MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__range_interface.10.smt2 | 0.330s | 31.484MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.106.smt2 | 0.331s | 33.276MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.52.smt2 | 0.331s | 30.7MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__snp_u.8.smt2 | 0.333s | 28.256MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.20.smt2 | 0.336s | 33.1MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.44.smt2 | 0.338s | 33.048MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl__PT.10.smt2 | 0.338s | 29.324MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.10.smt2 | 0.338s | 26.62MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_e.13.smt2 | 0.339s | 34.852MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.1.smt2 | 0.340s | 32.944MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.196.smt2 | 0.340s | 34.284MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__range_interface.5.smt2 | 0.343s | 27.936MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.34.smt2 | 0.343s | 29.068MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.19.smt2 | 0.343s | 30.08MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.220.smt2 | 0.345s | 34.708MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.12.smt2 | 0.347s | 29.808MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.71.smt2 | 0.347s | 28.452MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.155.smt2 | 0.348s | 30.736MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.8.smt2 | 0.348s | 30.364MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.213.smt2 | 0.349s | 35.88MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.95.smt2 | 0.349s | 30.64MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.216.smt2 | 0.350s | 32.884MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.49.smt2 | 0.350s | 32.728MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.172.smt2 | 0.350s | 33.88MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.40.smt2 | 0.352s | 30.62MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.198.smt2 | 0.353s | 35.26MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.19.smt2 | 0.354s | 33.148MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/lock__spincell_e.1.smt2 | 0.354s | 38.08MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.261.smt2 | 0.355s | 34.632MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.199.smt2 | 0.357s | 30.896MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__addr_s__page.6.smt2 | 0.357s | 23.792MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.44.smt2 | 0.361s | 31.936MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec_e__math__bits_e.8.smt2 | 0.363s | 31.592MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.350.smt2 | 0.364s | 34.132MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.32.smt2 | 0.364s | 25.976MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.11.smt2 | 0.365s | 30.58MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-segment.5.smt2 | 0.367s | 30.808MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.54.smt2 | 0.367s | 30.088MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/anvil/splinterdb-smt-marshalling__UniformSizedSeq_v.6.smt2 | 0.367s | 24.896MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/pagetable__pagetable_spec_impl.6.smt2 | 0.369s | 35.284MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.122.smt2 | 0.369s | 33.42MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.56.smt2 | 0.369s | 30.564MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__addr_interface.16.smt2 | 0.375s | 29.424MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.140.smt2 | 0.377s | 30.384MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.33.smt2 | 0.378s | 26.312MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.281.smt2 | 0.381s | 36.344MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__range_interface.13.smt2 | 0.383s | 32.284MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.34.smt2 | 0.383s | 29.824MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.32.smt2 | 0.385s | 29.728MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__os_refinement.1.smt2 | 0.385s | 30.504MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.81.smt2 | 0.386s | 30.736MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.366.smt2 | 0.386s | 32.66MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__addr_interface.2.smt2 | 0.386s | 28.488MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.99.smt2 | 0.386s | 29.768MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.64.smt2 | 0.387s | 27.948MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.39.smt2 | 0.389s | 28.98MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.5.smt2 | 0.391s | 31.232MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.152.smt2 | 0.394s | 33.784MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.85.smt2 | 0.396s | 30.82MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.124.smt2 | 0.396s | 34.812MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.364.smt2 | 0.397s | 36.204MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.201.smt2 | 0.398s | 34.384MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-alloc_generic.9.smt2 | 0.401s | 35.352MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__multilogimpl_v.12.smt2 | 0.401s | 31.144MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.8.smt2 | 0.402s | 33.916MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-definitions_ulib_definitions_u.x86_arch_inv._01.smt2 | 0.404s | 23.936MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.26.smt2 | 0.405s | 33.16MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.329.smt2 | 0.405s | 36.412MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.119.smt2 | 0.409s | 31.744MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.3.smt2 | 0.413s | 35.836MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-math.18.smt2 | 0.413s | 21.984MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.45.smt2 | 0.414s | 32.708MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.235.smt2 | 0.415s | 35.156MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.286.smt2 | 0.416s | 36.372MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.324.smt2 | 0.416s | 34.916MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.53.smt2 | 0.416s | 30.82MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.231.smt2 | 0.417s | 34.464MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.178.smt2 | 0.418s | 31.68MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.41.smt2 | 0.418s | 27.66MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.162.smt2 | 0.420s | 31.58MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.184.smt2 | 0.420s | 32.308MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.209.smt2 | 0.421s | 31.036MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.11.smt2 | 0.421s | 33.152MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.4.smt2 | 0.421s | 31.776MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.23.smt2 | 0.422s | 27.556MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__exe.1.smt2 | 0.424s | 31.624MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.78.smt2 | 0.424s | 29.984MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.186.smt2 | 0.426s | 32.424MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.19.smt2 | 0.427s | 28.408MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.47.smt2 | 0.432s | 30.9MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.176.smt2 | 0.433s | 33.768MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.11.smt2 | 0.434s | 35.364MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__mshyper__param_e.5.smt2 | 0.435s | 32.04MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__snp_u.16.smt2 | 0.436s | 34.808MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.256.smt2 | 0.436s | 34.364MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.22.smt2 | 0.439s | 29.28MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.91.smt2 | 0.442s | 33.032MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.308.smt2 | 0.443s | 35.312MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.68.smt2 | 0.443s | 29.94MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.17.smt2 | 0.444s | 31.128MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.51.smt2 | 0.444s | 31.312MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__params.23.smt2 | 0.449s | 39.636MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.83.smt2 | 0.454s | 29.304MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__ptram__ptram_p.10.smt2 | 0.455s | 35.548MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__range_interface.15.smt2 | 0.458s | 32.752MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.121.smt2 | 0.460s | 33.024MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.69.smt2 | 0.464s | 31.636MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-alloc_fast.3.smt2 | 0.464s | 36.096MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.26.smt2 | 0.471s | 34.22MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.233.smt2 | 0.471s | 35.844MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.206.smt2 | 0.471s | 34.476MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.239.smt2 | 0.471s | 31.288MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.175.smt2 | 0.472s | 33.54MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.47.smt2 | 0.473s | 25.896MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.2.smt2 | 0.475s | 27.708MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.393.smt2 | 0.478s | 32.808MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.73.smt2 | 0.478s | 33.012MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.2.smt2 | 0.479s | 36.152MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.88.smt2 | 0.479s | 29.928MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.46.smt2 | 0.483s | 32.548MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.282.smt2 | 0.483s | 31.896MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec_e__math__bits_e.5.smt2 | 0.485s | 33.292MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.18.smt2 | 0.487s | 23.156MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.338.smt2 | 0.491s | 32.444MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.16.smt2 | 0.497s | 29.896MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.19.smt2 | 0.498s | 35.484MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.58.smt2 | 0.499s | 32.344MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.21.smt2 | 0.500s | 34.328MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__replica.13.smt2 | 0.500s | 30.904MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.16.smt2 | 0.500s | 29.96MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.16.smt2 | 0.501s | 28.264MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__pgtable__entry_p.4.smt2 | 0.502s | 26.776MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.221.smt2 | 0.505s | 34.28MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.226.smt2 | 0.505s | 34.232MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/ironkv-smt-verus_extra__seq_lib_v.5.smt2 | 0.505s | 22.576MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.26.smt2 | 0.506s | 40.868MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-segment__segment_span_allocate.1.smt2 | 0.506s | 34.088MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpuid.16.smt2 | 0.508s | 42.376MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.3.smt2 | 0.508s | 36.424MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/allocator__page_allocator_spec_impl.4.smt2 | 0.512s | 29.372MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.32.smt2 | 0.512s | 29.964MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.56.smt2 | 0.516s | 28.244MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.53.smt2 | 0.516s | 27.956MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.38.smt2 | 0.517s | 33.228MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout.21.smt2 | 0.517s | 24.544MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.388.smt2 | 0.520s | 32.804MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.149.smt2 | 0.521s | 35.056MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.168.smt2 | 0.522s | 34.128MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.6.smt2 | 0.523s | 33.52MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec_e__math__bits_e.3.smt2 | 0.527s | 32.236MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.25.smt2 | 0.527s | 30.212MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__mshyper__param_e.1.smt2 | 0.531s | 35.592MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.86.smt2 | 0.531s | 33.156MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/pagetable__pagetable_spec_impl.7.smt2 | 0.532s | 37.04MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.225.smt2 | 0.532s | 34.644MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.55.smt2 | 0.532s | 32.116MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_commit.2.smt2 | 0.534s | 25.644MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-pagelib_page.page_init._01.smt2 | 0.536s | 30.36MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.20.smt2 | 0.537s | 32.88MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.19.smt2 | 0.538s | 30.588MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.348.smt2 | 0.539s | 32.372MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.28.smt2 | 0.539s | 33.572MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.9.smt2 | 0.539s | 33.588MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.408.smt2 | 0.540s | 33.088MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/allocator__page_allocator_spec_impl.7.smt2 | 0.542s | 30.392MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.415.smt2 | 0.544s | 36.384MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_e.12.smt2 | 0.544s | 34.932MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.423.smt2 | 0.544s | 33.144MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.380.smt2 | 0.545s | 33.548MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.336.smt2 | 0.546s | 32.22MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.306.smt2 | 0.547s | 36.468MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.370.smt2 | 0.547s | 33.52MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_e.15.smt2 | 0.549s | 34.248MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__pcr.8.smt2 | 0.550s | 51.088MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.240.smt2 | 0.553s | 34.98MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.30.smt2 | 0.553s | 32.904MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__params.12.smt2 | 0.556s | 49.94MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.363.smt2 | 0.557s | 32.484MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_e.2.smt2 | 0.558s | 40.604MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.6.smt2 | 0.558s | 27.84MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/memory_manager__spec_impl.12.smt2 | 0.561s | 25.588MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.28.smt2 | 0.561s | 56.892MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.7.smt2 | 0.562s | 27.932MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.398.smt2 | 0.563s | 33.008MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.371.smt2 | 0.566s | 33.532MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.5.smt2 | 0.571s | 30.22MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.144.smt2 | 0.574s | 35.032MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.283.smt2 | 0.576s | 35.568MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.208.smt2 | 0.579s | 35.82MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.12.smt2 | 0.583s | 37.676MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security.18.smt2 | 0.584s | 37.372MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.265.smt2 | 0.585s | 35.204MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.394.smt2 | 0.588s | 36.432MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.391.smt2 | 0.589s | 32.812MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.418.smt2 | 0.590s | 32.972MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.56.smt2 | 0.592s | 34.476MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.9.smt2 | 0.593s | 42.048MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.183.smt2 | 0.593s | 33.884MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.6.smt2 | 0.596s | 34.892MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.202.smt2 | 0.599s | 34.396MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec_e__math__align_e.1.smt2 | 0.600s | 32.872MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-os_mem_util.10.smt2 | 0.601s | 37.688MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.328.smt2 | 0.603s | 35.412MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.21.smt2 | 0.604s | 33.868MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_e.20.smt2 | 0.619s | 35.06MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.325.smt2 | 0.623s | 35.128MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.10.smt2 | 0.625s | 39.612MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.77.smt2 | 0.631s | 32.952MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.222.smt2 | 0.641s | 34.472MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.16.smt2 | 0.645s | 40.38MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.381.smt2 | 0.651s | 34.476MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/allocator__page_allocator_spec_impl.8.smt2 | 0.653s | 30.428MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.274.smt2 | 0.653s | 35.028MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.30.smt2 | 0.653s | 33.124MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.1.smt2 | 0.653s | 27.176MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.67.smt2 | 0.654s | 30.952MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__linkedlist.3.smt2 | 0.655s | 33.868MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.341.smt2 | 0.656s | 35.804MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.309.smt2 | 0.656s | 35.16MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.63.smt2 | 0.657s | 31.392MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.414.smt2 | 0.657s | 36.688MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.237.smt2 | 0.657s | 34.616MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.7.smt2 | 0.657s | 29.704MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.18.smt2 | 0.658s | 35.616MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.27.smt2 | 0.659s | 31.216MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.22.smt2 | 0.659s | 33.764MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.121.smt2 | 0.660s | 52.064MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.342.smt2 | 0.662s | 36.632MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.148.smt2 | 0.662s | 33.852MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.22.smt2 | 0.663s | 36.332MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpuid.14.smt2 | 0.667s | 40.748MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__init__mshv_fmt.1.smt2 | 0.667s | 47.056MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.395.smt2 | 0.668s | 36.22MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/splinterdb/marshalling__KVPairFormat_v.3.smt2 | 0.673s | 27.292MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.2.smt2 | 0.674s | 39.116MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.17.smt2 | 0.686s | 56.108MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.10.smt2 | 0.688s | 27.748MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/memory_manager__spec_impl.5.smt2 | 0.697s | 29.744MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.21.smt2 | 0.697s | 34.776MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__snp_s.smt2 | 0.699s | 37.408MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.3.smt2 | 0.700s | 32.196MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__slice_print.3.smt2 | 0.701s | 48.96MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__ptram__ptram_p.6.smt2 | 0.707s | 33.276MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.36.smt2 | 0.708s | 51.412MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.368.smt2 | 0.708s | 35.828MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.44.smt2 | 0.708s | 51.912MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__log.10.smt2 | 0.712s | 30.352MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.14.smt2 | 0.719s | 31.648MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype_test.5.smt2 | 0.725s | 31.404MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__secret.17.smt2 | 0.729s | 50.844MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.372.smt2 | 0.731s | 35.96MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.33.smt2 | 0.733s | 29.516MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__multilogimpl_v.9.smt2 | 0.734s | 33.256MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.362.smt2 | 0.735s | 36.908MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.29.smt2 | 0.738s | 40.456MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.412.smt2 | 0.740s | 37.372MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__secret.1.smt2 | 0.742s | 51.252MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.389.smt2 | 0.742s | 36.384MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.27.smt2 | 0.743s | 65.044MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.37.smt2 | 0.744s | 35.524MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_segment.6.smt2 | 0.746s | 35.804MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_refinement.5.smt2 | 0.747s | 30.444MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.390.smt2 | 0.751s | 36.18MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl__PT.15.smt2 | 0.751s | 33.3MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.417.smt2 | 0.756s | 37.528MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.7.smt2 | 0.757s | 39.8MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__idt__dummy.5.smt2 | 0.764s | 43.524MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.392.smt2 | 0.780s | 36.312MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.17.smt2 | 0.780s | 30.368MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.10.smt2 | 0.781s | 32.62MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.346.smt2 | 0.786s | 35.644MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.49.smt2 | 0.788s | 51.252MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.321.smt2 | 0.789s | 35.072MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.3.smt2 | 0.791s | 28.028MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.16.smt2 | 0.792s | 35.104MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/noderep-smt-exec__replica.11.smt2 | 0.795s | 30.316MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.8.smt2 | 0.812s | 41.904MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page.16.smt2 | 0.812s | 36.516MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.31.smt2 | 0.813s | 60.732MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__raw_ptr_s.1.smt2 | 0.813s | 44.42MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-bin_sizes.45.smt2 | 0.813s | 29.904MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__range_interface.14.smt2 | 0.815s | 36.256MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__mem_util.2.smt2 | 0.818s | 37.816MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__idt__dummy.3.smt2 | 0.818s | 42.452MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.1.smt2 | 0.820s | 59.464MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.7.smt2 | 0.825s | 59.148MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-queues.3.smt2 | 0.831s | 34.124MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.34.smt2 | 0.833s | 51.508MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__layout_v.30.smt2 | 0.840s | 31.556MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.5.smt2 | 0.841s | 30.928MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.14.smt2 | 0.866s | 65.884MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.1.smt2 | 0.867s | 37.18MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__linkedlist.11.smt2 | 0.871s | 40.852MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__params.14.smt2 | 0.871s | 45.324MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.25.smt2 | 0.872s | 51.236MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.40.smt2 | 0.878s | 51.496MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.34.smt2 | 0.879s | 51.868MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.20.smt2 | 0.881s | 39.04MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.64.smt2 | 0.887s | 56.752MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.93.smt2 | 0.889s | 58.652MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.30.smt2 | 0.892s | 65.88MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper__hypercall.2.smt2 | 0.898s | 51.204MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.8.smt2 | 0.899s | 63.828MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.11.smt2 | 0.908s | 59.62MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.7.smt2 | 0.911s | 41.916MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.94.smt2 | 0.912s | 35.096MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.11.smt2 | 0.916s | 59.992MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.58.smt2 | 0.919s | 56.664MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper__wakeup.1.smt2 | 0.919s | 51.088MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.6.smt2 | 0.919s | 32.876MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.11.smt2 | 0.929s | 43.304MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.39.smt2 | 0.930s | 32.424MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__create_and_share_pages.4.smt2 | 0.935s | 70.18MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.20.smt2 | 0.939s | 60.092MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.9.smt2 | 0.942s | 31.268MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.22.smt2 | 0.945s | 62.568MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.29.smt2 | 0.947s | 31.904MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__security__sectype.138.smt2 | 0.950s | 33.972MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__create_and_map_pages.1.smt2 | 0.952s | 37.584MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.2.smt2 | 0.952s | 65.928MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.12.smt2 | 0.962s | 62.372MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__pcr.2.smt2 | 0.962s | 59.168MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.14.smt2 | 0.963s | 37.876MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__secret.9.smt2 | 0.965s | 64.804MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.2.smt2 | 0.968s | 32.452MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.117.smt2 | 0.971s | 57.436MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.10.smt2 | 0.974s | 65.908MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.28.smt2 | 0.982s | 60.856MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.5.smt2 | 0.986s | 58.764MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.70.smt2 | 0.993s | 65.464MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.35.smt2 | 0.994s | 56.752MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.11.smt2 | 0.994s | 60.284MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__trackedcore__snpmulticore.1.smt2 | 1.001s | 68.34MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.7.smt2 | 1.003s | 34.872MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.18.smt2 | 1.003s | 65.892MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.25.smt2 | 1.003s | 67.432MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.138.smt2 | 1.004s | 56.956MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.5.smt2 | 1.005s | 59.216MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.15.smt2 | 1.011s | 38.048MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.16.smt2 | 1.012s | 43.264MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.13.smt2 | 1.017s | 58.864MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.37.smt2 | 1.020s | 56.196MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.71.smt2 | 1.020s | 64.452MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.23.smt2 | 1.027s | 67.204MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.107.smt2 | 1.029s | 66.288MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.26.smt2 | 1.029s | 67.072MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.48.smt2 | 1.036s | 31.416MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.1.smt2 | 1.040s | 30.484MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.30.smt2 | 1.045s | 62.248MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.27.smt2 | 1.045s | 57.892MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__monitor_params.smt2 | 1.051s | 39.224MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.14.smt2 | 1.053s | 62.18MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.89.smt2 | 1.078s | 63.88MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__schedule_idle_cpu.smt2 | 1.081s | 45.996MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__mem__mem_p.16.smt2 | 1.089s | 38.972MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.44.smt2 | 1.091s | 64.488MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__create_and_map_pages.6.smt2 | 1.093s | 49.788MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.3.smt2 | 1.103s | 32.784MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__mem__mem_p.11.smt2 | 1.106s | 37.252MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.25.smt2 | 1.107s | 64.44MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-linked_list.13.smt2 | 1.112s | 38.748MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.38.smt2 | 1.123s | 70.416MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.43.smt2 | 1.128s | 61.592MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__init__init_e.2.smt2 | 1.130s | 61.464MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.28.smt2 | 1.131s | 37.36MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__params.16.smt2 | 1.133s | 65.748MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.4.smt2 | 1.146s | 63.172MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.69.smt2 | 1.149s | 65.68MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.37.smt2 | 1.150s | 60.568MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.19.smt2 | 1.154s | 64.924MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.10.smt2 | 1.160s | 62.884MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.20.smt2 | 1.163s | 67.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.6.smt2 | 1.163s | 64.096MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.26.smt2 | 1.170s | 65.856MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.39.smt2 | 1.175s | 38.992MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.7.smt2 | 1.177s | 63.032MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.34.smt2 | 1.178s | 32.628MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__linkedlist.13.smt2 | 1.182s | 48.432MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/pagetable__pagetable_spec_impl.5.smt2 | 1.184s | 37.328MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.103.smt2 | 1.189s | 65.408MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.73.smt2 | 1.191s | 66.096MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.50.smt2 | 1.192s | 65.78MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__init__mshv_alloc.3.smt2 | 1.194s | 64.38MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.2.smt2 | 1.196s | 39.188MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.4.smt2 | 1.197s | 63.512MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.65.smt2 | 1.197s | 37.164MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.13.smt2 | 1.211s | 64.508MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.88.smt2 | 1.216s | 65.128MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.16.smt2 | 1.222s | 65.908MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.6.smt2 | 1.226s | 66.544MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__secret.24.smt2 | 1.226s | 63.728MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.42.smt2 | 1.227s | 64.864MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.10.smt2 | 1.251s | 67.876MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.4.smt2 | 1.254s | 65.984MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-init.13.smt2 | 1.254s | 40.172MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.102.smt2 | 1.255s | 65.724MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-tokens__Mim.26.smt2 | 1.259s | 39.276MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.17.smt2 | 1.259s | 33.576MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.126.smt2 | 1.262s | 70.644MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__ptr_e.9.smt2 | 1.264s | 40.516MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.127.smt2 | 1.270s | 70.14MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.83.smt2 | 1.270s | 66.624MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__secret.6.smt2 | 1.270s | 65.26MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.25.smt2 | 1.280s | 65.748MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.28.smt2 | 1.282s | 60.832MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.81.smt2 | 1.282s | 66.588MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.35.smt2 | 1.293s | 35.512MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-types.45.smt2 | 1.296s | 39.16MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.91.smt2 | 1.297s | 65.412MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.31.smt2 | 1.298s | 64.812MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.68.smt2 | 1.300s | 66.464MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.8.smt2 | 1.311s | 65.8MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.67.smt2 | 1.336s | 69.836MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/addr_e__range_interface.17.smt2 | 1.336s | 40.688MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.110.smt2 | 1.343s | 66.292MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__secret.22.smt2 | 1.350s | 62.08MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__raw_ptr_s.3.smt2 | 1.359s | 44.536MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.63.smt2 | 1.364s | 71.012MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.9.smt2 | 1.386s | 68.692MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.94.smt2 | 1.388s | 65.516MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.112.smt2 | 1.404s | 67.376MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.21.smt2 | 1.413s | 65.78MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl.10.smt2 | 1.413s | 29.448MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.104.smt2 | 1.417s | 64.74MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__secret.18.smt2 | 1.470s | 67.012MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1__impl_%1__lemma_resolve_refines.smt2 | 1.476s | 37.7MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.42.smt2 | 1.479s | 31.844MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.45.smt2 | 1.490s | 39.32MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-free.3.smt2 | 1.490s | 65.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-free.6.smt2 | 1.504s | 64.208MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.96.smt2 | 1.508s | 64.516MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.85.smt2 | 1.517s | 66.86MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_e.19.smt2 | 1.528s | 67.808MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.33.smt2 | 1.531s | 69.828MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/process_manager__spec_impl.26.smt2 | 1.539s | 66.3MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.38.smt2 | 1.549s | 64.352MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/tspec__math__align_s.5.smt2 | 1.566s | 33.028MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.27.smt2 | 1.568s | 67.46MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.45.smt2 | 1.576s | 66.132MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-alloc_generic.5.smt2 | 1.618s | 46.276MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.48.smt2 | 1.649s | 65.604MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.41.smt2 | 1.685s | 74.556MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.36.smt2 | 1.699s | 38.636MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.20.smt2 | 1.724s | 66.808MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.40.smt2 | 1.725s | 31.736MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.10.smt2 | 1.727s | 73.604MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.22.smt2 | 1.727s | 68.744MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.98.smt2 | 1.744s | 64.544MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__syscall_receive_empty.2.smt2 | 1.790s | 67.284MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.50.smt2 | 1.813s | 66.116MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.39.smt2 | 1.835s | 38.34MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.49.smt2 | 1.843s | 64.172MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.66.smt2 | 1.878s | 81.856MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.25.smt2 | 1.899s | 43.52MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.17.smt2 | 1.905s | 68.392MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.26.smt2 | 1.928s | 67.008MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-root.smt2 | 1.942s | 70.62MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.18.smt2 | 1.951s | 60.888MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.12.smt2 | 1.996s | 34.572MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.32.smt2 | 2.035s | 75.048MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper__wakeup.5.smt2 | 2.070s | 149.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__start_v.2.smt2 | 2.078s | 36.384MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__mem__mem_p.13.smt2 | 2.098s | 42.912MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.16.smt2 | 2.113s | 38.024MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.32.smt2 | 2.133s | 64.372MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/lock__spincell_e.5.smt2 | 2.236s | 72.904MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layoutlib_layout.align_up._02.smt2 | 2.242s | 26.848MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.44.smt2 | 2.258s | 64.148MiB| 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 | 2.315s | 39.388MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.79.smt2 | 2.331s | 39.288MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__def.31.smt2 | 2.343s | 38.216MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-page_organization__PageOrg.60.smt2 | 2.359s | 39.736MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.13.smt2 | 2.361s | 85.56MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__def_s.smt2 | 2.425s | 93.828MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.18.smt2 | 2.436s | 36.348MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.15.smt2 | 2.463s | 38.68MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__gdt.19.smt2 | 2.536s | 32.296MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.4.smt2 | 2.679s | 82.588MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_segment.1.smt2 | 2.877s | 33.264MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__create_and_share_pages.3.smt2 | 2.916s | 69.424MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.134.smt2 | 2.957s | 77.62MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.9.smt2 | 2.963s | 41.088MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__x64__x64_p.2.smt2 | 3.234s | 47.344MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/vbox__vbox.6.smt2 | 3.250s | 141.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.12.smt2 | 3.482s | 76.3MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.11.smt2 | 3.834s | 31.696MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__mem__mem_p.4.smt2 | 3.898s | 48.716MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.5.smt2 | 3.950s | 78.072MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/vbox__vbox.2.smt2 | 3.967s | 129.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.7.smt2 | 4.003s | 81.42MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__syscall_send_endpoint.smt2 | 4.053s | 121.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout__block_ptr_aligned_to_word.smt2 | 4.241s | 26.148MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/allocator__page_allocator_spec_impl.20.smt2 | 4.318s | 46.488MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.4.smt2 | 4.372s | 44.3MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__linux.17.smt2 | 4.413s | 74.8MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__init__init_s.smt2 | 4.516s | 144.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/lock__spin_perm_s.3.smt2 | 4.608s | 87.532MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__rmp__rmp_e.7.smt2 | 4.825s | 77.244MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.7.smt2 | 4.831s | 78.932MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_e.18.smt2 | 5.123s | 74.696MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__locked.1.smt2 | 5.236s | 100.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/allocator__page_allocator_spec_impl.10.smt2 | 5.277s | 48.772MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl__internal.2.smt2 | 5.497s | 130.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__rmp__rmp_e.5.smt2 | 5.686s | 96.2MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_impl.15.smt2 | 5.884s | 167.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.37.smt2 | 6.415s | 136.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__mem.38.smt2 | 6.446s | 264.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.15.smt2 | 6.573s | 48.384MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__linkedlist.6.smt2 | 6.702s | 95.112MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.23.smt2 | 7.777s | 144.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__linkedlist.10.smt2 | 8.320s | 72.98MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__syscall_send_pages.smt2 | 8.372s | 122.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.9.smt2 | 8.440s | 80.032MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.9.smt2 | 8.620s | 76.892MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__ghcb__proto_page.140.smt2 | 8.643s | 182.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/allocator__page_allocator_spec_impl.23.smt2 | 9.135s | 72.848MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.50.smt2 | 9.423s | 51.024MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/vbox__vbox.7.smt2 | 9.424s | 129.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/allocator__page_allocator_spec_impl.15.smt2 | 9.602s | 70.224MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/vbox__vbox.3.smt2 | 10.281s | 191.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.1.smt2 | 10.343s | 187.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/pgtable_e__pte.22.smt2 | 10.471s | 267.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-layout__align_downlib_layout.align_down._03.smt2 | 10.546s | 24.052MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.37.smt2 | 11.092s | 58.652MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/debug__ghcb_print.8.smt2 | 11.112s | 62.42MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.13.smt2 | 12.470s | 94.032MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/ptr__snp__rmp__rmp_e.3.smt2 | 13.307s | 135.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.12.smt2 | 14.201s | 137.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/arch__vram__vram_p.9.smt2 | 14.235s | 66.692MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper__wakeup.7.smt2 | 14.561s | 263.0MiB| unsat | 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 | 14.883s | 61.704MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/mshyper.19.smt2 | 15.091s | 198.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__pcr.5.smt2 | 16.338s | 286.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/kernel__syscall_new_proc.smt2 | 16.497s | 121.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l1.47.smt2 | 16.591s | 61.684MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.15.smt2 | 16.826s | 93.612MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.11.smt2 | 17.766s | 50.716MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.6.smt2 | 19.371s | 137.0MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__os_refinement.10.smt2 | 19.403s | 94.152MiB| unsat | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-segment__segment_slice_split.smt2 | 20.022s | 94.568MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl__PT.28.smt2 | 20.023s | 84.068MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/allocator__buddy.13.smt2 | 20.031s | 151.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-segment__segment_span_free_coalesce_before.smt2 | 20.031s | 121.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20230314-Jaroslav-Bendik-Certora/52759_b3ecd2335fd16ec2eee2_9_UFDTNIA.smt2 | 20.033s | 41.972MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.16.smt2 | 20.037s | 180.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.10.smt2 | 20.039s | 175.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.14.smt2 | 20.046s | 180.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_refinement.4.smt2 | 20.047s | 81.144MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__multilogimpl_v.5.smt2 | 20.050s | 83.56MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_impl__PT.18.smt2 | 20.062s | 99.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.062s | 28.236MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-queues__page_queue_push.smt2 | 20.065s | 119.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.24.smt2 | 20.068s | 153.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/snp__cpu__vmsa.2.smt2 | 20.071s | 529.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-queues__page_queue_push_back.smt2 | 20.075s | 124.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/linkedlist.4.smt2 | 20.077s | 144.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__secret.13.smt2 | 20.079s | 274.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__append_v.2.smt2 | 20.080s | 97.576MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-segment__segment_page_clear.smt2 | 20.093s | 121.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.12.smt2 | 20.103s | 280.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/page-table-smt-impl_u__l2_refinement.3.smt2 | 20.104s | 96.508MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/mimalloc-smt-commit_mask.31.smt2 | 20.106s | 752.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/security__monitor.15.smt2 | 20.116s | 202.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/atmosphere/pagetable__pagetable_spec_impl.1.smt2 | 20.129s | 332.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/verismo/boot__idt__def.4.smt2 | 20.130s | 309.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/20241211-verus/systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__setup_v.6.smt2 | 20.158s | 801.0MiB| timeout | 0 | | | |non-incremental/UFDTNIA/2019-Gleiss/non-interference/10-ni-rsa-exponentiation.spec.smt2 | 20.280s | 2166.0MiB| timeout | 0 | | |