20241211-verus Benchmarks

Family
Name	verus
Generation Date	2024-12-11
First Occurrence	2025-08-11
Benchmarks	2442

Benchmarks

UFBVDTLIA • Charts • Solver Isomap
verussystems/mimalloc-smt-flagslib_flags.impl_%0.set_in_full._01.smt2
verussystems/mimalloc-smt-flagslib_flags.impl_%0.set_is_committed._02.smt2
verussystems/mimalloc-smt-flagslib_flags.impl_%0.set_retire_expire._02.smt2
verussystems/mimalloc-smt-flagslib_flags.impl_%0.set_is_committed._01.smt2
verussystems/mimalloc-smt-flagslib_flags.impl_%0.get_retire_expire._01.smt2
verussystems/mimalloc-smt-flagslib_flags.impl_%0.set_is_zero_init._03.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_auto._01.smt2
atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._07.smt2
atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._25.smt2
atmosphere/pagetable__entrylib_pagetable.entry.zero_leads_is_empty_page_entry._06.smt2
atmosphere/pagetable__entrylib_pagetable.entry.usize2page_entry_perm._05.smt2
atmosphere/pagetable__entrylib_pagetable.entry.zero_leads_is_empty_page_entry._01.smt2
atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._12.smt2
atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._06.smt2
atmosphere/pagetable__entrylib_pagetable.entry.usize2page_entry_perm._01.smt2
atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._01.smt2
atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._05.smt2
atmosphere/pagetable__entrylib_pagetable.entry.usize2pa._01.smt2
atmosphere/pagetable__entrylib_pagetable.entry.usize2page_entry_perm._04.smt2
atmosphere/pagetable__entrylib_pagetable.entry.usize2page_entry_perm._03.smt2
atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._16.smt2
atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._32.smt2
atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._35.smt2
atmosphere/pagetable__entrylib_pagetable.entry.zero_leads_is_empty_page_entry._03.smt2

UFBVDTNIA • Charts • Solver Isomap
verussystems/mimalloc-smt-commit_masklib_commit_mask.impl_%0.next_run._05.smt2
verussystems/page-table-smt-impl_u__l2_refinementlib_impl_u.l2_refinement.lemma_page_table_walk_interp_aux_1._05.smt2
verussystems/mimalloc-smt-bin_sizeslib_bin_sizes.bin._04.smt2
verussystems/page-table-smt-impl_u__l2_impllib_impl_u.l2_impl.impl_%0.lemma_zero_entry_facts._03.smt2
verussystems/mimalloc-smt-commit_masklib_commit_mask.lemma_obtain_bit_index_1_aux._03.smt2
verussystems/mimalloc-smt-commit_masklib_commit_mask.lemma_obtain_bit_index_3_aux._02.smt2
verussystems/page-table-smt-impl_u__l2_refinementlib_impl_u.l2_refinement.lemma_page_table_walk_interp_aux_2._12.smt2
verussystems/mimalloc-smt-layoutlib_layout.bitand_with_mask_gives_rounding._07.smt2
verussystems/page-table-smt-impl_u__l2_refinementlib_impl_u.l2_refinement.lemma_page_table_walk_interp_aux_1._02.smt2
verussystems/page-table-smt-impl_u__l2_refinementlib_impl_u.l2_refinement.lemma_page_table_walk_interp_aux_1._03.smt2
verussystems/mimalloc-smt-linked_listlib_linked_list.masked_ptr_delay_get_ptr._01.smt2
verussystems/page-table-smt-impl_u__l2_impllib_impl_u.l2_impl.impl_%0.lemma_zero_entry_facts._02.smt2
verussystems/mimalloc-smt-bin_sizeslib_bin_sizes.shift_is_div._02.smt2
verussystems/mimalloc-smt-commit_masklib_commit_mask.lemma_bitmask_to_is_bit_set._02.smt2
verussystems/page-table-smt-impl_u__l2_refinementlib_impl_u.l2_refinement.lemma_page_table_walk_interp_aux_1._08.smt2
verussystems/mimalloc-smt-freelib_free.free_block_mt._01.smt2
verussystems/mimalloc-smt-commit_masklib_commit_mask.impl_%0.next_run._02.smt2
verussystems/mimalloc-smt-layoutlib_layout.calculate_segment_ptr_from_block._01.smt2
verussystems/mimalloc-smt-linked_listlib_linked_list.masked_ptr_delay_set_freeing._01.smt2
verussystems/mimalloc-smt-layoutlib_layout.bitand_with_mask_gives_rounding._08.smt2
verussystems/mimalloc-smt-commit_masklib_commit_mask.lemma_obtain_bit_index_3_aux._01.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_property_auto._01.smt2
verussystems/page-table-smt-impl_u__l2_refinementlib_impl_u.l2_refinement.lemma_page_table_walk_interp_aux_2._07.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._18.smt2
verussystems/mimalloc-smt-commit_masklib_commit_mask.impl_%0.next_run._10.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._57.smt2
verussystems/mimalloc-smt-linked_listlib_linked_list.impl_%8.take._01.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._24.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._25.smt2
verismo/tspec__math__pow_pverismo_tspec.math.pow_p.proof_pow2_to_bits._02.smt2
verismo/allocator__bit_pverismo_allocator.bit_p.lemma_get_low_bits_via_bit_op._02.smt2
verismo/tspec__math__integerverismo_tspec.math.integer.lemma_fill_ones._02.smt2
verismo/tspec__math__integerverismo_tspec.math.integer.lemma_fill_ones._06.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._12.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._14.smt2
verussystems/page-table-smt-impl_u__l2_refinementlib_impl_u.l2_refinement.lemma_page_table_walk_interp_aux_2._05.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._21.smt2
verussystems/mimalloc-smt-linked_listlib_linked_list.masked_ptr_delay_set_ptr._02.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._62.smt2
verismo/arch__pgtable__entry_pverismo_arch.pgtable.entry_p.impl_%0.lemma_size_offset._01.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._19.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._01.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._07.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._60.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._55.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._19.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._39.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._57.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._58.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._56.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._50.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._45.smt2
verismo/tspec__math__integerverismo_tspec.math.integer.lemma_fill_ones_bit_step._03.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.proof_align_down._03.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._03.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._07.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._22.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._04.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._34.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._11.smt2
verismo/tspec__math__integerverismo_tspec.math.integer.lemma_prev_power_of_two._02.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._18.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._31.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._31.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._64.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._27.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._11.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._02.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._30.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._56.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._34.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._17.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._44.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._40.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._50.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._27.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._37.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._40.smt2
verismo/tspec__math__integerverismo_tspec.math.integer.lemma_prev_power_of_two._01.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._51.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._54.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_clear_set_property._01.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._56.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._61.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._28.smt2
verismo/snp__cpu__gdtverismo_snp.cpu.gdt.impl_%16.empty._01.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._52.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._55.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._11.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._51.smt2
verismo/security__memverismo_security.mem.impl_%16.empty._01.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._26.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._02.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._25.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._06.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._48.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._30.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._55.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._56.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._58.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._11.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._12.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._05.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._17.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._41.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._14.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._49.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._47.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._54.smt2
verismo/arch__pgtable__entry_pverismo_arch.pgtable.entry_p.lemma_pt_entry_count._01.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._19.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._02.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._34.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._59.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._62.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._28.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._59.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._38.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._14.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._48.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._23.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._04.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._23.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._46.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._32.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._24.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._27.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._10.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._19.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._07.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._62.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._45.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._33.smt2
verismo/tspec__math__integerverismo_tspec.math.integer.lemma_prev_power_of_two._03.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._06.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._13.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._49.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._05.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._35.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._33.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._58.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._52.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._44.smt2
verismo/debug__ghcb_printverismo_debug.ghcb_print.int2bytes._01.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._36.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._16.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._38.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._36.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._49.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._28.smt2
verismo/tspec__security__sectype_test__pverismo_tspec.security.sectype_test.p.proof_test_bits2._01.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._04.smt2
verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._44.smt2
verismo/tspec__math__integerverismo_tspec.math.integer.lemma_next_power_of_two._02.smt2
verismo/snp__cpu__vmsaverismo_snp.cpu.vmsa.impl_%16.empty._01.smt2
atmosphere/util__page_ptr_util_ulib_util.page_ptr_util_u.v2l4index._01.smt2
atmosphere/util__page_ptr_util_ulib_util.page_ptr_util_u.v2l3index._01.smt2

