diff --git a/crates/cpu/src/reg_alloc/unit_free_regs_tracker.rs b/crates/cpu/src/reg_alloc/unit_free_regs_tracker.rs index 7d3dc0d..d19cf2a 100644 --- a/crates/cpu/src/reg_alloc/unit_free_regs_tracker.rs +++ b/crates/cpu/src/reg_alloc/unit_free_regs_tracker.rs @@ -131,17 +131,20 @@ mod tests { alloc_at_once: NonZeroUsize, reg_num_width: usize, ) { + let reg_count = 1usize << reg_num_width; // enough time to completely allocate all regs, free whatever we please, // allocate one, then completely free the rest - let history_len = (3 + 2 * (1 << reg_num_width)).max(5); + let mut history_len = 1; + history_len += reg_count.div_ceil(alloc_at_once.get()); + history_len += reg_count.div_ceil(free_at_once.get()); assert_formal( format_args!( "test_unit_free_regs_tracker_{free_at_once}_{alloc_at_once}_{reg_num_width}" ), unit_free_regs_tracker_test(free_at_once, alloc_at_once, reg_num_width, history_len), FormalMode::Prove, - history_len as u64 + 2, - None, + history_len as u64, + Some("z3"), ExportOptions { simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts), ..ExportOptions::default()