SMT-LIB · hansjoergschurr · Apr 17, 2025 · Apr 13, 2025 · Apr 13, 2025 · Apr 16, 2025
diff --git a/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._01.smt2 b/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._01.smt2
diff --git a/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._05.smt2 b/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._05.smt2
diff --git a/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._06.smt2 b/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._06.smt2
diff --git a/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._07.smt2 b/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._07.smt2
diff --git a/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._12.smt2 b/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._12.smt2
diff --git a/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._16.smt2 b/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._16.smt2
diff --git a/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._25.smt2 b/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._25.smt2
diff --git a/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._32.smt2 b/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._32.smt2
diff --git a/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._35.smt2 b/...A/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.page_entry2usize._35.smt2
diff --git a/...UFBVDTLIA/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.usize2pa._01.smt2 b/...UFBVDTLIA/20241211-verus/atmosphere/pagetable__entrylib_pagetable.entry.usize2pa._01.smt2
diff --git a/...41211-verus/atmosphere/pagetable__entrylib_pagetable.entry.usize2page_entry_perm._01.smt2 b/...41211-verus/atmosphere/pagetable__entrylib_pagetable.entry.usize2page_entry_perm._01.smt2
diff --git a/...41211-verus/atmosphere/pagetable__entrylib_pagetable.entry.usize2page_entry_perm._03.smt2 b/...41211-verus/atmosphere/pagetable__entrylib_pagetable.entry.usize2page_entry_perm._03.smt2
diff --git a/...41211-verus/atmosphere/pagetable__entrylib_pagetable.entry.usize2page_entry_perm._04.smt2 b/...41211-verus/atmosphere/pagetable__entrylib_pagetable.entry.usize2page_entry_perm._04.smt2
diff --git a/...41211-verus/atmosphere/pagetable__entrylib_pagetable.entry.usize2page_entry_perm._05.smt2 b/...41211-verus/atmosphere/pagetable__entrylib_pagetable.entry.usize2page_entry_perm._05.smt2
diff --git a/...us/atmosphere/pagetable__entrylib_pagetable.entry.zero_leads_is_empty_page_entry._01.smt2 b/...us/atmosphere/pagetable__entrylib_pagetable.entry.zero_leads_is_empty_page_entry._01.smt2
diff --git a/...us/atmosphere/pagetable__entrylib_pagetable.entry.zero_leads_is_empty_page_entry._03.smt2 b/...us/atmosphere/pagetable__entrylib_pagetable.entry.zero_leads_is_empty_page_entry._03.smt2
diff --git a/...us/atmosphere/pagetable__entrylib_pagetable.entry.zero_leads_is_empty_page_entry._06.smt2 b/...us/atmosphere/pagetable__entrylib_pagetable.entry.zero_leads_is_empty_page_entry._06.smt2
diff --git a/...241211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_auto._01.smt2 b/...241211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_auto._01.smt2
diff --git a/...0241211-verus/verussystems/mimalloc-smt-flagslib_flags.impl_%0.get_retire_expire._01.smt2 b/...0241211-verus/verussystems/mimalloc-smt-flagslib_flags.impl_%0.get_retire_expire._01.smt2
diff --git a/...TLIA/20241211-verus/verussystems/mimalloc-smt-flagslib_flags.impl_%0.set_in_full._01.smt2 b/...TLIA/20241211-verus/verussystems/mimalloc-smt-flagslib_flags.impl_%0.set_in_full._01.smt2
diff --git a/...20241211-verus/verussystems/mimalloc-smt-flagslib_flags.impl_%0.set_is_committed._01.smt2 b/...20241211-verus/verussystems/mimalloc-smt-flagslib_flags.impl_%0.set_is_committed._01.smt2
diff --git a/...20241211-verus/verussystems/mimalloc-smt-flagslib_flags.impl_%0.set_is_committed._02.smt2 b/...20241211-verus/verussystems/mimalloc-smt-flagslib_flags.impl_%0.set_is_committed._02.smt2
diff --git a/...20241211-verus/verussystems/mimalloc-smt-flagslib_flags.impl_%0.set_is_zero_init._03.smt2 b/...20241211-verus/verussystems/mimalloc-smt-flagslib_flags.impl_%0.set_is_zero_init._03.smt2
diff --git a/...0241211-verus/verussystems/mimalloc-smt-flagslib_flags.impl_%0.set_retire_expire._02.smt2 b/...0241211-verus/verussystems/mimalloc-smt-flagslib_flags.impl_%0.set_retire_expire._02.smt2
diff --git a/...0241211-verus/atmosphere/util__page_ptr_util_ulib_util.page_ptr_util_u.v2l3index._01.smt2 b/...0241211-verus/atmosphere/util__page_ptr_util_ulib_util.page_ptr_util_u.v2l3index._01.smt2
diff --git a/...0241211-verus/atmosphere/util__page_ptr_util_ulib_util.page_ptr_util_u.v2l4index._01.smt2 b/...0241211-verus/atmosphere/util__page_ptr_util_ulib_util.page_ptr_util_u.v2l4index._01.smt2
diff --git a/...us/verismo/allocator__bit_pverismo_allocator.bit_p.lemma_get_low_bits_via_bit_op._02.smt2 b/...us/verismo/allocator__bit_pverismo_allocator.bit_p.lemma_get_low_bits_via_bit_op._02.smt2
diff --git a/...smo/arch__pgtable__entry_pverismo_arch.pgtable.entry_p.impl_%0.lemma_size_offset._01.smt2 b/...smo/arch__pgtable__entry_pverismo_arch.pgtable.entry_p.impl_%0.lemma_size_offset._01.smt2
diff --git a/.../verismo/arch__pgtable__entry_pverismo_arch.pgtable.entry_p.lemma_pt_entry_count._01.smt2 b/.../verismo/arch__pgtable__entry_pverismo_arch.pgtable.entry_p.lemma_pt_entry_count._01.smt2
diff --git a/...DTNIA/20241211-verus/verismo/debug__ghcb_printverismo_debug.ghcb_print.int2bytes._01.smt2 b/...DTNIA/20241211-verus/verismo/debug__ghcb_printverismo_debug.ghcb_print.int2bytes._01.smt2
diff --git a/...FBVDTNIA/20241211-verus/verismo/security__memverismo_security.mem.impl_%16.empty._01.smt2 b/...FBVDTNIA/20241211-verus/verismo/security__memverismo_security.mem.impl_%16.empty._01.smt2
diff --git a/...UFBVDTNIA/20241211-verus/verismo/snp__cpu__gdtverismo_snp.cpu.gdt.impl_%16.empty._01.smt2 b/...UFBVDTNIA/20241211-verus/verismo/snp__cpu__gdtverismo_snp.cpu.gdt.impl_%16.empty._01.smt2
diff --git a/...BVDTNIA/20241211-verus/verismo/snp__cpu__vmsaverismo_snp.cpu.vmsa.impl_%16.empty._01.smt2 b/...BVDTNIA/20241211-verus/verismo/snp__cpu__vmsaverismo_snp.cpu.vmsa.impl_%16.empty._01.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._02.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._02.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._11.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._11.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._17.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._17.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._19.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._19.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._21.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._21.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._28.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._28.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._30.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._30.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._34.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._34.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._41.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._41.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._45.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._45.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._46.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._46.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._49.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._49.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._52.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._52.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._56.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._56.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._58.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._58.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._59.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._59.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._60.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._60.smt2
diff --git a/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._64.smt2 b/...rus/verismo/tspec__math__align_sverismo_tspec.math.align_s.lemma_bit_and_mod_rel._64.smt2
diff --git a/...11-verus/verismo/tspec__math__align_sverismo_tspec.math.align_s.proof_align_down._03.smt2 b/...11-verus/verismo/tspec__math__align_sverismo_tspec.math.align_s.proof_align_down._03.smt2
diff --git a/...1-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_property_auto._01.smt2 b/...1-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_property_auto._01.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._04.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._04.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._05.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._05.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._06.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._06.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._11.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._11.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._18.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._18.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._19.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._19.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._23.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._23.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._24.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._24.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._25.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._25.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._27.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._27.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._28.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._28.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._37.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._37.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._38.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._38.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._40.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._40.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._48.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._48.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._51.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._51.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._55.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._55.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._56.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._56.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._59.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._59.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._62.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shl_mul_rel._62.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._01.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._01.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._03.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._03.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._04.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._04.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._07.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._07.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._11.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._11.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._13.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._13.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._14.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._14.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._17.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._17.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._18.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._18.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._22.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._22.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._24.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._24.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._25.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._25.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._27.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._27.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._31.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._31.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._33.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._33.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._34.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._34.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._36.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._36.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._44.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._44.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._47.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._47.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._49.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._49.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._50.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._50.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._52.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._52.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._54.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._54.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._55.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._55.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._57.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._57.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._61.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._61.smt2
diff --git a/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._62.smt2 b/...211-verus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.bit64_shr_div_rel._62.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._02.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._02.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._06.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._06.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._07.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._07.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._10.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._10.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._12.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._12.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._14.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._14.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._19.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._19.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._23.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._23.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._26.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._26.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._27.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._27.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._31.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._31.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._32.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._32.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._35.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._35.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._39.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._39.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._44.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._44.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._45.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._45.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._48.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._48.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._50.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._50.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._55.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._55.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._56.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._56.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._57.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._57.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._58.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._58.smt2
diff --git a/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._62.smt2 b/...rus/verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_and_rel_mod._62.smt2
diff --git a/...ismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_clear_set_property._01.smt2 b/...ismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit64_clear_set_property._01.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._02.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._02.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._04.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._04.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._05.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._05.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._07.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._07.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._11.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._11.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._12.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._12.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._14.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._14.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._16.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._16.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._19.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._19.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._28.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._28.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._30.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._30.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._33.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._33.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._34.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._34.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._36.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._36.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._38.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._38.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._40.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._40.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._44.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._44.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._49.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._49.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._51.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._51.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._54.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._54.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._56.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._56.smt2
diff --git a/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._58.smt2 b/...verismo/tspec__math__bits_pverismo_tspec.math.bits_p.proof_bit_usize_and_rel_mod._58.smt2
diff --git a/...211-verus/verismo/tspec__math__integerverismo_tspec.math.integer.lemma_fill_ones._02.smt2 b/...211-verus/verismo/tspec__math__integerverismo_tspec.math.integer.lemma_fill_ones._02.smt2
diff --git a/...211-verus/verismo/tspec__math__integerverismo_tspec.math.integer.lemma_fill_ones._06.smt2 b/...211-verus/verismo/tspec__math__integerverismo_tspec.math.integer.lemma_fill_ones._06.smt2
diff --git a/.../verismo/tspec__math__integerverismo_tspec.math.integer.lemma_fill_ones_bit_step._03.smt2 b/.../verismo/tspec__math__integerverismo_tspec.math.integer.lemma_fill_ones_bit_step._03.smt2
diff --git a/...s/verismo/tspec__math__integerverismo_tspec.math.integer.lemma_next_power_of_two._02.smt2 b/...s/verismo/tspec__math__integerverismo_tspec.math.integer.lemma_next_power_of_two._02.smt2
diff --git a/...s/verismo/tspec__math__integerverismo_tspec.math.integer.lemma_prev_power_of_two._01.smt2 b/...s/verismo/tspec__math__integerverismo_tspec.math.integer.lemma_prev_power_of_two._01.smt2
diff --git a/...s/verismo/tspec__math__integerverismo_tspec.math.integer.lemma_prev_power_of_two._02.smt2 b/...s/verismo/tspec__math__integerverismo_tspec.math.integer.lemma_prev_power_of_two._02.smt2
diff --git a/...s/verismo/tspec__math__integerverismo_tspec.math.integer.lemma_prev_power_of_two._03.smt2 b/...s/verismo/tspec__math__integerverismo_tspec.math.integer.lemma_prev_power_of_two._03.smt2
diff --git a/...1211-verus/verismo/tspec__math__pow_pverismo_tspec.math.pow_p.proof_pow2_to_bits._02.smt2 b/...1211-verus/verismo/tspec__math__pow_pverismo_tspec.math.pow_p.proof_pow2_to_bits._02.smt2
diff --git a/..._security__sectype_test__pverismo_tspec.security.sectype_test.p.proof_test_bits2._01.smt2 b/..._security__sectype_test__pverismo_tspec.security.sectype_test.p.proof_test_bits2._01.smt2
@@ -0,0 +1,208 @@
+(set-info :smt-lib-version 2.6)
+(set-logic UFBVDTNIA)
+(set-info :source |
+Generated by: Amar Shah
+Generated on: 2024-12-11
+Generator: Verus
+Application: Verification of Rust Program
+Target solver: z3
+Time limit: 10
+Benchmarks generated by the Rust verifier Verus (https://verus-lang.github.io/verus/guide/) on the project Verismo (https://www.usenix.org/conference/osdi24/presentation/zhou) 
+and processed using Mariposa (https://github.com/secure-foundations/mariposa).
+ z3 solves this without nonlinear, but it cannot be expressed in SMTLib without a nonlinear theory.
+This benchmarks was originally run with z3 with the following options:
+    (set-option :auto_config false)
+    (set-option :smt.mbqi false)
+    (set-option :smt.case_split 3)
+    (set-option :smt.qi.eager_threshold 100.0)
+    (set-option :smt.delay_units true)
+    (set-option :smt.arith.solver 2)
+    (set-option :smt.arith.nl false)
+    (set-option :pi.enabled false)
+    (set-option :rewriter.sort_disjunctions false)
+    (set-option :sat.euf true)
+    (set-option :tactic.default_tactic sat)
+    (set-option :smt.ematching false)
+    (set-option :smt.case_split 0)
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-sort %%Function%% 0)
+(declare-sort FuelId 0)
+(declare-sort Fuel 0)
+(declare-const zero Fuel)
+(declare-fun succ (Fuel) Fuel)
+(declare-fun fuel_bool (FuelId) Bool)
+(declare-fun fuel_bool_default (FuelId) Bool)
+(declare-const fuel_defaults Bool)
+(assert (=> fuel_defaults (forall ((id FuelId)) (! (= (fuel_bool id) (fuel_bool_default id)) :pattern ((fuel_bool id))))))
+(declare-sort Char 0)
+(declare-fun char%from_unicode (Int) Char)
+(declare-fun char%to_unicode (Char) Int)
+(declare-sort StrSlice 0)
+(declare-fun str%strslice_is_ascii (StrSlice) Bool)
+(declare-fun str%strslice_len (StrSlice) Int)
+(declare-fun str%strslice_get_char (StrSlice Int) Char)
+(declare-fun str%new_strlit (Int) StrSlice)
+(declare-fun str%from_strlit (StrSlice) Int)
+(declare-datatypes ((fndef 0)) (((fndef_singleton ))))
+(declare-sort Poly 0)
+(declare-sort Height 0)
+(declare-fun I (Int) Poly)
+(declare-fun B (Bool) Poly)
+(declare-fun F (fndef) Poly)
+(declare-fun %I (Poly) Int)
+(declare-fun %B (Poly) Bool)
+(declare-fun %F (Poly) fndef)
+(declare-fun S (StrSlice) Poly)
+(declare-fun %S (Poly) StrSlice)
+(declare-fun C (Char) Poly)
+(declare-fun %C (Poly) Char)
+(declare-sort Type 0)
+(declare-const BOOL Type)
+(declare-const INT Type)
+(declare-const NAT Type)
+(declare-const STRSLICE Type)
+(declare-const CHAR Type)
+(declare-fun UINT (Int) Type)
+(declare-fun SINT (Int) Type)
+(declare-fun CONST_INT (Int) Type)
+(declare-sort Dcr 0)
+(declare-const $ Dcr)
+(declare-fun REF (Dcr) Dcr)
+(declare-fun MUT_REF (Dcr) Dcr)
+(declare-fun BOX (Dcr) Dcr)
+(declare-fun RC (Dcr) Dcr)
+(declare-fun ARC (Dcr) Dcr)
+(declare-fun GHOST (Dcr) Dcr)
+(declare-fun TRACKED (Dcr) Dcr)
+(declare-fun NEVER (Dcr) Dcr)
+(declare-fun ARRAY (Dcr Type Dcr Type) Type)
+(declare-fun SLICE (Dcr Type) Type)
+(declare-fun has_type (Poly Type) Bool)
+(declare-fun as_type (Poly Type) Poly)
+(declare-fun mk_fun (%%Function%%) %%Function%%)
+(declare-fun const_int (Type) Int)
+(assert (forall ((i Int)) (! (= i (const_int (CONST_INT i))) :pattern ((CONST_INT i)))))
+(assert (forall ((b Bool)) (! (has_type (B b) BOOL) :pattern ((has_type (B b) BOOL)))))
+(assert (forall ((x Poly) (t Type)) (! (and (has_type (as_type x t) t) (=> (has_type x t) (= x (as_type x t)))) :pattern ((as_type x t)))))
+(assert (forall ((x %%Function%%)) (! (= (mk_fun x) x) :pattern ((mk_fun x)))))
+(assert (forall ((x Bool)) (! (= x (%B (B x))) :pattern ((B x)))))
+(assert (forall ((x Int)) (! (= x (%I (I x))) :pattern ((I x)))))
+(assert (forall ((x Poly)) (! (=> (has_type x BOOL) (= x (B (%B x)))) :pattern ((has_type x BOOL)))))
+(assert (forall ((x Poly)) (! (=> (has_type x INT) (= x (I (%I x)))) :pattern ((has_type x INT)))))
+(assert (forall ((x Poly)) (! (=> (has_type x NAT) (= x (I (%I x)))) :pattern ((has_type x NAT)))))
+(assert (forall ((bits Int) (x Poly)) (! (=> (has_type x (UINT bits)) (= x (I (%I x)))) :pattern ((has_type x (UINT bits))))))
+(assert (forall ((bits Int) (x Poly)) (! (=> (has_type x (SINT bits)) (= x (I (%I x)))) :pattern ((has_type x (SINT bits))))))
+(assert (forall ((x Int)) (! (= (str%from_strlit (str%new_strlit x)) x) :pattern ((str%new_strlit x)))))
+(assert (forall ((x Poly)) (! (=> (has_type x STRSLICE) (= x (S (%S x)))) :pattern ((has_type x STRSLICE)))))
+(assert (forall ((x StrSlice)) (! (= x (%S (S x))) :pattern ((S x)))))
+(assert (forall ((x StrSlice)) (! (has_type (S x) STRSLICE) :pattern ((has_type (S x) STRSLICE)))))
+(declare-fun ext_eq (Bool Type Poly Poly) Bool)
+(assert (forall ((deep Bool) (t Type) (x Poly) (y Poly)) (! (= (= x y) (ext_eq deep t x y)) :pattern ((ext_eq deep t x y)))))
+(declare-const SZ Int)
+(assert (= SZ 64))
+(declare-fun uHi (Int) Int)
+(declare-fun iLo (Int) Int)
+(declare-fun iHi (Int) Int)
+(assert (= (uHi 8) 256))
+(assert (= (uHi 16) 65536))
+(assert (= (uHi 32) 4294967296))
+(assert (= (uHi 64) 18446744073709551616))
+(assert (= (uHi 128) (+ 1 340282366920938463463374607431768211455)))
+(assert (= (iLo 8) (- 128)))
+(assert (= (iLo 16) (- 32768)))
+(assert (= (iLo 32) (- 2147483648)))
+(assert (= (iLo 64) (- 9223372036854775808)))
+(assert (= (iLo 128) (- 170141183460469231731687303715884105728)))
+(assert (= (iHi 8) 128))
+(assert (= (iHi 16) 32768))
+(assert (= (iHi 32) 2147483648))
+(assert (= (iHi 64) 9223372036854775808))
+(assert (= (iHi 128) 170141183460469231731687303715884105728))
+(declare-fun nClip (Int) Int)
+(declare-fun uClip (Int Int) Int)
+(declare-fun iClip (Int Int) Int)
+(assert (forall ((i Int)) (! (and (<= 0 (nClip i)) (=> (<= 0 i) (= i (nClip i)))) :pattern ((nClip i)))))
+(assert (forall ((bits Int) (i Int)) (! (and (<= 0 (uClip bits i)) (< (uClip bits i) (uHi bits)) (=> (and (<= 0 i) (< i (uHi bits))) (= i (uClip bits i)))) :pattern ((uClip bits i)))))
+(assert (forall ((bits Int) (i Int)) (! (and (<= (iLo bits) (iClip bits i)) (< (iClip bits i) (iHi bits)) (=> (and (<= (iLo bits) i) (< i (iHi bits))) (= i (iClip bits i)))) :pattern ((iClip bits i)))))
+(declare-fun uInv (Int Int) Bool)
+(declare-fun iInv (Int Int) Bool)
+(assert (forall ((bits Int) (i Int)) (! (= (uInv bits i) (and (<= 0 i) (< i (uHi bits)))) :pattern ((uInv bits i)))))
+(assert (forall ((bits Int) (i Int)) (! (= (iInv bits i) (and (<= (iLo bits) i) (< i (iHi bits)))) :pattern ((iInv bits i)))))
+(assert (forall ((x Int)) (! (has_type (I x) INT) :pattern ((has_type (I x) INT)))))
+(assert (forall ((x Int)) (! (=> (<= 0 x) (has_type (I x) NAT)) :pattern ((has_type (I x) NAT)))))
+(assert (forall ((bits Int) (x Int)) (! (=> (uInv bits x) (has_type (I x) (UINT bits))) :pattern ((has_type (I x) (UINT bits))))))
+(assert (forall ((bits Int) (x Int)) (! (=> (iInv bits x) (has_type (I x) (SINT bits))) :pattern ((has_type (I x) (SINT bits))))))
+(assert (forall ((x Poly)) (! (=> (has_type x NAT) (<= 0 (%I x))) :pattern ((has_type x NAT)))))
+(assert (forall ((bits Int) (x Poly)) (! (=> (has_type x (UINT bits)) (uInv bits (%I x))) :pattern ((has_type x (UINT bits))))))
+(assert (forall ((bits Int) (x Poly)) (! (=> (has_type x (SINT bits)) (iInv bits (%I x))) :pattern ((has_type x (SINT bits))))))
+(declare-fun Add (Int Int) Int)
+(declare-fun Sub (Int Int) Int)
+(declare-fun Mul (Int Int) Int)
+(declare-fun EucDiv (Int Int) Int)
+(declare-fun EucMod (Int Int) Int)
+(assert (forall ((x Int) (y Int)) (! (= (Add x y) (+ x y)) :pattern ((Add x y)))))
+(assert (forall ((x Int) (y Int)) (! (= (Sub x y) (- x y)) :pattern ((Sub x y)))))
+(assert (forall ((x Int) (y Int)) (! (= (Mul x y) (* x y)) :pattern ((Mul x y)))))
+(assert (forall ((x Int) (y Int)) (! (= (EucDiv x y) (div x y)) :pattern ((EucDiv x y)))))
+(assert (forall ((x Int) (y Int)) (! (= (EucMod x y) (mod x y)) :pattern ((EucMod x y)))))
+(assert (forall ((x Int) (y Int)) (! (=> (and (<= 0 x) (<= 0 y)) (<= 0 (Mul x y))) :pattern ((Mul x y)))))
+(assert (forall ((x Int) (y Int)) (! (=> (and (<= 0 x) (< 0 y)) (and (<= 0 (EucDiv x y)) (<= (EucDiv x y) x))) :pattern ((EucDiv x y)))))
+(assert (forall ((x Int) (y Int)) (! (=> (and (<= 0 x) (< 0 y)) (and (<= 0 (EucMod x y)) (< (EucMod x y) y))) :pattern ((EucMod x y)))))
+(assert (forall ((x Poly)) (! (=> (has_type x CHAR) (= x (C (%C x)))) :pattern ((has_type x CHAR)))))
+(assert (forall ((x Char)) (! (= x (%C (C x))) :pattern ((C x)))))
+(assert (forall ((x Char)) (! (has_type (C x) CHAR) :pattern ((has_type (C x) CHAR)))))
+(assert (forall ((x Int)) (! (=> (and (<= 0 x) (< x (uHi 32))) (= x (char%to_unicode (char%from_unicode x)))) :pattern ((char%from_unicode x)))))
+(assert (forall ((c Char)) (! (and (<= 0 (char%to_unicode c)) (< (char%to_unicode c) (uHi 32))) :pattern ((char%to_unicode c)))))
+(declare-fun height (Poly) Height)
+(declare-fun height_lt (Height Height) Bool)
+(declare-fun partial-order (Height Height) Bool)
+(assert (forall ((x Height)) (partial-order x x)))
+(assert (forall ((x Height) (y Height)) (=> (and (partial-order x y) (partial-order y x)) (= x y))))
+(assert (forall ((x Height) (y Height) (z Height)) (=> (and (partial-order x y) (partial-order y z)) (partial-order x z))))
+(assert (forall ((x Height) (y Height)) (! (= (height_lt x y) (and (partial-order x y) (not (= x y)))) :pattern ((height_lt x y)))))
+(declare-fun fun_from_recursive_field (Poly) Poly)
+(declare-fun check_decrease_int (Int Int Bool) Bool)
+(assert (forall ((cur Int) (prev Int) (otherwise Bool)) (! (= (check_decrease_int cur prev otherwise) (or (and (<= 0 cur) (< cur prev)) (and (= cur prev) otherwise))) :pattern ((check_decrease_int cur prev otherwise)))))
+(declare-fun check_decrease_height (Poly Poly Bool) Bool)
+(assert (forall ((cur Poly) (prev Poly) (otherwise Bool)) (! (= (check_decrease_height cur prev otherwise) (or (height_lt (height cur) (height prev)) (and (= (height cur) (height prev)) otherwise))) :pattern ((check_decrease_height cur prev otherwise)))))
+(declare-fun uintxor (Int Poly Poly) Int)
+(declare-fun uintand (Int Poly Poly) Int)
+(declare-fun uintor (Int Poly Poly) Int)
+(declare-fun uintshr (Int Poly Poly) Int)
+(declare-fun uintshl (Int Poly Poly) Int)
+(declare-fun uintnot (Int Poly) Int)
+(declare-fun singular_mod (Int Int) Int)
+(assert (forall ((x Int) (y Int)) (! (=> (not (= y 0)) (= (EucMod x y) (singular_mod x y))) :pattern ((singular_mod x y)))))
+(declare-fun closure_req (Type Dcr Type Poly Poly) Bool)
+(declare-fun closure_ens (Type Dcr Type Poly Poly Poly) Bool)
+(assert true)
+(declare-datatypes ((tuple%0. 0)) (((tuple%0./tuple%0 ))))
+(declare-const TYPE%tuple%0. Type)
+(declare-fun Poly%tuple%0. (tuple%0.) Poly)
+(declare-fun %Poly%tuple%0. (Poly) tuple%0.)
+(assert (forall ((x tuple%0.)) (! (= x (%Poly%tuple%0. (Poly%tuple%0. x))) :pattern ((Poly%tuple%0. x)))))
+(assert (forall ((x Poly)) (! (=> (has_type x TYPE%tuple%0.) (= x (Poly%tuple%0. (%Poly%tuple%0. x)))) :pattern ((has_type x TYPE%tuple%0.)))))
+(assert (forall ((x tuple%0.)) (! (has_type (Poly%tuple%0. x) TYPE%tuple%0.) :pattern ((has_type (Poly%tuple%0. x) TYPE%tuple%0.)))))
+(declare-fun req%verismo!tspec.security.sectype_test.p.proof_test1. (Int Int) Bool)
+(declare-const %%global_location_label%%0 Bool)
+(declare-const %%global_location_label%%1 Bool)
+(assert (forall ((v1! Int) (v2! Int)) (! (= (req%verismo!tspec.security.sectype_test.p.proof_test1. v1! v2!) (and (=> %%global_location_label%%0 (< v1! 10)) (=> %%global_location_label%%1 (< v2! 10)))) :pattern ((req%verismo!tspec.security.sectype_test.p.proof_test1. v1! v2!)))))
+(declare-fun ens%verismo!tspec.security.sectype_test.p.proof_test1. (Int Int) Bool)
+(assert (forall ((v1! Int) (v2! Int)) (! (= (ens%verismo!tspec.security.sectype_test.p.proof_test1. v1! v2!) (< (Mul v1! v2!) 100)) :pattern ((ens%verismo!tspec.security.sectype_test.p.proof_test1. v1! v2!)))))
+(declare-fun req%verismo!tspec.security.sectype_test.p.proof_test_bits2. (Int Int) Bool)
+(declare-const %%global_location_label%%2 Bool)
+(declare-const %%global_location_label%%3 Bool)
+(assert (forall ((v1! Int) (v2! Int)) (! (= (req%verismo!tspec.security.sectype_test.p.proof_test_bits2. v1! v2!) (and (=> %%global_location_label%%2 (< v1! 10)) (=> %%global_location_label%%3 (< v2! 10)))) :pattern ((req%verismo!tspec.security.sectype_test.p.proof_test_bits2. v1! v2!)))))
+(declare-fun ens%verismo!tspec.security.sectype_test.p.proof_test_bits2. (Int Int) Bool)
+(assert (forall ((v1! Int) (v2! Int)) (! (= (ens%verismo!tspec.security.sectype_test.p.proof_test_bits2. v1! v2!) (< (uClip 64 (uintand 64 (I v1!) (I v2!))) 10)) :pattern ((ens%verismo!tspec.security.sectype_test.p.proof_test_bits2. v1! v2!)))))
+(declare-const v1!@0 (_ BitVec 64))
+(declare-const v2!@0 (_ BitVec 64))
+(assert (bvult v1!@0 (_ bv10 64)))
+(assert (bvult v2!@0 (_ bv10 64)))
+(declare-const %%location_label%%0 Bool)
+(assert (not (=> %%location_label%%0 (bvult (bvand v1!@0 v2!@0) (_ bv10 64)))))
+(check-sat)
+(exit)