UFDTLIA • Charts • Solver Isomap
verismo/tspec_e__array__array_e.2.smt2
verismo/arch__addr_s__def_s.1.smt2
verismo/arch__rmp__def_s.1.smt2
verismo/tspec_e__array__sort.7.smt2
verismo/tspec__seqlib__subseq.1.smt2
verismo/tspec_e__array__array_utils.3.smt2
verismo/tspec_e__array__array_e.10.smt2
verismo/tspec_e__math__minmax.1.smt2
verismo/arch__rmp__def_s.4.smt2
verismo/snp__percpu__def_s.2.smt2
verismo/tspec__math__cond_bound.1.smt2
verismo/tspec__seqlib__seq_multiset.4.smt2
verismo/tspec_e__array__array_e.4.smt2
verismo/arch__rmp__def_s.3.smt2
verismo/tspec__map_lib.1.smt2
verismo/tspec__setlib.4.smt2
verismo/arch__addr_s__def_s.2.smt2
verismo/tspec__range_set.5.smt2
verismo/tspec__setlib.5.smt2
verismo/snp__percpu__def_s.1.smt2
verismo/tspec_e__array__sort.5.smt2
verismo/tspec_e__array__array_utils.5.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v.22.smt2
anvil/splinterdb-smt-journal__PagedJournal_v.3.smt2
anvil/splinterdb-smt-betree__BufferDisk_v.2.smt2
anvil/splinterdb-smt-betree__PagedBetree_v.35.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.44.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.5.smt2
anvil/splinterdb-smt-journal__PagedJournalRefinement_v.24.smt2
anvil/splinterdb-smt-betree__PivotBetreeRefinement_v.17.smt2
anvil/splinterdb-smt-betree__FilteredBetree_v.23.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v.1.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.16.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v__Refinement_v.16.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.18.smt2
anvil/splinterdb-smt-betree__PivotTable_v.7.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournalRefinement_v.8.smt2
anvil/splinterdb-smt-betree__PagedBetreeRefinement_v.24.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__reconciler.2.smt2
anvil/splinterdb-smt-betree__PagedBetreeRefinement_v.34.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__trusted__spec_types.6.smt2
anvil/splinterdb-smt-betree__PagedBetree_v.22.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__proof.1.smt2
anvil/splinterdb-smt-allocation_layer__AllocationCrashAwareJournalRefinement_v.7.smt2
anvil/splinterdb-smt-journal__PagedJournalRefinement_v.12.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.74.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__helper_invariants__proof__lemma_always_resource_object_create_or_update_request_msg_has_one_controller_ref_and_no_finalizers.smt2
anvil/splinterdb-smt-allocation_layer__LikesBetree_v__LikesBetree.7.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__reconciler.6.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__reconciler.1.smt2
anvil/splinterdb-smt-allocation_layer__LikesBetree_v.4.smt2
anvil/splinterdb-smt-exec__Cache_v__Cache.2.smt2
anvil/splinterdb-smt-betree__Buffer_v.5.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__headless_service.7.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v.13.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.52.smt2
anvil/splinterdb-smt-abstract_system__MsgHistory_v.30.smt2
anvil/splinterdb-smt-allocation_layer__LikesBetree_v__LikesBetree.6.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__resource__role_binding.5.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.12.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v.12.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.10.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.89.smt2
anvil/splinterdb-smt-betree__PivotBetreeRefinement_v.13.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.24.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__admin_server_service.5.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__trusted__spec_types.3.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.27.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.38.smt2
anvil/splinterdb-smt-betree__Buffer_v.15.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__proof.7.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__reconciler.11.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__stateful_set.10.smt2
anvil/splinterdb-smt-allocation_layer__MiniAllocator_v.13.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__resource__common.3.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__reconciler.7.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.64.smt2
anvil/splinterdb-smt-allocation_layer__AllocationCrashAwareJournal_v.2.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__trusted__spec_types.5.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__proof.3.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.26.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__daemon_set_match.2.smt2
anvil/splinterdb-smt-journal__PagedJournal_v.29.smt2
anvil/splinterdb-smt-allocation_layer__UnifiedCrashAwareJournalRefinement_v.3.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v.43.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__proof.4.smt2
anvil/splinterdb-smt-journal__PagedJournalRefinement_v.10.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v.27.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__client_service.3.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.111.smt2
anvil/splinterdb-smt-allocation_layer__AllocationCrashAwareJournalRefinement_v.6.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof.11.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v__AllocationJournal.7.smt2
anvil/splinterdb-smt-journal__PagedJournalRefinement_v.17.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__resource__common.1.smt2
anvil/splinterdb-smt-betree__PagedBetree_v.11.smt2
anvil/splinterdb-smt-allocation_layer__MiniAllocator_v.3.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__headless_service.3.smt2
anvil/splinterdb-smt-allocation_layer__MiniAllocator_v.4.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__service.7.smt2
anvil/splinterdb-smt-betree__PivotBetree_v.40.smt2
anvil/splinterdb-smt-betree__PivotBetree_v.43.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v__LinkedBetreeVars.8.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.57.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.11.smt2
anvil/splinterdb-smt-abstract_system__MsgHistory_v.23.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.9.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v__LikesJournal.11.smt2
anvil/splinterdb-smt-betree__PagedBetreeRefinement_v.4.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof__lemma_eventually_always_every_resource_create_request_implies_at_after_create_resource_step.smt2
anvil/splinterdb-smt-betree__PivotBranchRefinement_v.18.smt2
anvil/splinterdb-smt-exec__Cache_v.1.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v.21.smt2
anvil/splinterdb-smt-betree__FilteredBetree_v.26.smt2
anvil/splinterdb-smt-betree__PivotBranchRefinement_v.11.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__zookeeper_api.15.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.24.smt2
anvil/splinterdb-smt-betree__Buffer_v.3.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__spec.9.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof.8.smt2
anvil/splinterdb-smt-betree__PivotBranchRefinement_v.21.smt2
anvil/splinterdb-smt-betree__BufferDisk_v.7.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__stateful_set.4.smt2
anvil/splinterdb-smt-betree__PivotBetreeRefinement_v.20.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__spec.18.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__unchangeable.5.smt2
anvil/splinterdb-smt-journal__PagedJournalRefinement_v.6.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__resource_match.7.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__common.2.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__zookeeper_api.12.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__proof__lemma_eventually_always_every_resource_create_request_implies_at_after_create_resource_step.smt2
anvil/splinterdb-smt-allocation_layer__AllocationCrashAwareJournal_v__AllocationCrashAwareJournal.4.smt2
anvil/splinterdb-smt-abstract_system__MsgHistory_v.16.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__headless_service.6.smt2
anvil/splinterdb-smt-betree__FilteredBetree_v.21.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.19.smt2
anvil/splinterdb-smt-betree__FilteredBetreeRefinement_v.23.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v__AllocationJournal.11.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__default_user_secret.6.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__spec.15.smt2
anvil/splinterdb-smt-allocation_layer__LikesBetree_v.18.smt2
anvil/splinterdb-smt-betree__Domain_v.3.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof__lemma_resource_create_or_update_request_msg_implies_key_in_reconcile_equals.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__spec.10.smt2
anvil/splinterdb-smt-betree__Memtable_v.6.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.12.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__spec.11.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__erlang_cookie.7.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__resource_match__lemma_from_key_not_exists_to_receives_not_found_resp_at_after_get_resource_step.smt2
anvil/splinterdb-smt-journal__PagedJournalRefinement_v.4.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.37.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__resource__service.7.smt2
anvil/fluent-smt-fluent_controller__fluentbit__trusted__spec_types.2.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__stateful_set_match__lemma_from_key_exists_to_receives_ok_resp_at_after_get_stateful_set_step.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__exec__resource__secret.8.smt2
anvil/splinterdb-smt-betree__PivotTable_v.10.smt2
anvil/splinterdb-smt-exec__MiniAllocator_v.2.smt2
anvil/splinterdb-smt-betree__Memtable_v.3.smt2
anvil/splinterdb-smt-betree__FilteredBetreeRefinement_v.3.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.60.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__headless_service.7.smt2
anvil/splinterdb-smt-betree__FilteredBetreeRefinement_v.30.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__daemon_set_match__lemma_from_key_exists_to_receives_ok_resp_at_after_get_daemon_set_step.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__resource_match.2.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__common.3.smt2
anvil/splinterdb-smt-betree__PivotBetreeRefinement_v.2.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v__Refinement_v.13.smt2
anvil/splinterdb-smt-betree__PagedBetree_v.19.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v.10.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__reconciler.7.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__resource__common.2.smt2
anvil/splinterdb-smt-betree__PivotBranchRefinement_v.9.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__resource__role.1.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__proof__lemma_eventually_always_every_resource_update_request_implies_at_after_update_resource_step.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.55.smt2
anvil/splinterdb-smt-journal__LinkedJournalRefinement_v.21.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__proof.2.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.70.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__stateful_set.2.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.57.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__proof.7.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__proof.12.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.42.smt2
anvil/splinterdb-smt-allocation_layer__LikesBetree_v__LikesBetree.8.smt2
anvil/splinterdb-smt-betree__Memtable_v.8.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v.42.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__proof.12.smt2
anvil/splinterdb-smt-allocation_layer__MiniAllocator_v.12.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__daemon_set_match__lemma_daemon_set_state_matches_at_after_update_daemon_set_step.smt2
anvil/splinterdb-smt-betree__FilteredBetree_v.35.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__role_binding.9.smt2
anvil/splinterdb-smt-betree__PivotBetree_v.9.smt2
anvil/splinterdb-smt-allocation_layer__UnifiedCrashAwareJournal_v.15.smt2
anvil/splinterdb-smt-disk__GenericDisk_v.8.smt2
anvil/splinterdb-smt-marshalling__Slice_v.1.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__spec.4.smt2
anvil/splinterdb-smt-journal__PagedJournal_v.6.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__zookeeper_api.16.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.6.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__erlang_cookie.2.smt2
anvil/splinterdb-smt-betree__FilteredBetree_v.19.smt2
anvil/splinterdb-smt-betree__PagedBetree_v.32.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__common.1.smt2
anvil/splinterdb-smt-journal__PagedJournal_v.14.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__proof.5.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.6.smt2
anvil/splinterdb-smt-allocation_layer__MiniAllocator_v.20.smt2
anvil/splinterdb-smt-betree__FilteredBetree_v.32.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__reconciler.8.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.4.smt2
anvil/zookeeper-smt-zookeeper_controller__trusted__spec_types.5.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.59.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__spec.13.smt2
anvil/splinterdb-smt-journal__PagedJournal_v.19.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__resource_match.4.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__trusted__spec_types.2.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__resource_match.1.smt2
anvil/splinterdb-smt-betree__PivotBetree_v.4.smt2
anvil/splinterdb-smt-journal__PagedJournalRefinement_v.19.smt2
anvil/splinterdb-smt-allocation_layer__LikesBetree_v__LikesBetree.5.smt2
anvil/splinterdb-smt-abstract_system__MsgHistory_v.5.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v.28.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.23.smt2
anvil/splinterdb-smt-allocation_layer__AllocationCrashAwareJournalRefinement_v.3.smt2
anvil/splinterdb-smt-allocation_layer__UnifiedCrashAwareJournal_v.14.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__proof.4.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.40.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.112.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__exec__resource__secret.2.smt2
anvil/splinterdb-smt-betree__FilteredBetree_v.41.smt2
anvil/splinterdb-smt-allocation_layer__MiniAllocator_v.17.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__proof__helper_invariants__proof__lemma_resource_create_or_update_request_msg_implies_key_in_reconcile_equals.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__rabbitmq_plugins.5.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.21.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.47.smt2
anvil/splinterdb-smt-betree__FilteredBetreeRefinement_v.32.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v__AllocationJournal.1.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.27.smt2
anvil/splinterdb-smt-betree__FilteredBetreeRefinement_v.9.smt2
anvil/splinterdb-smt-betree__PagedBetreeRefinement_v.25.smt2
anvil/splinterdb-smt-journal__PagedJournal_v.27.smt2
anvil/splinterdb-smt-betree__PagedBetree_v.21.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.72.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__resource_match.1.smt2
anvil/splinterdb-smt-betree__FilteredBetreeRefinement_v.5.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.30.smt2
anvil/splinterdb-smt-exec__MiniAllocator_v.3.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__spec.4.smt2
anvil/splinterdb-smt-allocation_layer__MiniAllocator_v.15.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.43.smt2
anvil/zookeeper-smt-zookeeper_controller__trusted__spec_types.3.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.51.smt2
anvil/splinterdb-smt-journal__PagedJournal_v.15.smt2
anvil/splinterdb-smt-abstract_system__MsgHistory_v.21.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v__LinkedBetreeVars.5.smt2
anvil/splinterdb-smt-betree__PivotBetree_v.22.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof__lemma_eventually_always_object_in_response_at_after_update_resource_step_is_same_as_etcd.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournalRefinement_v.3.smt2
anvil/splinterdb-smt-journal__PagedJournal_v.4.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__helper_invariants__unchangeable.1.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.87.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v.13.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof__lemma_always_no_update_status_request_msg_not_from_bc_in_flight_of_stateful_set.smt2
anvil/splinterdb-smt-betree__PivotBranch_v.30.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.11.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v.14.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v__Refinement_v.29.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v__Refinement_v.23.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.105.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.22.smt2
anvil/splinterdb-smt-abstract_system__MsgHistory_v.14.smt2
anvil/splinterdb-smt-abstract_system__MsgHistory_v.10.smt2
anvil/splinterdb-smt-journal__LinkedJournalRefinement_v.23.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.29.smt2
anvil/splinterdb-smt-journal__PagedJournal_v.20.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__service.6.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.35.smt2
anvil/splinterdb-smt-betree__PivotBranch_v.32.smt2
anvil/splinterdb-smt-abstract_system__AbstractCrashAwareSystemRefinement_v.26.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__config_map.4.smt2
anvil/splinterdb-smt-betree__PagedBetreeRefinement_v.7.smt2
anvil/splinterdb-smt-abstract_system__AbstractCrashAwareSystemRefinement_v.3.smt2
anvil/splinterdb-smt-betree__PivotBetreeRefinement_v.10.smt2
anvil/splinterdb-smt-betree__FilteredBetreeRefinement_v.6.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.5.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__role.7.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__config_map.1.smt2
anvil/splinterdb-smt-betree__Buffer_v.12.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.35.smt2
anvil/splinterdb-smt-journal__PagedJournal_v.13.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.61.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__proof.1.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.62.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.51.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__headless_service.4.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__role_binding.10.smt2
anvil/splinterdb-smt-betree__FilteredBetreeRefinement_v.21.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__reconciler.8.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.90.smt2
anvil/splinterdb-smt-betree__FilteredBetree_v.30.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.10.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__proof.1.smt2
anvil/splinterdb-smt-journal__PagedJournalRefinement_v.1.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__stateful_set.1.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__proof__helper_invariants__owner_ref.2.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__admin_server_service.1.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__resource__service_account.4.smt2
anvil/splinterdb-smt-betree__PivotBranch_v.16.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__stateful_set.8.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__stateful_set_match.2.smt2
anvil/splinterdb-smt-betree__PagedBetree_v.12.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof.2.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v.31.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.86.smt2
anvil/splinterdb-smt-betree__PivotBetree_v.20.smt2
anvil/splinterdb-smt-journal__PagedJournalRefinement_v.11.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__proof.4.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__role.4.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__headless_service.8.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__service_account.6.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v__Refinement_v.35.smt2
anvil/splinterdb-smt-betree__PivotBetree_v.33.smt2
anvil/splinterdb-smt-betree__PagedBetree_v.9.smt2
anvil/splinterdb-smt-journal__PagedJournal_v.16.smt2
anvil/splinterdb-smt-journal__LinkedJournalRefinement_v.5.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__config_map.6.smt2
anvil/splinterdb-smt-allocation_layer__MiniAllocator_v.14.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.29.smt2
anvil/splinterdb-smt-betree__Buffer_v.11.smt2
anvil/splinterdb-smt-abstract_system__MsgHistory_v.26.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__proof.5.smt2
anvil/splinterdb-smt-betree__PagedBetree_v.10.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.16.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.19.smt2
anvil/splinterdb-smt-betree__Utils_v.3.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__common.4.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof__lemma_eventually_always_every_resource_update_request_implies_at_after_update_resource_step.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__reconciler.12.smt2
anvil/splinterdb-smt-abstract_system__MsgHistory_v.18.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.9.smt2
anvil/splinterdb-smt-betree__BufferOffsets_v.4.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__resource_match.4.smt2
anvil/splinterdb-smt-journal__LinkedJournalRefinement_v.29.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__proof__helper_invariants__proof__lemma_always_response_at_after_get_resource_step_is_resource_get_response.smt2
anvil/splinterdb-smt-allocation_layer__LikesBetree_v.9.smt2
anvil/splinterdb-smt-betree__FilteredBetreeRefinement_v.20.smt2
anvil/splinterdb-smt-exec__MiniAllocator_v.11.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournalRefinement_v.3.smt2
anvil/splinterdb-smt-allocation_layer__UnifiedCrashAwareJournal_v.12.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__config_map.5.smt2
anvil/splinterdb-smt-journal__PagedJournal_v.2.smt2
anvil/splinterdb-smt-marshalling__Slice_v.5.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.18.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__reconciler.1.smt2
anvil/splinterdb-smt-betree__BufferSeq_v.12.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__resource__service.6.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__client_service.1.smt2
anvil/splinterdb-smt-betree__PivotBranchRefinement_v.4.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__client_service.8.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.50.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.30.smt2
anvil/splinterdb-smt-abstract_system__AbstractCrashAwareSystemRefinement_v.13.smt2
anvil/splinterdb-smt-betree__PagedBetree_v.7.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof.9.smt2
anvil/splinterdb-smt-betree__PivotBetree_v.27.smt2
anvil/splinterdb-smt-betree__PagedBetree_v.2.smt2
anvil/splinterdb-smt-abstract_system__AbstractJournal_v__AbstractJournal.2.smt2
anvil/splinterdb-smt-betree__FilteredBetreeRefinement_v.8.smt2
anvil/splinterdb-smt-betree__PivotBranch_v.25.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__reconciler.6.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.31.smt2
anvil/splinterdb-smt-abstract_system__AbstractCrashAwareSystemRefinement_v.29.smt2
anvil/splinterdb-smt-allocation_layer__LikesBetree_v.19.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__proof__helper_invariants__proof__lemma_always_no_update_status_request_msg_in_flight.smt2
anvil/splinterdb-smt-betree__PivotBetree_v.8.smt2
anvil/splinterdb-smt-betree__PagedBetree_v.26.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v__LikesJournal.3.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v__Refinement_v.21.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof.7.smt2
anvil/splinterdb-smt-betree__BufferOffsets_v.7.smt2
anvil/splinterdb-smt-allocation_layer__LikesBetree_v.15.smt2
anvil/splinterdb-smt-abstract_system__AbstractCrashAwareSystemRefinement_v.25.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.52.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__spec.2.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.20.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.100.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.20.smt2
anvil/splinterdb-smt-betree__FilteredBetreeRefinement_v.29.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.32.smt2
anvil/splinterdb-smt-abstract_system__MsgHistory_v.27.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__client_service.7.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof__lemma_eventually_always_no_delete_resource_request_msg_in_flight.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__spec.10.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__config_map.8.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__zookeeper_api__lemma_eventually_always_every_zk_create_node_request_implies_at_after_create_zk_node_step.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__service.2.smt2
anvil/splinterdb-smt-betree__Domain_v.5.smt2
anvil/splinterdb-smt-betree__PivotBranch_v.21.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournalRefinement_v.5.smt2
anvil/splinterdb-smt-betree__FilteredBetreeRefinement_v.33.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.3.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__helper_invariants__proof__make_fluentbit_pod_spec_determined_by_spec_and_name.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.34.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__reconciler.3.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v__LikesJournal.4.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__erlang_cookie.5.smt2
anvil/splinterdb-smt-betree__PivotBetree_v.26.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v.16.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v.18.smt2
anvil/splinterdb-smt-abstract_system__StampedMap_v.3.smt2
anvil/splinterdb-smt-betree__FilteredBetree_v.38.smt2
anvil/splinterdb-smt-betree__PagedBetreeRefinement_v.1.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.8.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.9.smt2
anvil/splinterdb-smt-spec__AppIO_t.1.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__unchangeable.3.smt2
anvil/splinterdb-smt-betree__Buffer_v.14.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.1.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v.2.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__zookeeper_api__lemma_zk_request_implies_step_helper.smt2
anvil/splinterdb-smt-journal__PagedJournal_v.21.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__proof__lemma_always_cm_rv_stays_unchanged.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.19.smt2
anvil/splinterdb-smt-betree__PivotBranchRefinement_v.17.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__resource__daemon_set.4.smt2
anvil/splinterdb-smt-betree__PivotBranch_v.5.smt2
anvil/splinterdb-smt-betree__PivotBranch_v.7.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__trusted__spec_types.3.smt2
anvil/splinterdb-smt-journal__LinkedJournalRefinement_v.9.smt2
anvil/splinterdb-smt-betree__FilteredBetree_v.6.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__role.2.smt2
anvil/splinterdb-smt-allocation_layer__LikesBetree_v.1.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.25.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__resource__service_account.8.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.39.smt2
anvil/splinterdb-smt-betree__SplitRequest_v.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__resource__role.5.smt2
anvil/splinterdb-smt-betree__BufferOffsets_v.2.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__spec.3.smt2
anvil/splinterdb-smt-abstract_system__MsgHistory_v.11.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournalRefinement_v.6.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.44.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.62.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v__AllocationJournal.12.smt2
anvil/splinterdb-smt-journal__PagedJournalRefinement_v.9.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__spec.10.smt2
anvil/splinterdb-smt-abstract_system__AbstractCrashAwareSystemRefinement_v.15.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__config_map.1.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v.9.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__resource_match.9.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.38.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__config_map.8.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__reconciler.9.smt2
anvil/splinterdb-smt-allocation_layer__AllocationCrashAwareJournal_v__AllocationCrashAwareJournal.7.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__headless_service.6.smt2
anvil/splinterdb-smt-betree__BufferSeq_v.9.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__terminate.1.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__helper_invariants__unchangeable.4.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v.44.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__reconciler.5.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v__LinkedJournal.11.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__proof.9.smt2
anvil/splinterdb-smt-betree__LinkedSeq_v.7.smt2
anvil/zookeeper-smt-zookeeper_controller__trusted__spec_types.6.smt2
anvil/splinterdb-smt-journal__PagedJournal_v.12.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v__AllocationJournal.16.smt2
anvil/splinterdb-smt-allocation_layer__LikesBetree_v.17.smt2
anvil/splinterdb-smt-betree__PagedBetreeRefinement_v.10.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v.22.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.47.smt2
anvil/splinterdb-smt-betree__Buffer_v.2.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__exec__reconciler.7.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__stateful_set_match.1.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.108.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v__LinkedJournal.2.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.49.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__helper_invariants__proof__lemma_always_no_update_status_request_msg_not_from_bc_in_flight_of_daemon_set.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__resource_match.7.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__reconciler.16.smt2
anvil/splinterdb-smt-journal__PagedJournalRefinement_v.16.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__zookeeper_api.1.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v__Refinement_v.34.smt2
anvil/splinterdb-smt-journal__LinkedJournalRefinement_v.27.smt2
anvil/splinterdb-smt-betree__PagedBetree_v.31.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__trusted__spec_types.4.smt2
anvil/splinterdb-smt-betree__PivotBetree_v.17.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__validation__lemma_always_object_in_resource_update_request_msg_has_smaller_rv_than_etcd.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__proof__lemma_resource_update_request_msg_implies_key_in_reconcile_equals.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__spec.1.smt2
anvil/splinterdb-smt-betree__PivotBranch_v.1.smt2
anvil/splinterdb-smt-betree__PagedBetreeRefinement_v.20.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__unchangeable.3.smt2
anvil/zookeeper-smt-zookeeper_controller__trusted__spec_types.1.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v__LinkedBetreeVars.6.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__spec.15.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__resource_match.6.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__default_user_secret.7.smt2
anvil/splinterdb-smt-betree__BufferSeq_v.5.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__headless_service.5.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__terminate.1.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__rabbitmq_plugins.2.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.15.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v__Refinement_v.1.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.31.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof__lemma_always_no_update_status_request_msg_in_flight_of_except_stateful_set.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v.29.smt2
anvil/splinterdb-smt-betree__PivotBetreeRefinement_v.23.smt2
anvil/splinterdb-smt-betree__PivotTable_v.8.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v.6.smt2
anvil/splinterdb-smt-betree__FilteredBetree_v.34.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__resource__service_account.5.smt2
anvil/splinterdb-smt-betree__FilteredBetree_v.20.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__proof.9.smt2
anvil/splinterdb-smt-betree__PivotBetreeRefinement_v.28.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.39.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__rabbitmq_plugins.7.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__rabbitmq_plugins.8.smt2
anvil/splinterdb-smt-betree__PivotBetree_v.1.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__role_binding.6.smt2
anvil/splinterdb-smt-journal__PagedJournalRefinement_v.15.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__client_service.6.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__config_map.4.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.65.smt2
anvil/splinterdb-smt-journal__PagedJournalRefinement_v.25.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.51.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__resource__service.8.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__spec.1.smt2
anvil/splinterdb-smt-allocation_layer__AllocationCrashAwareJournal_v__AllocationCrashAwareJournal.6.smt2
anvil/splinterdb-smt-allocation_layer__UnifiedCrashAwareJournal_v__UnifiedCrashAwareJournal.3.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.75.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.54.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v__LikesJournal.2.smt2
anvil/splinterdb-smt-betree__FilteredBetree_v.37.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__default_user_secret.4.smt2
anvil/splinterdb-smt-journal__PagedJournalRefinement_v.22.smt2
anvil/splinterdb-smt-betree__PivotBetree_v.34.smt2
anvil/splinterdb-smt-exec__MiniAllocator_v.1.smt2
anvil/splinterdb-smt-betree__BufferOffsets_v.5.smt2
anvil/splinterdb-smt-betree__LinkedSeq_v.6.smt2
anvil/splinterdb-smt-betree__PivotBranchRefinement_v.7.smt2
anvil/splinterdb-smt-marshalling__IntegerMarshalling_v.3.smt2
anvil/splinterdb-smt-journal__LinkedJournalRefinement_v.2.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.21.smt2
anvil/splinterdb-smt-allocation_layer__AllocationJournal_v.46.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__reconciler.19.smt2
anvil/splinterdb-smt-exec__Cache_v__Cache.4.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__resource_match.5.smt2
anvil/splinterdb-smt-betree__PivotBetree_v.31.smt2
anvil/splinterdb-smt-betree__PivotBranch_v.31.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.24.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.35.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__terminate.1.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.40.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__proof.6.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__proof.6.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.40.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__resource_match.1.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__terminate.2.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v.8.smt2
anvil/splinterdb-smt-betree__PivotBetreeRefinement_v.25.smt2
anvil/splinterdb-smt-betree__FilteredBetreeRefinement_v.14.smt2
anvil/splinterdb-smt-betree__LinkedSeq_v.4.smt2
anvil/splinterdb-smt-allocation_layer__LikesBetree_v.14.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__proof.10.smt2
anvil/splinterdb-smt-betree__PagedBetree_v.20.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__proof.11.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v.5.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__headless_service.2.smt2
anvil/splinterdb-smt-betree__PagedBetreeRefinement_v.21.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v__Refinement_v.24.smt2
anvil/splinterdb-smt-betree__PagedBetreeRefinement_v.6.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__proof.9.smt2
anvil/splinterdb-smt-journal__LinkedJournalRefinement_v.19.smt2
anvil/splinterdb-smt-betree__FilteredBetree_v.9.smt2
anvil/splinterdb-smt-betree__PivotBetree_v.36.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__erlang_cookie.1.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__daemon_set_match__lemma_from_after_get_daemon_set_step_to_after_update_daemon_set_step.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__resource__daemon_set.6.smt2
anvil/splinterdb-smt-abstract_system__MsgHistory_v.8.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v.27.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__reconciler.9.smt2
anvil/splinterdb-smt-betree__PagedBetreeRefinement_v.29.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__resource_match.8.smt2
anvil/splinterdb-smt-betree__Buffer_v.10.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v.15.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__resource__service_account.1.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__resource_match__lemma_from_after_get_resource_step_to_after_create_resource_step.smt2
anvil/splinterdb-smt-journal__PagedJournalRefinement_v.2.smt2
anvil/splinterdb-smt-journal__PagedJournal_v.18.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.76.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__spec.5.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.8.smt2
anvil/splinterdb-smt-betree__PivotBetreeRefinement_v.29.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__exec__reconciler.3.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.16.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v__LinkedBetreeVars.2.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__proof__helper_invariants__proof__lemma_always_resource_object_create_or_update_request_msg_has_one_controller_ref_and_no_finalizers.smt2
anvil/splinterdb-smt-allocation_layer__LikesJournal_v.16.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v__Refinement_v.22.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__proof.9.smt2
anvil/splinterdb-smt-journal__LinkedJournalRefinement_v.16.smt2
anvil/splinterdb-smt-allocation_layer__AllocationCrashAwareJournal_v__AllocationCrashAwareJournal.11.smt2
anvil/fluent-smt-fluent_controller__fluentbit__exec__reconciler.3.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.5.smt2
anvil/splinterdb-smt-betree__PagedBetree_v.16.smt2
anvil/splinterdb-smt-betree__LinkedBetree_v.83.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v__Refinement_v.37.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__config_map.2.smt2
anvil/splinterdb-smt-allocation_layer__UnifiedCrashAwareJournal_v.11.smt2
anvil/splinterdb-smt-abstract_system__AbstractCrashAwareSystemRefinement_v.11.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v.13.smt2
anvil/splinterdb-smt-journal__LinkedJournal_v.37.smt2
anvil/splinterdb-smt-betree__LinkedBranch_v__Refinement_v.9.smt2
atmosphere/define.5.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__liveness__resource_match.7.smt2
anvil/zookeeper-smt-zookeeper_controller__exec__resource__config_map.7.smt2
atmosphere/pagetable__entry.4.smt2
anvil/splinterdb-smt-allocation_layer__UnifiedCrashAwareJournal_v__UnifiedCrashAwareJournal.4.smt2
atmosphere/array_set.7.smt2
atmosphere/trap.6.smt2
atmosphere/define.3.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__proof.7.smt2
atmosphere/array_vec.6.smt2
atmosphere/pagetable__entry.1.smt2
atmosphere/process_manager__container_tree_spec_impl.7.smt2
atmosphere/process_manager__thread.3.smt2
atmosphere/array_vec.2.smt2
atmosphere/process_manager__thread.2.smt2
atmosphere/process_manager__container_tree_spec_impl.12.smt2
atmosphere/slinkedlist__spec_impl_u.1.smt2
atmosphere/pagetable__pagemap_util_t.1.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__liveness__stateful_set_match.5.smt2
atmosphere/pagetable__entry.8.smt2
atmosphere/trap.1.smt2
atmosphere/process_manager__container_tree_spec_impl.6.smt2
atmosphere/trap.9.smt2
atmosphere/process_manager__container_tree_spec_impl.10.smt2
atmosphere/pagetable__pagemap.4.smt2
atmosphere/array.5.smt2
atmosphere/process_manager__endpoint_util_t.smt2
atmosphere/array.7.smt2
anvil/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof.14.smt2
atmosphere/trap.2.smt2
atmosphere/array.2.smt2
atmosphere/process_manager__container_tree_spec_impl.4.smt2
atmosphere/define.1.smt2
anvil/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__proof.13.smt2
atmosphere/slinkedlist__spec_impl_u.6.smt2
atmosphere/array_set.3.smt2
atmosphere/array_set.4.smt2
atmosphere/process_manager__container_tree_spec_impl.14.smt2
atmosphere/pagetable__pagemap.5.smt2
anvil/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__spec.2.smt2
splinterdb/exec__MiniAllocator_v.11.smt2
atmosphere/process_manager__container_tree_spec_impl.16.smt2
splinterdb/allocation_layer__AllocationJournal_v.2.smt2
anvil/splinterdb-smt-betree__Utils_v.1.smt2
splinterdb/betree__LinkedBranch_v.10.smt2
splinterdb/betree__FilteredBetree_v.7.smt2
splinterdb/allocation_layer__LikesJournal_v__LikesJournal.1.smt2
splinterdb/betree__BufferSeq_v.7.smt2
splinterdb/betree__LinkedBetree_v.21.smt2
splinterdb/betree__FilteredBetreeRefinement_v.11.smt2
splinterdb/journal__LinkedJournal_v.55.smt2
splinterdb/journal__LinkedJournal_v.49.smt2
anvil/fluent-smt-fluent_controller__fluentbit__proof__helper_invariants__proof__lemma_eventually_always_every_resource_update_request_implies_at_after_update_resource_step.smt2
splinterdb/betree__PivotBranchRefinement_v.9.smt2
splinterdb/betree__Buffer_v.9.smt2
splinterdb/betree__Utils_v.5.smt2
splinterdb/betree__PivotBetreeRefinement_v.7.smt2
splinterdb/allocation_layer__LikesJournal_v.21.smt2
splinterdb/allocation_layer__UnifiedCrashAwareJournal_v.3.smt2
splinterdb/betree__PagedBetree_v.19.smt2
splinterdb/betree__Buffer_v.3.smt2
splinterdb/betree__OffsetMap_v.2.smt2
splinterdb/betree__FilteredBetree_v.2.smt2
splinterdb/betree__Domain_v.4.smt2
splinterdb/allocation_layer__AllocationJournalRefinement_v.3.smt2
splinterdb/allocation_layer__MiniAllocator_v.20.smt2
splinterdb/abstract_system__MsgHistory_v.2.smt2
splinterdb/abstract_system__MsgHistory_v.5.smt2
splinterdb/betree__BufferSeq_v.5.smt2
splinterdb/abstract_system__AbstractCrashAwareSystemRefinement_v.13.smt2
splinterdb/allocation_layer__LikesJournal_v__LikesJournal.2.smt2
splinterdb/betree__BufferDisk_v.14.smt2
splinterdb/allocation_layer__AllocationJournal_v.41.smt2
splinterdb/allocation_layer__LikesBetree_v__LikesBetree.5.smt2
splinterdb/betree__BufferSeq_v.1.smt2
splinterdb/allocation_layer__LikesBetree_v__LikesBetree.2.smt2
splinterdb/betree__PagedBetreeRefinement_v.30.smt2
splinterdb/betree__PagedBetreeRefinement_v.35.smt2
splinterdb/journal__PagedJournalRefinement_v.25.smt2
splinterdb/marshalling__IntegerMarshalling_v.26.smt2
splinterdb/betree__LinkedBetree_v__LinkedBetreeVars.3.smt2
splinterdb/betree__LinkedSeq_v.3.smt2
splinterdb/betree__LinkedBetree_v.19.smt2
splinterdb/betree__PivotBetree_v.16.smt2
splinterdb/allocation_layer__AllocationCrashAwareJournalRefinement_v.1.smt2
splinterdb/abstract_system__AbstractJournal_v__AbstractJournal.2.smt2
splinterdb/betree__FilteredBetree_v.3.smt2
splinterdb/allocation_layer__AllocationJournal_v.34.smt2
splinterdb/allocation_layer__AllocationJournal_v.36.smt2
splinterdb/allocation_layer__AllocationJournal_v__AllocationJournal.6.smt2
splinterdb/allocation_layer__MiniAllocator_v.5.smt2
splinterdb/betree__PagedBetree_v.10.smt2
splinterdb/betree__FilteredBetree_v.30.smt2
splinterdb/abstract_system__AbstractCrashAwareSystemRefinement_v.15.smt2
splinterdb/betree__LinkedBranch_v.23.smt2
splinterdb/betree__LinkedBetree_v.38.smt2
splinterdb/marshalling__IntegerMarshalling_v.3.smt2
splinterdb/betree__PivotBranchRefinement_v.22.smt2
splinterdb/exec__MiniAllocator_v.12.smt2
splinterdb/betree__LinkedBranch_v__Refinement_v.34.smt2
splinterdb/betree__Buffer_v.7.smt2
splinterdb/betree__FilteredBetree_v.1.smt2
splinterdb/betree__LinkedBranch_v.67.smt2
splinterdb/betree__LinkedBetree_v.56.smt2
splinterdb/allocation_layer__LikesJournal_v__LikesJournal.8.smt2
splinterdb/betree__LinkedBetree_v.20.smt2
splinterdb/abstract_system__AbstractCrashAwareSystemRefinement_v.23.smt2
splinterdb/allocation_layer__AllocationJournal_v.43.smt2
splinterdb/betree__LinkedBetree_v.59.smt2
splinterdb/betree__LinkedBranch_v.58.smt2
splinterdb/allocation_layer__AllocationCrashAwareJournalRefinement_v.4.smt2
splinterdb/allocation_layer__AllocationJournal_v.42.smt2
splinterdb/journal__LinkedJournal_v__LinkedJournal.4.smt2
splinterdb/journal__PagedJournalRefinement_v.7.smt2
splinterdb/journal__LinkedJournalRefinement_v.30.smt2
splinterdb/abstract_system__MsgHistory_v.4.smt2
splinterdb/betree__LinkedBetree_v.86.smt2
splinterdb/abstract_system__MsgHistory_v.9.smt2
splinterdb/allocation_layer__LikesJournal_v.24.smt2
splinterdb/betree__LinkedBetree_v.1.smt2
splinterdb/journal__PagedJournal_v.15.smt2
splinterdb/betree__PivotBetree_v.42.smt2
splinterdb/allocation_layer__LikesBetree_v__LikesBetree.4.smt2
splinterdb/betree__PagedBetree_v.7.smt2
splinterdb/journal__PagedJournal_v.32.smt2
splinterdb/betree__Buffer_v.15.smt2
splinterdb/betree__LinkedBranch_v.50.smt2
splinterdb/abstract_system__AbstractCrashAwareSystemRefinement_v.4.smt2
splinterdb/journal__LinkedJournal_v.48.smt2
splinterdb/betree__PivotBetreeRefinement_v.9.smt2
splinterdb/marshalling__IntegerMarshalling_v.8.smt2
splinterdb/journal__LinkedJournal_v.7.smt2
splinterdb/betree__PivotBetree_v.38.smt2
splinterdb/betree__PivotBetreeRefinement_v.28.smt2
splinterdb/betree__PivotBranch_v.1.smt2
splinterdb/abstract_system__AbstractJournal_v__AbstractJournal.1.smt2
splinterdb/journal__LinkedJournal_v.11.smt2
splinterdb/betree__LinkedBranch_v.9.smt2
splinterdb/betree__LinkedBranch_v.14.smt2
splinterdb/allocation_layer__AllocationJournal_v.21.smt2
splinterdb/allocation_layer__LikesJournal_v.17.smt2
splinterdb/betree__PivotBranch_v.12.smt2
splinterdb/betree__FilteredBetree_v.37.smt2
splinterdb/journal__PagedJournal_v.8.smt2
splinterdb/betree__PivotBranchRefinement_v.8.smt2
splinterdb/betree__LinkedBetree_v.81.smt2
splinterdb/betree__PagedBetree_v.13.smt2
splinterdb/allocation_layer__UnifiedCrashAwareJournal_v.10.smt2
splinterdb/betree__LinkedBetree_v.6.smt2
splinterdb/betree__LinkedBetree_v.109.smt2
splinterdb/betree__LinkedBranch_v.3.smt2
splinterdb/betree__LinkedBetree_v.15.smt2
splinterdb/betree__FilteredBetree_v.41.smt2
splinterdb/betree__FilteredBetreeRefinement_v.19.smt2
splinterdb/journal__LinkedJournal_v.2.smt2
splinterdb/betree__LinkedBranch_v.32.smt2
splinterdb/betree__FilteredBetreeRefinement_v.9.smt2
splinterdb/journal__LinkedJournal_v.25.smt2
splinterdb/betree__LinkedBetree_v.85.smt2
splinterdb/betree__PivotBetree_v.43.smt2
splinterdb/betree__PagedBetree_v.23.smt2
splinterdb/betree__LinkedBetree_v.89.smt2
splinterdb/betree__PivotBranchRefinement_v.16.smt2
splinterdb/marshalling__IntegerMarshalling_v.25.smt2
splinterdb/exec__Cache_v__Cache.6.smt2
splinterdb/betree__PivotTable_v.9.smt2
splinterdb/betree__BufferDisk_v.12.smt2
splinterdb/allocation_layer__LikesJournal_v.30.smt2
splinterdb/betree__BufferDisk_v.7.smt2
splinterdb/betree__LinkedBranch_v__Refinement_v.2.smt2
splinterdb/betree__LinkedBranch_v.44.smt2
splinterdb/allocation_layer__LikesJournal_v.12.smt2
splinterdb/allocation_layer__LikesJournalRefinement_v.3.smt2
splinterdb/betree__Memtable_v.12.smt2
splinterdb/betree__LinkedBetree_v.42.smt2
splinterdb/betree__FilteredBetree_v.13.smt2
splinterdb/allocation_layer__MiniAllocator_v.11.smt2
splinterdb/abstract_system__AbstractCrashAwareSystemRefinement_v.3.smt2
splinterdb/allocation_layer__MiniAllocator_v.9.smt2
splinterdb/abstract_system__AbstractCrashAwareSystemRefinement_v.8.smt2
splinterdb/journal__PagedJournal_v.12.smt2
splinterdb/betree__PivotBetreeRefinement_v.18.smt2
splinterdb/disk__GenericDisk_v.5.smt2
splinterdb/betree__LinkedBranch_v__Refinement_v.31.smt2
splinterdb/betree__LinkedBetree_v__LinkedBetreeVars.7.smt2
splinterdb/betree__LinkedBranch_v.2.smt2
splinterdb/allocation_layer__MiniAllocator_v.21.smt2
splinterdb/allocation_layer__AllocationCrashAwareJournal_v__AllocationCrashAwareJournal.2.smt2
splinterdb/allocation_layer__AllocationCrashAwareJournal_v.1.smt2
splinterdb/allocation_layer__UnifiedCrashAwareJournalRefinement_v.7.smt2
splinterdb/betree__BufferDisk_v.4.smt2
splinterdb/allocation_layer__AllocationJournal_v.23.smt2
splinterdb/abstract_system__AbstractCrashAwareSystemRefinement_v.22.smt2
splinterdb/betree__Memtable_v.7.smt2
splinterdb/allocation_layer__AllocationJournal_v.26.smt2
splinterdb/betree__Buffer_v.4.smt2
splinterdb/betree__LinkedBetree_v.93.smt2
splinterdb/marshalling__IntegerMarshalling_v.15.smt2
splinterdb/exec__Cache_v__Cache.5.smt2
splinterdb/marshalling__IntegerMarshalling_v.29.smt2
splinterdb/journal__LinkedJournalRefinement_v.18.smt2
splinterdb/betree__PivotBetree_v.32.smt2
splinterdb/journal__LinkedJournal_v.8.smt2
splinterdb/betree__LinkedBetree_v.82.smt2
splinterdb/betree__PagedBetree_v.22.smt2
splinterdb/betree__LinkedBranch_v__Refinement_v.18.smt2
splinterdb/abstract_system__MsgHistory_v.29.smt2
splinterdb/abstract_system__MsgHistory_v.16.smt2
splinterdb/betree__LinkedBranch_v__Refinement_v.22.smt2
splinterdb/allocation_layer__UnifiedCrashAwareJournal_v.14.smt2
splinterdb/betree__BufferOffsets_v.5.smt2
splinterdb/betree__FilteredBetree_v.32.smt2
splinterdb/abstract_system__MsgHistory_v.21.smt2
splinterdb/betree__BufferOffsets_v.6.smt2
splinterdb/marshalling__SeqMarshalling_v.3.smt2
splinterdb/betree__LinkedBranch_v__Refinement_v.14.smt2
splinterdb/betree__FilteredBetree_v.17.smt2
splinterdb/betree__PagedBetree_v.12.smt2
splinterdb/betree__FilteredBetreeRefinement_v.21.smt2
splinterdb/allocation_layer__LikesBetree_v__LikesBetree.7.smt2
splinterdb/betree__PagedBetreeRefinement_v.12.smt2
splinterdb/betree__LinkedBetree_v.43.smt2
splinterdb/journal__LinkedJournal_v.27.smt2
splinterdb/allocation_layer__AllocationJournal_v.47.smt2
splinterdb/allocation_layer__AllocationJournal_v.27.smt2
splinterdb/abstract_system__AbstractCrashAwareSystemRefinement_v.19.smt2
splinterdb/betree__PagedBetreeRefinement_v.25.smt2
splinterdb/journal__LinkedJournalRefinement_v.17.smt2
splinterdb/journal__LinkedJournal_v.47.smt2
splinterdb/betree__PivotBranchRefinement_v.18.smt2
splinterdb/exec__Cache_v__Cache.1.smt2
splinterdb/betree__LinkedBetree_v.96.smt2
splinterdb/betree__Domain_v.5.smt2
splinterdb/allocation_layer__AllocationCrashAwareJournal_v__AllocationCrashAwareJournal.6.smt2
splinterdb/betree__Buffer_v.13.smt2
splinterdb/betree__LinkedBranch_v.39.smt2
splinterdb/betree__PivotBetree_v.29.smt2
splinterdb/betree__LinkedBetree_v.40.smt2
splinterdb/betree__LinkedBranch_v.16.smt2
splinterdb/betree__BufferSeq_v.16.smt2
splinterdb/allocation_layer__LikesBetree_v.14.smt2
splinterdb/betree__PagedBetreeRefinement_v.3.smt2
splinterdb/abstract_system__StampedMap_v.3.smt2
splinterdb/betree__BufferSeq_v.21.smt2
splinterdb/betree__Buffer_v.10.smt2
splinterdb/journal__LinkedJournal_v.1.smt2
splinterdb/betree__LinkedBetree_v.17.smt2
splinterdb/journal__PagedJournal_v.1.smt2
splinterdb/betree__LinkedBetree_v.83.smt2
splinterdb/betree__BufferOffsets_v.3.smt2
splinterdb/allocation_layer__UnifiedCrashAwareJournalRefinement_v.3.smt2
splinterdb/allocation_layer__LikesBetree_v__LikesBetree.6.smt2
splinterdb/exec__Cache_v__Cache.10.smt2
splinterdb/journal__LinkedJournalRefinement_v.16.smt2
splinterdb/journal__LinkedJournalRefinement_v.8.smt2
splinterdb/betree__PivotBranch_v.11.smt2
splinterdb/betree__LinkedBetree_v.94.smt2
splinterdb/betree__FilteredBetree_v.23.smt2
splinterdb/allocation_layer__AllocationJournal_v.33.smt2
splinterdb/allocation_layer__AllocationJournal_v.38.smt2
splinterdb/allocation_layer__AllocationJournal_v.22.smt2
splinterdb/betree__FilteredBetree_v.29.smt2
splinterdb/allocation_layer__LikesJournal_v.8.smt2
splinterdb/allocation_layer__LikesJournal_v.27.smt2
splinterdb/allocation_layer__AllocationJournal_v__AllocationJournal.7.smt2
splinterdb/betree__FilteredBetree_v.15.smt2
splinterdb/allocation_layer__AllocationCrashAwareJournal_v__AllocationCrashAwareJournal.3.smt2
splinterdb/abstract_system__AbstractCrashAwareSystemRefinement_v.11.smt2
splinterdb/journal__PagedJournal_v.33.smt2
splinterdb/betree__PivotBetreeRefinement_v.12.smt2
splinterdb/betree__LinkedBranch_v__Refinement_v.32.smt2
splinterdb/betree__PivotBetree_v.33.smt2
splinterdb/journal__LinkedJournal_v.24.smt2
splinterdb/betree__OffsetMap_v.4.smt2
splinterdb/journal__PagedJournal_v.31.smt2
splinterdb/betree__LinkedBetree_v.33.smt2
splinterdb/allocation_layer__AllocationJournal_v.14.smt2
splinterdb/abstract_system__MsgHistory_v.13.smt2
splinterdb/allocation_layer__MiniAllocator_v.16.smt2
splinterdb/allocation_layer__LikesJournal_v__LikesJournal.10.smt2
splinterdb/betree__LinkedBranch_v.28.smt2
splinterdb/betree__LinkedBranch_v.38.smt2
splinterdb/abstract_system__StampedMap_v.4.smt2
splinterdb/betree__PivotBetree_v.24.smt2
splinterdb/betree__PivotBetree_v.14.smt2
splinterdb/journal__PagedJournal_v.27.smt2
splinterdb/betree__LinkedBranch_v.29.smt2
splinterdb/betree__BufferSeq_v.12.smt2
splinterdb/betree__LinkedBranch_v__Refinement_v.3.smt2
splinterdb/allocation_layer__UnifiedCrashAwareJournalRefinement_v.8.smt2
splinterdb/journal__LinkedJournal_v.42.smt2
splinterdb/journal__PagedJournalRefinement_v.22.smt2
splinterdb/abstract_system__MsgHistory_v.10.smt2
splinterdb/betree__PivotBetreeRefinement_v.10.smt2
splinterdb/marshalling__IntegerMarshalling_v.55.smt2
splinterdb/spec__AppIO_t.3.smt2
splinterdb/marshalling__IntegerMarshalling_v.6.smt2
splinterdb/journal__PagedJournal_v.28.smt2
splinterdb/betree__LinkedBetree_v.25.smt2
splinterdb/betree__FilteredBetree_v.19.smt2
splinterdb/betree__FilteredBetreeRefinement_v.25.smt2
splinterdb/allocation_layer__LikesJournalRefinement_v.2.smt2
splinterdb/betree__Buffer_v.16.smt2
splinterdb/allocation_layer__AllocationCrashAwareJournal_v__AllocationCrashAwareJournal.9.smt2
splinterdb/journal__LinkedJournal_v.12.smt2
splinterdb/abstract_system__AbstractCrashAwareSystemRefinement_v.21.smt2
splinterdb/betree__PagedBetreeRefinement_v.17.smt2
splinterdb/journal__PagedJournalRefinement_v.2.smt2
splinterdb/allocation_layer__AllocationJournal_v.20.smt2
splinterdb/journal__PagedJournalRefinement_v.19.smt2
splinterdb/betree__PivotBranch_v.30.smt2
splinterdb/betree__PivotBranch_v.26.smt2
splinterdb/betree__LinkedBetree_v.75.smt2
splinterdb/allocation_layer__AllocationJournal_v.3.smt2
splinterdb/betree__LinkedBranch_v.27.smt2
splinterdb/allocation_layer__LikesBetree_v.13.smt2
splinterdb/betree__LinkedBetree_v.41.smt2
splinterdb/betree__FilteredBetree_v.22.smt2
splinterdb/betree__FilteredBetreeRefinement_v.15.smt2
splinterdb/abstract_system__AbstractCrashAwareSystemRefinement_v.17.smt2
splinterdb/exec__Cache_v__Cache.9.smt2
splinterdb/journal__LinkedJournalRefinement_v.24.smt2
splinterdb/journal__LinkedJournalRefinement_v.12.smt2
splinterdb/journal__PagedJournalRefinement_v.18.smt2
splinterdb/betree__PivotBetreeRefinement_v.2.smt2
splinterdb/marshalling__IntegerMarshalling_v.23.smt2
splinterdb/betree__PagedBetree_v.18.smt2
splinterdb/allocation_layer__LikesBetree_v.6.smt2
splinterdb/allocation_layer__AllocationJournal_v.12.smt2
splinterdb/abstract_system__MsgHistory_v.20.smt2
splinterdb/abstract_system__MsgHistory_v.25.smt2
splinterdb/betree__FilteredBetreeRefinement_v.6.smt2
splinterdb/journal__PagedJournal_v.3.smt2
splinterdb/betree__FilteredBetree_v__FilteredBetree.smt2
splinterdb/betree__LinkedBetree_v.67.smt2
splinterdb/betree__PivotBranchRefinement_v.10.smt2
splinterdb/journal__LinkedJournalRefinement_v.2.smt2
splinterdb/marshalling__IntegerMarshalling_v.32.smt2
splinterdb/betree__LinkedBetree_v__LinkedBetreeVars.6.smt2
splinterdb/betree__PivotBetree_v.40.smt2
splinterdb/abstract_system__MsgHistory_v.22.smt2
splinterdb/betree__LinkedBetree_v.76.smt2
splinterdb/allocation_layer__LikesJournal_v.7.smt2
splinterdb/allocation_layer__AllocationJournal_v__AllocationJournal.11.smt2
splinterdb/marshalling__SeqMarshalling_v.1.smt2
splinterdb/journal__PagedJournal_v.2.smt2
splinterdb/allocation_layer__AllocationJournal_v__AllocationJournal.8.smt2
splinterdb/allocation_layer__AllocationJournal_v.10.smt2
splinterdb/marshalling__IntegerMarshalling_v.21.smt2
splinterdb/allocation_layer__AllocationJournal_v__AllocationJournal.4.smt2
splinterdb/allocation_layer__AllocationJournal_v.18.smt2
splinterdb/betree__LinkedBetree_v.105.smt2
splinterdb/journal__LinkedJournal_v.10.smt2
splinterdb/betree__LinkedBetree_v.68.smt2
splinterdb/betree__LinkedBetree_v.111.smt2
splinterdb/marshalling__IntegerMarshalling_v.40.smt2
splinterdb/betree__LinkedBetree_v.44.smt2
splinterdb/disk__GenericDisk_v.6.smt2
splinterdb/betree__FilteredBetree_v.9.smt2
splinterdb/allocation_layer__LikesJournal_v.18.smt2
splinterdb/disk__GenericDisk_v.10.smt2
splinterdb/marshalling__IntegerMarshalling_v.41.smt2
splinterdb/abstract_system__AbstractCrashAwareSystemRefinement_v.6.smt2
splinterdb/betree__PivotBetreeRefinement_v.4.smt2
splinterdb/betree__PivotBetreeRefinement_v.17.smt2
splinterdb/journal__PagedJournalRefinement_v.21.smt2
splinterdb/marshalling__IntegerMarshalling_v.53.smt2
splinterdb/betree__PivotBetree_v.12.smt2
splinterdb/journal__LinkedJournal_v.37.smt2
splinterdb/betree__LinkedBetree_v__LinkedBetreeVars.2.smt2
splinterdb/journal__LinkedJournal_v.19.smt2
splinterdb/allocation_layer__LikesBetree_v.12.smt2
splinterdb/betree__PagedBetreeRefinement_v.19.smt2
splinterdb/betree__FilteredBetree_v.16.smt2
splinterdb/allocation_layer__AllocationJournal_v.6.smt2
splinterdb/betree__BufferDisk_v.10.smt2
splinterdb/abstract_system__MsgHistory_v.26.smt2
splinterdb/allocation_layer__AllocationJournal_v.8.smt2
splinterdb/journal__PagedJournalRefinement_v.5.smt2
splinterdb/betree__LinkedBetree_v.108.smt2
splinterdb/marshalling__IntegerMarshalling_v.14.smt2
splinterdb/betree__PagedBetree_v.2.smt2
splinterdb/allocation_layer__AllocationJournal_v.9.smt2
splinterdb/betree__LinkedBranch_v__Refinement_v.1.smt2
splinterdb/betree__LinkedBranch_v.30.smt2
splinterdb/allocation_layer__MiniAllocator_v.3.smt2
splinterdb/journal__PagedJournal_v.11.smt2
splinterdb/exec__MiniAllocator_v.6.smt2
splinterdb/allocation_layer__AllocationJournal_v.7.smt2
splinterdb/betree__LinkedBetree_v.107.smt2
splinterdb/allocation_layer__MiniAllocator_v.8.smt2
splinterdb/betree__LinkedBranch_v.48.smt2
splinterdb/journal__PagedJournal_v__PagedJournal.3.smt2
splinterdb/betree__LinkedBetree_v.102.smt2
splinterdb/betree__PivotBranchRefinement_v.21.smt2
splinterdb/marshalling__IntegerMarshalling_v.30.smt2
splinterdb/marshalling__IntegerMarshalling_v.31.smt2
splinterdb/betree__BufferSeq_v.6.smt2
splinterdb/allocation_layer__LikesJournal_v.16.smt2
splinterdb/journal__LinkedJournal_v__LinkedJournal.2.smt2
splinterdb/allocation_layer__LikesJournal_v.2.smt2
splinterdb/abstract_system__MsgHistory_v.1.smt2
splinterdb/allocation_layer__UnifiedCrashAwareJournal_v__UnifiedCrashAwareJournal.11.smt2
splinterdb/betree__BufferDisk_v.8.smt2
splinterdb/betree__LinkedBetree_v.24.smt2
splinterdb/betree__LinkedBetree_v.72.smt2
splinterdb/betree__LinkedBranch_v.62.smt2
splinterdb/betree__LinkedBetree_v.45.smt2
splinterdb/betree__PagedBetree_v.24.smt2
splinterdb/betree__FilteredBetreeRefinement_v.5.smt2
splinterdb/marshalling__IntegerMarshalling_v.9.smt2
splinterdb/betree__FilteredBetreeRefinement_v.14.smt2
splinterdb/betree__PivotBranchRefinement_v.19.smt2
splinterdb/betree__PivotBetree_v__PivotBetree.smt2
splinterdb/marshalling__IntegerMarshalling_v.39.smt2
splinterdb/betree__PivotBetreeRefinement_v.6.smt2
splinterdb/betree__BufferDisk_v.2.smt2
splinterdb/betree__BufferDisk_v.3.smt2
splinterdb/abstract_system__AbstractCrashAwareSystemRefinement_v.29.smt2
splinterdb/betree__FilteredBetreeRefinement_v.22.smt2
splinterdb/allocation_layer__UnifiedCrashAwareJournal_v__UnifiedCrashAwareJournal.7.smt2
splinterdb/journal__LinkedJournal_v.4.smt2
splinterdb/betree__LinkedBetree_v.31.smt2
splinterdb/betree__PivotTable_v.5.smt2
splinterdb/allocation_layer__LikesJournal_v__LikesJournal.5.smt2
splinterdb/betree__PivotBranch_v.6.smt2
splinterdb/allocation_layer__LikesJournalRefinement_v.4.smt2
splinterdb/betree__PagedBetree_v.1.smt2
splinterdb/journal__LinkedJournalRefinement_v.28.smt2
splinterdb/journal__PagedJournalRefinement_v.11.smt2
splinterdb/marshalling__IntegerMarshalling_v.48.smt2
splinterdb/marshalling__IntegerMarshalling_v.11.smt2
splinterdb/journal__LinkedJournal_v.17.smt2
splinterdb/betree__Memtable_v.5.smt2
splinterdb/allocation_layer__UnifiedCrashAwareJournal_v.4.smt2
splinterdb/betree__BufferSeq_v.20.smt2
splinterdb/betree__PivotBetreeRefinement_v.25.smt2
systems/ironkv-smt-delegation_map_v.4.smt2
systems/noderep-smt-spec__unbounded_log.7.smt2
systems/ironkv-smt-single_delivery_state_v.15.smt2
systems/ironkv-smt-marshal_v.36.smt2
systems/ironkv-smt-seq_is_unique_v.6.smt2
systems/ironkv-smt-host_protocol_t.13.smt2
systems/ironkv-smt-marshal_v.6.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-kv__kvimpl_t.1.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-kv__kvimpl_v.15.smt2
splinterdb/betree__LinkedBranch_v__Refinement_v.26.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-kv__kvimpl_t.11.smt2
systems/ironkv-smt-marshal_ironsht_specific_v.8.smt2
systems/ironkv-smt-marshal_v.35.smt2
splinterdb/allocation_layer__LikesJournal_v.13.smt2
systems/mimalloc-smt-pigeonhole.2.smt2
systems/noderep-smt-spec__unbounded_log__UnboundedLog.19.smt2
systems/ironkv-smt-marshal_v.46.smt2
systems/ironkv-smt-single_delivery_t.1.smt2
systems/ironkv-smt-single_delivery_t.10.smt2
systems/noderep-smt-root.1.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-kv__kvimpl_v.4.smt2
systems/ironkv-smt-marshal_ironsht_specific_v.46.smt2
systems/ironkv-smt-delegation_map_v.11.smt2
systems/ironkv-smt-host_protocol_t.22.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.5.smt2
systems/noderep-smt-spec__rwlock__RwLockSpec.7.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-kv__inv_v.1.smt2
systems/ironkv-smt-host_protocol_t.27.smt2
systems/noderep-smt-spec__rwlock__RwLockSpec.6.smt2
systems/mimalloc-smt-flags.5.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-pmem__traits_t.1.smt2
systems/noderep-smt-exec__context.4.smt2
systems/mimalloc-smt-pigeonhole.1.smt2
systems/noderep-smt-spec__unbounded_log_refines_simplelog.7.smt2
systems/ironkv-smt-marshal_v.32.smt2
systems/ironkv-smt-verus_extra__seq_lib_v.10.smt2
systems/ironkv-smt-delegation_map_v.52.smt2
systems/ironkv-smt-delegation_map_v.1.smt2
systems/ironkv-smt-single_delivery_state_v.8.smt2
systems/noderep-smt-exec__utils.4.smt2
systems/ironkv-smt-delegation_map_v.37.smt2
systems/noderep-smt-spec__linearization.2.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-kv__kvimpl_v.14.smt2
systems/ironkv-smt-host_protocol_t.6.smt2
systems/ironkv-smt-marshal_v.48.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-kv__kvimpl_t.6.smt2
systems/ironkv-smt-marshal_ironsht_specific_v.45.smt2
systems/ironkv-smt-delegation_map_v.34.smt2
systems/ironkv-smt-marshal_ironsht_specific_v.19.smt2
systems/ironkv-smt-marshal_v.13.smt2
systems/ironkv-smt-delegation_map_v.53.smt2
systems/ironkv-smt-marshal_v.19.smt2
systems/ironkv-smt-marshal_ironsht_specific_v.36.smt2
systems/noderep-smt-spec__flat_combiner__FlatCombiner.5.smt2
systems/noderep-smt-spec__unbounded_log__UnboundedLog.27.smt2
systems/noderep-smt-spec__rwlock__RwLockSpec.3.smt2
systems/mimalloc-smt-flags.6.smt2
systems/noderep-smt-spec__flat_combiner__FlatCombiner.7.smt2
systems/noderep-smt-spec__unbounded_log__UnboundedLog.30.smt2
systems/noderep-smt-exec__rwlock.1.smt2
systems/noderep-smt-spec__unbounded_log__UnboundedLog.8.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-kv__kvimpl_t.7.smt2
systems/noderep-smt-spec__unbounded_log__UnboundedLog.3.smt2
systems/mimalloc-smt-types__BoolAgree.2.smt2
systems/ironkv-smt-host_impl_v.1.smt2
systems/ironkv-smt-single_delivery_state_v.5.smt2
systems/ironkv-smt-host_protocol_t.7.smt2
systems/ironkv-smt-marshal_v.34.smt2
systems/noderep-smt-exec__rwlock.7.smt2
systems/ironkv-smt-marshal_v.7.smt2
systems/ironkv-smt-delegation_map_v.48.smt2
systems/ironkv-smt-delegation_map_v.41.smt2
systems/ironkv-smt-seq_is_unique_v.5.smt2
systems/ironkv-smt-cmessage_v.5.smt2
systems/ironkv-smt-marshal_ironsht_specific_v.2.smt2
systems/ironkv-smt-host_impl_v.4.smt2
systems/ironkv-smt-single_delivery_model_v.1.smt2
systems/noderep-smt-spec__simple_log__SimpleLog.1.smt2
systems/noderep-smt-spec__unbounded_log__UnboundedLog.20.smt2
systems/ironkv-smt-host_protocol_t.8.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-kv__kvimpl_t.4.smt2
systems/mimalloc-smt-config.4.smt2
systems/mimalloc-smt-config.2.smt2
systems/noderep-smt-spec__linearization.1.smt2
systems/noderep-smt-exec__context.5.smt2
systems/mimalloc-smt-flags.8.smt2
systems/ironkv-smt-delegation_map_v.43.smt2
systems/ironkv-smt-verus_extra__set_lib_ext_v.4.smt2
systems/ironkv-smt-marshal_v.37.smt2
systems/ironkv-smt-host_protocol_t.31.smt2
systems/noderep-smt-exec__rwlock.10.smt2
systems/ironkv-smt-seq_is_unique_v.2.smt2
systems/ironkv-smt-verus_extra__set_lib_ext_v.19.smt2
systems/ironkv-smt-marshal_ironsht_specific_v.18.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-kv__kvimpl_t.14.smt2
systems/ironkv-smt-single_delivery_model_v.3.smt2
systems/noderep-smt-spec__simple_log.smt2
systems/ironkv-smt-delegation_map_v.42.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.6.smt2
systems/ironkv-smt-verus_extra__set_lib_ext_v.24.smt2
systems/ironkv-smt-marshal_ironsht_specific_v.9.smt2
systems/ironkv-smt-delegation_map_v.12.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__layout_v.4.smt2
systems/noderep-smt-spec__flat_combiner__FlatCombiner.14.smt2
systems/noderep-smt-spec__unbounded_log__UnboundedLog.15.smt2
systems/ironkv-smt-host_protocol_t.25.smt2
systems/ironkv-smt-verus_extra__seq_lib_v.8.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-kv__kvimpl_v.12.smt2
systems/noderep-smt-spec__rwlock__RwLockSpec.10.smt2
systems/ironkv-smt-delegation_map_v.28.smt2
systems/ironkv-smt-marshal_v.1.smt2
systems/ironkv-smt-host_protocol_t.3.smt2
systems/noderep-smt-exec__rwlock.5.smt2
systems/noderep-smt-spec__unbounded_log.18.smt2
systems/ironkv-smt-marshal_ironsht_specific_v.3.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__layout_v.3.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-pmem__linux_pmemfile_t.4.smt2
systems/ironkv-smt-single_delivery_t.9.smt2
systems/ironkv-smt-verus_extra__set_lib_ext_v.21.smt2
systems/noderep-smt-root.3.smt2
systems/noderep-smt-spec__unbounded_log__UnboundedLog.16.smt2
systems/noderep-smt-spec__rwlock__RwLockSpec.12.smt2
systems/ironkv-smt-host_protocol_t.11.smt2
systems/ironkv-smt-host_protocol_t.17.smt2
systems/noderep-smt-spec__unbounded_log.2.smt2
systems/ironkv-smt-seq_is_unique_v.7.smt2
systems/ironkv-smt-delegation_map_v.2.smt2
systems/noderep-smt-exec__rwlock.2.smt2
systems/noderep-smt-spec__unbounded_log__UnboundedLog.13.smt2
systems/ironkv-smt-marshal_ironsht_specific_v.39.smt2
systems/ironkv-smt-verus_extra__set_lib_ext_v.7.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-pmemspec_t.1.smt2
systems/ironkv-smt-keys_t.5.smt2
systems/ironkv-smt-verus_extra__seq_lib_v.7.smt2
systems/ironkv-smt-keys_t.6.smt2
systems/ironkv-smt-keys_t.3.smt2
systems/ironkv-smt-host_impl_v.10.smt2
systems/ironkv-smt-delegation_map_v.7.smt2
systems/ironkv-smt-cmessage_v.2.smt2
systems/ironkv-smt-delegation_map_v.38.smt2
systems/noderep-smt-spec__rwlock__RwLockSpec.19.smt2
systems/ironkv-smt-host_protocol_t.20.smt2
systems/noderep-smt-spec__unbounded_log__UnboundedLog.17.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-kv__kvimpl_v.9.smt2
systems/ironkv-smt-marshal_ironsht_specific_v.32.smt2
systems/ironkv-smt-host_protocol_t.18.smt2
systems/ironkv-smt-marshal_v.52.smt2
systems/ironkv-smt-host_impl_t.1.smt2
systems/noderep-smt-spec__linearization.8.smt2
systems/noderep-smt-spec__simple_log__SimpleLog.8.smt2
systems/noderep-smt-spec__simple_log__SimpleLog.7.smt2
systems/ironkv-smt-marshal_v.42.smt2
systems/ironkv-smt-marshal_v.47.smt2
systems/ironkv-smt-cmessage_v.10.smt2
systems/noderep-smt-spec__simple_log__SimpleLog.5.smt2
systems/ironkv-smt-marshal_v.45.smt2
systems/ironkv-smt-single_delivery_model_v.7.smt2
systems/noderep-smt-spec__unbounded_log.13.smt2
systems/ironkv-smt-marshal_v.29.smt2
systems/ironkv-smt-delegation_map_v.31.smt2
systems/noderep-smt-spec__unbounded_log__UnboundedLog.4.smt2
systems/noderep-smt-spec__flat_combiner__FlatCombiner.13.smt2
systems/ironkv-smt-delegation_map_v.54.smt2
systems/ironkv-smt-cmessage_v.17.smt2
systems/ironkv-smt-single_delivery_model_v.2.smt2
systems/ironkv-smt-seq_is_unique_v.11.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-kv__kvimpl_t.9.smt2
systems/noderep-smt-spec__unbounded_log_refines_simplelog.9.smt2
systems/mimalloc-smt-linked_list__StuffAgree.1.smt2
systems/ironkv-smt-marshal_v.5.smt2
systems/ironkv-smt-args_t.2.smt2
systems/noderep-smt-spec__unbounded_log.6.smt2
systems/ironkv-smt-delegation_map_v.44.smt2
systems/mimalloc-smt-pigeonhole.6.smt2
systems/ironkv-smt-keys_t.7.smt2
systems/noderep-smt-spec__unbounded_log__UnboundedLog.22.smt2
systems/ironkv-smt-marshal_v.10.smt2
systems/ironkv-smt-verus_extra__set_lib_ext_v.23.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-pmem__linux_pmemfile_t.3.smt2
systems/ironkv-smt-host_protocol_t.30.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-kv__kvspec_t.1.smt2
systems/noderep-smt-spec__unbounded_log.4.smt2
systems/ironkv-smt-verus_extra__seq_lib_v.1.smt2
systems/ironkv-smt-verus_extra__set_lib_ext_v.14.smt2
systems/noderep-smt-spec__linearization.9.smt2
systems/mimalloc-smt-tokens.1.smt2
systems/ironkv-smt-delegation_map_v.32.smt2
systems/noderep-smt-spec__unbounded_log__UnboundedLog.2.smt2
systems/ironkv-smt-single_delivery_state_v.9.smt2
systems/noderep-smt-spec__flat_combiner__FlatCombiner.8.smt2
systems/ironkv-smt-marshal_v.44.smt2
systems/ironkv-smt-endpoint_hashmap_t.smt2
systems/ironkv-smt-verus_extra__set_lib_ext_v.8.smt2
systems/ironkv-smt-marshal_v.11.smt2
systems/noderep-smt-spec__unbounded_log.16.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.3.smt2
systems/ironkv-smt-marshal_v.23.smt2
systems/ironkv-smt-marshal_v.31.smt2
systems/ironkv-smt-verus_extra__set_lib_ext_v.18.smt2
systems/noderep-smt-exec__rwlock.9.smt2
systems/ironkv-smt-delegation_map_v.24.smt2
systems/ironkv-smt-marshal_ironsht_specific_v.33.smt2
systems/noderep-smt-spec__flat_combiner__FlatCombiner.2.smt2
systems/noderep-smt-spec__unbounded_log.15.smt2
systems/ironkv-smt-io_t.4.smt2

UFDTNIA • Charts • Solver Isomap
verismo/snp__ghcb__proto_s.22.smt2
verismo/tspec_e__math__bits_e.8.smt2
verismo/arch__vram__vram_p.22.smt2
verismo/primitives_e__vec.2.smt2
verismo/ptr__raw_ptr_s.3.smt2
verismo/snp__cpuid.2.smt2
verismo/arch__addr_s__def_s.3.smt2
verismo/addr_e__addr_interface.2.smt2
verismo/snp__ghcb__proto_s.5.smt2
verismo/snp__ghcb__proto_page.32.smt2
verismo/snp__ghcb__proto_page.4.smt2
verismo/snp__ghcb__proto_e.13.smt2
verismo/arch__vram__vram_p.12.smt2
verismo/security.9.smt2
verismo/arch__vram__vram_p.15.smt2
verismo/snp__cpu__vmsa.49.smt2
verismo/tspec__security__sectype.98.smt2
verismo/tspec__math__bits_p.9.smt2
verismo/tspec__security__sectype.73.smt2
verismo/snp__ghcb__proto_page.73.smt2
verismo/arch__vram__vram_p.7.smt2
verismo/tspec__security__sectype.109.smt2
verismo/ptr__snp__rmp__rmp_t.8.smt2
verismo/pgtable_e__def.20.smt2
verismo/snp__cpu__gdt.4.smt2
verismo/tspec__security__sectype.235.smt2
verismo/tspec__security__sectype.342.smt2
verismo/debug__ghcb_print.2.smt2
verismo/tspec__security__sectype.338.smt2
verismo/debug__ghcb_print.26.smt2
verismo/tspec__security__sectype.408.smt2
verismo/arch__vram__vram_p.9.smt2
verismo/lock__spincell_e.6.smt2
verismo/tspec__security__sectype.417.smt2
verismo/tspec__cast.5.smt2
verismo/snp__ghcb__proto_e.2.smt2
verismo/mshyper__wakeup.1.smt2
verismo/allocator__buddy.3.smt2
verismo/boot__linux.35.smt2
verismo/snp__ghcb__proto_impl.20.smt2
verismo/snp__cpuid.14.smt2
verismo/security__monitor.5.smt2
verismo/boot__init__init_s.smt2
verismo/snp__ghcb__proto_s.9.smt2
verismo/pgtable_e__pte.29.smt2
verismo/security__monitor.24.smt2
verismo/snp__ghcb__proto_impl.13.smt2
verismo/security__mem.27.smt2
verismo/security__monitor.15.smt2
verismo/tspec__security__sectype.108.smt2
verismo/boot__params.14.smt2
verismo/tspec__security__sectype.394.smt2
verismo/snp__cpu__gdt.39.smt2
verismo/tspec__security__sectype.206.smt2
verismo/tspec__security__sectype.5.smt2
verismo/snp__cpu__gdt.41.smt2
verismo/boot__init__init_e.2.smt2
verismo/mshyper.17.smt2
verismo/mshyper.14.smt2
verismo/boot__idt__dummy.2.smt2
verismo/security__monitor.6.smt2
verismo/security__mem.38.smt2
verismo/tspec__security__sectype.193.smt2
verismo/snp__cpu__gdt.49.smt2
verismo/addr_e__range_interface.17.smt2
verismo/tspec__security__sectype.26.smt2
verismo/snp__ghcb__proto_page.31.smt2
verismo/tspec__security__sectype.393.smt2
verismo/tspec__security__sectype.138.smt2
verismo/ptr__snp__snp_u.8.smt2
verismo/snp__cpu__gdt.48.smt2
verismo/tspec__setlib.12.smt2
verismo/snp__ghcb__proto_page.18.smt2
verismo/tspec__security__sectype.261.smt2
verismo/tspec__security__sectype.307.smt2
verismo/tspec__security__sectype.233.smt2
verismo/tspec__security__sectype.231.smt2
verismo/snp__ghcb__proto_page.89.smt2
verismo/tspec__security__sectype.325.smt2
verismo/tspec__cast.2.smt2
verismo/boot__params.16.smt2
verismo/tspec__security__sectype.46.smt2
verismo/pgtable_e__pte.26.smt2
verismo/tspec__security__sectype.209.smt2
verismo/pgtable_e__def.16.smt2
verismo/snp__ghcb__proto_s.3.smt2
verismo/tspec__security__sectype.121.smt2
verismo/snp__cpu__vmsa.1.smt2
verismo/lock__spincell_e.1.smt2
verismo/arch__vram__vram_p.1.smt2
verismo/snp__ghcb__proto_s.43.smt2
verismo/snp__cpu__gdt.57.smt2
verismo/lock__spincell_e.5.smt2
verismo/ptr__snp__snp_u.2.smt2
verismo/snp__cpu__vmsa.4.smt2
verismo/tspec__security__sectype.81.smt2
verismo/tspec__security__sectype.72.smt2
verismo/snp__ghcb__proto_impl__internal.2.smt2
verismo/snp__ghcb__proto_page.134.smt2
verismo/allocator__buddy.6.smt2
verismo/tspec_e__math__align_e.1.smt2
verismo/snp__cpu__gdt.53.smt2
verismo/snp__ghcb__proto_page.38.smt2
verismo/tspec__security__sectype.106.smt2
verismo/tspec__security__sectype.321.smt2
verismo/snp__cpu__vmsa.2.smt2
verismo/snp__ghcb__proto_impl.22.smt2
verismo/tspec__security__sectype.144.smt2
verismo/boot__mshyper__param_e.1.smt2
verismo/snp__cpuid.16.smt2
verismo/tspec__security__sectype.149.smt2
verismo/snp__ghcb__proto_e.20.smt2
verismo/tspec__math__bits_p.8.smt2
verismo/primitives_e__seq.2.smt2
verismo/ptr__snp__rmp__rmp_t.5.smt2
verismo/debug__slice_print.3.smt2
verismo/snp__cpu__vmsa.18.smt2
verismo/ptr__ptr_e.9.smt2
verismo/tspec__security__sectype.199.smt2
verismo/addr_e__range_interface.15.smt2
verismo/tspec__security__sectype.196.smt2
verismo/mshyper__wakeup.5.smt2
verismo/tspec__security__sectype.27.smt2
verismo/tspec__math__bits_p.4.smt2
verismo/tspec__security__sectype.152.smt2
verismo/allocator__buddy.4.smt2
verismo/linkedlist.13.smt2
verismo/boot__linux.13.smt2
verismo/snp__ghcb__proto_page.121.smt2
verismo/linkedlist.12.smt2
verismo/pgtable_e__def.44.smt2
verismo/tspec__security__sectype.389.smt2
verismo/snp__cpu__gdt.63.smt2
verismo/boot__idt__def.4.smt2
verismo/tspec__security__sectype.176.smt2
verismo/tspec__math__align_s.5.smt2
verismo/snp__cpuid.5.smt2
verismo/security__secret.18.smt2
verismo/tspec__security__sectype.198.smt2
verismo/tspec__security__sectype.418.smt2
verismo/security__monitor.10.smt2
verismo/tspec__security__sectype.336.smt2
verismo/tspec__security__sectype.286.smt2
verismo/snp__ghcb__proto_page.94.smt2
verismo/tspec__security__sectype.363.smt2
verismo/tspec__math__bits_p.7.smt2
verismo/snp__ghcb__proto_page.85.smt2
verismo/snp__ghcb__proto_page.93.smt2
verismo/snp__ghcb__proto_s.27.smt2
verismo/snp__ghcb__proto_page.96.smt2
verismo/tspec__security__sectype_test.8.smt2
verismo/snp__cpu__vmsa.7.smt2
verismo/snp__ghcb__proto_impl.17.smt2
verismo/mshyper.1.smt2
verismo/security__monitor.12.smt2
verismo/pgtable_e__def.34.smt2
verismo/snp__trackedcore__snpmulticore.1.smt2
verismo/debug__ghcb_print.7.smt2
verismo/snp__cpu__vmsa.64.smt2
verismo/snp__ghcb__proto_impl.10.smt2
verismo/allocator__bit_p.smt2
verismo/snp__ghcb__proto_impl.27.smt2
verismo/boot__linux.17.smt2
verismo/trusted_hacl__stub.7.smt2
verismo/snp__cpu__gdt.26.smt2
verismo/snp__ghcb__proto_page.140.smt2
verismo/snp__ghcb__proto_page.14.smt2
verismo/allocator__linkedlist.13.smt2
verismo/snp__cpu__vmsa.5.smt2
verismo/tspec__security__sectype.140.smt2
verismo/debug__ghcb_print.10.smt2
verismo/linkedlist.4.smt2
verismo/tspec__security__sectype.56.smt2
verismo/boot__params.23.smt2
verismo/tspec__security__sectype.172.smt2
verismo/tspec__security__sectype.392.smt2
verismo/snp__ghcb__proto_s.23.smt2
verismo/tspec__security__sectype.9.smt2
verismo/allocator__buddy.13.smt2
verismo/snp__cpu__gdt.2.smt2
verismo/snp__ghcb__proto_s.41.smt2
verismo/pgtable_e__pte.7.smt2
verismo/mshyper.11.smt2
verismo/security__monitor.16.smt2
verismo/allocator__linkedlist.10.smt2
verismo/tspec_e__math__bits_e.3.smt2
verismo/snp__ghcb__proto_s.13.smt2
verismo/snp__ghcb__proto_page.16.smt2
verismo/arch__pgtable__entry_p.4.smt2
verismo/tspec_e__math__bits_e.5.smt2
verismo/snp__ghcb__proto_page.110.smt2
verismo/snp__ghcb__proto_page.34.smt2
verismo/tspec__security__sectype.348.smt2
verismo/tspec__security__sectype.350.smt2
verismo/tspec__security__sectype.341.smt2
verismo/tspec__security__sectype.324.smt2
verismo/tspec__security__sectype.237.smt2
verismo/arch__pgtable__entry_p.7.smt2
verismo/tspec__security__sectype.309.smt2
verismo/tspec__security__sectype.17.smt2
verismo/boot__linux.11.smt2
verismo/ptr__raw_ptr_s.1.smt2
verismo/ptr__snp__snp_u.15.smt2
verismo/arch__addr_s__page.6.smt2
verismo/tspec__cast.7.smt2
verismo/security.12.smt2
verismo/pgtable_e__pte.23.smt2
verismo/snp__cpu__gdt.40.smt2
verismo/boot__mshyper__param_e.5.smt2
verismo/snp__cpu__vmsa.58.smt2
verismo/snp__cpu__gdt.34.smt2
verismo/debug__ghcb_print.12.smt2
verismo/boot__idt__dummy.5.smt2
verismo/addr_e__addr_interface.13.smt2
verismo/security__secret.17.smt2
verismo/linkedlist.14.smt2
verismo/debug__ghcb_print.28.smt2
verismo/tspec__security__sectype.239.smt2
verismo/ptr__def_s.smt2
verismo/snp__cpu__gdt.13.smt2
verismo/security__mem.20.smt2
verismo/snp__cpu__vmsa.14.smt2
verismo/addr_e__addr_interface.3.smt2
verismo/arch__addr_s__def_s.8.smt2
verismo/allocator__buddy.9.smt2
verismo/arch__vram__vram_p.18.smt2
verismo/snp__ghcb__proto_page.67.smt2
verismo/tspec__security__sectype.225.smt2
verismo/linkedlist.6.smt2
verismo/linkedlist.16.smt2
verismo/snp__ghcb__proto_page.83.smt2
verismo/tspec__security__sectype.423.smt2
verismo/snp__ghcb__proto_page.63.smt2
verismo/tspec__security__sectype.183.smt2
verismo/ptr__snp__rmp__rmp_t.7.smt2
verismo/security.3.smt2
verismo/snp__ghcb__proto_page.44.smt2
verismo/snp__ghcb__proto_impl.25.smt2
verismo/snp__cpu__gdt.45.smt2
verismo/arch__vram__vram_p.26.smt2
verismo/tspec__security__sectype.38.smt2
verismo/snp__ghcb__proto_impl.21.smt2
verismo/snp__cpu__gdt.17.smt2
verismo/security.21.smt2
verismo/pgtable_e__def.42.smt2
verismo/snp__ghcb__def_s.2.smt2
verismo/tspec__math__integer.8.smt2
verismo/registers__msr_t.7.smt2
verismo/allocator__linkedlist.3.smt2
verismo/allocator__buddy.7.smt2
verismo/tspec__cast.6.smt2
verismo/snp__ghcb__proto_e.15.smt2
verismo/pgtable_e__def.26.smt2
verismo/security__secret.9.smt2
verismo/ptr__snp__rmp__rmp_e.3.smt2
verismo/snp__ghcb__proto_page.88.smt2
verismo/tspec__security__sectype.226.smt2
verismo/tspec__security__sectype.308.smt2
verismo/tspec__security__sectype.220.smt2
verismo/tspec__security__sectype.297.smt2
verismo/tspec__security__sectype.216.smt2
verismo/boot__linux.44.smt2
verismo/boot__params.12.smt2
verismo/debug__ghcb_print.6.smt2
verismo/boot__params.5.smt2
verismo/boot__linux.40.smt2
verismo/snp__ghcb__proto_page.91.smt2
verismo/arch__mem__mem_p.13.smt2
verismo/registers__msr_t.2.smt2
verismo/security__mem.49.smt2
verismo/mshyper.19.smt2
verismo/tspec__security__sectype.91.smt2
verismo/tspec__security__sectype.95.smt2
verismo/tspec__security__sectype.390.smt2
verismo/pgtable_e__pte.11.smt2
verismo/allocator__linkedlist.11.smt2
verismo/security__monitor.14.smt2
verismo/arch__mem__mem_p.4.smt2
verismo/arch__ptram__ptram_s.smt2
verismo/tspec__security__sectype_test.1.smt2
verismo/tspec__security__sectype.148.smt2
verismo/snp__ghcb__proto_page.104.smt2
verismo/arch__pgtable__memmap_p.5.smt2
verismo/snp__cpu__gdt.5.smt2
verismo/tspec__security__sectype.370.smt2
verismo/lock__spin_perm_s.3.smt2
verismo/snp__ghcb__proto_page.66.smt2
verismo/tspec__security__sectype.119.smt2
verismo/boot__linux.22.smt2
verismo/tspec__security__sectype.48.smt2
verismo/tspec__security__sectype.208.smt2
verismo/addr_e__exe.1.smt2
verismo/mshyper.7.smt2
verismo/snp__ghcb__proto_page.69.smt2
verismo/security__mem.42.smt2
verismo/tspec__security__sectype.50.smt2
verismo/tspec__security__sectype.306.smt2
verismo/primitives_e__vec.1.smt2
verismo/snp__ghcb__proto_page.98.smt2
verismo/boot__params.8.smt2
verismo/debug__ghcb_print.23.smt2
verismo/tspec__security__sectype.213.smt2
verismo/tspec__security__sectype.362.smt2
verismo/boot__linux.8.smt2
verismo/tspec__security__sectype.39.smt2
verismo/snp__cpu__gdt.6.smt2
verismo/snp__cpu__gdt.27.smt2
verismo/snp__ghcb__proto_impl.15.smt2
verismo/tspec__security__sectype.124.smt2
verismo/snp__ghcb__proto_s.2.smt2
verismo/snp__cpu__gdt.61.smt2
verismo/tspec__security__sectype.151.smt2
verismo/allocator__linkedlist.6.smt2
verismo/mshyper__wakeup.7.smt2
verismo/arch__x64__x64_p.2.smt2
verismo/tspec__security__sectype.366.smt2
verismo/snp__cpu__gdt.66.smt2
verismo/registers__msr_t.3.smt2
verismo/pgtable_e__def.7.smt2
verismo/addr_e__range_interface.13.smt2
verismo/pgtable_e__pte.22.smt2
verismo/snp__ghcb__proto_e.12.smt2
verismo/snp__ghcb__proto_impl.11.smt2
verismo/snp__cpu__vmsa.10.smt2
verismo/tspec__security__sectype.371.smt2
verismo/arch__pgtable__entry_p.3.smt2
verismo/tspec__security__sectype.86.smt2
verismo/tspec__security__sectype.282.smt2
verismo/pgtable_e__pte.2.smt2
verismo/boot__init__mshv_alloc.3.smt2
verismo/addr_e__range_interface.7.smt2
verismo/security__pcr.2.smt2
verismo/tspec__security__sectype.40.smt2
verismo/snp__ghcb__proto_page.19.smt2
verismo/boot__idt__dummy.3.smt2
verismo/snp__cpu__vmsa.28.smt2
verismo/snp__ghcb__proto_page.26.smt2
verismo/snp__ghcb__proto_page.48.smt2
verismo/addr_e__addr_interface.10.smt2
verismo/security__mem.25.smt2
verismo/snp__cpu__vmsa.37.smt2
verismo/tspec__security__sectype.346.smt2
verismo/security.18.smt2
verismo/security__secret.24.smt2
verismo/linkedlist.9.smt2
verismo/tspec__security__sectype.178.smt2
verismo/arch__ptram__ptram_p.6.smt2
verismo/tspec__security__sectype.130.smt2
verismo/arch__vram__vram_p.28.smt2
verismo/snp__ghcb__proto_page.27.smt2
verismo/snp__ghcb__proto_page.112.smt2
verismo/snp__ghcb__proto_s.31.smt2
verismo/snp__cpu__gdt.60.smt2
verismo/addr_e__range_interface.10.smt2
verismo/snp__cpu__vmsa.13.smt2
verismo/mshyper.6.smt2
verismo/mshyper.15.smt2
verismo/snp__cpu__vmsa.12.smt2
verismo/ptr__snp__rmp__rmp_t.6.smt2
verismo/addr_e__range_interface.5.smt2
verismo/ptr__snp__snp_s.smt2
verismo/tspec__security__sectype.122.smt2
verismo/tspec__security__sectype.395.smt2
verismo/tspec__setlib.11.smt2
verismo/tspec__security__sectype.51.smt2
verismo/tspec__security__sectype.240.smt2
verismo/tspec__security__sectype.281.smt2
verismo/tspec__security__sectype.184.smt2
verismo/snp__cpu__vmsa.11.smt2
verismo/ptr__snp__rmp__rmp_e.7.smt2
verismo/snp__cpuid.13.smt2
verismo/pgtable_e__pte.3.smt2
verismo/pgtable_e__pte.16.smt2
verismo/arch__vram__vram_p.21.smt2
verismo/linkedlist.11.smt2
verismo/ptr__snp__rmp__rmp_e.5.smt2
verismo/tspec__security__sectype.45.smt2
verismo/tspec__security__sectype.168.smt2
verismo/snp__ghcb__proto_page.2.smt2
verismo/snp__ghcb__proto_page.138.smt2
verismo/addr_e__range_interface.14.smt2
verismo/security__monitor.1.smt2
verismo/tspec__security__sectype.155.smt2
verismo/tspec__cast.4.smt2
verismo/security.6.smt2
verismo/snp__cpu__vmsa.38.smt2
verismo/tspec__math__pow_p.1.smt2
verismo/arch__pgtable__memmap_p.3.smt2
verismo/boot__linux.20.smt2
verismo/arch__addr_s__page.1.smt2
verismo/tspec__security__sectype.20.smt2
verismo/tspec__security__sectype.222.smt2
verismo/tspec__security__sectype.283.smt2
verismo/snp__ghcb__proto_s.25.smt2
verismo/snp__ghcb__proto_s.10.smt2
verismo/tspec__security__sectype.115.smt2
verismo/tspec__security__sectype.6.smt2
verismo/boot__monitor_params.smt2
verismo/boot__linux.1.smt2
verismo/security__mem.45.smt2
verismo/allocator__buddy.15.smt2
verismo/snp__ghcb__proto_page.81.smt2
verismo/addr_e__addr_interface.11.smt2
verismo/tspec__security__sectype.165.smt2
verismo/snp__cpu__gdt.42.smt2
verismo/security__secret.22.smt2
verismo/pgtable_e__pte.25.smt2
verismo/tspec__security__sectype.97.smt2
verismo/tspec__security__sectype.413.smt2
verismo/vbox__vbox.6.smt2
verismo/vbox__vbox.2.smt2
verismo/tspec__security__sectype.403.smt2
verismo/security.11.smt2
verismo/ptr__snp__rmp__rmp_t.2.smt2
verismo/tspec__security__sectype.256.smt2
verismo/tspec__security__sectype.58.smt2
verismo/tspec__security__sectype.69.smt2
verismo/arch__ptram__ptram_p.10.smt2
verismo/snp__ghcb__proto_s.18.smt2
verismo/vbox__vbox.7.smt2
verismo/linkedlist.7.smt2
verismo/tspec__stream__basic.1.smt2
verismo/snp__ghcb__proto_impl.26.smt2
verismo/snp__cpuid.11.smt2
verismo/snp__ghcb__proto_page.127.smt2
verismo/tspec__security__sectype_test.5.smt2
verismo/tspec__security__sectype.102.smt2
verismo/security.2.smt2
verismo/tspec__size_s.4.smt2
verismo/security__monitor.9.smt2
verismo/security__mem.28.smt2
verismo/allocator__buddy.2.smt2
verismo/snp__ghcb__proto_page.107.smt2
verismo/tspec__security__sectype.186.smt2
verismo/tspec__security__sectype.32.smt2
verismo/debug__ghcb_print.8.smt2
verismo/pgtable_e__pte.9.smt2
verismo/vcell__vcell.smt2
verismo/mshyper__hypercall.2.smt2
verismo/registers__msr_t.11.smt2
verismo/security__pcr.5.smt2
verismo/snp__ghcb__proto_page.10.smt2
verismo/snp__ghcb__proto_impl.28.smt2
verismo/tspec_e__math__bits_e.1.smt2
verismo/arch__ptram__ptram_u.smt2
verismo/allocator__buddy.11.smt2
verismo/boot__init__mshv_fmt.1.smt2
verismo/tspec__security__sectype.175.smt2
verismo/tspec__security__sectype.202.smt2
verismo/tspec__security__sectype.99.smt2
verismo/tspec__security__sectype.391.smt2
verismo/vbox__vbox.3.smt2
verismo/allocator__locked.1.smt2
verismo/pgtable_e__def.39.smt2
verismo/tspec__security__sectype.30.smt2
verismo/tspec__security__sectype.49.smt2
verismo/boot__linux.34.smt2
verismo/snp__ghcb__proto_page.102.smt2
verismo/snp__ghcb__proto_page.8.smt2
verismo/snp__ghcb__proto_page.71.smt2
verismo/security__monitor.17.smt2
verismo/pgtable_e__pte.8.smt2
verismo/security__secret.1.smt2
verismo/boot__linux.43.smt2
verismo/tspec__security__sectype.274.smt2
verismo/tspec__security__sectype.265.smt2
verismo/snp__cpu__gdt.19.smt2
verismo/tspec__security__sectype.77.smt2
verismo/tspec__security__sectype.85.smt2
verismo/ptr__snp__snp_u.16.smt2
verismo/snp__ghcb__proto_page.41.smt2
verismo/snp__ghcb__proto_impl.7.smt2
verismo/pgtable_e__def.31.smt2
verismo/tspec__security__sectype.162.smt2
verismo/snp__ghcb__proto_e.19.smt2
verismo/security__secret.13.smt2
verismo/mshyper.5.smt2
verismo/snp__ghcb__proto_e.18.smt2
verismo/security.19.smt2
verismo/security.10.smt2
verismo/snp__cpu__gdt.21.smt2
verismo/security__monitor.25.smt2
verismo/security__mem.50.smt2
verismo/tspec__security__sectype.201.smt2
verismo/arch__mem__mem_p.11.smt2
verismo/snp__cpu__vmsa.31.smt2
verismo/boot__idt__def.3.smt2
verismo/tspec__security__sectype.380.smt2
verismo/tspec__security__sectype.398.smt2
verismo/tspec__security__sectype.412.smt2
verismo/tspec__security__sectype.368.smt2
verismo/tspec__security__sectype.388.smt2
verismo/security__secret.6.smt2
verismo/tspec__security__sectype.381.smt2
verismo/tspec__math__integer.2.smt2
verismo/snp__cpu__vmsa.50.smt2
verismo/tspec__stream__basic.2.smt2
verismo/snp__ghcb__proto_page.30.smt2
verismo/tspec__security__sectype.415.smt2
verismo/snp__cpu__vmsa.32.smt2
verismo/snp__ghcb__proto_page.117.smt2
verismo/snp__ghcb__proto_page.70.smt2
verismo/snp__ghcb__proto_impl.4.smt2
verismo/snp__ghcb__proto_impl.6.smt2
verismo/snp__cpu__gdt.20.smt2
verismo/pgtable_e__def.36.smt2
verismo/snp__cpu__gdt.38.smt2
verismo/addr_e__addr_interface.16.smt2
verismo/boot__linux.36.smt2
verismo/debug__ghcb_print.5.smt2
verismo/tspec__security__sectype.221.smt2
verismo/security__mem.37.smt2
verismo/tspec__security__sectype.329.smt2
verismo/debug__ghcb_print.25.smt2
verismo/tspec__security__sectype.328.smt2
verismo/tspec_e__size_e.smt2
verismo/snp__cpu__vmsa.44.smt2
verismo/snp__ghcb__proto_s.24.smt2
verismo/arch__vram__vram_p.2.smt2
verismo/arch__mem__mem_p.16.smt2
verismo/tspec__math__align_sverismo_tspec.math.align_s.proof_align_down._01.smt2
verismo/pgtable_e__def.32.smt2
verismo/boot__linux.30.smt2
verismo/security__pcr.8.smt2
anvil/splinterdb-smt-marshalling__math_v.smt2
anvil/splinterdb-smt-marshalling__math_vlib_marshalling.math_v.distribute_left._01.smt2
verismo/ptr__snp__snp_u.13.smt2
anvil/splinterdb-smt-marshalling__ResizableUniformSizedSeq_v.7.smt2
verismo/tspec__security__sectype.364.smt2
anvil/splinterdb-smt-marshalling__UniformSizedSeq_v.6.smt2
anvil/splinterdb-smt-marshalling__UniformSizedSeq_v.5.smt2
anvil/splinterdb-smt-marshalling__ResizableUniformSizedSeq_v.4.smt2
anvil/splinterdb-smt-marshalling__UniformSizedSeq_v.1.smt2
anvil/splinterdb-smt-marshalling__UniformSizedSeq_v.2.smt2
anvil/splinterdb-smt-marshalling__ResizableUniformSizedSeq_v.9.smt2
anvil/splinterdb-smt-marshalling__UniformSizedSeq_v.4.smt2
atmosphere/define.29.smt2
atmosphere/va_range.2.smt2
verismo/snp__ghcb__proto_s.26.smt2
atmosphere/memory_manager__spec_impl.12.smt2
atmosphere/define.39.smt2
atmosphere/kernel__syscall_send_pages.smt2
verismo/tspec__security__sectype.8.smt2
verismo/snp__ghcb__proto_page.103.smt2
verismo/security__mem.10.smt2
atmosphere/define.37.smt2
atmosphere/pagetable__pagetable_spec_impl.6.smt2
verismo/tspec__security__sectype.414.smt2
atmosphere/allocator__page_allocator_spec_impl.23.smt2
atmosphere/define.16.smt2
atmosphere/pagetable__pagetable_spec_impl.5.smt2
atmosphere/allocator__page_allocator_spec_impl.8.smt2
atmosphere/process_manager__spec_impl.24.smt2
atmosphere/define.22.smt2
atmosphere/lemma__lemma_u.2.smt2
atmosphere/kernel__create_and_map_pages.1.smt2
atmosphere/process_manager__spec_impl.2.smt2
atmosphere/process_manager__spec_impl.14.smt2
atmosphere/allocator__page_allocator_spec_impl.7.smt2
atmosphere/process_manager__spec_impl.3.smt2
atmosphere/define.33.smt2
atmosphere/process_manager__spec_impl.13.smt2
atmosphere/kernel__create_and_share_pages.4.smt2
atmosphere/define.19.smt2
atmosphere/define.23.smt2
verismo/snp__ghcb__proto_page.126.smt2
atmosphere/pagetable__pagetable_spec_impl.10.smt2
atmosphere/process_manager__spec_impl.33.smt2
atmosphere/process_manager__spec_impl.6.smt2
atmosphere/allocator__page_allocator_spec_impl.20.smt2
verismo/snp__ghcb__proto_page.68.smt2
atmosphere/process_manager__spec_impl.7.smt2
atmosphere/kernel__syscall_new_proc.smt2
atmosphere/allocator__page_allocator_spec_impl.4.smt2
atmosphere/allocator__page_allocator_spec_impl.15.smt2
atmosphere/util__page_ptr_util_u.8.smt2
atmosphere/kernel__syscall_send_endpoint.smt2
atmosphere/process_manager__spec_impl.8.smt2
atmosphere/util__page_ptr_util_u.13.smt2
atmosphere/memory_manager__spec_impl.9.smt2
atmosphere/util__page_ptr_util_u.14.smt2
atmosphere/kernel__schedule_idle_cpu.smt2
atmosphere/define.43.smt2
atmosphere/process_manager__spec_impl.1.smt2
verismo/tspec__security__sectype.372.smt2
atmosphere/allocator__page_allocator_spec_impl.10.smt2
atmosphere/pagetable__pagetable_spec_impl.1.smt2
atmosphere/kernel__mem_util.2.smt2
atmosphere/memory_manager__spec_impl.2.smt2
atmosphere/pagetable__pagetable_spec_impl.11.smt2
atmosphere/define.20.smt2
atmosphere/process_manager__spec_impl.20.smt2
atmosphere/memory_manager__spec_impl.5.smt2
atmosphere/kernel__create_and_map_pages.6.smt2
atmosphere/lemma__lemma_u.1.smt2
atmosphere/kernel__create_and_share_pages.3.smt2
splinterdb/marshalling__KVPairFormat_v.1.smt2
atmosphere/process_manager__spec_impl.12.smt2
atmosphere/memory_manager__spec_impl.8.smt2
splinterdb/marshalling__ResizableUniformSizedSeq_v.9.smt2
splinterdb/marshalling__ResizableUniformSizedSeq_v.3.smt2
atmosphere/process_manager__spec_impl.26.smt2
atmosphere/pagetable__pagetable_spec_impl.7.smt2
splinterdb/marshalling__ResizableUniformSizedSeq_v.10.smt2
atmosphere/define.44.smt2
atmosphere/kernel__syscall_receive_empty.2.smt2
splinterdb/marshalling__UniformSizedSeq_v.5.smt2
splinterdb/marshalling__math_vlib_marshalling.math_v.distribute_left._01.smt2
splinterdb/marshalling__math_v.smt2
atmosphere/process_manager__spec_impl.21.smt2
splinterdb/marshalling__UniformSizedSeq_v.2.smt2
systems/page-table-smt-definitions_ulib_definitions_u.overflow_bounds._02.smt2
systems/page-table-smt-impl_u__l0.15.smt2
atmosphere/process_manager__spec_impl.19.smt2
splinterdb/marshalling__KVPairFormat_v.7.smt2
systems/mimalloc-smt-init.11.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.3.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-math.18.smt2
systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.5.smt2
systems/mimalloc-smt-commit_mask.4.smt2
systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.6.smt2
systems/page-table-smt-definitions_u.11.smt2
systems/page-table-smt-definitions_ulib_definitions_u.x86_arch_inv._01.smt2
systems/page-table-smt-definitions_t.20.smt2
splinterdb/marshalling__KVPairFormat_v.3.smt2
systems/mimalloc-smt-os_alloc.6.smt2
systems/mimalloc-smt-page_organization__PageOrg.79.smt2
systems/noderep-smt-constants.8.smt2
systems/mimalloc-smt-page_organization__PageOrg.40.smt2
systems/mimalloc-smt-pagelib_page.page_init._02.smt2
systems/mimalloc-smt-bin_sizes.47.smt2
systems/mimalloc-smt-tokens__Mim.3.smt2
systems/mimalloc-smt-tokens__Mim.27.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.12.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.10.smt2
systems/page-table-smt-impl_u__l2_refinement.5.smt2
systems/page-table-smt-impl_u__l2_refinement.1.smt2
systems/page-table-smt-impl_u__l2_impl__PT.10.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_fundamental_div_mod_converse_helper_1._01.smt2
systems/mimalloc-smt-types.4.smt2
systems/noderep-smt-exec__log.20.smt2
systems/page-table-smt-impl_u__l1.35.smt2
systems/page-table-smt-spec_t__hardware.1.smt2
systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.17.smt2
systems/page-table-smt-spec_t__hardware.17.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.10.smt2
systems/ironkv-smt-verus_extra__seq_lib_v.15.smt2
systems/page-table-smt-extra.7.smt2
systems/page-table-smt-impl_u__l1.27.smt2
systems/mimalloc-smt-config.22.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.42.smt2
systems/page-table-smt-impl_u__l1.12.smt2
systems/mimalloc-smt-linked_list.11.smt2
systems/mimalloc-smt-tokens__Mim.32.smt2
systems/mimalloc-smt-alloc_generic.5.smt2
systems/mimalloc-smt-bin_sizes.19.smt2
systems/page-table-smt-impl_u__l2_impl.1.smt2
systems/mimalloc-smt-linked_list.39.smt2
systems/mimalloc-smt-commit_mask.35.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_is_associative._01.smt2
systems/mimalloc-smt-page_organization__PageOrg.28.smt2
systems/page-table-smt-impl_u__os_refinement.10.smt2
systems/mimalloc-smt-page_organization__PageOrg.67.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__multilogimpl_v.5.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.10.smt2
systems/mimalloc-smt-config.38.smt2
systems/mimalloc-smt-commit_mask.27.smt2
systems/mimalloc-smt-layout.22.smt2
systems/page-table-smt-impl_u__l1.34.smt2
systems/page-table-smt-extralib_extra.mod_mult_zero_implies_mod_zero._01.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_left_inequality._01.smt2
systems/page-table-smt-impl_u__l1.47.smt2
systems/mimalloc-smt-linked_list.22.smt2
systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.23.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.24.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-root.smt2
systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.3.smt2
systems/noderep-smt-exec__replica.6.smt2
systems/mimalloc-smt-types.51.smt2
systems/mimalloc-smt-layout.13.smt2
systems/mimalloc-smt-init.12.smt2
systems/mimalloc-smt-tokens__Mim.20.smt2
systems/mimalloc-smt-init.10.smt2
systems/mimalloc-smt-tokens__Mim.1.smt2
systems/mimalloc-smt-alloc_generic__page_free_list_extendlib_alloc_generic.page_free_list_extend._06.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-math.2.smt2
systems/mimalloc-smt-types.19.smt2
systems/page-table-smt-impl_u__l1__impl_%1__lemma_resolve_refines.smt2
systems/mimalloc-smt-page_organization__PageOrg.88.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-main_t.4.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-math.5.smt2
systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.30.smt2
systems/noderep-smt-exec__replica.12.smt2
systems/page-table-smt-spec_t__hardware.6.smt2
systems/page-table-smt-extralib_extra.mult_leq_mono_both._01.smt2
systems/noderep-smt-exec__replica.1.smt2
systems/noderep-smt-exec__replica.19.smt2
systems/page-table-smt-impl_u__l1.41.smt2
systems/page-table-smt-impl_u__l1.13.smt2
systems/noderep-smt-exec.1.smt2
systems/mimalloc-smt-commit_mask.23.smt2
systems/mimalloc-smt-linked_list.4.smt2
systems/mimalloc-smt-config.15.smt2
systems/mimalloc-smt-segment__segment_page_clear.smt2
systems/page-table-smt-impl_u__l0.14.smt2
systems/mimalloc-smt-commit_segment.1.smt2
systems/page-table-smt-extralib_extra.aligned_transitive._02.smt2
systems/mimalloc-smt-linked_list.21.smt2
systems/mimalloc-smt-types.11.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.17.smt2
systems/mimalloc-smt-alloc_generic__page_free_list_extendlib_alloc_generic.page_free_list_extend._07.smt2
systems/mimalloc-smt-page_organization__PageOrg.5.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.18.smt2
systems/page-table-smt-impl_u__l2_refinement.3.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_div_equal._01.smt2
systems/noderep-smt-exec__log.10.smt2
systems/page-table-smt-impl_u__l1.42.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__start_v.2.smt2
systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.22.smt2
systems/page-table-smt-impl_u__indexinglib_impl_u.indexing.lemma_entry_base_from_index._05.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.38.smt2
systems/page-table-smt-impl_u__l0.5.smt2
systems/mimalloc-smt-types.23.smt2
systems/page-table-smt-impl_u__l1.10.smt2
systems/mimalloc-smt-bin_sizes.14.smt2
systems/mimalloc-smt-linked_list.14.smt2
systems/page-table-smt-definitions_ulib_definitions_u.impl_%3.lemma_entry_sizes_aligned._02.smt2
systems/page-table-smt-definitions_ulib_definitions_u.impl_%2.index_for_vaddr._01.smt2
systems/mimalloc-smt-segment__segment_slice_split.smt2
systems/mimalloc-smt-linked_list.26.smt2
systems/page-table-smt-extralib_extra.mul_commute._01.smt2
systems/mimalloc-smt-os_mem_util.9.smt2
systems/mimalloc-smt-page_organization__PageOrg.60.smt2
systems/page-table-smt-impl_u__l2_impl__PT.15.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.7.smt2
systems/page-table-smt-impl_u__l1.53.smt2
systems/page-table-smt-impl_u__l2_impl__PT.8.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.34.smt2
systems/mimalloc-smt-bin_sizes.10.smt2
systems/mimalloc-smt-types.44.smt2
systems/page-table-smt-spec_t__hardware.19.smt2
systems/mimalloc-smt-types.18.smt2
systems/mimalloc-smt-linked_list.16.smt2
systems/mimalloc-smt-segment__segment_span_free_coalesce_before.smt2
systems/page-table-smt-impl_u__l1__impl_%1__lemma_interp_of_entry_contains_mapping_implies_interp_aux_contains_mapping.smt2
systems/mimalloc-smt-page_organization__PageOrg.25.smt2
systems/mimalloc-smt-tokens__Mim.31.smt2
systems/page-table-smt-spec_t__hardware.2.smt2
systems/mimalloc-smt-page_organization__PageOrg.83.smt2
systems/mimalloc-smt-root.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_is_distributive._01.smt2
systems/mimalloc-smt-page_organization__PageOrg.94.smt2
systems/mimalloc-smt-linked_listlib_linked_list.impl_%2.prepend_contiguous_blocks._08.smt2
systems/mimalloc-smt-commit_segment.6.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_is_distributive_sub_other_way._01.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.1.smt2
systems/mimalloc-smt-types.24.smt2
systems/mimalloc-smt-tokens__Mim.54.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__layout_v.30.smt2
systems/page-table-smt-definitions_t.24.smt2
systems/mimalloc-smt-tokens__Mim.55.smt2
systems/page-table-smt-impl_u__indexinglib_impl_u.indexing.lemma_entry_base_from_index._01.smt2
systems/mimalloc-smt-types.45.smt2
systems/mimalloc-smt-tokens__Mim.5.smt2
systems/mimalloc-smt-segment__segment_span_allocate.1.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_is_distributive_add._01.smt2
systems/noderep-smt-exec.4.smt2
systems/mimalloc-smt-page_organization__PageOrg.45.smt2
systems/mimalloc-smt-queues__page_queue_push.smt2
systems/mimalloc-smt-alloc_generic__page_free_list_extendlib_alloc_generic.page_free_list_extend._03.smt2
systems/mimalloc-smt-pagelib_page.page_init._01.smt2
systems/mimalloc-smt-config.18.smt2
systems/mimalloc-smt-bin_sizes.33.smt2
systems/mimalloc-smt-alloc_fast.4.smt2
systems/mimalloc-smt-page_organization__PageOrg.32.smt2
systems/page-table-smt-extralib_extra.mod_less_eq._01.smt2
systems/mimalloc-smt-free.6.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__append_v.2.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__multilogimpl_v.1.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.3.smt2
systems/page-table-smt-definitions_ulib_definitions_u.impl_%2.next_entry_base._01.smt2
systems/mimalloc-smt-layout.26.smt2
systems/mimalloc-smt-tokens__Mim.40.smt2
systems/mimalloc-smt-page_organization__PageOrg.71.smt2
systems/mimalloc-smt-layout.4.smt2
systems/mimalloc-smt-layoutlib_layout.calculate_slice_page_ptr_from_block._01.smt2
systems/mimalloc-smt-layoutlib_layout.align_up._02.smt2
systems/mimalloc-smt-os_alloc.8.smt2
systems/page-table-smt-impl_u__l0.24.smt2
systems/mimalloc-smt-linked_listlib_linked_list.impl_%2.prepend_contiguous_blocks._03.smt2
systems/mimalloc-smt-alloc_generic__page_free_list_extendlib_alloc_generic.page_free_list_extend._05.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-math.28.smt2
systems/page-table-smt-extra.8.smt2
systems/mimalloc-smt-segment__segment_alloclib_segment.segment_alloc._02.smt2
systems/page-table-smt-definitions_t.11.smt2
systems/mimalloc-smt-init.1.smt2
systems/mimalloc-smt-bin_sizes.30.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.16.smt2
systems/noderep-smt-spec__cyclicbufferlib_spec.cyclicbuffer.log_entry_alive_value_wrap_around._01.smt2
systems/mimalloc-smt-alloc_generic.2.smt2
systems/mimalloc-smt-layoutlib_layout.calculate_page_block_at._02.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-main_t.7.smt2
systems/mimalloc-smt-alloc_generic.9.smt2
systems/mimalloc-smt-os_mem_util.2.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.50.smt2
systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.1.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__layout_v.31.smt2
systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.11.smt2
systems/mimalloc-smt-config.21.smt2
systems/page-table-smt-spec_t__hardware.4.smt2
systems/noderep-smt-root.5.smt2
systems/noderep-smt-exec__replica.4.smt2
systems/mimalloc-smt-config.27.smt2
systems/page-table-smt-definitions_ulib_definitions_u.impl_%3.lemma_entry_sizes_increase._01.smt2
systems/page-table-smt-definitions_t.15.smt2
systems/mimalloc-smt-os_commit.2.smt2
systems/mimalloc-smt-linked_listlib_linked_list.impl_%2.prepend_contiguous_blocks._09.smt2
systems/page-table-smt-impl_u__l0.6.smt2
systems/mimalloc-smt-page_organization__PageOrg.68.smt2
systems/mimalloc-smt-os_mem_util.16.smt2
systems/page-table-smt-impl_u__l0.19.smt2
systems/mimalloc-smt-commit_mask.2.smt2
systems/noderep-smt-constants.3.smt2
systems/mimalloc-smt-linked_list.13.smt2
systems/noderep-smt-constants.6.smt2
systems/mimalloc-smt-alloc_generic__page_free_list_extendlib_alloc_generic.page_free_list_extend._09.smt2
systems/mimalloc-smt-linked_list.3.smt2
systems/page-table-smt-impl_u__l1.33.smt2
systems/noderep-smt-spec__cyclicbuffer.4.smt2
systems/page-table-smt-impl_u__l1__impl_%1__lemma_no_mapping_in_interp_of_entry_implies_no_mapping_in_interp.smt2
systems/mimalloc-smt-alloc_fast.3.smt2
systems/page-table-smt-impl_u__l2_impl.14.smt2
systems/page-table-smt-impl_u__l1.7.smt2
systems/mimalloc-smt-commit_mask.6.smt2
systems/mimalloc-smt-page_organization__PageOrg.51.smt2
systems/mimalloc-smt-types.15.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.32.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_fundamental_div_mod_converse_helper_2._01.smt2
systems/noderep-smt-exec__log.14.smt2
systems/noderep-smt-exec__replica.11.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.9.smt2
systems/mimalloc-smt-types.36.smt2
systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.28.smt2
systems/page-table-smt-impl_u__indexinglib_impl_u.indexing.lemma_entry_base_from_index_support._02.smt2
systems/mimalloc-smt-bin_sizes.40.smt2
systems/mimalloc-smt-bin_sizes.45.smt2
systems/mimalloc-smt-linked_listlib_linked_list.impl_%2.prepend_contiguous_blocks._06.smt2
systems/mimalloc-smt-page_organization__PageOrg.7.smt2
systems/mimalloc-smt-os_mem_utillib_os_mem_util.preserves_mem_chunk_good_on_transfer_to_capacity._02.smt2
systems/mimalloc-smt-layout__align_downlib_layout.align_down._03.smt2
systems/mimalloc-smt-os_mem_util.5.smt2
systems/mimalloc-smt-os_mem_util.19.smt2
systems/mimalloc-smt-alloc_generic__page_free_list_extendlib_alloc_generic.page_free_list_extend._04.smt2
systems/page-table-smt-impl_u__l1lib_impl_u.l1.impl_%1.lemma_ranges_disjoint_interp_aux_interp_of_entry._01.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__layout_v.27.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-math.16.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__multilogimpl_v.9.smt2
systems/mimalloc-smt-tokens__Mim.51.smt2
systems/mimalloc-smt-commit_mask.1.smt2
systems/mimalloc-smt-types.35.smt2
systems/mimalloc-smt-layout.27.smt2
systems/page-table-smt-impl_u__l2_impl.10.smt2
systems/noderep-smt-spec__cyclicbuffer.5.smt2
systems/mimalloc-smt-bin_sizes.1.smt2
systems/mimalloc-smt-page.15.smt2
systems/ironkv-smt-verus_extra__seq_lib_vlib_verus_extra.seq_lib_v.lemma_seq_fold_left_sum_le._01.smt2
systems/mimalloc-smt-page_organization__PageOrg.16.smt2
verismo/boot__linux.37.smt2
systems/mimalloc-smt-page_organization__PageOrg.29.smt2
systems/mimalloc-smt-page_organization__PageOrg.35.smt2
systems/mimalloc-smt-config.28.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__layout_v.26.smt2
systems/mimalloc-smt-page_organization__PageOrg.65.smt2
systems/mimalloc-smt-init.13.smt2
systems/noderep-smt-exec__log.7.smt2
systems/page-table-smt-impl_u__l2_impl__PT.28.smt2
systems/mimalloc-smt-page_organization__PageOrg.78.smt2
systems/mimalloc-smt-tokens__Mim.11.smt2
systems/mimalloc-smt-layout.17.smt2
systems/noderep-smt-exec__log.16.smt2
systems/page-table-smt-impl_u__l0.23.smt2
systems/mimalloc-smt-config.17.smt2
systems/mimalloc-smt-types.3.smt2
systems/mimalloc-smt-tokens__Mim.53.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-math.15.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-math.7.smt2
systems/mimalloc-smt-os_mem_util.10.smt2
systems/mimalloc-smt-os_mem_util.15.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.12.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.7.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.2.smt2
systems/page-table-smt-definitions_t.25.smt2
systems/page-table-smt-definitions_t.18.smt2
systems/mimalloc-smt-types.42.smt2
systems/page-table-smt-definitions_ulib_definitions_u.impl_%2.next_entry_base._02.smt2
systems/mimalloc-smt-bin_sizeslib_bin_sizes.mod8._01.smt2
systems/noderep-smt-exec__log.1.smt2
systems/mimalloc-smt-commit_mask.5.smt2
systems/mimalloc-smt-tokens__Mim.19.smt2
systems/mimalloc-smt-layout__align_downlib_layout.align_down._02.smt2
systems/mimalloc-smt-os_mem_utillib_os_mem_util.preserves_mem_chunk_good_except._01.smt2
systems/mimalloc-smt-page_organization__PageOrg.56.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.51.smt2
systems/page-table-smt-impl_u__l2_refinement.4.smt2
systems/mimalloc-smt-layout__align_down.smt2
systems/page-table-smt-extralib_extra.lemma_aligned_iff_eq_mul_div._01.smt2
systems/page-table-smt-impl_u__l1lib_impl_u.l1.impl_%1.lemma_interp_of_entries_disjoint._04.smt2
systems/page-table-smt-extra.1.smt2
systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.10.smt2
systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.32.smt2
systems/mimalloc-smt-config.24.smt2
systems/page-table-smt-extralib_extra.mult_less_mono_both2._01.smt2
systems/noderep-smt-exec__replica.13.smt2
systems/mimalloc-smt-bin_sizes.31.smt2
systems/mimalloc-smt-bin_sizes.41.smt2
systems/mimalloc-smt-bin_sizes.42.smt2
systems/page-table-smt-impl_u__indexinglib_impl_u.indexing.lemma_index_from_base_and_addr._01.smt2
systems/mimalloc-smt-types.2.smt2
systems/mimalloc-smt-os_alloc.3.smt2
systems/mimalloc-smt-os_mem_util.3.smt2
systems/mimalloc-smt-queues.3.smt2
systems/mimalloc-smt-free.3.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.18.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.33.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_mul_one_to_one._01.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.9.smt2
systems/page-table-smt-extra.3.smt2
systems/page-table-smt-impl_u__l2_impl__PT.18.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__setup_v.6.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.15.smt2
systems/mimalloc-smt-layout__block_ptr_aligned_to_word.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-mathmain_math.lemma_small_mod._01.smt2
systems/page-table-smt-impl_u__l2_impl.5.smt2
systems/page-table-smt-impl_u__l1.3.smt2
systems/mimalloc-smt-config.23.smt2
systems/mimalloc-smt-types.37.smt2
systems/page-table-smt-impl_u__l2_impl__PT.5.smt2
systems/noderep-smt-spec__cyclicbuffer__CyclicBuffer.16.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.4.smt2
systems/page-table-smt-spec_t__hardware.21.smt2
systems/page-table-smt-extralib_extra.mult_leq_mono2._01.smt2
systems/noderep-smt-exec__log.8.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__multilogimpl_v.12.smt2
systems/mimalloc-smt-bin_sizeslib_bin_sizes.lemma_div_is_ordered._01.smt2
systems/mimalloc-smt-layout.12.smt2
systems/mimalloc-smt-commit_mask.31.smt2
systems/mimalloc-smt-layout.21.smt2
systems/mimalloc-smt-layoutlib_layout.bitand_with_mask_gives_rounding._09.smt2
systems/mimalloc-smt-tokens__Mim.26.smt2
systems/mimalloc-smt-linked_list.32.smt2
systems/page-table-smt-definitions_u.1.smt2
systems/mimalloc-smt-commit_mask.17.smt2
systems/mimalloc-smt-config.32.smt2
systems/page-table-smt-definitions_ulib_definitions_u.impl_%2.entry_base._01.smt2
systems/mimalloc-smt-layout.19.smt2
systems/ironkv-smt-verus_extra__seq_lib_v.5.smt2
systems/mimalloc-smt-config.36.smt2
systems/mimalloc-smt-segment__segments_page_find_and_allocate.3.smt2
systems/mimalloc-smt-queues__page_queue_push_back.smt2
systems/noderep-smt-exec__log.3.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.15.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.17.smt2
systems/mimalloc-smt-commit_mask.13.smt2
systems/mimalloc-smt-linked_list.9.smt2
systems/mimalloc-smt-bin_sizes.35.smt2
systems/noderep-smt-exec.3.smt2
systems/page-table-smt-definitions_t.13.smt2
systems/mimalloc-smt-page_organization__PageOrg.19.smt2
systems/mimalloc-smt-page_organization__PageOrg.22.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-math.10.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-multilog__layout_v.32.smt2
systems/page-table-smt-extralib_extra.lemma_aligned_iff_eq_mul_div._02.smt2
systems/mimalloc-smt-linked_listlib_linked_list.impl_%2.prepend_contiguous_blocks._05.smt2
systems/page-table-smt-impl_u__l1.45.smt2
systems/mimalloc-smt-types.30.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__layout_v.30.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-math.20.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-pmem__pmcopy_t.3.smt2
systems/mimalloc-smt-tokens__Mim.47.smt2
systems/mimalloc-smt-tokens__Mim.6.smt2
systems/page-table-smt-impl_u__l1.20.smt2
systems/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.15.smt2
systems/page-table-smt-definitions_t.22.smt2
systems/mimalloc-smt-layout.6.smt2
systems/mimalloc-smt-commit_mask.11.smt2
systems/mimalloc-smt-page.8.smt2
systems/mimalloc-smt-layout__two_mul_with_bit1lib_layout.two_mul_with_bit1._01.smt2
systems/mimalloc-smt-bin_sizes.12.smt2
systems/mimalloc-smt-linked_list.24.smt2
systems/mimalloc-smt-tokens__Mim.16.smt2
systems/page-table-smt-impl_u__l2_impl__PT.1.smt2
systems/mimalloc-smt-segment.5.smt2
systems/page-table-smt-impl_u__os_refinement.1.smt2
systems/verified-storage-smt-verified-storage-smt-pmemlog-logimpl_v.37.smt2
systems/page-table-smt-spec_t__hardware.7.smt2
systems/mimalloc-smt-tokens__Mim.52.smt2
systems/mimalloc-smt-tokens__Mim.56.smt2
systems/mimalloc-smt-layout__two_mul_with_bit1.smt2
systems/page-table-smt-impl_u__l1.22.smt2
systems/mimalloc-smt-os_mem_util.11.smt2
systems/mimalloc-smt-page_organization__PageOrg.64.smt2
systems/mimalloc-smt-page_organization__PageOrg.39.smt2
systems/mimalloc-smt-page.16.smt2
systems/mimalloc-smt-page_organization__PageOrg.8.smt2
systems/mimalloc-smt-tokens__Mim.39.smt2
systems/mimalloc-smt-page_organization__PageOrg.33.smt2