rapx/verify/smt_check/

common.rs

//! Common SMT checking backend for the staged verifier.
//!
//! The SMT layer consumes the abstract facts produced by `verifying` and
//! exposes one property-oriented entry point. Safety properties do not call Z3
//! directly. Instead, each property-specific module lowers its requirement into
//! one of the common SMT obligations below, and the common backend discharges
//! that obligation against the path-local abstract facts.
//!
//! Current common obligations:
//!
//! - `SmtObligation::Aligned`: prove `addr(place) % align == 0`.
//! - `SmtObligation::NonZero`: prove `addr(place) != 0`.
//! - `SmtObligation::Range`: reserved for future bounds-style checks.
//!
//! Current property lowering:
//!
//! - `Align(p, T)` lowers to `Aligned { place: p, align: align_of(T) }`.
//! - `NonNull(p)` lowers to `NonZero { place: p }`.
//! - `ValidPtr(p, T, n)` is decomposed by `valid_ptr.rs` into primitive SMT
//!   checks that are implemented today, while unsupported primitives remain
//!   explicit `Unknown` notes.
//!
//! Future SPs should add small lowering modules next to `align.rs` and reuse
//! `SmtModel`, `SmtQuery`, and `SmtCheckResult` instead of constructing solver
//! queries ad hoc.

use std::collections::{HashMap, HashSet};

use rustc_middle::{
    mir::{BinOp, Local, Operand, Rvalue, TerminatorKind, UnOp},
    ty::{ConstKind, GenericArgKind, PseudoCanonicalInput, Ty, TyCtxt, TyKind, UintTy},
};
use z3::{
    Config, Context, SatResult, Solver,
    ast::{Ast, Bool, Int},
};

use super::{
    alias, align, alive, allocated, deref, in_bound, init, non_null, non_overlap, typed, valid_num,
    valid_ptr,
};

use crate::verify::{
    contract::{
        ContractExpr, ContractPlace, ContractProjection, NumericOp, NumericPredicate, PlaceBase,
        Property, PropertyArg, PropertyKind, RelOp,
    },
    def_use::{PlaceBaseKey, PlaceKey},
    generic::GenericTypeCandidates,
    helpers::{Checkpoint, callee_param_index_for_local},
    path_extractor::PathStep,
    primitive::PrimitiveCall,
    report::CheckResult,
    verifier::{AbstractValue, CallSummary, ForwardVisitResult, StateFact},
};

type ValueCursor = usize;
type TraceSeen = HashSet<(PlaceKey, ValueCursor)>;

#[derive(Clone, Copy)]
struct PathCursorCutoff {
    block: rustc_middle::mir::BasicBlock,
    statement_index: Option<usize>,
}

/// SMT backend for verifier properties.
pub struct SmtChecker<'tcx> {
    pub(crate) tcx: TyCtxt<'tcx>,
}

fn ty_has_param_const(ty: Ty<'_>) -> bool {
    for arg in ty.walk() {
        match arg.kind() {
            GenericArgKind::Const(c) if matches!(c.kind(), ConstKind::Param(_)) => return true,
            GenericArgKind::Type(inner_ty) if matches!(inner_ty.kind(), TyKind::Alias(..)) => {
                return true;
            }
            _ => {}
        }
    }
    false
}

fn safe_type_layout<'tcx>(
    tcx: TyCtxt<'tcx>,
    caller: rustc_hir::def_id::DefId,
    ty: Ty<'tcx>,
) -> Option<(u64, u64)> {
    if let TyKind::Ref(_, _, _) | TyKind::RawPtr(_, _) = ty.kind() {
        let ptr_size = tcx.data_layout.pointer_size().bytes();
        let ptr_align = tcx.data_layout.pointer_align().abi.bytes();
        return Some((ptr_align, ptr_size));
    }
    if ty_has_param_const(ty) {
        return None;
    }
    let typing_env = rustc_middle::ty::TypingEnv::post_analysis(tcx, caller);
    let input = PseudoCanonicalInput {
        typing_env,
        value: ty,
    };
    match tcx.layout_of(input) {
        Ok(layout) => Some((layout.align.abi.bytes(), layout.size.bytes())),
        Err(_) if matches!(ty.kind(), TyKind::Param(_)) => Some((0, 0)),
        Err(_) => None,
    }
}

impl<'tcx> SmtChecker<'tcx> {
    /// Create an SMT checker for the current compiler type context.
    pub fn new(tcx: TyCtxt<'tcx>) -> Self {
        Self { tcx }
    }

    /// Try to prove one property using SMT.
    pub fn check(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        property: &Property<'tcx>,
        forward: &ForwardVisitResult<'tcx>,
    ) -> SmtCheckResult {
        match property.kind {
            PropertyKind::Align => align::check(self, checkpoint, property, forward),
            PropertyKind::Alias => alias::check(self, checkpoint, property, forward),
            PropertyKind::Alive => alive::check(self, checkpoint, property, forward),
            PropertyKind::Allocated => allocated::check(self, checkpoint, property, forward),
            PropertyKind::Deref => deref::check(self, checkpoint, property, forward),
            PropertyKind::NonNull => non_null::check(self, checkpoint, property, forward),
            PropertyKind::InBound => in_bound::check(self, checkpoint, property, forward),
            PropertyKind::Init => init::check(self, checkpoint, property, forward),
            PropertyKind::NonOverlap => non_overlap::check(self, checkpoint, property, forward),
            PropertyKind::Typed => typed::check(self, checkpoint, property, forward),
            PropertyKind::ValidNum => valid_num::check(self, checkpoint, property, forward),
            PropertyKind::ValidPtr => valid_ptr::check(self, checkpoint, property, forward),
            PropertyKind::NonVolatile => super::non_volatile::check(self, checkpoint, property, forward),
            _ => SmtCheckResult::unknown("no SMT lowering for this property yet"),
        }
    }

    /// Try to prove one property at a return checkpoint (struct invariant).
    ///
    /// Unlike [`check`], this does not use callee-to-caller argument mapping
    /// because struct invariant properties are already resolved in the caller's
    /// local namespace.
    pub fn check_for_checkpoint(
        &self,
        caller: rustc_hir::def_id::DefId,
        property: &Property<'tcx>,
        forward: &ForwardVisitResult<'tcx>,
    ) -> SmtCheckResult {
        match property.kind {
            PropertyKind::Align => align::check_for_checkpoint(self, caller, property, forward),
            PropertyKind::Allocated => {
                SmtCheckResult::unknown("Allocated struct invariant not implemented yet")
            }
            PropertyKind::NonNull => {
                SmtCheckResult::unknown("NonNull struct invariant not implemented yet")
            }
            PropertyKind::InBound => {
                in_bound::check_for_checkpoint(self, caller, property, forward)
            }
            PropertyKind::Init => init::check_for_checkpoint(self, caller, property, forward),
            PropertyKind::ValidPtr => {
                SmtCheckResult::unknown("ValidPtr struct invariant not implemented yet")
            }
            _ => SmtCheckResult::unknown("no struct invariant SMT lowering for this property yet"),
        }
    }

    /// Prove one already-lowered common SMT obligation.
    pub(crate) fn prove_obligation(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        forward: &ForwardVisitResult<'tcx>,
        obligation: SmtObligation,
    ) -> SmtCheckResult {
        let has_contracts = forward
            .facts
            .iter()
            .any(|f| matches!(f, StateFact::Contract(_)));

        // Build the SMT model once.  Contract facts (caller_requires)
        // are always asserted, even when the path has forgets from
        // unsupported intrinsics.
        let cfg = Config::new();
        let ctx = Context::new(&cfg);
        let solver = Solver::new(&ctx);
        let mut model = SmtModel::new(self.tcx, checkpoint, forward, &ctx);
        model.assert_forward_facts(&solver);

        if matches!(solver.check(), SatResult::Unsat) {
            return SmtCheckResult::proved(
                "path facts are infeasible; the obligation holds vacuously on this path",
            )
            .with_query(SmtQuery::new(
                obligation,
                model.assumptions().to_vec(),
                SmtPredicate::Custom(String::from("path constraints are unsat")),
            ));
        }

        if !forward.forgets.is_empty() && !has_contracts {
            let reasons = forward
                .forgets
                .iter()
                .map(|reason| format!("{reason:?}"))
                .collect::<Vec<_>>()
                .join(", ");
            return SmtCheckResult::unknown(
                "path has precision loss; SMT proof is not trusted without a summary",
            )
            .with_note(format!("precision loss: {reasons}"));
        }

        // When forgets exist but contracts provide path assumptions,
        // allow the SMT check to proceed against the contract-fact
        // model.  The contract assertions may be sufficient to
        // discharge the obligation even without full path precision.
        // (No early return — fall through to obligation match.)

        match &obligation {
            SmtObligation::Aligned {
                place,
                align,
                ty_name,
            } => {
                if *align > 0 && *align <= 1 {
                    return SmtCheckResult {
                        result: CheckResult::Proved,
                        query: Some(SmtQuery::new(
                            obligation.clone(),
                            model.assumptions().to_vec(),
                            SmtPredicate::Custom(format!(
                                "{} has trivial 1-byte alignment",
                                place_label(place)
                            )),
                        )),
                        notes: vec![String::from("alignment requirement is trivial")],
                    };
                }

                let target_label = place_label(place);
                let Some(target_term) = model.term_for_place(place) else {
                    return SmtCheckResult::unknown(format!(
                        "could not build an address term for {target_label}"
                    ))
                    .with_query(SmtQuery::new(
                        obligation.clone(),
                        model.assumptions().to_vec(),
                        SmtPredicate::Not(Box::new(SmtPredicate::Divisible {
                            term: SmtTerm::Place(place.clone()),
                            modulus: *align,
                        })),
                    ));
                };

                let is_symbolic = *align == 0;
                let align_term = if is_symbolic {
                    model.symbolic_align_term(&ty_name)
                } else {
                    Int::from_u64(&ctx, *align)
                };
                let align_u64 = if is_symbolic { 0 } else { *align };
                let zero = Int::from_u64(&ctx, 0);
                let goal = target_term.modulo(&align_term)._eq(&zero);
                let query = SmtQuery::new(
                    obligation.clone(),
                    model.assumptions().to_vec(),
                    SmtPredicate::Not(Box::new(SmtPredicate::Divisible {
                        term: SmtTerm::Place(place.clone()),
                        modulus: align_u64,
                    })),
                );

                solver.assert(&goal.not());
                match solver.check() {
                    SatResult::Unsat => SmtCheckResult::proved(
                        "alignment proved; no counterexample satisfies the path facts",
                    )
                    .with_query(query),
                    SatResult::Sat => {
                        rap_debug!("  [SMT Align] {} sat: counterexample found", target_label);
                        SmtCheckResult::unknown(
                            "current path facts do not prove the required alignment",
                        )
                        .with_query(query)
                        .with_note(
                            "hint: add an offset-alignment guard or provide a pointer-add/layout summary",
                        )
                    }
                    SatResult::Unknown => {
                        rap_info!("  [SMT Align] {} unknown result", target_label);
                        SmtCheckResult::unknown("solver returned unknown").with_query(query)
                    }
                }
            }
            SmtObligation::NonZero { place } => {
                let target_label = place_label(place);
                let Some(target_term) = model.term_for_place(place) else {
                    return SmtCheckResult::unknown(format!(
                        "could not build an address term for {target_label}"
                    ))
                    .with_query(SmtQuery::new(
                        obligation.clone(),
                        model.assumptions().to_vec(),
                        SmtPredicate::Eq(SmtTerm::Place(place.clone()), SmtTerm::Const(0)),
                    ));
                };

                let zero = Int::from_u64(&ctx, 0);
                let query = SmtQuery::new(
                    obligation.clone(),
                    model.assumptions().to_vec(),
                    SmtPredicate::Eq(SmtTerm::Place(place.clone()), SmtTerm::Const(0)),
                );

                solver.assert(&target_term._eq(&zero));
                match solver.check() {
                    SatResult::Unsat => SmtCheckResult::proved(
                        "non-null proved; no zero-address model satisfies the path facts",
                    )
                    .with_query(query),
                    SatResult::Sat => SmtCheckResult::unknown(
                        "current path facts do not prove the target is non-null",
                    )
                    .with_query(query)
                    .with_note("hint: add a non-null guard or provide a source/provenance summary"),
                    SatResult::Unknown => {
                        SmtCheckResult::unknown("solver returned unknown").with_query(query)
                    }
                }
            }
            SmtObligation::InBounds {
                place,
                ty_name,
                access_count,
                ..
            } => {
                let target_label = place_label(place);
                if model.has_index_access_assumptions {
                    return SmtCheckResult::proved(
                        "IndexAccess in-bounds proved via caller contract",
                    )
                    .with_query(SmtQuery::new(
                        obligation.clone(),
                        model.assumptions().to_vec(),
                        SmtPredicate::Custom(String::from("IndexAccess InBound by contract")),
                    ));
                }
                let Some(bounds) = model.pointer_bounds_for_place(place) else {
                    rap_debug!(
                        "  [SMT InBound] could not recover pointer bounds for {target_label}"
                    );
                    if model.has_equivalent_contract_fact(place, PropertyKind::InBound) {
                        return SmtCheckResult::proved(
                            "in-bounds proved via caller contract on equivalent place",
                        )
                        .with_query(SmtQuery::new(
                            obligation.clone(),
                            model.assumptions().to_vec(),
                            SmtPredicate::Not(Box::new(SmtPredicate::InBounds {
                                index: SmtTerm::Value("index(?)".to_string()),
                                access_count: access_count.clone(),
                                len: SmtTerm::Value("len(?)".to_string()),
                            })),
                        ))
                        .with_note("caller contract provides InBound for raw pointer parameter");
                    }
                    return SmtCheckResult::unknown(format!(
                        "could not connect {target_label} to a slice length and pointer-add index"
                    ))
                    .with_query(SmtQuery::new(
                        obligation.clone(),
                        model.assumptions().to_vec(),
                        SmtPredicate::Not(Box::new(SmtPredicate::InBounds {
                            index: SmtTerm::Value("index(?)".to_string()),
                            access_count: access_count.clone(),
                            len: SmtTerm::Value("len(?)".to_string()),
                        })),
                    ))
                    .with_note(
                        "hint: this first InBound lowering needs slice.as_ptr(), ptr.add(index), and a matching index < slice.len() path fact",
                    );
                };

                let zero = Int::from_u64(&ctx, 0);
                let Some(access) = model.term_for_smt_term(access_count) else {
                    rap_debug!(
                        "  [SMT InBound] could not lower access-count term {}",
                        access_count.describe()
                    );
                    return SmtCheckResult::unknown(format!(
                        "could not build an access-count term for {}",
                        access_count.describe()
                    ))
                    .with_query(SmtQuery::new(
                        obligation.clone(),
                        model.assumptions().to_vec(),
                        SmtPredicate::Not(Box::new(SmtPredicate::InBounds {
                            index: bounds.index_term,
                            access_count: access_count.clone(),
                            len: bounds.len_term,
                        })),
                    ));
                };
                let index_non_negative = bounds.index.ge(&zero);
                let access_non_negative = access.ge(&zero);
                let len_non_negative = bounds.len.ge(&zero);
                let covered_end = Int::add(&ctx, &[bounds.index.clone(), access]);
                let within_len = covered_end.le(&bounds.len);
                solver.assert(&index_non_negative);
                solver.assert(&access_non_negative);
                solver.assert(&len_non_negative);
                model.assumptions.push(SmtPredicate::Ge(
                    bounds.index_term.clone(),
                    SmtTerm::Const(0),
                ));
                model
                    .assumptions
                    .push(SmtPredicate::Ge(access_count.clone(), SmtTerm::Const(0)));
                let goal = Bool::and(
                    &ctx,
                    &[&index_non_negative, &access_non_negative, &within_len],
                );
                let query = SmtQuery::new(
                    obligation.clone(),
                    model.assumptions().to_vec(),
                    SmtPredicate::Not(Box::new(SmtPredicate::InBounds {
                        index: bounds.index_term,
                        access_count: access_count.clone(),
                        len: bounds.len_term,
                    })),
                );

                solver.assert(&goal.not());
                match solver.check() {
                    SatResult::Unsat => SmtCheckResult::proved(format!(
                        "in-bounds proved for {target_label}; {} {ty_name} element(s) fit under the matched slice length",
                        access_count.describe()
                    ))
                    .with_query(query),
                    SatResult::Sat => {
                        rap_debug!(
                            "  [SMT InBound] sat for {target_label}; assumptions: {:?}; negated goal: {}",
                            query.assumptions,
                            query.negated_goal.describe()
                        );
                        SmtCheckResult::unknown(
                            "current path facts do not prove the required bounds",
                        )
                        .with_query(query)
                        .with_note(
                            "hint: add an index < len guard or provide a richer object-size summary",
                        )
                    }
                    SatResult::Unknown => {
                        SmtCheckResult::unknown("solver returned unknown").with_query(query)
                    }
                }
            }
            SmtObligation::PointerRangeInBounds {
                place,
                ty_name,
                lower_delta,
                upper_delta,
            } => {
                let target_label = place_label(place);
                let Some(bounds) = model.pointer_bounds_for_place(place) else {
                    return SmtCheckResult::unknown(format!(
                        "could not connect {target_label} to a slice length and pointer index"
                    ))
                    .with_query(SmtQuery::new(
                        obligation.clone(),
                        model.assumptions().to_vec(),
                        pointer_range_negated_goal(
                            SmtTerm::Value("index(?)".to_string()),
                            lower_delta.clone(),
                            upper_delta.clone(),
                            SmtTerm::Value("len(?)".to_string()),
                        ),
                    ))
                    .with_note(
                        "hint: pointer arithmetic bounds need a recoverable base object and index/length facts",
                    );
                };

                let Some(lower) = model.term_for_smt_term(lower_delta) else {
                    return SmtCheckResult::unknown(format!(
                        "could not build a lower pointer-range term for {}",
                        lower_delta.describe()
                    ));
                };
                let Some(upper) = model.term_for_smt_term(upper_delta) else {
                    return SmtCheckResult::unknown(format!(
                        "could not build an upper pointer-range term for {}",
                        upper_delta.describe()
                    ));
                };

                model.assert_unsigned_bounds_for_term(&solver, lower_delta, &mut HashSet::new());
                model.assert_unsigned_bounds_for_term(&solver, upper_delta, &mut HashSet::new());

                let zero = Int::from_u64(&ctx, 0);
                // A recovered object length is a slice/allocation size and is
                // therefore non-negative.  Without this fact the solver may pick
                // a negative `len`, defeating goals whose offset is expressed as
                // `len - x` (e.g. `ptr.add(len - half_len)`), where the bound
                // `len - x <= len` only holds because `x >= 0` and `len >= 0`.
                solver.assert(&bounds.len.ge(&zero));
                model
                    .assumptions
                    .push(SmtPredicate::Ge(bounds.len_term.clone(), SmtTerm::Const(0)));

                let lower_index = Int::add(&ctx, &[bounds.index.clone(), lower]);
                let upper_index = Int::add(&ctx, &[bounds.index.clone(), upper]);
                let base_non_negative = bounds.index.ge(&zero);
                let base_within_len = bounds.index.le(&bounds.len);
                let lower_in_object = lower_index.ge(&zero);
                let upper_in_object = upper_index.le(&bounds.len);

                let goal = Bool::and(
                    &ctx,
                    &[
                        &base_non_negative,
                        &base_within_len,
                        &lower_in_object,
                        &upper_in_object,
                    ],
                );
                let query = SmtQuery::new(
                    obligation.clone(),
                    model.assumptions().to_vec(),
                    pointer_range_negated_goal(
                        bounds.index_term,
                        lower_delta.clone(),
                        upper_delta.clone(),
                        bounds.len_term,
                    ),
                );

                solver.assert(&goal.not());
                match solver.check() {
                    SatResult::Unsat => SmtCheckResult::proved(format!(
                        "pointer arithmetic range proved for {target_label}; the {ty_name} range stays inside the matched object"
                    ))
                    .with_query(query),
                    SatResult::Sat => SmtCheckResult::unknown(
                        "current path facts do not prove the pointer arithmetic stays in bounds",
                    )
                    .with_query(query)
                    .with_note("hint: add bounds guards for the pointer arithmetic count"),
                    SatResult::Unknown => {
                        SmtCheckResult::unknown("solver returned unknown").with_query(query)
                    }
                }
            }
            SmtObligation::Initialized {
                place,
                ty_name,
                elements,
                elem_size,
                array_elem_size,
                array_len_term,
            } => {
                if *elem_size == Some(0) {
                    return SmtCheckResult::proved(format!(
                        "initialization proved; zero-sized type {ty_name}"
                    ));
                }
                if let (Some(ae), Some(alt)) = (array_elem_size, array_len_term) {
                    if *ae > 0 {
                        if let Some(len_term) = model.term_for_smt_term(alt) {
                            let zero = Int::from_u64(&ctx, 0);
                            let size_term = Int::from_u64(&ctx, *ae);
                            let total_gt_zero =
                                Bool::and(&ctx, &[&len_term.gt(&zero), &size_term.gt(&zero)]);
                            solver.push();
                            solver.assert(&total_gt_zero);
                            let check = solver.check();
                            solver.pop(1);
                            if matches!(check, SatResult::Unsat) {
                                return SmtCheckResult::proved(format!(
                                    "initialization proved; array length is provably zero for {ty_name}"
                                ));
                            }
                        }
                    }
                }
                let target_label = place_label(place);
                let target_terms = model.init_target_terms(place);
                if target_terms.is_empty() {
                    return SmtCheckResult::unknown(format!(
                        "could not build an address term for {target_label}"
                    ))
                    .with_query(SmtQuery::new(
                        obligation.clone(),
                        model.assumptions().to_vec(),
                        SmtPredicate::Custom(format!(
                            "not Init({}, {ty_name}, {elements})",
                            target_label,
                            elements = elements.describe()
                        )),
                    ));
                }

                if model.has_equivalent_contract_fact(place, PropertyKind::Init) {
                    return SmtCheckResult::proved(
                        "initialized proved via caller contract on equivalent place",
                    )
                    .with_query(SmtQuery::new(
                        obligation.clone(),
                        model.assumptions().to_vec(),
                        SmtPredicate::Custom(format!(
                            "Init({}, {ty_name}, {elements})",
                            target_label,
                            elements = elements.describe()
                        )),
                    ))
                    .with_note("caller contract provides Init for raw pointer parameter");
                }

                if let Some(bounds) = model.pointer_bounds_for_place(place)
                    && model.origin_is_initialized_for_ty(&bounds.origin_key, ty_name)
                {
                    let Some(access) = model.term_for_smt_term(elements) else {
                        return SmtCheckResult::unknown(format!(
                            "could not build an Init element-count term for {}",
                            elements.describe()
                        ));
                    };
                    model.assert_unsigned_bounds_for_term(&solver, elements, &mut HashSet::new());
                    let zero = Int::from_u64(&ctx, 0);
                    let index_non_negative = bounds.index.ge(&zero);
                    let access_non_negative = access.ge(&zero);
                    let len_non_negative = bounds.len.ge(&zero);
                    let covered_end = Int::add(&ctx, &[bounds.index.clone(), access]);
                    let within_len = covered_end.le(&bounds.len);
                    solver.assert(&len_non_negative);
                    let goal = Bool::and(
                        &ctx,
                        &[&index_non_negative, &access_non_negative, &within_len],
                    );
                    let query = SmtQuery::new(
                        obligation.clone(),
                        model.assumptions().to_vec(),
                        SmtPredicate::Custom(format!(
                            "not initialized_object_range({}, {}, {})",
                            target_label,
                            bounds.index_term.describe(),
                            elements.describe()
                        )),
                    );

                    solver.assert(&goal.not());
                    return match solver.check() {
                        SatResult::Unsat => SmtCheckResult::proved(format!(
                            "initialization proved; {target_label} covers {} initialized {ty_name} element(s) from its source object",
                            elements.describe()
                        ))
                        .with_query(query),
                        SatResult::Sat => SmtCheckResult::unknown(
                            "current path facts do not prove the initialized object range covers the target",
                        )
                        .with_query(query)
                        .with_note("hint: keep object length facts for the initialized source"),
                        SatResult::Unknown => {
                            SmtCheckResult::unknown("solver returned unknown").with_query(query)
                        }
                    };
                }

                let init_facts: Vec<_> = forward
                    .facts
                    .iter()
                    .filter_map(|fact| match fact {
                        StateFact::KnownInit {
                            place,
                            ty_name,
                            elements,
                            reason,
                        } => Some((place.clone(), ty_name.clone(), *elements, reason.clone())),
                        _ => None,
                    })
                    .collect();

                let mut checked_any_init_fact = false;
                for target_term in &target_terms {
                    let mut matched_elements = 0_u64;
                    let mut matched_places = HashSet::new();
                    let mut matched_notes = Vec::new();
                    let mut last_query = None;
                    let Some(required_elements) = smt_term_const_u64(elements) else {
                        continue;
                    };

                    for (init_place, init_ty_name, init_elements, init_reason) in &init_facts {
                        if !init_type_compatible(init_ty_name, ty_name) {
                            continue;
                        }
                        if !matched_places.insert(init_place.clone()) {
                            continue;
                        }
                        let init_terms = model.init_source_terms(init_place);
                        if init_terms.is_empty() {
                            continue;
                        }

                        for init_term in &init_terms {
                            let query = SmtQuery::new(
                                obligation.clone(),
                                model.assumptions().to_vec(),
                                SmtPredicate::Custom(format!(
                                    "not same_addr({}, {}) for Init({}, {ty_name}, {elements})",
                                    target_label,
                                    place_label(init_place),
                                    target_label,
                                    elements = elements.describe()
                                )),
                            );
                            solver.push();
                            solver.assert(&target_term._eq(init_term).not());
                            let check = solver.check();
                            solver.pop(1);
                            if matches!(check, SatResult::Unsat) {
                                checked_any_init_fact = true;
                                matched_elements = matched_elements.saturating_add(*init_elements);
                                matched_notes.push(format!(
                                    "{} element(s) from {} ({init_reason})",
                                    init_elements,
                                    place_label(init_place)
                                ));
                                last_query = Some(query);
                                break;
                            }
                        }

                        if matched_elements >= required_elements {
                            let query = last_query.unwrap_or_else(|| {
                                SmtQuery::new(
                                    obligation.clone(),
                                    model.assumptions().to_vec(),
                                    SmtPredicate::Custom(format!(
                                        "not Init({}, {ty_name}, {elements})",
                                        target_label,
                                        elements = elements.describe()
                                    )),
                                )
                            });
                            return SmtCheckResult::proved(format!(
                                "initialization proved; {target_label} aliases {matched_elements} initialized element(s)"
                            ))
                            .with_query(query)
                            .with_note(format!(
                                "matched initialized writes: {}",
                                matched_notes.join("; ")
                            ));
                        }
                    }
                }

                let mut result = SmtCheckResult::unknown(
                    "current path facts do not prove the target memory is initialized",
                )
                .with_query(SmtQuery::new(
                    obligation.clone(),
                    model.assumptions().to_vec(),
                    SmtPredicate::Custom(format!(
                        "not Init({}, {ty_name}, {elements})",
                        target_label,
                        elements = elements.describe()
                    )),
                ));
                if checked_any_init_fact {
                    result = result.with_note(
                        "hint: a write was found, but SMT could not prove it aliases the Init target",
                    );
                } else {
                    result = result.with_note(
                        "hint: add a preceding ptr.write summary or a verified init-range summary",
                    );
                }
                result
            }
            SmtObligation::Allocated {
                place,
                ty_name,
                elements,
            } => {
                let target_label = place_label(place);

                if let Some(bounds) = model.pointer_bounds_for_place(place) {
                    let zero = Int::from_u64(&ctx, 0);
                    let Some(access) = model.term_for_smt_term(elements) else {
                        return SmtCheckResult::unknown(format!(
                            "could not build an allocation element-count term for {}",
                            elements.describe()
                        ))
                        .with_query(SmtQuery::new(
                            obligation.clone(),
                            model.assumptions().to_vec(),
                            SmtPredicate::Custom(format!(
                                "not Allocated({}, {ty_name}, {})",
                                target_label,
                                elements.describe()
                            )),
                        ));
                    };
                    let index_non_negative = bounds.index.ge(&zero);
                    let access_non_negative = access.ge(&zero);
                    let len_non_negative = bounds.len.ge(&zero);
                    let covered_end = Int::add(&ctx, &[bounds.index.clone(), access]);
                    let within_len = covered_end.le(&bounds.len);
                    solver.assert(&index_non_negative);
                    solver.assert(&access_non_negative);
                    solver.assert(&len_non_negative);
                    model.assumptions.push(SmtPredicate::Ge(
                        bounds.index_term.clone(),
                        SmtTerm::Const(0),
                    ));
                    model
                        .assumptions
                        .push(SmtPredicate::Ge(elements.clone(), SmtTerm::Const(0)));
                    model.assumptions.push(SmtPredicate::Ge(
                        bounds.len_term.clone(),
                        SmtTerm::Const(0),
                    ));
                    let goal = Bool::and(
                        &ctx,
                        &[&index_non_negative, &access_non_negative, &within_len],
                    );
                    let query = SmtQuery::new(
                        obligation.clone(),
                        model.assumptions().to_vec(),
                        SmtPredicate::Custom(format!(
                            "not same_object_bounds({}, {}, {})",
                            target_label,
                            bounds.index_term.describe(),
                            elements.describe()
                        )),
                    );

                    solver.assert(&goal.not());
                    return match solver.check() {
                        SatResult::Unsat => SmtCheckResult::proved(format!(
                            "allocation proved for {target_label}; requested range stays inside the matched object"
                        ))
                        .with_query(query),
                        SatResult::Sat => SmtCheckResult::unknown(
                            "current path facts do not prove the requested range stays inside one allocation",
                        )
                        .with_query(query)
                        .with_note(
                            "hint: add an object-length guard or provide a richer allocation summary",
                        ),
                        SatResult::Unknown => {
                            SmtCheckResult::unknown("solver returned unknown").with_query(query)
                        }
                    };
                }

                let Some(target_term) = model.term_for_place(place) else {
                    return SmtCheckResult::unknown(format!(
                        "could not build an address term for {target_label}"
                    ))
                    .with_query(SmtQuery::new(
                        obligation.clone(),
                        model.assumptions().to_vec(),
                        SmtPredicate::Custom(format!(
                            "not Allocated({}, {ty_name}, {})",
                            target_label,
                            elements.describe()
                        )),
                    ));
                };
                let Some(required_elements) = model.term_for_smt_term(elements) else {
                    return SmtCheckResult::unknown(format!(
                        "could not build an allocation element-count term for {}",
                        elements.describe()
                    ))
                    .with_query(SmtQuery::new(
                        obligation.clone(),
                        model.assumptions().to_vec(),
                        SmtPredicate::Custom(format!(
                            "not Allocated({}, {ty_name}, {})",
                            target_label,
                            elements.describe()
                        )),
                    ));
                };

                let allocated_facts = forward
                    .facts
                    .iter()
                    .filter_map(|fact| match fact {
                        StateFact::KnownAllocated {
                            place,
                            object,
                            ty_name,
                            elements,
                            reason,
                        } => Some((
                            place.clone(),
                            object.clone(),
                            ty_name.clone(),
                            *elements,
                            reason.clone(),
                        )),
                        _ => None,
                    })
                    .collect::<Vec<_>>();

                for (alloc_place, object, alloc_ty_name, alloc_elements, reason) in allocated_facts
                {
                    if !allocated_type_compatible(&alloc_ty_name, ty_name) {
                        continue;
                    }
                    if allocation_object_invalidated(forward, &object) {
                        continue;
                    }
                    let Some(alloc_term) = model.term_for_place(&alloc_place) else {
                        continue;
                    };
                    let query = SmtQuery::new(
                        obligation.clone(),
                        model.assumptions().to_vec(),
                        SmtPredicate::Custom(format!(
                            "not same_allocated_object({}, {}) or {} > {}",
                            target_label,
                            place_label(&alloc_place),
                            elements.describe(),
                            alloc_elements
                        )),
                    );

                    solver.push();
                    solver.assert(&target_term._eq(&alloc_term).not());
                    let same_address = matches!(solver.check(), SatResult::Unsat);
                    solver.pop(1);
                    if !same_address {
                        continue;
                    }

                    solver.push();
                    solver.assert(&required_elements.gt(&Int::from_u64(&ctx, alloc_elements)));
                    let enough_elements = matches!(solver.check(), SatResult::Unsat);
                    solver.pop(1);
                    if enough_elements {
                        return SmtCheckResult::proved(format!(
                            "allocation proved; {target_label} aliases {} element(s) of {} ({reason})",
                            alloc_elements, alloc_ty_name
                        ))
                        .with_query(query);
                    }
                }

                SmtCheckResult::unknown(
                    "current path facts do not prove the target range is backed by one live allocation",
                )
                .with_query(SmtQuery::new(
                    obligation.clone(),
                    model.assumptions().to_vec(),
                    SmtPredicate::Custom(format!(
                        "not Allocated({}, {ty_name}, {})",
                        target_label,
                        elements.describe()
                    )),
                ))
                .with_note(
                    "hint: keep pointer provenance, object length, and lifetime facts for the target object",
                )
            }
            SmtObligation::NonOverlapping {
                left,
                right,
                left_count,
                right_count,
                elem_size,
            } => {
                if let (Some((left_object, left_offset)), Some((right_object, right_offset))) = (
                    model.pointer_object_offset_for_place(left),
                    model.pointer_object_offset_for_place(right),
                ) && left_object == right_object
                {
                    let Some(left_offset_term) = model.term_for_smt_term(&left_offset) else {
                        return SmtCheckResult::unknown(format!(
                            "could not lower object offset {}",
                            left_offset.describe()
                        ));
                    };
                    let Some(right_offset_term) = model.term_for_smt_term(&right_offset) else {
                        return SmtCheckResult::unknown(format!(
                            "could not lower object offset {}",
                            right_offset.describe()
                        ));
                    };
                    let Some(left_count_term) = model.term_for_smt_term(left_count) else {
                        return SmtCheckResult::unknown(format!(
                            "could not build a range-count term for {}",
                            left_count.describe()
                        ));
                    };
                    let Some(right_count_term) = model.term_for_smt_term(right_count) else {
                        return SmtCheckResult::unknown(format!(
                            "could not build a range-count term for {}",
                            right_count.describe()
                        ));
                    };
                    let left_end = Int::add(&ctx, &[left_offset_term.clone(), left_count_term]);
                    let right_end = Int::add(&ctx, &[right_offset_term.clone(), right_count_term]);
                    let disjoint = Bool::or(
                        &ctx,
                        &[
                            &left_end.le(&right_offset_term),
                            &right_end.le(&left_offset_term),
                        ],
                    );
                    let negated = SmtPredicate::Not(Box::new(SmtPredicate::NonOverlapping {
                        left: left_offset,
                        right: right_offset,
                        left_count: left_count.clone(),
                        right_count: right_count.clone(),
                        elem_size: 1,
                    }));
                    let query =
                        SmtQuery::new(obligation.clone(), model.assumptions().to_vec(), negated);

                    model.assert_unsigned_bounds_for_term(&solver, left_count, &mut HashSet::new());
                    model.assert_unsigned_bounds_for_term(
                        &solver,
                        right_count,
                        &mut HashSet::new(),
                    );
                    solver.assert(&disjoint.not());
                    return match solver.check() {
                        SatResult::Unsat => SmtCheckResult::proved(format!(
                            "non-overlap proved inside allocation {}",
                            place_label(&left_object)
                        ))
                        .with_query(query),
                        SatResult::Sat => {
                            failed_smt("the two ranges overlap within the same allocation object")
                                .with_query(query)
                        }
                        SatResult::Unknown => {
                            SmtCheckResult::unknown("solver returned unknown").with_query(query)
                        }
                    };
                }

                let Some(left_addr) = model.term_for_place(left) else {
                    return SmtCheckResult::unknown(format!(
                        "could not build an address term for {}",
                        place_label(left)
                    ));
                };
                let Some(right_addr) = model.term_for_place(right) else {
                    return SmtCheckResult::unknown(format!(
                        "could not build an address term for {}",
                        place_label(right)
                    ));
                };
                let Some(left_count_term) = model.term_for_smt_term(left_count) else {
                    return SmtCheckResult::unknown(format!(
                        "could not build a range-count term for {}",
                        left_count.describe()
                    ));
                };
                let Some(right_count_term) = model.term_for_smt_term(right_count) else {
                    return SmtCheckResult::unknown(format!(
                        "could not build a range-count term for {}",
                        right_count.describe()
                    ));
                };

                let size = Int::from_u64(&ctx, *elem_size);
                let left_end = Int::add(
                    &ctx,
                    &[
                        left_addr.clone(),
                        Int::mul(&ctx, &[left_count_term, size.clone()]),
                    ],
                );
                let right_end = Int::add(
                    &ctx,
                    &[
                        right_addr.clone(),
                        Int::mul(&ctx, &[right_count_term, size]),
                    ],
                );
                let disjoint = Bool::or(
                    &ctx,
                    &[&left_end.le(&right_addr), &right_end.le(&left_addr)],
                );
                let negated = SmtPredicate::Not(Box::new(SmtPredicate::NonOverlapping {
                    left: SmtTerm::Place(left.clone()),
                    right: SmtTerm::Place(right.clone()),
                    left_count: left_count.clone(),
                    right_count: right_count.clone(),
                    elem_size: *elem_size,
                }));
                let query =
                    SmtQuery::new(obligation.clone(), model.assumptions().to_vec(), negated);

                model.assert_unsigned_bounds_for_term(&solver, left_count, &mut HashSet::new());
                model.assert_unsigned_bounds_for_term(&solver, right_count, &mut HashSet::new());
                solver.assert(&disjoint.not());
                match solver.check() {
                    SatResult::Unsat => SmtCheckResult::proved(
                        "non-overlap proved; the two pointer ranges cannot intersect on this path",
                    )
                    .with_query(query),
                    SatResult::Sat => failed_smt(
                        "the two pointer ranges may overlap under the current path facts",
                    )
                    .with_query(query),
                    SatResult::Unknown => {
                        SmtCheckResult::unknown("solver returned unknown").with_query(query)
                    }
                }
            }
            SmtObligation::Predicate { predicates } => {
                // If caller contract already provides IndexAccess InBound assumptions,
                // the proof is trivial
                if model.has_index_access_assumptions {
                    return SmtCheckResult::proved(
                        "IndexAccess in-bounds proved via caller contract",
                    );
                }
                if predicates.is_empty() {
                    return SmtCheckResult::unknown("ValidNum predicate set is empty").with_query(
                        SmtQuery::new(
                            obligation.clone(),
                            model.assumptions().to_vec(),
                            SmtPredicate::Custom(String::from("empty ValidNum predicate")),
                        ),
                    );
                }
                model.assert_unsigned_bounds_for_predicates(&solver, predicates);

                let Some(goal) = model.bool_for_predicates(predicates) else {
                    return SmtCheckResult::unknown(
                        "ValidNum predicate could not be lowered to SMT",
                    )
                    .with_query(SmtQuery::new(
                        obligation.clone(),
                        model.assumptions().to_vec(),
                        SmtPredicate::Not(Box::new(if predicates.len() == 1 {
                            predicates[0].clone()
                        } else {
                            SmtPredicate::And(predicates.clone())
                        })),
                    ));
                };
                let query = SmtQuery::new(
                    obligation.clone(),
                    model.assumptions().to_vec(),
                    SmtPredicate::Not(Box::new(if predicates.len() == 1 {
                        predicates[0].clone()
                    } else {
                        SmtPredicate::And(predicates.clone())
                    })),
                );

                solver.assert(&goal.not());
                match solver.check() {
                    SatResult::Unsat => SmtCheckResult::proved(
                        "numeric precondition proved; no counterexample satisfies the path facts",
                    )
                    .with_query(query),
                    SatResult::Sat => SmtCheckResult::unknown(
                        "current path facts do not prove the numeric precondition",
                    )
                    .with_query(query)
                    .with_note("hint: add a matching numeric guard or expose a stronger summary"),
                    SatResult::Unknown => {
                        SmtCheckResult::unknown("solver returned unknown").with_query(query)
                    }
                }
            }
            SmtObligation::Range { .. } => SmtCheckResult::unknown(
                "range obligations are not implemented yet",
            )
            .with_query(SmtQuery::new(
                obligation.clone(),
                model.assumptions().to_vec(),
                SmtPredicate::Custom(String::from("range refutation not implemented")),
            )),
        }
    }

    /// Prove one lowered obligation at a return checkpoint (struct invariant).
    ///
    /// Wraps `prove_obligation` with a minimal dummy checkpoint that only carries
    /// the caller DefId. No callee-to-caller argument mapping is needed.
    pub(crate) fn prove_obligation_for_checkpoint(
        &self,
        caller: rustc_hir::def_id::DefId,
        forward: &ForwardVisitResult<'tcx>,
        obligation: SmtObligation,
    ) -> SmtCheckResult {
        let dummy_checkpoint = Checkpoint {
            caller,
            callee: Some(caller),
            block: rustc_middle::mir::BasicBlock::from_usize(0),
            span: rustc_span::Span::default(),
            args: Vec::new(),
            kind: crate::helpers::mir_scan::CheckpointKind::UnsafeCall,
            is_ref: false,
        };
        self.prove_obligation(&dummy_checkpoint, forward, obligation)
    }

    /// Resolve the target place of a property at a concrete checkpoint.
    pub(crate) fn property_target(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        property: &Property<'tcx>,
    ) -> Option<PlaceKey> {
        let arg = property.args.first()?;
        match arg {
            PropertyArg::Place(place) => self.contract_place_to_callsite_place(checkpoint, place),
            PropertyArg::Expr(ContractExpr::Place(place)) => {
                self.contract_place_to_callsite_place(checkpoint, place)
            }
            PropertyArg::Expr(ContractExpr::IndexAccess { slice, .. }) => {
                match slice.as_ref() {
                    ContractExpr::Place(place) => {
                        self.contract_place_to_callsite_place(checkpoint, place)
                    }
                    _ => None,
                }
            }
            PropertyArg::Expr(ContractExpr::Const(index)) => {
                let index = usize::try_from(*index).ok()?;
                self.callsite_arg_place(checkpoint, index)
            }
            _ => None,
        }
    }

    /// Resolve the `index`-th property argument as a concrete checkpoint place.
    pub(crate) fn property_place_arg(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        property: &Property<'tcx>,
        index: usize,
    ) -> Option<PlaceKey> {
        let arg = property.args.get(index)?;
        match arg {
            PropertyArg::Place(place) => self.contract_place_to_callsite_place(checkpoint, place),
            PropertyArg::Expr(ContractExpr::Place(place)) => {
                self.contract_place_to_callsite_place(checkpoint, place)
            }
            PropertyArg::Expr(ContractExpr::Const(arg_index)) => {
                let arg_index = usize::try_from(*arg_index).ok()?;
                self.callsite_arg_place(checkpoint, arg_index)
            }
            _ => None,
        }
    }

    /// Resolve the target place of a property directly from a contract place
    /// without going through callee argument mapping.
    pub(crate) fn property_target_direct(&self, property: &Property<'tcx>) -> Option<PlaceKey> {
        let arg = property.args.first()?;
        match arg {
            PropertyArg::Place(place) => Some(self.resolve_contract_place(place)),
            PropertyArg::Expr(ContractExpr::Place(place)) => {
                Some(self.resolve_contract_place(place))
            }
            _ => None,
        }
    }

    /// Convert a contract place to a PlaceKey, resolving Arg(n) to Local(n+1).
    fn resolve_contract_place(&self, place: &ContractPlace<'tcx>) -> PlaceKey {
        let mut key = PlaceKey::from_contract_place(place);
        if let PlaceBaseKey::Arg(index) = key.base {
            key.base = PlaceBaseKey::Local(index + 1);
        }
        key
    }

    /// Resolve the type argument used by an alignment property.
    pub(crate) fn property_required_ty(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        property: &Property<'tcx>,
    ) -> Option<Ty<'tcx>> {
        property.args.iter().find_map(|arg| {
            let PropertyArg::Ty(ty) = arg else {
                return None;
            };
            Some(self.instantiate_callsite_ty(checkpoint, *ty))
        })
    }

    /// Resolve the type argument of a property directly without callee generic instantiation.
    pub(crate) fn property_required_ty_direct(
        &self,
        property: &Property<'tcx>,
    ) -> Option<Ty<'tcx>> {
        property.args.iter().find_map(|arg| {
            let PropertyArg::Ty(ty) = arg else {
                return None;
            };
            Some(*ty)
        })
    }

    /// Resolve the trailing length expression directly (without checkpoint binding).
    ///
    /// For checkpoint checks this extracts the last argument as an expression
    /// using the function's own parameter space.
    pub(crate) fn property_len_expr_direct(
        &self,
        property: &Property<'tcx>,
    ) -> Option<ContractExpr<'tcx>> {
        property.args.iter().rev().find_map(|arg| {
            let PropertyArg::Expr(expr) = arg else {
                return None;
            };
            Some(expr.clone())
        })
    }

    /// Resolve the trailing length expression at a concrete checkpoint.
    ///
    /// This keeps constants unchanged and rewrites callee argument places, such
    /// as `Arg_2` from std-contract JSON, to the concrete MIR place passed by
    /// the caller at this checkpoint.  Composite numeric expressions are rebound
    /// recursively.
    pub(crate) fn property_len_expr(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        property: &Property<'tcx>,
    ) -> Option<ContractExpr<'tcx>> {
        property.args.iter().rev().find_map(|arg| {
            let PropertyArg::Expr(expr) = arg else {
                return None;
            };
            self.bind_contract_expr_to_callsite(checkpoint, expr)
        })
    }

    /// Lower a rebound contract arithmetic expression into the common SMT term model.
    pub(crate) fn contract_expr_to_smt_term(
        &self,
        caller: rustc_hir::def_id::DefId,
        expr: &ContractExpr<'tcx>,
    ) -> Option<SmtTerm> {
        match expr {
            ContractExpr::Place(place) => {
                Some(SmtTerm::Place(PlaceKey::from_contract_place(place)))
            }
            ContractExpr::Const(value) => u64::try_from(*value).ok().map(SmtTerm::Const),
            ContractExpr::ConstParam { name, .. } => {
                Some(SmtTerm::ConstParam(name.clone()))
            }
            ContractExpr::SizeOf(ty) => {
                let size = self.required_size(caller, *ty)?;
                Some(SmtTerm::Const(size))
            }
            ContractExpr::AlignOf(ty) => {
                let align = self.required_alignment(caller, *ty)?;
                Some(SmtTerm::Const(align))
            }
            ContractExpr::Len(expr) => Some(SmtTerm::Value(format!(
                "len({})",
                self.contract_expr_label(expr)?
            ))),
            ContractExpr::IndexAccess { .. } => None,
            ContractExpr::Binary { op, lhs, rhs } => {
                let lhs = Box::new(self.contract_expr_to_smt_term(caller, lhs)?);
                let rhs = Box::new(self.contract_expr_to_smt_term(caller, rhs)?);
                match op {
                    NumericOp::Add => Some(SmtTerm::Add(lhs, rhs)),
                    NumericOp::Sub => Some(SmtTerm::Sub(lhs, rhs)),
                    NumericOp::Mul => Some(SmtTerm::Mul(lhs, rhs)),
                    NumericOp::Div => Some(SmtTerm::Div(lhs, rhs)),
                    NumericOp::Rem => Some(SmtTerm::Rem(lhs, rhs)),
                    NumericOp::BitAnd | NumericOp::BitOr | NumericOp::BitXor => None,
                }
            }
            ContractExpr::Unary { .. } | ContractExpr::Unknown => None,
        }
    }

    /// Resolve a `ValidNum` predicate list at a concrete checkpoint.
    pub(crate) fn property_numeric_predicates(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        property: &Property<'tcx>,
    ) -> Option<Vec<NumericPredicate<'tcx>>> {
        property.args.iter().find_map(|arg| {
            let PropertyArg::Predicates(predicates) = arg else {
                return None;
            };
            predicates
                .iter()
                .map(|predicate| {
                    Some(NumericPredicate {
                        lhs: self.bind_contract_expr_to_callsite(checkpoint, &predicate.lhs)?,
                        op: predicate.op,
                        rhs: self.bind_contract_expr_to_callsite(checkpoint, &predicate.rhs)?,
                    })
                })
                .collect()
        })
    }

    /// Convert a rebound contract predicate into the shared SMT predicate model.
    pub(crate) fn numeric_predicate_to_smt_predicate(
        &self,
        caller: rustc_hir::def_id::DefId,
        predicate: &NumericPredicate<'tcx>,
    ) -> Option<SmtPredicate> {
        let lhs = self.contract_expr_to_smt_term(caller, &predicate.lhs)?;
        let rhs = self.contract_expr_to_smt_term(caller, &predicate.rhs)?;
        Some(match predicate.op {
            RelOp::Eq => SmtPredicate::Eq(lhs, rhs),
            RelOp::Ne => SmtPredicate::Ne(lhs, rhs),
            RelOp::Lt => SmtPredicate::Lt(lhs, rhs),
            RelOp::Le => SmtPredicate::Le(lhs, rhs),
            RelOp::Gt => SmtPredicate::Gt(lhs, rhs),
            RelOp::Ge => SmtPredicate::Ge(lhs, rhs),
        })
    }

    /// Resolve and lower `ValidNum` predicates, expanding non-scalar helpers.
    pub(crate) fn property_numeric_smt_predicates(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        property: &Property<'tcx>,
    ) -> Option<Vec<SmtPredicate>> {
        let predicates = self.property_numeric_predicates(checkpoint, property)?;
        let mut lowered = Vec::new();
        for predicate in predicates {
            if let Some(expanded) = self.expand_index_access_predicate(checkpoint, &predicate)? {
                lowered.extend(expanded);
            } else {
                lowered
                    .push(self.numeric_predicate_to_smt_predicate(checkpoint.caller, &predicate)?);
            }
        }
        Some(lowered)
    }

    /// Resolve an `InBound(index_access(slice, index))` property to range predicates.
    pub(crate) fn property_index_access_in_bound_predicates(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        property: &Property<'tcx>,
    ) -> Option<Vec<SmtPredicate>> {
        property.args.iter().find_map(|arg| {
            let PropertyArg::Expr(expr) = arg else {
                return None;
            };
            if !matches!(expr, ContractExpr::IndexAccess { .. }) {
                return None;
            }
            let rebound = self.bind_contract_expr_to_callsite(checkpoint, expr)?;
            self.index_access_in_bound_predicates(checkpoint, &rebound)
        })
    }

    fn expand_index_access_predicate(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        predicate: &NumericPredicate<'tcx>,
    ) -> Option<Option<Vec<SmtPredicate>>> {
        let ContractExpr::IndexAccess { slice, index } = &predicate.lhs else {
            if matches!(predicate.rhs, ContractExpr::IndexAccess { .. }) {
                return None;
            }
            return Some(None);
        };
        if !matches!(predicate.op, RelOp::Ne) || !matches!(predicate.rhs, ContractExpr::Const(0)) {
            return None;
        }

        self.index_access_in_bound_predicates(
            checkpoint,
            &ContractExpr::IndexAccess {
                slice: slice.clone(),
                index: index.clone(),
            },
        )
        .map(Some)
    }

    fn index_access_in_bound_predicates(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        expr: &ContractExpr<'tcx>,
    ) -> Option<Vec<SmtPredicate>> {
        let ContractExpr::IndexAccess { slice, index } = expr else {
            return None;
        };
        let len = SmtTerm::Value(format!("len({})", self.contract_expr_label(slice)?));
        let (lower, upper) = self.slice_index_bounds(checkpoint.caller, index, len.clone())?;
        Some(vec![
            SmtPredicate::Le(SmtTerm::Const(0), lower.clone()),
            SmtPredicate::Le(lower, upper.clone()),
            SmtPredicate::Le(upper, len),
        ])
    }

    fn slice_index_bounds(
        &self,
        caller: rustc_hir::def_id::DefId,
        index: &ContractExpr<'tcx>,
        len: SmtTerm,
    ) -> Option<(SmtTerm, SmtTerm)> {
        let index_term = self.contract_expr_to_smt_term(caller, index)?;
        let Some(kind) = self.slice_index_kind(caller, index) else {
            return Some((
                index_term.clone(),
                SmtTerm::Add(Box::new(index_term), Box::new(SmtTerm::Const(1))),
            ));
        };

        match kind {
            SliceIndexKind::Scalar => Some((
                index_term.clone(),
                SmtTerm::Add(Box::new(index_term), Box::new(SmtTerm::Const(1))),
            )),
            SliceIndexKind::Range => Some((
                self.contract_expr_field_term(caller, index, 0)?,
                self.contract_expr_field_term(caller, index, 1)?,
            )),
            SliceIndexKind::RangeFrom => Some((
                self.contract_expr_field_term(caller, index, 0)?,
                len,
            )),
            SliceIndexKind::RangeTo => Some((
                SmtTerm::Const(0),
                self.contract_expr_field_term(caller, index, 0)?,
            )),
            SliceIndexKind::RangeFull => Some((SmtTerm::Const(0), len)),
            SliceIndexKind::RangeInclusive => {
                let start = self.contract_expr_field_term(caller, index, 0)?;
                let end = self.contract_expr_field_term(caller, index, 1)?;
                Some((
                    start,
                    SmtTerm::Add(Box::new(end), Box::new(SmtTerm::Const(1))),
                ))
            }
            SliceIndexKind::RangeToInclusive => {
                let end = self.contract_expr_field_term(caller, index, 0)?;
                Some((
                    SmtTerm::Const(0),
                    SmtTerm::Add(Box::new(end), Box::new(SmtTerm::Const(1))),
                ))
            }
        }
    }

    fn slice_index_kind(
        &self,
        caller: rustc_hir::def_id::DefId,
        index: &ContractExpr<'tcx>,
    ) -> Option<SliceIndexKind> {
        let place = self.contract_expr_place(index)?;
        let ty = self.place_ty_for_caller(caller, &place)?;
        if matches!(ty.kind(), TyKind::Uint(UintTy::Usize)) {
            return Some(SliceIndexKind::Scalar);
        }

        let ty_name = format!("{ty:?}");
        if ty_name.contains("RangeToInclusive<usize>") {
            Some(SliceIndexKind::RangeToInclusive)
        } else if ty_name.contains("RangeInclusive<usize>") {
            Some(SliceIndexKind::RangeInclusive)
        } else if ty_name.contains("RangeFrom<usize>") {
            Some(SliceIndexKind::RangeFrom)
        } else if ty_name.contains("RangeTo<usize>") {
            Some(SliceIndexKind::RangeTo)
        } else if ty_name.contains("RangeFull") {
            Some(SliceIndexKind::RangeFull)
        } else if ty_name.contains("Range<usize>") || ty_name.contains("IndexRange") {
            Some(SliceIndexKind::Range)
        } else {
            None
        }
    }

    fn contract_expr_field_term(
        &self,
        caller: rustc_hir::def_id::DefId,
        expr: &ContractExpr<'tcx>,
        field: usize,
    ) -> Option<SmtTerm> {
        let mut place = self.contract_expr_place(expr)?;
        place.fields.push(field);
        self.contract_expr_to_smt_term(caller, &contract_expr_from_place_key(place))
    }

    fn contract_expr_place(&self, expr: &ContractExpr<'tcx>) -> Option<PlaceKey> {
        let ContractExpr::Place(place) = expr else {
            return None;
        };
        Some(PlaceKey::from_contract_place(place))
    }

    fn contract_expr_label(&self, expr: &ContractExpr<'tcx>) -> Option<String> {
        match expr {
            ContractExpr::Place(place) => Some(place_label(&PlaceKey::from_contract_place(place))),
            ContractExpr::Const(value) => Some(value.to_string()),
            ContractExpr::ConstParam { name, .. } => Some(name.clone()),
            _ => None,
        }
    }

    fn place_ty_for_caller(
        &self,
        caller: rustc_hir::def_id::DefId,
        place: &PlaceKey,
    ) -> Option<Ty<'tcx>> {
        if !place.fields.is_empty() {
            return None;
        }
        let local = match place.base {
            PlaceBaseKey::Return => Local::from_usize(0),
            PlaceBaseKey::Local(local) => Local::from_usize(local),
            PlaceBaseKey::Arg(_) => return None,
        };
        Some(self.tcx.optimized_mir(caller).local_decls[local].ty)
    }

    pub(crate) fn infer_pointee_ty(
        &self,
        caller: rustc_hir::def_id::DefId,
        place: &PlaceKey,
    ) -> Option<Ty<'tcx>> {
        let ty = self.place_ty_for_caller(caller, place)?;
        infer_element_ty(ty)
    }

    /// Return true if a place is a safe reference/slice/string carrying object length.
    pub(crate) fn is_len_carrying_place_for_caller(
        &self,
        caller: rustc_hir::def_id::DefId,
        place: &PlaceKey,
    ) -> bool {
        self.place_ty_for_caller(caller, place)
            .is_some_and(is_len_carrying_ty)
    }

    fn bind_contract_expr_to_callsite(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        expr: &ContractExpr<'tcx>,
    ) -> Option<ContractExpr<'tcx>> {
        match expr {
            ContractExpr::Place(place) => self.contract_place_to_callsite_expr(checkpoint, place),
            ContractExpr::Const(value) => Some(ContractExpr::Const(*value)),
            ContractExpr::ConstParam { index, name } => self
                .instantiate_callsite_const(checkpoint, *index)
                .map(ContractExpr::Const)
                .or_else(|| {
                    Some(ContractExpr::ConstParam {
                        index: *index,
                        name: name.clone(),
                    })
                }),
            ContractExpr::SizeOf(ty) => Some(ContractExpr::SizeOf(
                self.instantiate_callsite_ty(checkpoint, *ty),
            )),
            ContractExpr::AlignOf(ty) => Some(ContractExpr::AlignOf(
                self.instantiate_callsite_ty(checkpoint, *ty),
            )),
            ContractExpr::Len(expr) => Some(ContractExpr::Len(Box::new(
                self.bind_contract_expr_to_callsite(checkpoint, expr)?,
            ))),
            ContractExpr::IndexAccess { slice, index } => Some(ContractExpr::IndexAccess {
                slice: Box::new(self.bind_contract_expr_to_callsite(checkpoint, slice)?),
                index: Box::new(self.bind_contract_expr_to_callsite(checkpoint, index)?),
            }),
            ContractExpr::Binary { op, lhs, rhs } => Some(ContractExpr::Binary {
                op: *op,
                lhs: Box::new(self.bind_contract_expr_to_callsite(checkpoint, lhs)?),
                rhs: Box::new(self.bind_contract_expr_to_callsite(checkpoint, rhs)?),
            }),
            ContractExpr::Unary { op, expr } => Some(ContractExpr::Unary {
                op: *op,
                expr: Box::new(self.bind_contract_expr_to_callsite(checkpoint, expr)?),
            }),
            ContractExpr::Unknown => Some(ContractExpr::Unknown),
        }
    }

    fn contract_place_to_callsite_expr(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        place: &ContractPlace<'tcx>,
    ) -> Option<ContractExpr<'tcx>> {
        let key = PlaceKey::from_contract_place(place);
        match place.base {
            PlaceBase::Arg(index) => self.callsite_arg_expr(checkpoint, index, &key.fields),
            PlaceBase::Local(local) => {
                if let Some(index) = checkpoint
                    .callee
                    .and_then(|callee| callee_param_index_for_local(self.tcx, callee, local))
                {
                    self.callsite_arg_expr(checkpoint, index, &key.fields)
                } else {
                    Some(ContractExpr::Place(place.clone()))
                }
            }
            PlaceBase::Return => Some(ContractExpr::Place(place.clone())),
        }
    }

    fn callsite_arg_expr(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        index: usize,
        fields: &[usize],
    ) -> Option<ContractExpr<'tcx>> {
        // Try checkpoint args first
        let operand = checkpoint.args.get(index)
            // Fallback: read MIR body directly (needed for Rust 1.96+ where
            // checkpoint may miss some call arguments)
            .or_else(|| {
                let body = self.tcx.optimized_mir(checkpoint.caller);
                let terminator = body.basic_blocks[checkpoint.block].terminator();
                if let TerminatorKind::Call { args, .. } = &terminator.kind {
                    args.get(index).map(|a| &a.node)
                } else {
                    None
                }
            })?;
        if fields.is_empty()
            && let Operand::Constant(constant) = operand
        {
            let const_debug = format!("{:?}", constant.const_);
            if let Some(value) = const_int_from_debug(&const_debug) {
                return Some(ContractExpr::Const(value));
            }
            if let Some(name) = const_param_name_from_debug(&const_debug) {
                return Some(ContractExpr::ConstParam {
                    index: 0,
                    name,
                });
            }
            rap_warn!("callsite Const debug={}", const_debug);
        }
        self.callsite_arg_place_with_fields(checkpoint, index, fields)
            .map(contract_expr_from_place_key)
    }

    /// Convert a contract place into a concrete MIR place when possible.
    pub(crate) fn contract_place_to_callsite_place(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        place: &ContractPlace<'tcx>,
    ) -> Option<PlaceKey> {
        match place.base {
            PlaceBase::Arg(index) => self.callsite_arg_place_with_fields(
                checkpoint,
                index,
                &PlaceKey::from_contract_place(place).fields,
            ),
            PlaceBase::Local(local) => {
                if let Some(index) = checkpoint
                    .callee
                    .and_then(|callee| callee_param_index_for_local(self.tcx, callee, local))
                {
                    self.callsite_arg_place_with_fields(
                        checkpoint,
                        index,
                        &PlaceKey::from_contract_place(place).fields,
                    )
                } else {
                    Some(PlaceKey::from_contract_place(place))
                }
            }
            PlaceBase::Return => Some(PlaceKey::from_contract_place(place)),
        }
    }

    /// Return the concrete MIR place used as the `index`-th call argument.
    pub(crate) fn callsite_arg_place(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        index: usize,
    ) -> Option<PlaceKey> {
        let operand = checkpoint.args.get(index)?;
        operand_place(operand)
    }

    /// Return the `index`-th call argument as a common SMT term.
    pub(crate) fn callsite_arg_smt_term(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        index: usize,
    ) -> Option<SmtTerm> {
        let expr = self.callsite_arg_expr(checkpoint, index, &[])?;
        self.contract_expr_to_smt_term(checkpoint.caller, &expr)
    }

    /// Return the pointee size for a concrete pointer place.
    pub(crate) fn place_pointee_size(
        &self,
        caller: rustc_hir::def_id::DefId,
        place: &PlaceKey,
    ) -> Option<u64> {
        if !place.fields.is_empty() {
            return None;
        }
        let local = match place.base {
            PlaceBaseKey::Return => Local::from_usize(0),
            PlaceBaseKey::Local(local) => Local::from_usize(local),
            PlaceBaseKey::Arg(_) => return None,
        };
        let body = self.tcx.optimized_mir(caller);
        let ty = body.local_decls[local].ty;
        let pointee = pointee_ty(ty)?;
        self.type_layout(caller, pointee).map(|(_, size)| size)
    }

    /// Return the `index`-th call argument with contract projections appended.
    pub(crate) fn callsite_arg_place_with_fields(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        index: usize,
        fields: &[usize],
    ) -> Option<PlaceKey> {
        let mut place = self.callsite_arg_place(checkpoint, index)?;
        place.fields.extend(fields.iter().copied());
        Some(place)
    }

    /// Replace a callee generic parameter with its concrete checkpoint type.
    pub(crate) fn instantiate_callsite_ty(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        ty: Ty<'tcx>,
    ) -> Ty<'tcx> {
        let TyKind::Param(param) = ty.kind() else {
            return ty;
        };

        let body = self.tcx.optimized_mir(checkpoint.caller);
        let terminator = body.basic_blocks[checkpoint.block].terminator();
        let TerminatorKind::Call { func, .. } = &terminator.kind else {
            return ty;
        };
        let Operand::Constant(func_constant) = func else {
            return ty;
        };
        let TyKind::FnDef(_, args) = func_constant.const_.ty().kind() else {
            return ty;
        };
        let Some(arg) = args.get(param.index as usize) else {
            return ty;
        };
        match arg.kind() {
            GenericArgKind::Type(actual_ty) => actual_ty,
            _ => ty,
        }
    }

    /// Replace a callee const generic parameter with its concrete checkpoint value.
    pub(crate) fn instantiate_callsite_const(
        &self,
        checkpoint: &Checkpoint<'tcx>,
        index: u32,
    ) -> Option<u128> {
        let body = self.tcx.optimized_mir(checkpoint.caller);
        let terminator = body.basic_blocks[checkpoint.block].terminator();
        let TerminatorKind::Call { func, .. } = &terminator.kind else {
            return None;
        };
        let Operand::Constant(func_constant) = func else {
            return None;
        };
        let TyKind::FnDef(_, args) = func_constant.const_.ty().kind() else {
            return None;
        };
        let arg = args.get(index as usize)?;
        match arg.kind() {
            GenericArgKind::Const(actual_const) => actual_const
                .try_to_target_usize(self.tcx)
                .map(|value| value as u128)
                .or_else(|| const_int_from_debug(&format!("{actual_const:?}"))),
            _ => None,
        }
    }

    /// Return ABI alignment and size for a type.
    pub(crate) fn type_layout(
        &self,
        caller: rustc_hir::def_id::DefId,
        ty: Ty<'tcx>,
    ) -> Option<(u64, u64)> {
        safe_type_layout(self.tcx, caller, ty)
    }

    /// Return the alignment required by a property type.
    ///
    /// For concrete types this is the ABI alignment. For generic parameters with
    /// finite representative candidates, the requirement must hold for every
    /// candidate, so we use the maximum candidate alignment.
    pub(crate) fn required_alignment(
        &self,
        caller: rustc_hir::def_id::DefId,
        ty: Ty<'tcx>,
    ) -> Option<u64> {
        if let Some((align, _)) = self.type_layout(caller, ty).filter(|(align, _)| *align > 0) {
            return Some(align);
        }
        if let Some(max_align) = self
            .generic_candidate_alignments(caller, ty)
            .and_then(|candidates| candidates.into_iter().max())
        {
            return Some(max_align);
        }
        if let TyKind::Array(elem, _) = ty.kind()
            && matches!(elem.kind(), TyKind::Param(_))
        {
            return Some(0);
        }
        if matches!(ty.kind(), TyKind::Param(_)) {
            return Some(0);
        }
        if matches!(ty.kind(), TyKind::Ref(..) | TyKind::RawPtr(..)) {
            return Some(0);
        }
        None
    }

    /// Return a conservative byte size for a concrete or bounded generic type.
    ///
    /// For a generic parameter with representative candidates, every candidate
    /// must satisfy a numeric precondition.  We therefore use the maximum
    /// candidate size for upper-bound formulas such as
    /// `size_of(T) * len <= isize::MAX`.
    pub(crate) fn required_size(
        &self,
        caller: rustc_hir::def_id::DefId,
        ty: Ty<'tcx>,
    ) -> Option<u64> {
        if let TyKind::Array(elem, _) = ty.kind()
            && matches!(elem.kind(), TyKind::Param(_))
        {
            return Some(0);
        }
        if !matches!(ty.kind(), TyKind::Param(_)) {
            return self.type_layout(caller, ty).map(|(_, size)| size);
        }
        if let Some(max_size) = self
            .generic_candidate_sizes(caller, ty)
            .and_then(|candidates| candidates.into_iter().max())
        {
            return Some(max_size);
        }
        if matches!(ty.kind(), TyKind::Param(_)) {
            return Some(0);
        }
        None
    }

    /// Classify whether a type is definitely zero-sized, definitely non-zero,
    /// or still layout-ambiguous under the current generic bounds.
    pub(crate) fn type_size_class(
        &self,
        caller: rustc_hir::def_id::DefId,
        ty: Ty<'tcx>,
    ) -> TypeSizeClass {
        if let TyKind::Array(elem, _) = ty.kind()
            && matches!(elem.kind(), TyKind::Param(_))
        {
            return TypeSizeClass::Unknown;
        }
        if !matches!(ty.kind(), TyKind::Param(_)) {
            return match self.type_layout(caller, ty).map(|(_, size)| size) {
                Some(0) => TypeSizeClass::Zero,
                Some(_) => TypeSizeClass::NonZero,
                None => TypeSizeClass::Unknown,
            };
        }

        let Some(sizes) = self.generic_candidate_sizes(caller, ty) else {
            return TypeSizeClass::Unknown;
        };
        if sizes.iter().all(|size| *size == 0) {
            TypeSizeClass::Zero
        } else if sizes.iter().all(|size| *size > 0) {
            TypeSizeClass::NonZero
        } else {
            TypeSizeClass::Unknown
        }
    }

    fn generic_candidate_alignments(
        &self,
        caller: rustc_hir::def_id::DefId,
        ty: Ty<'tcx>,
    ) -> Option<Vec<u64>> {
        let candidates = GenericTypeCandidates::for_def(self.tcx, caller);
        let alignments = candidates
            .candidates_for_ty(ty)?
            .iter()
            .filter_map(|candidate| self.type_layout(caller, *candidate).map(|(align, _)| align))
            .filter(|align| *align > 0)
            .collect::<Vec<_>>();
        if alignments.is_empty() {
            None
        } else {
            Some(alignments)
        }
    }

    fn generic_candidate_sizes(
        &self,
        caller: rustc_hir::def_id::DefId,
        ty: Ty<'tcx>,
    ) -> Option<Vec<u64>> {
        let candidates = GenericTypeCandidates::for_def(self.tcx, caller);
        let sizes = candidates
            .candidates_for_ty(ty)?
            .iter()
            .filter_map(|candidate| self.type_layout(caller, *candidate).map(|(_, size)| size))
            .collect::<Vec<_>>();
        if sizes.is_empty() { None } else { Some(sizes) }
    }
}

/// Trivalent size classification for type-dependent composite SPs.
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub(crate) enum TypeSizeClass {
    Zero,
    NonZero,
    Unknown,
}

#[derive(Clone, Copy, Debug, Eq, PartialEq)]
enum SliceIndexKind {
    Scalar,
    Range,
    RangeFrom,
    RangeTo,
    RangeFull,
    RangeInclusive,
    RangeToInclusive,
}

/// General SMT obligation produced by an SP-specific lowering.
#[derive(Clone, Debug)]
pub enum SmtObligation {
    /// Prove that the address denoted by `place` is aligned to `align` bytes.
    Aligned {
        place: PlaceKey,
        align: u64,
        ty_name: String,
    },
    /// Future form for non-zero integer/address requirements.
    NonZero { place: PlaceKey },
    /// Future form for interval/bounds requirements.
    Range {
        value: PlaceKey,
        lower: i128,
        upper: Option<i128>,
    },
    /// Prove that `place` points to `access_count` elements inside its object.
    InBounds {
        place: PlaceKey,
        ty_name: String,
        elem_size: u64,
        access_count: SmtTerm,
    },
    /// Prove that pointer arithmetic starting at `place` stays inside the
    /// matched object for the whole delta range.
    PointerRangeInBounds {
        place: PlaceKey,
        ty_name: String,
        lower_delta: SmtTerm,
        upper_delta: SmtTerm,
    },
    /// Prove that `place` denotes initialized memory for `elements` elements.
    Initialized {
        place: PlaceKey,
        ty_name: String,
        elements: SmtTerm,
        /// Byte size of one element of the required type (None = unknown).
        elem_size: Option<u64>,
        /// Per-element size of the inner array element type.
        array_elem_size: Option<u64>,
        /// SMT term for the array length const-generic (when type is [T; N]).
        array_len_term: Option<SmtTerm>,
    },
    /// Prove that `place` points to `elements` elements in one live allocation.
    Allocated {
        place: PlaceKey,
        ty_name: String,
        elements: SmtTerm,
    },
    /// Prove that two pointer ranges do not overlap.
    NonOverlapping {
        left: PlaceKey,
        right: PlaceKey,
        left_count: SmtTerm,
        right_count: SmtTerm,
        elem_size: u64,
    },
    /// Prove one or more numeric predicates.
    Predicate { predicates: Vec<SmtPredicate> },
}

impl SmtObligation {
    /// Render a compact obligation description for diagnostics.
    pub fn describe(&self) -> String {
        match self {
            SmtObligation::Aligned {
                place,
                align,
                ty_name,
            } => {
                format!(
                    "Align({}, {}, {}-byte boundary)",
                    place_label(place),
                    ty_name,
                    align
                )
            }
            SmtObligation::NonZero { place } => format!("NonZero({})", place_label(place)),
            SmtObligation::Range {
                value,
                lower,
                upper,
            } => match upper {
                Some(upper) => format!("Range({}, {lower}..{upper})", place_label(value)),
                None => format!("Range({}, {lower}..)", place_label(value)),
            },
            SmtObligation::InBounds {
                place,
                ty_name,
                elem_size,
                access_count,
            } => format!(
                "InBound({}, {}, {} element(s), {} byte(s) each)",
                place_label(place),
                ty_name,
                access_count.describe(),
                elem_size
            ),
            SmtObligation::PointerRangeInBounds {
                place,
                ty_name,
                lower_delta,
                upper_delta,
            } => format!(
                "PointerRangeInBound({}, {}, lower={}, upper={})",
                place_label(place),
                ty_name,
                lower_delta.describe(),
                upper_delta.describe()
            ),
            SmtObligation::Initialized {
                place,
                ty_name,
                elements,
                ..
            } => format!(
                "Init({}, {}, {} element(s))",
                place_label(place),
                ty_name,
                elements.describe()
            ),
            SmtObligation::Allocated {
                place,
                ty_name,
                elements,
            } => format!(
                "Allocated({}, {}, {} element(s))",
                place_label(place),
                ty_name,
                elements.describe()
            ),
            SmtObligation::NonOverlapping {
                left,
                right,
                left_count,
                right_count,
                elem_size,
            } => format!(
                "NonOverlap({}, {}, left={} element(s), right={} element(s), elem_size={})",
                place_label(left),
                place_label(right),
                left_count.describe(),
                right_count.describe(),
                elem_size
            ),
            SmtObligation::Predicate { predicates } => {
                let rendered = predicates
                    .iter()
                    .map(SmtPredicate::describe)
                    .collect::<Vec<_>>()
                    .join(" && ");
                format!("ValidNum({rendered})")
            }
        }
    }
}

/// Common SMT term used by diagnostics and property-independent query building.
#[derive(Clone, Debug)]
pub enum SmtTerm {
    Place(PlaceKey),
    Value(String),
    Const(u64),
    /// Const-generic parameter value (produces the same SMT constant as
    /// `term_for_value` for `AbstractValue::Const`).
    ConstParam(String),
    Add(Box<SmtTerm>, Box<SmtTerm>),
    Sub(Box<SmtTerm>, Box<SmtTerm>),
    Mul(Box<SmtTerm>, Box<SmtTerm>),
    Div(Box<SmtTerm>, Box<SmtTerm>),
    Rem(Box<SmtTerm>, Box<SmtTerm>),
}

impl SmtTerm {
    /// Render this term in compact source-facing form.
    pub fn describe(&self) -> String {
        match self {
            SmtTerm::Place(place) => place_label(place),
            SmtTerm::Value(value) => value.clone(),
            SmtTerm::ConstParam(value) => value.clone(),
            SmtTerm::Const(value) => value.to_string(),
            SmtTerm::Add(lhs, rhs) => format!("({} + {})", lhs.describe(), rhs.describe()),
            SmtTerm::Sub(lhs, rhs) => format!("({} - {})", lhs.describe(), rhs.describe()),
            SmtTerm::Mul(lhs, rhs) => format!("({} * {})", lhs.describe(), rhs.describe()),
            SmtTerm::Div(lhs, rhs) => format!("({} / {})", lhs.describe(), rhs.describe()),
            SmtTerm::Rem(lhs, rhs) => format!("({} % {})", lhs.describe(), rhs.describe()),
        }
    }
}

/// Common boolean predicate asserted or refuted by SMT queries.
#[derive(Clone, Debug)]
pub enum SmtPredicate {
    Eq(SmtTerm, SmtTerm),
    Ne(SmtTerm, SmtTerm),
    Le(SmtTerm, SmtTerm),
    Lt(SmtTerm, SmtTerm),
    Ge(SmtTerm, SmtTerm),
    Gt(SmtTerm, SmtTerm),
    And(Vec<SmtPredicate>),
    Divisible {
        term: SmtTerm,
        modulus: u64,
    },
    InBounds {
        index: SmtTerm,
        access_count: SmtTerm,
        len: SmtTerm,
    },
    NonOverlapping {
        left: SmtTerm,
        right: SmtTerm,
        left_count: SmtTerm,
        right_count: SmtTerm,
        elem_size: u64,
    },
    Not(Box<SmtPredicate>),
    Custom(String),
}

impl SmtPredicate {
    /// Render this predicate for diagnostics.
    pub fn describe(&self) -> String {
        match self {
            SmtPredicate::Eq(lhs, rhs) => format!("{} == {}", lhs.describe(), rhs.describe()),
            SmtPredicate::Ne(lhs, rhs) => format!("{} != {}", lhs.describe(), rhs.describe()),
            SmtPredicate::Le(lhs, rhs) => format!("{} <= {}", lhs.describe(), rhs.describe()),
            SmtPredicate::Lt(lhs, rhs) => format!("{} < {}", lhs.describe(), rhs.describe()),
            SmtPredicate::Ge(lhs, rhs) => format!("{} >= {}", lhs.describe(), rhs.describe()),
            SmtPredicate::Gt(lhs, rhs) => format!("{} > {}", lhs.describe(), rhs.describe()),
            SmtPredicate::And(predicates) => predicates
                .iter()
                .map(SmtPredicate::describe)
                .collect::<Vec<_>>()
                .join(" && "),
            SmtPredicate::Divisible { term, modulus } => {
                format!("{} % {modulus} == 0", term.describe())
            }
            SmtPredicate::InBounds {
                index,
                access_count,
                len,
            } => format!(
                "0 <= {} && {} + {} <= {}",
                index.describe(),
                index.describe(),
                access_count.describe(),
                len.describe()
            ),
            SmtPredicate::NonOverlapping {
                left,
                right,
                left_count,
                right_count,
                elem_size,
            } => format!(
                "{} + {} * {} <= {} || {} + {} * {} <= {}",
                left.describe(),
                left_count.describe(),
                elem_size,
                right.describe(),
                right.describe(),
                right_count.describe(),
                elem_size,
                left.describe()
            ),
            SmtPredicate::Not(predicate) => format!("not({})", predicate.describe()),
            SmtPredicate::Custom(text) => text.clone(),
        }
    }
}

/// Solver query built from path facts plus one negated obligation.
#[derive(Clone, Debug)]
pub struct SmtQuery {
    /// Property-specific obligation being proved.
    pub obligation: SmtObligation,
    /// Assumptions asserted from forward facts.
    pub assumptions: Vec<SmtPredicate>,
    /// Negated goal sent to the solver.
    pub negated_goal: SmtPredicate,
}

impl SmtQuery {
    /// Create a query description.
    pub fn new(
        obligation: SmtObligation,
        assumptions: Vec<SmtPredicate>,
        negated_goal: SmtPredicate,
    ) -> Self {
        Self {
            obligation,
            assumptions,
            negated_goal,
        }
    }
}

/// Result of one SMT check.
#[derive(Clone, Debug)]
pub struct SmtCheckResult {
    /// Final status produced by the SMT backend.
    pub result: CheckResult,
    /// Optional structured query description.
    pub query: Option<SmtQuery>,
    /// Human-readable explanation.
    pub notes: Vec<String>,
}

impl SmtCheckResult {
    /// Build a proved SMT result.
    pub fn proved(note: impl Into<String>) -> Self {
        Self {
            result: CheckResult::Proved,
            query: None,
            notes: vec![note.into()],
        }
    }

    /// Build an unknown SMT result.
    pub fn unknown(note: impl Into<String>) -> Self {
        Self {
            result: CheckResult::Unknown,
            query: None,
            notes: vec![note.into()],
        }
    }

    /// Attach the query that produced this result.
    pub fn with_query(mut self, query: SmtQuery) -> Self {
        self.query = Some(query);
        self
    }

    /// Add a diagnostic note to this result.
    pub fn with_note(mut self, note: impl Into<String>) -> Self {
        self.notes.push(note.into());
        self
    }

    /// Render this SMT result as a diagnostic block.
    pub fn describe(&self) -> String {
        let mut lines = vec![format!("      smt check: {:?}", self.result)];
        if let Some(query) = &self.query {
            lines.push(format!("        |_ goal: {}", query.obligation.describe()));
            if !query.assumptions.is_empty() {
                lines.push("        |_ known facts:".to_string());
                for assumption in &query.assumptions {
                    lines.push(format!("        |  |_ {}", assumption.describe()));
                }
            }
            lines.push(format!(
                "        |_ checked: {}",
                query.negated_goal.describe()
            ));
        }
        if let Some((first, rest)) = self.notes.split_first() {
            lines.push(format!("        |_ verdict: {first}"));
            for note in rest {
                if let Some(hint) = note.strip_prefix("hint: ") {
                    lines.push(format!("        |_ hint: {hint}"));
                } else {
                    lines.push(format!("        |_ detail: {note}"));
                }
            }
        }
        lines.join("\n")
    }
}

fn failed_smt(note: impl Into<String>) -> SmtCheckResult {
    SmtCheckResult {
        result: CheckResult::Failed,
        query: None,
        notes: vec![note.into()],
    }
}

fn smt_term_const_u64(term: &SmtTerm) -> Option<u64> {
    match term {
        SmtTerm::Const(value) => Some(*value),
        _ => None,
    }
}

fn pointer_range_negated_goal(
    index: SmtTerm,
    lower_delta: SmtTerm,
    upper_delta: SmtTerm,
    len: SmtTerm,
) -> SmtPredicate {
    let lower_index = SmtTerm::Add(Box::new(index.clone()), Box::new(lower_delta));
    let upper_index = SmtTerm::Add(Box::new(index.clone()), Box::new(upper_delta));
    SmtPredicate::Not(Box::new(SmtPredicate::And(vec![
        SmtPredicate::Ge(index.clone(), SmtTerm::Const(0)),
        SmtPredicate::Le(index, len.clone()),
        SmtPredicate::Ge(lower_index, SmtTerm::Const(0)),
        SmtPredicate::Le(upper_index, len),
    ])))
}

/// Per-query SMT term builder over a forward visit result.
pub(crate) struct SmtModel<'a, 'ctx, 'tcx> {
    tcx: TyCtxt<'tcx>,
    checkpoint: &'a Checkpoint<'tcx>,
    forward: &'a ForwardVisitResult<'tcx>,
    ctx: &'ctx Context,
    place_terms: HashMap<PlaceKey, Int<'ctx>>,
    /// Shared Z3 constants per MIR local — ensures every reference to the
    /// same local produces the exact same SMT term (e.g. `mid` used in both
    /// `ptr.add` and `unchecked_sub`).
    local_terms: HashMap<usize, Int<'ctx>>,
    symbolic_align_terms: HashMap<String, Int<'ctx>>,
    symbolic_len_terms: HashMap<String, Int<'ctx>>,
    const_terms: HashMap<String, Int<'ctx>>,
    assumptions: Vec<SmtPredicate>,
    /// Set to true when IndexAccess InBound assumptions were added from caller contract
    has_index_access_assumptions: bool,
}

impl<'a, 'ctx, 'tcx> SmtModel<'a, 'ctx, 'tcx> {
    /// Create a fresh SMT model builder.
    pub(crate) fn new(
        tcx: TyCtxt<'tcx>,
        checkpoint: &'a Checkpoint<'tcx>,
        forward: &'a ForwardVisitResult<'tcx>,
        ctx: &'ctx Context,
    ) -> Self {
        Self {
            tcx,
            checkpoint,
            forward,
            ctx,
            place_terms: HashMap::new(),
            local_terms: HashMap::new(),
            symbolic_align_terms: HashMap::new(),
            symbolic_len_terms: HashMap::new(),
            const_terms: HashMap::new(),
            assumptions: Vec::new(),
            has_index_access_assumptions: false,
        }
    }

    /// Create or return a cached symbolic alignment constant for a type name.
    pub(crate) fn symbolic_align_term(&mut self, ty_name: &str) -> Int<'ctx> {
        let ty_name = normalize_init_ty_name(ty_name);
        if let Some(term) = self.symbolic_align_terms.get(&ty_name) {
            return term.clone();
        }
        let term = Int::new_const(self.ctx, format!("align_{ty_name}"));
        self.symbolic_align_terms
            .insert(ty_name.to_string(), term.clone());
        term
    }

    fn symbolic_len_term(&mut self, len_key: &str) -> Int<'ctx> {
        let name = sanitize_smt_name(len_key);
        if let Some(term) = self.symbolic_len_terms.get(&name) {
            return term.clone();
        }
        let term = Int::new_const(self.ctx, name.as_str());
        self.symbolic_len_terms.insert(name, term.clone());
        term
    }

    /// Check whether a ContractFact in the forward facts targets the same
    /// (or Cast-equivalent) place with the given property kind.
    ///
    /// Used by struct-invariant checkpoint checks to short-circuit when a
    /// caller `#[rapx::requires]` already establishes the property.
    fn has_equivalent_contract_fact(&mut self, place: &PlaceKey, _kind: PropertyKind) -> bool {
        let Some(target_term) = self.term_for_place(place) else {
            return false;
        };
        for fact in &self.forward.facts {
            let StateFact::Contract(property) = fact else {
                continue;
            };
            let is_target_kind =
                matches!(property.kind, PropertyKind::InBound | PropertyKind::Init);
            if !is_target_kind {
                continue;
            }
            let Some(contract_target) = property.args.first().and_then(|arg| {
                if let PropertyArg::Place(contract_place) = arg {
                    let mut key = PlaceKey::from_contract_place(contract_place);
                    if let PlaceBaseKey::Arg(index) = key.base {
                        key.base = PlaceBaseKey::Local(index + 1);
                    }
                    Some(key)
                } else {
                    None
                }
            }) else {
                continue;
            };
            let Some(contract_term) = self.term_for_place(&contract_target) else {
                continue;
            };
            if target_term.eq(&contract_term) {
                return true;
            }
        }
        false
    }

    fn contract_predicate_to_smt(
        &mut self,
        predicate: &NumericPredicate<'tcx>,
    ) -> Option<SmtPredicate> {
        let lhs = self.smt_term_from_contract_expr(&predicate.lhs)?;
        let rhs = self.smt_term_from_contract_expr(&predicate.rhs)?;
        Some(match predicate.op {
            RelOp::Eq => SmtPredicate::Eq(lhs, rhs),
            RelOp::Ne => SmtPredicate::Ne(lhs, rhs),
            RelOp::Lt => SmtPredicate::Lt(lhs, rhs),
            RelOp::Le => SmtPredicate::Le(lhs, rhs),
            RelOp::Gt => SmtPredicate::Gt(lhs, rhs),
            RelOp::Ge => SmtPredicate::Ge(lhs, rhs),
        })
    }

    fn smt_term_from_contract_expr(
        &mut self,
        expr: &ContractExpr<'tcx>,
    ) -> Option<SmtTerm> {
        match expr {
            ContractExpr::Place(place) => {
                let mut key = PlaceKey::from_contract_place(place);
                if let PlaceBaseKey::Arg(index) = key.base {
                    key.base = PlaceBaseKey::Local(index + 1);
                }
                Some(SmtTerm::Place(key))
            }
            ContractExpr::Const(value) => {
                u64::try_from(*value).ok().map(SmtTerm::Const)
            }
            ContractExpr::ConstParam { name, .. } => {
                Some(SmtTerm::ConstParam(name.clone()))
            }
            ContractExpr::Len(inner) => {
                let origin = match inner.as_ref() {
                    ContractExpr::Place(cp) => {
                        let mut key = PlaceKey::from_contract_place(cp);
                        if let PlaceBaseKey::Arg(index) = key.base {
                            key.base = PlaceBaseKey::Local(index + 1);
                        }
                        let val = AbstractValue::Place(key.clone());
                        self.origin_key_for_value(&val, &mut TraceSeen::new())
                    }
                    _ => None,
                };

                // Try to link the contract's `len(self)` to the actual MIR
                // `slice::len()` call result on this path.
                let origin_str = origin.clone().unwrap_or_default();
                let mut first_len_dest: Option<PlaceKey> = None;
                for fact in &self.forward.facts {
                    let StateFact::Call(call) = fact else { continue };
                    let is_len_call = call.func.ends_with("::len")
                        || call.func.contains("::len(");
                    if !is_len_call {
                        continue;
                    }
                    for effect in &call.effects {
                        let crate::verify::call_summary::CallEffect::ReturnLengthOfArg {
                            arg,
                        } = effect
                        else {
                            continue;
                        };
                        let dest = PlaceKey {
                            base: PlaceBaseKey::Local(call.destination.as_usize()),
                            fields: Vec::new(),
                        };
                        // Remember first len call for fallback.
                        if first_len_dest.is_none() {
                            first_len_dest = Some(dest.clone());
                        }
                        let Some(arg_value) = call.args.get(*arg) else {
                            continue;
                        };
                        let arg_origin = self.origin_key_for_value(
                            arg_value,
                            &mut TraceSeen::new(),
                        );
                        let matches = arg_origin.as_deref() == Some(&origin_str)
                            || arg_origin
                                .as_deref()
                                .is_some_and(|ao| ao.starts_with(&origin_str));
                        if matches {
                            return Some(SmtTerm::Place(dest));
                        }
                    }
                }
                // Fallback: use any len() call result on this path.
                if let Some(dest) = first_len_dest {
                    return Some(SmtTerm::Place(dest));
                }

                Some(SmtTerm::Value(format!("len({})", origin_str)))
            }
            ContractExpr::Binary { op, lhs, rhs } => {
                let lhs = Box::new(self.smt_term_from_contract_expr(lhs)?);
                let rhs = Box::new(self.smt_term_from_contract_expr(rhs)?);
                Some(match op {
                    NumericOp::Add => SmtTerm::Add(lhs, rhs),
                    NumericOp::Sub => SmtTerm::Sub(lhs, rhs),
                    NumericOp::Mul => SmtTerm::Mul(lhs, rhs),
                    NumericOp::Div => SmtTerm::Div(lhs, rhs),
                    NumericOp::Rem => SmtTerm::Rem(lhs, rhs),
                    _ => return None,
                })
            }
            _ => None,
        }
    }

    fn value_to_int(&mut self, value: &AbstractValue<'tcx>) -> Option<Int<'ctx>> {
        match value {
            AbstractValue::ConstInt(v) => u64::try_from(*v).ok().map(|v| Int::from_u64(self.ctx, v)),
            AbstractValue::Place(place) => self.term_for_place(place),
            AbstractValue::ConstParam(name) => Some(Int::new_const(self.ctx, format!("const_{name}").as_str())),
            AbstractValue::Const(name) => Some(Int::new_const(self.ctx, sanitize_smt_name(name).as_str())),
            _ => None,
        }
    }

    /// Assert facts collected by the forward visitor.
    pub(crate) fn assert_forward_facts(&mut self, solver: &Solver<'ctx>) {
        for fact in &self.forward.facts {
            match fact {
                StateFact::PointsTo { pointer, source } => {
                    self.assert_place_non_zero(
                        solver,
                        pointer,
                        "created from a reference/raw pointer",
                    );
                    // Only assert alignment on the pointer when the pointee types
                    // match — pointer-arithmetic wrappers produce pointers of a
                    // different pointee type whose alignment must be proved from
                    // guard facts, not from the raw type alone.
                    // Normalize types (strip MaybeUninit, array/slice brackets)
                    // so that e.g. [T] and T share the same alignment key.
                    let ptr_pointee_str = self.place_ty(pointer)
                        .and_then(|ty| pointee_ty_str(ty))
                        .map(|s| normalize_init_ty_name(&s));
                    let src_pointee_str = self.place_ty(source)
                        .and_then(|ty| pointee_ty_str(ty))
                        .map(|s| normalize_init_ty_name(&s));
                    if ptr_pointee_str == src_pointee_str {
                        self.assert_place_alignment(solver, pointer);
                    }
                    self.assert_place_alignment(solver, source);
                    self.assert_length_alias(solver, pointer, source);
                }
                StateFact::Call(call) => {
                    if is_as_ptr_call(&call.func) {
                        let place = PlaceKey {
                            base: PlaceBaseKey::Local(call.destination.as_usize()),
                            fields: Vec::new(),
                        };
                        self.assert_place_non_zero(solver, &place, "returned by as_ptr");
                        self.assert_place_alignment(solver, &place);
                    }
                    self.record_call_effect_assumptions(call);
                    // exact_div(x, y) returns x / y.  Assert result <= x
                    // so that downstream bounds checks (e.g.
                    // from_raw_parts(ptr, exact_div(len, N))) can infer
                    // chunk_count <= len.
                    if call.func.contains("exact_div") {
                        let dest = PlaceKey {
                            base: PlaceBaseKey::Local(call.destination.as_usize()),
                            fields: Vec::new(),
                        };
                        if let Some(dest_term) = self.term_for_place(&dest)
                            && let Some(arg0) = call.args.get(0)
                        {
                            let cursor = self.call_definition_cursor(call);
                            if let Some(arg0_term) = self.term_for_value_at(
                                arg0,
                                cursor,
                                &mut TraceSeen::new(),
                            ) {
                                solver.assert(&dest_term.le(&arg0_term));
                                // Cache the term so subsequent uses of this
                                // local (e.g. Allocated check) get the same
                                // Z3 variable.
                                self.place_terms.insert(dest.clone(), dest_term);
                                self.assumptions.push(SmtPredicate::Le(
                                    SmtTerm::Place(dest),
                                    SmtTerm::Value(value_label(arg0)),
                                ));
                            }
                        }
                    }
                }
                StateFact::KnownNonZero { place, reason } => {
                    self.assert_place_non_zero(solver, place, reason);
                }
                StateFact::KnownAligned {
                    place,
                    align,
                    ty_name,
                    reason,
                } => {
                    self.assert_known_alignment(solver, place, *align, ty_name, reason);
                }
                StateFact::KnownInit {
                    place,
                    ty_name,
                    elements,
                    reason,
                } => {
                    self.assumptions.push(SmtPredicate::Custom(format!(
                        "{} initialized for {ty_name}, {elements} element(s) ({reason})",
                        place_label(place)
                    )));
                }
                StateFact::KnownAllocated {
                    place,
                    object,
                    ty_name,
                    elements,
                    reason,
                } => {
                    self.assumptions.push(SmtPredicate::Custom(format!(
                        "{} allocated in {} for {ty_name}, {elements} element(s) ({reason})",
                        place_label(place),
                        place_label(object)
                    )));
                }
                StateFact::KnownConst {
                    place,
                    value,
                    reason,
                } => {
                    self.assert_known_const(solver, place, *value, reason);
                }
                StateFact::BranchEq { value, equals, cmp_op, cmp_lhs, cmp_rhs } => {
                    if let Some(term) = self.term_for_value(value, &mut HashSet::new()) {
                        let expected = Int::from_u64(self.ctx, *equals as u64);
                        solver.assert(&term._eq(&expected));
                        self.assumptions.push(SmtPredicate::Eq(
                            SmtTerm::Value(value_label(value)),
                            SmtTerm::Const(*equals as u64),
                        ));
                    }
                    if let (Some(op), Some(lhs), Some(rhs)) = (cmp_op, cmp_lhs, cmp_rhs) {
                        if let (Some(lhs_t), Some(rhs_t)) = (
                            self.value_to_int(lhs), self.value_to_int(rhs),
                        ) {
                            let holds = *equals == 1;
                            match (op, holds) {
                                (BinOp::Eq, true) | (BinOp::Ne, false) => solver.assert(&lhs_t._eq(&rhs_t)),
                                (BinOp::Ne, true) | (BinOp::Eq, false) => solver.assert(&lhs_t._eq(&rhs_t).not()),
                                (BinOp::Lt, true) | (BinOp::Ge, false) => solver.assert(&lhs_t.lt(&rhs_t)),
                                (BinOp::Le, true) | (BinOp::Gt, false) => solver.assert(&lhs_t.le(&rhs_t)),
                                (BinOp::Gt, true) | (BinOp::Le, false) => solver.assert(&lhs_t.gt(&rhs_t)),
                                (BinOp::Ge, true) | (BinOp::Lt, false) => solver.assert(&lhs_t.ge(&rhs_t)),
                                _ => {}
                            }
                        }
                    }
                }
                StateFact::Cast { target, source, .. } => {
                    self.assumptions.push(SmtPredicate::Eq(
                        SmtTerm::Place(target.clone()),
                        SmtTerm::Value(value_label(source)),
                    ));
                    if let AbstractValue::Place(source_place) = source {
                        if self
                            .place_ty(source_place)
                            .is_some_and(|ty| pointee_ty(ty).is_some())
                        {
                            self.assert_place_alignment(solver, source_place);
                        }
                    }
                    if let Some(term) = self.term_for_value(source, &mut HashSet::new()) {
                        self.place_terms.insert(target.clone(), term);
                    }
                }
                StateFact::Binary {
                    target,
                    op,
                    lhs,
                    rhs,
                } => {
                    self.assumptions.push(SmtPredicate::Eq(
                        SmtTerm::Place(target.clone()),
                        SmtTerm::Value(format!(
                            "({} {} {})",
                            value_label(lhs),
                            binop_label(*op),
                            value_label(rhs)
                        )),
                    ));
                }
                StateFact::Contract(property) => match property.kind {
                    PropertyKind::Align => {
                        let Some(target) = (|| {
                            let arg = property.args.first()?;
                            let PropertyArg::Place(place) = arg else {
                                return None;
                            };
                            let mut key = PlaceKey::from_contract_place(place);
                            if let PlaceBaseKey::Arg(index) = key.base {
                                key.base = PlaceBaseKey::Local(index + 1);
                            }
                            Some(key)
                        })() else {
                            continue;
                        };
                        let Some(required_ty) = property.args.iter().find_map(|arg| {
                            if let PropertyArg::Ty(ty) = arg {
                                Some(*ty)
                            } else {
                                None
                            }
                        }) else {
                            continue;
                        };
                        let Some((align, _)) = self.type_layout(required_ty) else {
                            continue;
                        };
                        if align == 0 {
                            let ty_name = format!("{required_ty:?}");
                            if let Some(term) = self.term_for_place(&target) {
                                let align_term = self.symbolic_align_term(&ty_name);
                                let zero = Int::from_u64(self.ctx, 0);
                                solver.assert(&term.modulo(&align_term)._eq(&zero));
                                self.assumptions.push(SmtPredicate::Custom(format!(
                                    "{} aligned for {ty_name} (symbolic, struct-invariant)",
                                    place_label(&target)
                                )));
                            }
                        } else {
                            self.assert_known_alignment(
                                solver,
                                &target,
                                align,
                                &format!("{required_ty:?}"),
                                "struct-invariant",
                            );
                        }
                    }
                    PropertyKind::NonNull => {
                        let Some(target) = (|| {
                            let arg = property.args.first()?;
                            let PropertyArg::Place(place) = arg else {
                                return None;
                            };
                            let mut key = PlaceKey::from_contract_place(place);
                            if let PlaceBaseKey::Arg(index) = key.base {
                                key.base = PlaceBaseKey::Local(index + 1);
                            }
                            Some(key)
                        })() else {
                            continue;
                        };
                        self.assert_place_non_zero(solver, &target, "caller-contract");
                    }
                    PropertyKind::InBound => {
                        if let Some(PropertyArg::Expr(ContractExpr::IndexAccess {
                            slice,
                            index,
                        })) = property.args.first()
                        {
                            let slice_key = match slice.as_ref() {
                                ContractExpr::Place(place) => {
                                    let mut key = PlaceKey::from_contract_place(place);
                                    if let PlaceBaseKey::Arg(ix) = key.base {
                                        key.base = PlaceBaseKey::Local(ix + 1);
                                    }
                                    key
                                }
                                _ => {
                                    continue;
                                }
                            };
                            let slice_label = place_label(&slice_key);
                            let len =
                                SmtTerm::Value(format!("len({slice_label})"));

                            if let ContractExpr::Place(place) = index.as_ref() {
                                let mut index_key =
                                    PlaceKey::from_contract_place(place);
                                if let PlaceBaseKey::Arg(ix) = index_key.base {
                                    index_key.base = PlaceBaseKey::Local(ix + 1);
                                }
                                if let Some(ty) = self.place_ty(&index_key)
                                    && let TyKind::Array(_, len_const) = ty.kind()
                                {
                                    if let Some(array_len) =
                                        len_const.try_to_target_usize(self.tcx)
                                    {
                                        for j in 0..array_len {
                                            let elem_key = PlaceKey {
                                                base: index_key.base.clone(),
                                                fields: vec![j as usize],
                                            };
                                            let index_term =
                                                SmtTerm::Place(elem_key);
                                            let lower = index_term.clone();
                                            let upper = SmtTerm::Add(
                                                Box::new(index_term),
                                                Box::new(SmtTerm::Const(1)),
                                            );
                                            let preds = vec![
                                                SmtPredicate::Le(
                                                    SmtTerm::Const(0),
                                                    lower.clone(),
                                                ),
                                                SmtPredicate::Le(
                                                    lower.clone(),
                                                    upper.clone(),
                                                ),
                                                SmtPredicate::Le(
                                                    upper,
                                                    len.clone(),
                                                ),
                                            ];
                                            for pred in &preds {
                                                if let Some(bool_term) =
                                                    self.bool_for_predicate(pred)
                                                {
                                                    solver.assert(&bool_term);
                                                }
                                                self.assumptions
                                                    .push(pred.clone());
                                            }
                                        }
                                        self.has_index_access_assumptions =
                                            true;
                                        continue;
            }
        }
        // Const-generic parameters (e.g. const N: usize) are
        // always non-negative.  Assert this so that constraints like
        // N != 0 or N >= 1 are provable.
        for term in self.const_terms.values() {
            solver.assert(&term.ge(&Int::from_u64(self.ctx, 0)));
        }
    }

                            let index_term = match index.as_ref() {
                                ContractExpr::Place(place) => {
                                    let mut key =
                                        PlaceKey::from_contract_place(place);
                                    if let PlaceBaseKey::Arg(ix) = key.base {
                                        key.base = PlaceBaseKey::Local(ix + 1);
                                    }
                                    Some(SmtTerm::Place(key))
                                }
                                ContractExpr::Const(value) => {
                                    u64::try_from(*value).ok().map(SmtTerm::Const)
                                }
                                _ => None,
                            };
                            let Some(index_term) = index_term else {
                                continue;
                            };
                            let lower = index_term.clone();
                            let upper = SmtTerm::Add(
                                Box::new(index_term),
                                Box::new(SmtTerm::Const(1)),
                            );
                            let preds = vec![
                                SmtPredicate::Le(
                                    SmtTerm::Const(0),
                                    lower.clone(),
                                ),
                                SmtPredicate::Le(
                                    lower.clone(),
                                    upper.clone(),
                                ),
                                SmtPredicate::Le(upper, len),
                            ];
                            for pred in &preds {
                                if let Some(bool_term) =
                                    self.bool_for_predicate(pred)
                                {
                                    solver.assert(&bool_term);
                                }
                                self.assumptions.push(pred.clone());
                            }
                            self.has_index_access_assumptions = true;
                            continue;
                        }
                        // Handle 3-arg InBound(ptr, Ty, index) form
                        // args = [Place(slice_ptr), Ty(T), Expr(index)]
                        if property.args.len() == 3 {
                            let slice_place = match property.args.get(0) {
                                Some(PropertyArg::Place(place)) => place,
                                _ => {
                                    continue;
                                }
                            };
                            let index_expr = match property.args.get(2) {
                                Some(PropertyArg::Expr(expr)) => expr,
                                _ => {
                                    continue;
                                }
                            };
                            let slice_label = {
                                let mut key = PlaceKey::from_contract_place(slice_place);
                                if let PlaceBaseKey::Arg(ix) = key.base {
                                    key.base = PlaceBaseKey::Local(ix + 1);
                                }
                                place_label(&key)
                            };
                            let len = SmtTerm::Value(format!("len({slice_label})"));
                            let index_term = match index_expr {
                                ContractExpr::Place(place) => {
                                    let mut key = PlaceKey::from_contract_place(place);
                                    if let PlaceBaseKey::Arg(ix) = key.base {
                                        key.base = PlaceBaseKey::Local(ix + 1);
                                    }
                                    Some(SmtTerm::Place(key))
                                }
                                ContractExpr::Const(value) => {
                                    u64::try_from(*value).ok().map(SmtTerm::Const)
                                }
                                _ => None,
                            };
                            let Some(index_term) = index_term else {
                                continue;
                            };
                            let lower = index_term.clone();
                            let upper = SmtTerm::Add(
                                Box::new(index_term),
                                Box::new(SmtTerm::Const(1)),
                            );
                            let preds = vec![
                                SmtPredicate::Le(SmtTerm::Const(0), lower.clone()),
                                SmtPredicate::Le(lower.clone(), upper.clone()),
                                SmtPredicate::Le(upper, len),
                            ];
                            for pred in &preds {
                                if let Some(bool_term) = self.bool_for_predicate(pred) {
                                    solver.assert(&bool_term);
                                }
                                self.assumptions.push(pred.clone());
                            }
                            self.has_index_access_assumptions = true;
                            continue;
                        }
                        let Some(target) = (|| {
                            let arg = property.args.first()?;
                            let PropertyArg::Place(place) = arg else {
                                return None;
                            };
                            let mut key = PlaceKey::from_contract_place(place);
                            if let PlaceBaseKey::Arg(index) = key.base {
                                key.base = PlaceBaseKey::Local(index + 1);
                            }
                            Some(key)
                        })() else {
                            continue;
                        };
                        let Some(required_ty) = property.args.iter().find_map(|arg| {
                            if let PropertyArg::Ty(ty) = arg {
                                Some(*ty)
                            } else {
                                None
                            }
                        }) else {
                            continue;
                        };
                        let Some((_, elem_size)) = self.type_layout(required_ty) else {
                            continue;
                        };
                        let access_count = property
                            .args
                            .iter()
                            .rev()
                            .find_map(|arg| {
                                let PropertyArg::Expr(ContractExpr::Const(value)) = arg else {
                                    return None;
                                };
                                u64::try_from(*value).ok()
                            })
                            .unwrap_or(0);
                        self.assumptions.push(SmtPredicate::InBounds {
                            index: SmtTerm::Const(0),
                            access_count: SmtTerm::Const(access_count),
                            len: SmtTerm::Value(format!("precond_len_{}", place_label(&target))),
                        });
                        if elem_size > 0 && access_count > 0 {
                            self.assumptions.push(SmtPredicate::Custom(format!(
                                "InBound({}, T, {access_count}) holds (caller-contract, elem_size={elem_size})",
                                place_label(&target)
                            )));
                        } else {
                            self.assumptions.push(SmtPredicate::Custom(format!(
                                "InBound({}, T, {access_count}) holds (caller-contract, symbolic)",
                                place_label(&target)
                            )));
                        }
                    }
                    PropertyKind::Init => {
                        let Some(target) = (|| {
                            let arg = property.args.first()?;
                            let PropertyArg::Place(place) = arg else {
                                return None;
                            };
                            let mut key = PlaceKey::from_contract_place(place);
                            if let PlaceBaseKey::Arg(index) = key.base {
                                key.base = PlaceBaseKey::Local(index + 1);
                            }
                            Some(key)
                        })() else {
                            continue;
                        };
                        let Some(required_ty) = property.args.iter().find_map(|arg| {
                            if let PropertyArg::Ty(ty) = arg {
                                Some(*ty)
                            } else {
                                None
                            }
                        }) else {
                            continue;
                        };
                        let elements = property
                            .args
                            .iter()
                            .rev()
                            .find_map(|arg| {
                                let PropertyArg::Expr(ContractExpr::Const(value)) = arg else {
                                    return None;
                                };
                                u64::try_from(*value).ok()
                            })
                            .unwrap_or(0);
                        self.assumptions.push(SmtPredicate::Custom(format!(
                            "{} initialized for {:?}, {elements} element(s) (caller-contract)",
                            place_label(&target),
                            required_ty
                        )));
                    }
                    PropertyKind::ValidNum => {
                        if let Some(PropertyArg::Predicates(predicates)) =
                            property.args.first()
                        {
                            for predicate in predicates {
                                if let Some(smt_pred) = self.contract_predicate_to_smt(predicate) {
                                    if let Some(z3_bool) = self.bool_for_predicate(&smt_pred) {
                                        solver.assert(&z3_bool);
                                    }
                                    self.assumptions.push(smt_pred);
                                }
                            }
                        }
                    }
                    _ => {}
                },
                StateFact::PathCondition(_)
                | StateFact::Drop(_)
                | StateFact::LocalDead(_)
                | StateFact::CallEffect(_) => {}
            }
        }

        // Assert unsigned-integer function arguments are non-negative.
        // Arguments are atomic inputs (MIR locals `1..=arg_count`), so this is
        // universally true for usize / u8..u128 and does not over-constrain any
        // computed value.  It is required for proving bounds goals where the
        // offset involves subtraction (e.g. `ptr.add(len - k)` needs `k >= 0`
        // together with `len >= 0`).
        let body = self.tcx.optimized_mir(self.checkpoint.caller);
        for arg in 1..=body.arg_count {
            let place = PlaceKey {
                base: PlaceBaseKey::Local(arg),
                fields: Vec::new(),
            };
            let Some(ty) = self.place_ty(&place) else { continue };
            if !is_unsigned_integral_ty(ty) { continue }
            let Some(term) = self.term_for_place(&place) else { continue };
            let zero = Int::from_u64(self.ctx, 0);
            solver.assert(&term.ge(&zero));
            self.assumptions.push(SmtPredicate::Ge(
                SmtTerm::Place(place),
                SmtTerm::Const(0),
            ));
        }
    }

    /// Return the path assumptions asserted by this model.
    pub(crate) fn assumptions(&self) -> &[SmtPredicate] {
        &self.assumptions
    }

    fn latest_cursor(&self) -> ValueCursor {
        self.forward.value_definitions.len()
    }

    fn call_definition_cursor(&self, call: &CallSummary<'tcx>) -> ValueCursor {
        self.forward
            .value_definitions
            .iter()
            .find_map(|definition| {
                if definition.local != call.destination {
                    return None;
                }
                let AbstractValue::CallResult(recorded) = &definition.value else {
                    return None;
                };
                if recorded.func == call.func && recorded.arg_count == call.arg_count {
                    Some(definition.ordinal)
                } else {
                    None
                }
            })
            .unwrap_or_else(|| self.latest_cursor())
    }

    /// Try to recover the slice index/length terms behind a pointer result.
    ///
    /// Supported forms:
    ///
    /// - `slice.as_ptr().add(index)` and wrappers summarized as `ReturnPointerAdd`
    /// - plain `slice.as_ptr()` / `slice.as_mut_ptr()`, treated as index `0`
    pub(crate) fn pointer_bounds_for_place(
        &mut self,
        place: &PlaceKey,
    ) -> Option<PointerBounds<'ctx>> {
        if let Some(call) = self.pointer_add_call_for_place(place) {
            let (base_arg, offset_arg) = call.effects.iter().find_map(|effect| {
                match effect {
                    crate::verify::call_summary::CallEffect::ReturnPointerAdd {
                        base_arg,
                        offset_arg,
                        ..
                    }
                    | crate::verify::call_summary::CallEffect::ReturnPointerSub {
                        base_arg,
                        offset_arg,
                        ..
                    } => Some((*base_arg, *offset_arg)),
                    _ => None,
                }
            })?;
            let base = call.args.get(base_arg)?;
            let index = call.args.get(offset_arg)?;
            let call_cursor = self.call_definition_cursor(&call);
            let base_origin =
                self.origin_key_for_value_before(base, call_cursor, &mut TraceSeen::new())?;

            let index_term = self.term_for_value_at(index, call_cursor, &mut TraceSeen::new())?;
            let (len_term_int, len_term) = self.bounds_len_for_origin(&base_origin, Some(index))?;

            // For pointer arithmetic on a base pointer that is a Range field,
            // adjust the index: base_offset +/- count instead of just count.
            let result_index_smt: SmtTerm;
            let result_index_val: Int<'ctx>;
            if let AbstractValue::Place(base_place) = base {
                let (base_smt, base_val) = self.field_projection_index(
                    base_place, &base_origin, &len_term,
                );
                if !matches!(&base_smt, SmtTerm::Const(0)) {
                    // base has a non-zero offset — adjust by the arithmetic
                    let is_sub = call_has_pointer_sub_effect(&call);
                    let (adjusted_val, adjusted_smt) = if is_sub {
                        let v = Int::sub(&self.ctx, &[base_val, index_term]);
                        let s = SmtTerm::Sub(Box::new(base_smt), Box::new(SmtTerm::Value(value_label(index))));
                        (v, s)
                    } else {
                        let v = Int::add(&self.ctx, &[base_val, index_term]);
                        let s = SmtTerm::Add(Box::new(base_smt), Box::new(SmtTerm::Value(value_label(index))));
                        (v, s)
                    };
                    result_index_val = adjusted_val;
                    result_index_smt = adjusted_smt;
                } else {
                    result_index_val = index_term;
                    result_index_smt = SmtTerm::Value(value_label(index));
                }
            } else {
                result_index_val = index_term;
                result_index_smt = SmtTerm::Value(value_label(index));
            }

            return Some(PointerBounds {
                index: result_index_val,
                len: len_term_int,
                index_term: result_index_smt,
                len_term,
                origin_key: base_origin,
            });
        }

        let value = self
            .resolved_value_for_place(place, &mut TraceSeen::new())
            .unwrap_or_else(|| AbstractValue::Place(place.clone()));
        let base_origin =
            self.origin_key_for_value_before(&value, self.latest_cursor(), &mut TraceSeen::new())?;
        let zero = AbstractValue::ConstInt(0);
        let (mut len_term_int, mut len_term) = self.bounds_len_for_origin(&base_origin, Some(&zero))?;

        if place.fields.is_empty()
            && let Some(local) = place.local()
            && let Some(definition) = self.forward.latest_value_definition_before(local, self.latest_cursor())
        {
            if let AbstractValue::Cast(inner, cast_ty) = &definition.value {
                let caller = self.checkpoint.caller;
                if let Some(dst_pt) = pointee_ty(*cast_ty) {
                    let dst_size = safe_type_layout(self.tcx, caller, dst_pt).map(|(_, s)| s);
                    let src_ty = match &**inner {
                        AbstractValue::Place(inner_place)
                        | AbstractValue::RawPtr(inner_place)
                        | AbstractValue::Ref(inner_place) => {
                            inner_place.local().and_then(|local| {
                                let body = self.tcx.optimized_mir(caller);
                                let ty = body.local_decls[local].ty;
                                pointee_ty(ty)
                            })
                        }
                        _ => None,
                    };
                    let src_size = src_ty.and_then(|pt| safe_type_layout(self.tcx, caller, pt).map(|(_, s)| s));
                    let ratio_smt = match (src_size, dst_size) {
                        (Some(src), Some(dst)) if src > dst && src % dst == 0 => Some(SmtTerm::Const(src / dst)),
                        _ => {
                            if let (Some(src_pty), Some(dst_pty)) = (src_ty, Some(dst_pt)) {
                                pointee_stride_from_types(self.tcx, src_pty, dst_pty)
                            } else {
                                None
                            }
                        }
                    };
                    if let Some(ratio_smt) = ratio_smt {
                        let ratio_int = self.term_for_smt_term(&ratio_smt)?;
                        len_term_int = Int::mul(self.ctx, &[len_term_int, ratio_int]);
                        len_term = SmtTerm::Mul(Box::new(len_term), Box::new(ratio_smt));
                    }
                }
            }
        }

        // Compute the correct index for field projections from Range types.
        // Field [0] (start) is at offset 0; field [1] (end) is at offset len.
        let (index_term, index_val) = self.field_projection_index(place, &base_origin, &len_term);

        Some(PointerBounds {
            index: index_val,
            len: len_term_int,
            index_term,
            len_term,
            origin_key: base_origin,
        })
    }

    /// Walk the value chain for `place` to determine if it is a field projection
    /// from an `as_ptr_range`/`as_mut_ptr_range` result (or an inlined equivalent).
    /// Returns (index_term, index_val).  Field [0] (start) → offset 0;
    /// field [1] (end) → offset len.
    fn field_projection_index(
        &mut self,
        place: &PlaceKey,
        origin_key: &str,
        len_term: &SmtTerm,
    ) -> (SmtTerm, Int<'ctx>) {
        let default_index = SmtTerm::Const(0);
        let default_val = Int::from_u64(self.ctx, 0);

        let mut cur_place = place.clone();
        loop {
            if !cur_place.fields.is_empty() {
                let field_idx = cur_place.fields.as_slice();
                let mut base = cur_place.clone();
                base.fields.clear();
                if let Some(local) = base.local() {
                    if let Some(definition) = self.forward.latest_value_definition_before(
                        local,
                        self.latest_cursor(),
                    ) {
                        let is_range = match &definition.value {
                            AbstractValue::CallResult(call) => {
                                let prim = PrimitiveCall::classify(&call.func);
                                prim == Some(PrimitiveCall::AsPtrRange)
                                    || prim == Some(PrimitiveCall::AsMutPtrRange)
                            }
                            AbstractValue::Aggregate(_, _) => true,
                            _ => false,
                        };
                        if is_range {
                            if field_idx == [0] {
                                return (SmtTerm::Const(0), Int::from_u64(self.ctx, 0));
                            }
                            if field_idx == [1] {
                                let len_key = format!("len({})", origin_key);
                                let len_val = self.symbolic_len_term(&len_key);
                                return (SmtTerm::Value(len_key), len_val);
                            }
                        }
                        // Follow Cast facts for inlined aggregates
                        for fact in &self.forward.facts {
                            if let StateFact::Cast { target, source, .. } = fact {
                                if *target == cur_place {
                                    if let AbstractValue::Place(p) = source {
                                        cur_place = p.clone();
                                        // Try again with the new place
                                        if cur_place.fields.as_slice() == [1] {
                                            let mut inner_base = cur_place.clone();
                                            inner_base.fields.clear();
                                            if let Some(inner_local) = inner_base.local() {
                                                if let Some(inner_def) = self.forward.latest_value_definition_before(inner_local, self.latest_cursor()) {
                                                    if let AbstractValue::CallResult(inner_call) = &inner_def.value {
                                                        let inner_prim = PrimitiveCall::classify(&inner_call.func);
                                                        if inner_prim == Some(PrimitiveCall::AsPtrRange) || inner_prim == Some(PrimitiveCall::AsMutPtrRange) {
                                                            let len_key = format!("len({})", origin_key);
                                                            let len_val = self.symbolic_len_term(&len_key);
                                                            return (SmtTerm::Value(len_key), len_val);
                                                        }
                                                    }
                                                }
                                            }
                                        }
                                        continue;
                                    }
                                }
                            }
                        }
                    }
                }
                return (default_index, default_val);
            }

            if let Some(local) = cur_place.local() {
                if let Some(definition) =
                    self.forward.latest_value_definition_before(local, self.latest_cursor())
                {
                    match &definition.value {
                        AbstractValue::Place(p) => {
                            cur_place = p.clone();
                            continue;
                        }
                        _ => {}
                    }
                }
            }
            return (default_index, default_val);
        }
    }

    /// Compute the offset index for a pointer-arithmetic call result.
    /// result_offset = base_offset (+ or -) count
    fn compute_pointer_arith_index(
        &mut self,
        base: &AbstractValue<'tcx>,
        base_origin: &str,
        len_term: &SmtTerm,
        call: &CallSummary<'tcx>,
        call_cursor: ValueCursor,
    ) -> (SmtTerm, Int<'ctx>) {
        // Get the base pointer's PlaceKey
        let base_place = match base {
            AbstractValue::Place(p) => p.clone(),
            _ => {
                // Fallback: use the count as the index (old behavior)
                if let Some(index) = call.effects.iter().find_map(|effect| match effect {
                    crate::verify::call_summary::CallEffect::ReturnPointerAdd { offset_arg, .. }
                    | crate::verify::call_summary::CallEffect::ReturnPointerSub { offset_arg, .. } => {
                        call.args.get(*offset_arg)
                    }
                    _ => None,
                }) {
                    let count_smt = SmtTerm::Value(value_label(index));
                    let count_val = self.term_for_value_at(index, call_cursor, &mut TraceSeen::new())
                        .unwrap_or(Int::from_u64(self.ctx, 0));
                    return (count_smt, count_val);
                }
                return (SmtTerm::Const(0), Int::from_u64(self.ctx, 0));
            }
        };

        // Compute base offset using field_projection_index
        let (base_idx_smt, _base_idx_val) = self.field_projection_index(
            &base_place, base_origin, len_term,
        );

        // Get the count term
        let count = call.effects.iter().find_map(|effect| match effect {
            crate::verify::call_summary::CallEffect::ReturnPointerAdd { offset_arg, .. }
            | crate::verify::call_summary::CallEffect::ReturnPointerSub { offset_arg, .. } => {
                call.args.get(*offset_arg)
            }
            _ => None,
        });

        let count_smt = if let Some(c) = count {
            SmtTerm::Value(value_label(c))
        } else {
            SmtTerm::Const(0)
        };

        let is_sub = call_has_pointer_sub_effect(call);
        let result_smt = if is_sub {
            SmtTerm::Sub(Box::new(base_idx_smt), Box::new(count_smt))
        } else {
            SmtTerm::Add(Box::new(base_idx_smt), Box::new(count_smt))
        };

        let result_val = self.term_for_smt_term(&result_smt)
            .unwrap_or(Int::from_u64(self.ctx, 0));

        (result_smt, result_val)
    }

    /// Recover the allocation object and element offset for a pointer-like
    /// place. This is intentionally small: it handles base pointers returned by
    /// `as_ptr`/`as_mut_ptr` and offsets produced by pointer arithmetic
    /// summaries.
    fn pointer_object_offset_for_place(&self, place: &PlaceKey) -> Option<(PlaceKey, SmtTerm)> {
        self.pointer_object_offset_for_place_before(
            place,
            self.latest_cursor(),
            &mut TraceSeen::new(),
        )
    }

    fn pointer_object_offset_for_place_before(
        &self,
        place: &PlaceKey,
        cursor: ValueCursor,
        seen: &mut TraceSeen,
    ) -> Option<(PlaceKey, SmtTerm)> {
        if let Some(object) = self.allocated_object_for_place(place) {
            return Some((object, SmtTerm::Const(0)));
        }
        let seen_key = (place.clone(), cursor);
        if !seen.insert(seen_key) {
            return None;
        }
        let local = place.local()?;
        let definition = self.forward.latest_value_definition_before(local, cursor)?;
        self.pointer_object_offset_for_value(&definition.value, definition.ordinal, seen)
    }

    fn pointer_object_offset_for_value(
        &self,
        value: &AbstractValue<'tcx>,
        cursor: ValueCursor,
        seen: &mut TraceSeen,
    ) -> Option<(PlaceKey, SmtTerm)> {
        match value {
            AbstractValue::Place(place) => {
                self.pointer_object_offset_for_place_before(place, cursor, seen)
            }
            AbstractValue::Cast(inner, _) => {
                self.pointer_object_offset_for_value(inner, cursor, seen)
            }
            AbstractValue::CallResult(call) => {
                if call_has_pointer_add_effect(call) || is_pointer_add_call(&call.func) {
                    let (base_arg, offset_arg) = call
                        .effects
                        .iter()
                        .find_map(|effect| {
                            let crate::verify::call_summary::CallEffect::ReturnPointerAdd {
                                base_arg,
                                offset_arg,
                                ..
                            } = effect
                            else {
                                return None;
                            };
                            Some((*base_arg, *offset_arg))
                        })
                        .unwrap_or((0, 1));
                    let call_cursor = self.call_definition_cursor(call);
                    let (object, base_offset) = self.pointer_object_offset_for_value(
                        call.args.get(base_arg)?,
                        call_cursor,
                        seen,
                    )?;
                    let offset = smt_term_for_value(call.args.get(offset_arg)?)?;
                    return Some((
                        object,
                        SmtTerm::Add(Box::new(base_offset), Box::new(offset)),
                    ));
                }
                if call_has_pointer_sub_effect(call) || is_pointer_sub_call(&call.func) {
                    let (base_arg, offset_arg) = call
                        .effects
                        .iter()
                        .find_map(|effect| {
                            let crate::verify::call_summary::CallEffect::ReturnPointerSub {
                                base_arg,
                                offset_arg,
                                ..
                            } = effect
                            else {
                                return None;
                            };
                            Some((*base_arg, *offset_arg))
                        })
                        .unwrap_or((0, 1));
                    let call_cursor = self.call_definition_cursor(call);
                    let (object, base_offset) = self.pointer_object_offset_for_value(
                        call.args.get(base_arg)?,
                        call_cursor,
                        seen,
                    )?;
                    let offset = smt_term_for_value(call.args.get(offset_arg)?)?;
                    return Some((
                        object,
                        SmtTerm::Sub(Box::new(base_offset), Box::new(offset)),
                    ));
                }
                let destination = PlaceKey {
                    base: PlaceBaseKey::Local(call.destination.as_usize()),
                    fields: Vec::new(),
                };
                self.allocated_object_for_place(&destination)
                    .map(|object| (object, SmtTerm::Const(0)))
            }
            _ => None,
        }
    }

    fn allocated_object_for_place(&self, place: &PlaceKey) -> Option<PlaceKey> {
        // 1) KnownAllocated facts (concrete allocations).
        if let Some(object) = self.forward.facts.iter().find_map(|fact| match fact {
            StateFact::KnownAllocated {
                place: allocated_place,
                object,
                ..
            } if allocated_place == place => Some(object.clone()),
            _ => None,
        }) {
            return Some(object);
        }
        // 2) PointsTo facts — when a pointer (or a projection of one)
        //    traces to a reference, the reference is the allocation object.
        let base = if place.fields.is_empty() {
            place.clone()
        } else {
            PlaceKey { base: place.base.clone(), fields: Vec::new() }
        };
        if let Some(source) = self.forward.facts.iter().find_map(|fact| match fact {
            StateFact::PointsTo { pointer, source } if *pointer == base => Some(source.clone()),
            _ => None,
        }) {
            return Some(source);
        }
        None
    }

    /// Assert that a place is known to denote a non-zero address.
    pub(crate) fn assert_place_non_zero(
        &mut self,
        solver: &Solver<'ctx>,
        place: &PlaceKey,
        reason: &str,
    ) {
        if let Some(term) = self.term_for_place(place) {
            let zero = Int::from_u64(self.ctx, 0);
            solver.assert(&term._eq(&zero).not());
            self.assumptions.push(SmtPredicate::Custom(format!(
                "{} != 0 ({reason})",
                place_label(place)
            )));
        }
    }

    /// Assert known alignment for a place when its MIR type provides one.
    fn assert_place_alignment(&mut self, solver: &Solver<'ctx>, place: &PlaceKey) {
        let Some(ty) = self.place_ty(place) else {
            return;
        };
        let Some(align_ty) = pointee_ty(ty).or(Some(ty)) else {
            return;
        };
        let Some(align) = self.guaranteed_alignment(align_ty) else {
            return;
        };
        if align > 0 && align <= 1 {
            return;
        }
        if let Some(term) = self.term_for_place(place) {
            let zero = Int::from_u64(self.ctx, 0);
            let align_term = if align == 0 {
                self.symbolic_align_term(&format!("{align_ty:?}"))
            } else {
                Int::from_u64(self.ctx, align)
            };
            solver.assert(&term.modulo(&align_term)._eq(&zero));
            self.assumptions.push(SmtPredicate::Custom(format!(
                "{} aligned for {align_ty:?} ({} bytes)",
                place_label(place),
                if align == 0 { "symbolic".to_string() } else { align.to_string() }
            )));
        }
    }

    /// Assert an explicitly summarized alignment fact.
    fn assert_known_alignment(
        &mut self,
        solver: &Solver<'ctx>,
        place: &PlaceKey,
        align: u64,
        ty_name: &str,
        reason: &str,
    ) {
        if align == 0 {
            if let Some(term) = self.term_for_place(place) {
                let align_term = self.symbolic_align_term(ty_name);
                let zero = Int::from_u64(self.ctx, 0);
                solver.assert(&term.modulo(&align_term)._eq(&zero));
                self.assumptions.push(SmtPredicate::Custom(format!(
                    "{} aligned for {ty_name} (symbolic, {reason})",
                    place_label(place)
                )));
            }
            return;
        }
        if align <= 1 {
            return;
        }
        if let Some(term) = self.term_for_place(place) {
            let align_term = Int::from_u64(self.ctx, align);
            let k = Int::new_const(self.ctx, format!("{}_ka_k", place_label(place)));
            solver.assert(&term._eq(&Int::mul(self.ctx, &[k, align_term.clone()])));
            let zero = Int::from_u64(self.ctx, 0);
            solver.assert(&term.modulo(&align_term)._eq(&zero));
            self.assumptions.push(SmtPredicate::Custom(format!(
                "{} aligned for {ty_name} ({align} bytes, {reason})",
                place_label(place)
            )));
        }
    }

    /// Assert that a place is equal to a concrete layout/numeric constant.
    fn assert_known_const(
        &mut self,
        solver: &Solver<'ctx>,
        place: &PlaceKey,
        value: u64,
        reason: &str,
    ) {
        if let Some(term) = self.term_for_place(place) {
            let value_term = Int::from_u64(self.ctx, value);
            solver.assert(&term._eq(&value_term));
            self.assumptions.push(SmtPredicate::Custom(format!(
                "{} == {value} ({reason})",
                place_label(place)
            )));
        }
    }

    /// Assert equal slice lengths for two slice-like places that alias.
    fn assert_length_alias(&mut self, solver: &Solver<'ctx>, left: &PlaceKey, right: &PlaceKey) {
        if !self.is_len_carrying_place(left) || !self.is_len_carrying_place(right) {
            return;
        }
        let left_label = place_label(left);
        let right_label = place_label(right);
        let lhs = self.symbolic_len_term(&format!("len({left_label})"));
        let rhs = self.symbolic_len_term(&format!("len({right_label})"));
        solver.assert(&lhs._eq(&rhs));
        self.assumptions.push(SmtPredicate::Eq(
            SmtTerm::Value(format!("len({left_label})")),
            SmtTerm::Value(format!("len({right_label})")),
        ));
    }

    fn is_len_carrying_place(&self, place: &PlaceKey) -> bool {
        self.place_ty(place).is_some_and(is_len_carrying_ty)
    }

    /// Record call-effect definitions that the term builder understands.
    fn record_call_effect_assumptions(&mut self, call: &CallSummary<'tcx>) {
        let destination = PlaceKey {
            base: PlaceBaseKey::Local(call.destination.as_usize()),
            fields: Vec::new(),
        };
        let cursor = self.call_definition_cursor(call);
        for effect in &call.effects {
            match effect {
                crate::verify::call_summary::CallEffect::ReturnPointerAdd {
                    base_arg,
                    offset_arg,
                    stride,
                } => {
                    let base_term = call
                        .args
                        .get(*base_arg)
                        .and_then(|v| self.term_for_value_at(v, cursor, &mut TraceSeen::new()));
                    let offset_term = call
                        .args
                        .get(*offset_arg)
                        .and_then(|v| self.term_for_value_at(v, cursor, &mut TraceSeen::new()));
                    if let (Some(base), Some(offset)) = (base_term, offset_term) {
                        let stride = Int::from_u64(self.ctx, stride.unwrap_or(1));
                        let term =
                            Int::add(self.ctx, &[base, Int::mul(self.ctx, &[offset, stride])]);
                        self.place_terms.insert(destination.clone(), term);
                    }
                }
                crate::verify::call_summary::CallEffect::ReturnPointerSub {
                    base_arg,
                    offset_arg,
                    stride,
                } => {
                    let base_term = call
                        .args
                        .get(*base_arg)
                        .and_then(|v| self.term_for_value_at(v, cursor, &mut TraceSeen::new()));
                    let offset_term = call
                        .args
                        .get(*offset_arg)
                        .and_then(|v| self.term_for_value_at(v, cursor, &mut TraceSeen::new()));
                    if let (Some(base), Some(offset)) = (base_term, offset_term) {
                        let stride = Int::from_u64(self.ctx, stride.unwrap_or(1));
                        let term =
                            Int::sub(self.ctx, &[base, Int::mul(self.ctx, &[offset, stride])]);
                        self.place_terms.insert(destination.clone(), term);
                    }
                }
                crate::verify::call_summary::CallEffect::ReturnLengthOfArg { arg } => {
                    let raw_source = call
                        .args
                        .get(*arg)
                        .and_then(|value| {
                            self.origin_key_for_value_before(value, cursor, &mut TraceSeen::new())
                        })
                        .or_else(|| call.args.get(*arg).map(value_label))
                        .unwrap_or_else(|| format!("arg{arg}"));
                    // Strip Deref projections (e.g. _1.* → _1) so the
                    // length term matches the contract's len(self) key.
                    let source = raw_source.split('.').next().unwrap_or(&raw_source);
                    let len_key = format!("len({source})");
                    let len_term = self.symbolic_len_term(&len_key);
                    self.place_terms.insert(destination.clone(), len_term);
                    self.assumptions.push(SmtPredicate::Eq(
                        SmtTerm::Place(destination.clone()),
                        SmtTerm::Value(len_key),
                    ));
                }
                crate::verify::call_summary::CallEffect::ReturnPointerFromArg { arg }
                | crate::verify::call_summary::CallEffect::ReturnAliasArg { arg } => {
                    let source_value = call.args.get(*arg);
                    if let Some(term) = source_value.and_then(|value| {
                        self.term_for_value_at(value, cursor, &mut TraceSeen::new())
                    }) {
                        self.place_terms.insert(destination.clone(), term);
                    }
                    let source = source_value
                        .map(value_label)
                        .unwrap_or_else(|| format!("arg{arg}"));
                    self.assumptions.push(SmtPredicate::Eq(
                        SmtTerm::Place(destination.clone()),
                        SmtTerm::Value(source),
                    ));
                }
                crate::verify::call_summary::CallEffect::ReturnConst { .. } => {}
                crate::verify::call_summary::CallEffect::ReturnTupleFieldLength {
                    field,
                    from_arg,
                } => {
                    if *field == 0 {
                        let cursor = self.call_definition_cursor(call);
                        if let Some(mid_term) = call
                            .args
                            .get(*from_arg)
                            .and_then(|v| {
                                self.term_for_value_at(v, cursor, &mut TraceSeen::new())
                            })
                        {
                            let label = value_label(
                                call.args.get(*from_arg)
                                    .unwrap_or(&AbstractValue::Unknown(String::new())),
                            );
                            let dest_key = PlaceKey {
                                base: PlaceBaseKey::Local(call.destination.as_usize()),
                                fields: vec![0],
                            };
                            self.place_terms.insert(dest_key.clone(), mid_term);
                            self.assumptions.push(SmtPredicate::Eq(
                                SmtTerm::Place(dest_key),
                                SmtTerm::Value(label),
                            ));
                        }
                    }
                }
                crate::verify::call_summary::CallEffect::ReturnNonZero
                | crate::verify::call_summary::CallEffect::ReturnAligned { .. }
                | crate::verify::call_summary::CallEffect::ReadMemory { .. }
                | crate::verify::call_summary::CallEffect::WriteMemory { .. }
                | crate::verify::call_summary::CallEffect::ForgetArgFacts { .. } => {}
            }
        }
    }

    /// Build an SMT term for a place.
    pub(crate) fn term_for_place(&mut self, place: &PlaceKey) -> Option<Int<'ctx>> {
        self.term_for_place_before(place, self.latest_cursor(), &mut TraceSeen::new())
    }

    /// Build an SMT term for a place using only definitions before `cursor`.
    fn term_for_place_before(
        &mut self,
        place: &PlaceKey,
        cursor: ValueCursor,
        seen: &mut TraceSeen,
    ) -> Option<Int<'ctx>> {
        let seen_key = (place.clone(), cursor);
        if !seen.insert(seen_key) {
            return None;
        }

        if !place.fields.is_empty() {
            if let Some(term) = self.projected_term_for_place(place, cursor, seen) {
                return Some(term);
            }
            if let Some(term) = self.place_terms.get(place) {
                return Some(term.clone());
            }
            let term = Int::new_const(self.ctx, place_name(place));
            self.place_terms.insert(place.clone(), term.clone());
            return Some(term);
        }

        if let Some(local) = place.local()
            && let Some(definition) = self.forward.latest_value_definition_before(local, cursor)
        {
            if let Some(term) = self.term_for_value_at(&definition.value, definition.ordinal, seen)
            {
                return Some(term);
            }
        }

        if let Some(value) = self.path_value_definition_before(place, cursor)
            && let Some(term) = self.term_for_value_at(&value, cursor, seen)
        {
            return Some(term);
        }

        if let Some(term) = self.place_terms.get(place) {
            return Some(term.clone());
        }

        // Use a shared per-local cache so every reference to the same MIR
        // local (e.g. parameter `mid`) produces the identical Z3 term.
        if place.fields.is_empty()
            && let Some(local) = place.local()
        {
            let id = local.as_usize();
            if let Some(term) = self.local_terms.get(&id) {
                let term = term.clone();
                self.place_terms.insert(place.clone(), term.clone());
                return Some(term);
            }
            let term = Int::new_const(self.ctx, place_name(place));
            self.local_terms.insert(id, term.clone());
            self.place_terms.insert(place.clone(), term.clone());
            return Some(term);
        }

        let term = Int::new_const(self.ctx, place_name(place));
        self.place_terms.insert(place.clone(), term.clone());
        Some(term)
    }

    /// Build terms for well-known aggregate projections.
    ///
    /// Checked integer arithmetic is represented as `(value, overflow)` in MIR.
    /// For numeric reasoning we can use field `0` as the mathematical result.
    /// Field `1` remains a fresh value, so overflow assertions do not become
    /// accidental constraints on the result itself.
    fn projected_term_for_place(
        &mut self,
        place: &PlaceKey,
        cursor: ValueCursor,
        seen: &mut TraceSeen,
    ) -> Option<Int<'ctx>> {
        let mut base = place.clone();
        base.fields.clear();
        let local = base.local()?;
        let definition = self.forward.latest_value_definition_before(local, cursor)?;
        let value = &definition.value;

        // Handle field projections from as_ptr_range / as_mut_ptr_range results.
        // Field 0 is the start pointer (== arg0's address).
        // Field 1 is the end pointer (== arg0's address + len of arg0).
        if let AbstractValue::CallResult(call) = value {
            let prim = PrimitiveCall::classify(&call.func);
            if prim == Some(PrimitiveCall::AsPtrRange)
                || prim == Some(PrimitiveCall::AsMutPtrRange)
            {
                let arg_index = if place.fields.as_slice() == [0] {
                    0 // field 0 = start = arg0.as_ptr()
                } else if place.fields.as_slice() == [1] {
                    0 // field 1 = end = arg0.as_ptr() + len (use base arg0 term)
                } else {
                    return None;
                };
                let call_cursor = self.call_definition_cursor(call);
                return call
                    .args
                    .get(arg_index)
                    .and_then(|arg| self.term_for_value_at(arg, call_cursor, seen));
            }
        }

        if place.fields.as_slice() != [0] {
            return None;
        }
        let AbstractValue::Binary(op, lhs, rhs) = value else {
            return None;
        };
        if !matches!(
            op,
            BinOp::AddWithOverflow | BinOp::SubWithOverflow | BinOp::MulWithOverflow
        ) {
            return None;
        }
        if matches!(op, BinOp::MulWithOverflow) {
            if let Some(len_origin) = ptr_metadata_origin(lhs, self) {
                let len_key = format!("len({len_origin})");
                let len_term = self.symbolic_len_term(&len_key);
                let rhs_term = self.term_for_value_at(rhs, definition.ordinal, seen)?;
                return Some(Int::mul(self.ctx, &[len_term, rhs_term]));
            }
        }
        let lhs = self.term_for_value_at(lhs, definition.ordinal, seen)?;
        let rhs = self.term_for_value_at(rhs, definition.ordinal, seen)?;
        self.term_for_binary(*op, &lhs, &rhs)
    }

    /// Build an SMT term for an abstract value.
    fn term_for_value(
        &mut self,
        value: &AbstractValue<'tcx>,
        seen: &mut TraceSeen,
    ) -> Option<Int<'ctx>> {
        self.term_for_value_at(value, self.latest_cursor(), seen)
    }

    /// Build an address expression for a call summarized as pointer arithmetic.
    fn term_for_pointer_arith_call(
        &mut self,
        call: &CallSummary<'tcx>,
        cursor: ValueCursor,
        seen: &mut TraceSeen,
    ) -> Option<Int<'ctx>> {
        let effect = call.effects.iter().find_map(|effect| match effect {
            crate::verify::call_summary::CallEffect::ReturnPointerAdd {
                base_arg,
                offset_arg,
                stride,
            } => Some((false, *base_arg, *offset_arg, *stride)),
            crate::verify::call_summary::CallEffect::ReturnPointerSub {
                base_arg,
                offset_arg,
                stride,
            } => Some((true, *base_arg, *offset_arg, *stride)),
            _ => None,
        });

        let (is_sub, base_arg, offset_arg, stride) = effect.or_else(|| {
            if is_pointer_add_call(&call.func) {
                Some((false, 0, 1, self.call_destination_stride(call)))
            } else if is_pointer_sub_call(&call.func) {
                Some((true, 0, 1, self.call_destination_stride(call)))
            } else {
                None
            }
        })?;

        let base = call.args.get(base_arg)?;
        let offset = call.args.get(offset_arg)?;
        let base = self.term_for_value_at(base, cursor, seen)?;
        let offset = self.term_for_value_at(offset, cursor, seen)?;
        let stride = Int::from_u64(self.ctx, stride.unwrap_or(1));
        let scaled_offset = Int::mul(self.ctx, &[offset, stride]);

        if is_sub {
            Some(Int::sub(self.ctx, &[base, scaled_offset]))
        } else {
            Some(Int::add(self.ctx, &[base, scaled_offset]))
        }
    }

    /// Build a stable `len(origin)` term for calls summarized as length reads.
    fn term_for_length_call(
        &mut self,
        call: &CallSummary<'tcx>,
        cursor: ValueCursor,
        seen: &mut TraceSeen,
    ) -> Option<Int<'ctx>> {
        let arg = call.effects.iter().find_map(|effect| {
            let crate::verify::call_summary::CallEffect::ReturnLengthOfArg { arg } = effect else {
                return None;
            };
            Some(*arg)
        })?;
        let source = call.args.get(arg)?;
        let source = self
            .origin_key_for_value_before(source, cursor, seen)
            .unwrap_or_else(|| value_label(source));
        let len_key = format!("len({source})");
        Some(self.symbolic_len_term(&len_key))
    }

    /// Return a cached Z3 integer symbol for a const generic parameter,
    /// keyed by its plain name (e.g. `N`).  Accepts either a plain name or a
    /// rustc debug string such as `Ty(usize, N/#1)` / `Param(N)`, so that a
    /// const parameter referenced from a MIR operand, a contract, and an array
    /// length all resolve to the same `const_<name>` symbol.
    fn const_param_symbol(&mut self, name_or_debug: &str) -> Int<'ctx> {
        let plain = const_param_name_from_debug(name_or_debug)
            .unwrap_or_else(|| name_or_debug.to_string());
        let key = format!("const_{}", sanitize_smt_name(&plain));
        if let Some(term) = self.const_terms.get(&key) {
            return term.clone();
        }
        let term = Int::new_const(self.ctx, key.as_str());
        self.const_terms.insert(key, term.clone());
        term
    }

    /// Build an SMT term for an abstract value at a program point.
    fn term_for_value_at(
        &mut self,
        value: &AbstractValue<'tcx>,
        cursor: ValueCursor,
        seen: &mut TraceSeen,
    ) -> Option<Int<'ctx>> {
        match value {
            AbstractValue::ConstInt(value) => Some(Int::from_u64(self.ctx, *value as u64)),
            AbstractValue::ConstParam(name) => Some(self.const_param_symbol(name)),
            AbstractValue::Const(text) => {
                const_int_from_debug(text).map(|value| Int::from_u64(self.ctx, value as u64))
                    .or_else(|| {
                        // A constant operand may be a const generic parameter
                        // (e.g. debug `Ty(usize, N/#1)`).  Normalize its symbol
                        // to `const_<name>` so it unifies with the same const
                        // parameter referenced elsewhere (contracts, array
                        // lengths) instead of minting `const_Ty_usize__N__1_`.
                        if let Some(param) = const_param_name_from_debug(text) {
                            return Some(self.const_param_symbol(&param));
                        }
                        let name = sanitize_smt_name(text);
                        if name.is_empty() { None }
                        else { Some(Int::new_const(self.ctx, format!("const_{name}"))) }
                    })
            }
            AbstractValue::Place(place) => self.term_for_place_before(place, cursor, seen),
            AbstractValue::Cast(inner, _) => self.term_for_value_at(inner, cursor, seen),
            AbstractValue::Ref(place) | AbstractValue::RawPtr(place) => Some(Int::new_const(
                self.ctx,
                format!("addr_{}", place_name(place)),
            )),
            AbstractValue::Binary(op, lhs, rhs) => {
                let lhs = self.term_for_value_at(lhs, cursor, seen)?;
                let rhs = self.term_for_value_at(rhs, cursor, seen)?;
                self.term_for_binary(*op, &lhs, &rhs)
            }
            AbstractValue::CallResult(call) => {
                if let Some(term) = self.term_for_pointer_arith_call(call, cursor, seen) {
                    return Some(term);
                }
                if let Some(term) = self.term_for_length_call(call, cursor, seen) {
                    return Some(term);
                }
                let place = PlaceKey {
                    base: PlaceBaseKey::Local(call.destination.as_usize()),
                    fields: Vec::new(),
                };
                Some(Int::new_const(self.ctx, place_name(&place)))
            }
            AbstractValue::Unknown(_)
            | AbstractValue::ThreadLocal(_)
            | AbstractValue::Repeat(_)
            | AbstractValue::Nullary(_)
            | AbstractValue::Discriminant(_)
            | AbstractValue::Aggregate(_, _) => None,
            AbstractValue::Unary(op, inner) => match op {
                UnOp::PtrMetadata => {
                    let source = self
                        .origin_key_for_value_before(inner, cursor, seen)
                        .unwrap_or_else(|| value_label(inner));
                    let len_key = format!("len({source})");
                    Some(self.symbolic_len_term(&len_key))
                }
                _ => None,
            },
            #[cfg(not(rapx_rustc_ge_196))]
            AbstractValue::ShallowInitBox(_, _) => None,
        }
    }

    /// Build an SMT integer term from a property-independent diagnostic term.
    fn term_for_smt_term(&mut self, term: &SmtTerm) -> Option<Int<'ctx>> {
        match term {
            SmtTerm::Place(place) => self.term_for_place(place),
            SmtTerm::Value(name) => {
                if name.starts_with("len(") {
                    Some(self.symbolic_len_term(name))
                } else {
                    Some(Int::new_const(self.ctx, sanitize_smt_name(name)))
                }
            }
            SmtTerm::Const(value) => Some(Int::from_u64(self.ctx, *value)),
            SmtTerm::ConstParam(text) => {
                if sanitize_smt_name(text).is_empty() {
                    return None;
                }
                Some(self.const_param_symbol(text))
            }
            SmtTerm::Add(lhs, rhs) => {
                let lhs = self.term_for_smt_term(lhs)?;
                let rhs = self.term_for_smt_term(rhs)?;
                Some(Int::add(self.ctx, &[lhs, rhs]))
            }
            SmtTerm::Sub(lhs, rhs) => {
                let lhs = self.term_for_smt_term(lhs)?;
                let rhs = self.term_for_smt_term(rhs)?;
                Some(Int::sub(self.ctx, &[lhs, rhs]))
            }
            SmtTerm::Mul(lhs, rhs) => {
                let lhs = self.term_for_smt_term(lhs)?;
                let rhs = self.term_for_smt_term(rhs)?;
                Some(Int::mul(self.ctx, &[lhs, rhs]))
            }
            SmtTerm::Div(lhs, rhs) => {
                let lhs = self.term_for_smt_term(lhs)?;
                let rhs = self.term_for_smt_term(rhs)?;
                Some(lhs.div(&rhs))
            }
            SmtTerm::Rem(lhs, rhs) => {
                let lhs = self.term_for_smt_term(lhs)?;
                let rhs = self.term_for_smt_term(rhs)?;
                Some(lhs.modulo(&rhs))
            }
        }
    }

    /// Build a boolean term for a conjunction of shared predicates.
    fn bool_for_predicates(&mut self, predicates: &[SmtPredicate]) -> Option<Bool<'ctx>> {
        match predicates {
            [] => None,
            [predicate] => self.bool_for_predicate(predicate),
            predicates => {
                let bools = predicates
                    .iter()
                    .map(|predicate| self.bool_for_predicate(predicate))
                    .collect::<Option<Vec<_>>>()?;
                let refs = bools.iter().collect::<Vec<_>>();
                Some(Bool::and(self.ctx, &refs))
            }
        }
    }

    /// Build a boolean term from a shared diagnostic/query predicate.
    fn bool_for_predicate(&mut self, predicate: &SmtPredicate) -> Option<Bool<'ctx>> {
        match predicate {
            SmtPredicate::Eq(lhs, rhs) => {
                let lhs = self.term_for_smt_term(lhs)?;
                let rhs = self.term_for_smt_term(rhs)?;
                Some(lhs._eq(&rhs))
            }
            SmtPredicate::Ne(lhs, rhs) => {
                let lhs = self.term_for_smt_term(lhs)?;
                let rhs = self.term_for_smt_term(rhs)?;
                Some(lhs._eq(&rhs).not())
            }
            SmtPredicate::Le(lhs, rhs) => {
                let lhs = self.term_for_smt_term(lhs)?;
                let rhs = self.term_for_smt_term(rhs)?;
                Some(lhs.le(&rhs))
            }
            SmtPredicate::Lt(lhs, rhs) => {
                let lhs = self.term_for_smt_term(lhs)?;
                let rhs = self.term_for_smt_term(rhs)?;
                Some(lhs.lt(&rhs))
            }
            SmtPredicate::Ge(lhs, rhs) => {
                let lhs = self.term_for_smt_term(lhs)?;
                let rhs = self.term_for_smt_term(rhs)?;
                Some(lhs.ge(&rhs))
            }
            SmtPredicate::Gt(lhs, rhs) => {
                let lhs = self.term_for_smt_term(lhs)?;
                let rhs = self.term_for_smt_term(rhs)?;
                Some(lhs.gt(&rhs))
            }
            SmtPredicate::And(predicates) => self.bool_for_predicates(predicates),
            SmtPredicate::Divisible { term, modulus } => {
                let term = self.term_for_smt_term(term)?;
                let modulus = Int::from_u64(self.ctx, *modulus);
                let zero = Int::from_u64(self.ctx, 0);
                Some(term.modulo(&modulus)._eq(&zero))
            }
            SmtPredicate::InBounds {
                index,
                access_count,
                len,
            } => {
                let index = self.term_for_smt_term(index)?;
                let access_count = self.term_for_smt_term(access_count)?;
                let len = self.term_for_smt_term(len)?;
                let zero = Int::from_u64(self.ctx, 0);
                let covered_end = Int::add(self.ctx, &[index.clone(), access_count]);
                Some(Bool::and(
                    self.ctx,
                    &[&index.ge(&zero), &covered_end.le(&len)],
                ))
            }
            SmtPredicate::NonOverlapping {
                left,
                right,
                left_count,
                right_count,
                elem_size,
            } => {
                let left = self.term_for_smt_term(left)?;
                let right = self.term_for_smt_term(right)?;
                let left_count = self.term_for_smt_term(left_count)?;
                let right_count = self.term_for_smt_term(right_count)?;
                let elem_size = Int::from_u64(self.ctx, *elem_size);
                let left_end = Int::add(
                    self.ctx,
                    &[
                        left.clone(),
                        Int::mul(self.ctx, &[left_count, elem_size.clone()]),
                    ],
                );
                let right_end = Int::add(
                    self.ctx,
                    &[right.clone(), Int::mul(self.ctx, &[right_count, elem_size])],
                );
                Some(Bool::or(
                    self.ctx,
                    &[&left_end.le(&right), &right_end.le(&left)],
                ))
            }
            SmtPredicate::Not(predicate) => Some(self.bool_for_predicate(predicate)?.not()),
            SmtPredicate::Custom(_) => None,
        }
    }

    /// Assert Rust unsigned integer lower bounds for terms that appear in a
    /// numeric obligation.
    fn assert_unsigned_bounds_for_predicates(
        &mut self,
        solver: &Solver<'ctx>,
        predicates: &[SmtPredicate],
    ) {
        let mut seen = HashSet::new();
        for predicate in predicates {
            self.assert_unsigned_bounds_for_predicate(solver, predicate, &mut seen);
        }
    }

    fn assert_unsigned_bounds_for_predicate(
        &mut self,
        solver: &Solver<'ctx>,
        predicate: &SmtPredicate,
        seen: &mut HashSet<PlaceKey>,
    ) {
        match predicate {
            SmtPredicate::Eq(lhs, rhs)
            | SmtPredicate::Ne(lhs, rhs)
            | SmtPredicate::Le(lhs, rhs)
            | SmtPredicate::Lt(lhs, rhs)
            | SmtPredicate::Ge(lhs, rhs)
            | SmtPredicate::Gt(lhs, rhs) => {
                self.assert_unsigned_bounds_for_term(solver, lhs, seen);
                self.assert_unsigned_bounds_for_term(solver, rhs, seen);
            }
            SmtPredicate::And(predicates) => {
                for predicate in predicates {
                    self.assert_unsigned_bounds_for_predicate(solver, predicate, seen);
                }
            }
            SmtPredicate::Divisible { term, .. } => {
                self.assert_unsigned_bounds_for_term(solver, term, seen);
            }
            SmtPredicate::InBounds {
                index,
                access_count,
                len,
            } => {
                self.assert_unsigned_bounds_for_term(solver, index, seen);
                self.assert_unsigned_bounds_for_term(solver, access_count, seen);
                self.assert_unsigned_bounds_for_term(solver, len, seen);
            }
            SmtPredicate::NonOverlapping {
                left_count,
                right_count,
                ..
            } => {
                self.assert_unsigned_bounds_for_term(solver, left_count, seen);
                self.assert_unsigned_bounds_for_term(solver, right_count, seen);
            }
            SmtPredicate::Not(predicate) => {
                self.assert_unsigned_bounds_for_predicate(solver, predicate, seen);
            }
            SmtPredicate::Custom(_) => {}
        }
    }

    fn assert_unsigned_bounds_for_term(
        &mut self,
        solver: &Solver<'ctx>,
        term: &SmtTerm,
        seen: &mut HashSet<PlaceKey>,
    ) {
        match term {
            SmtTerm::Place(place) => {
                if !seen.insert(place.clone()) {
                    return;
                }
                let Some(ty) = self.place_ty(place) else {
                    return;
                };
                if !is_unsigned_integral_ty(ty) {
                    return;
                }
                let Some(int_term) = self.term_for_place(place) else {
                    return;
                };
                let zero = Int::from_u64(self.ctx, 0);
                solver.assert(&int_term.ge(&zero));
                self.assumptions.push(SmtPredicate::Ge(
                    SmtTerm::Place(place.clone()),
                    SmtTerm::Const(0),
                ));
            }
            SmtTerm::Add(lhs, rhs)
            | SmtTerm::Sub(lhs, rhs)
            | SmtTerm::Mul(lhs, rhs)
            | SmtTerm::Div(lhs, rhs)
            | SmtTerm::Rem(lhs, rhs) => {
                self.assert_unsigned_bounds_for_term(solver, lhs, seen);
                self.assert_unsigned_bounds_for_term(solver, rhs, seen);
            }
            SmtTerm::Value(_) | SmtTerm::Const(_) | SmtTerm::ConstParam(_) => {}
        }
    }

    /// Lower a binary MIR operation to an integer term.
    fn term_for_binary(&self, op: BinOp, lhs: &Int<'ctx>, rhs: &Int<'ctx>) -> Option<Int<'ctx>> {
        let one = Int::from_u64(self.ctx, 1);
        let zero = Int::from_u64(self.ctx, 0);
        Some(match op {
            BinOp::Add | BinOp::AddWithOverflow => Int::add(self.ctx, &[lhs.clone(), rhs.clone()]),
            BinOp::Sub | BinOp::SubWithOverflow => Int::sub(self.ctx, &[lhs.clone(), rhs.clone()]),
            BinOp::Mul | BinOp::MulWithOverflow => Int::mul(self.ctx, &[lhs.clone(), rhs.clone()]),
            BinOp::Div => lhs.div(rhs),
            BinOp::Rem => lhs.modulo(rhs),
            BinOp::Eq => lhs._eq(rhs).ite(&one, &zero),
            BinOp::Ne => lhs._eq(rhs).not().ite(&one, &zero),
            BinOp::Lt => lhs.lt(rhs).ite(&one, &zero),
            BinOp::Le => lhs.le(rhs).ite(&one, &zero),
            BinOp::Gt => lhs.gt(rhs).ite(&one, &zero),
            BinOp::Ge => lhs.ge(rhs).ite(&one, &zero),
            _ => return None,
        })
    }

    /// Return the byte stride for a typed pointer-add call destination.
    fn call_destination_stride(&self, call: &CallSummary<'tcx>) -> Option<u64> {
        let place = PlaceKey {
            base: PlaceBaseKey::Local(call.destination.as_usize()),
            fields: Vec::new(),
        };
        let destination_ty = self.place_ty(&place)?;
        let pointee = pointee_ty(destination_ty)?;
        self.type_layout(pointee).map(|(_, size)| size)
    }

    /// Return the MIR type for a simple place key.
    fn place_ty(&self, place: &PlaceKey) -> Option<Ty<'tcx>> {
        if !place.fields.is_empty() {
            return self.forward.facts.iter().find_map(|fact| {
                let StateFact::Cast { target, ty, .. } = fact else {
                    return None;
                };
                if target == place { Some(*ty) } else { None }
            });
        }
        let local = match place.base {
            PlaceBaseKey::Return => Local::from_usize(0),
            PlaceBaseKey::Local(local) => Local::from_usize(local),
            PlaceBaseKey::Arg(_) => return None,
        };
        Some(self.tcx.optimized_mir(self.checkpoint.caller).local_decls[local].ty)
    }

    fn type_layout(&self, ty: Ty<'tcx>) -> Option<(u64, u64)> {
        safe_type_layout(self.tcx, self.checkpoint.caller, ty)
    }

    /// Return the alignment guaranteed by a concrete or generic type.
    fn guaranteed_alignment(&self, ty: Ty<'tcx>) -> Option<u64> {
        if let Some((align, _)) = self.type_layout(ty).filter(|(align, _)| *align > 0) {
            return Some(align);
        }
        if let Some(alignments) = self.generic_candidate_alignments(ty) {
            return alignments.into_iter().min();
        }
        if matches!(ty.kind(), TyKind::Param(_) | TyKind::Array(..) | TyKind::Ref(..) | TyKind::RawPtr(..)) {
            return Some(0);
        }
        None
    }

    fn generic_candidate_alignments(&self, ty: Ty<'tcx>) -> Option<Vec<u64>> {
        let candidates = GenericTypeCandidates::for_def(self.tcx, self.checkpoint.caller);
        let alignments = candidates
            .candidates_for_ty(ty)?
            .iter()
            .filter_map(|candidate| self.type_layout(*candidate).map(|(align, _)| align))
            .filter(|align| *align > 0)
            .collect::<Vec<_>>();
        if alignments.is_empty() {
            None
        } else {
            Some(alignments)
        }
    }

    /// Return the pointer-add call/effect that produced a place after copies/casts.
    fn pointer_add_call_for_place(&self, place: &PlaceKey) -> Option<CallSummary<'tcx>> {
        let value = self.resolved_value_for_place_before(
            place,
            self.latest_cursor(),
            &mut TraceSeen::new(),
        )?;
        match value {
            AbstractValue::CallResult(call)
                if call_has_pointer_add_effect(&call) || call_has_pointer_sub_effect(&call) =>
            {
                Some(call)
            }
            _ => None,
        }
    }

    /// Resolve copy/cast chains for a MIR place into the value at their source.
    fn resolved_value_for_place(
        &self,
        place: &PlaceKey,
        seen: &mut TraceSeen,
    ) -> Option<AbstractValue<'tcx>> {
        self.resolved_value_for_place_before(place, self.latest_cursor(), seen)
    }

    fn resolved_value_for_place_before(
        &self,
        place: &PlaceKey,
        cursor: ValueCursor,
        seen: &mut TraceSeen,
    ) -> Option<AbstractValue<'tcx>> {
        let seen_key = (place.clone(), cursor);
        if !seen.insert(seen_key) {
            return None;
        }
        if !place.fields.is_empty() {
            let mut base = place.clone();
            base.fields.clear();
            let local = base.local()?;
            if let Some(definition) = self.forward.latest_value_definition_before(local, cursor) {
                // Handle as_ptr_range / as_mut_ptr_range (call result)
                if let AbstractValue::CallResult(call) = &definition.value {
                    let prim = PrimitiveCall::classify(&call.func);
                    if prim == Some(PrimitiveCall::AsPtrRange)
                        || prim == Some(PrimitiveCall::AsMutPtrRange)
                    {
                        if let Some(source_arg) = call.effects.iter().find_map(|effect| {
                            match effect {
                                crate::verify::call_summary::CallEffect::ReturnAliasArg { arg }
                                | crate::verify::call_summary::CallEffect::ReturnPointerFromArg { arg } => Some(*arg),
                                _ => None,
                            }
                        }) {
                            let call_cursor = self.call_definition_cursor(call);
                            if let Some(arg_value) = call.args.get(source_arg) {
                                return self.resolved_value_before(arg_value, call_cursor, seen);
                            }
                        }
                    }
                }
                // Handle inlined as_ptr_range (aggregate of as_ptr + add results)
                // Find Cast facts that connect field places to their source values
                if let AbstractValue::Aggregate(_, _) = &definition.value {
                    for fact in &self.forward.facts {
                        if let StateFact::Cast { target, source, .. } = fact {
                            if *target == *place {
                                return self.resolved_value_before(source, definition.ordinal, seen);
                            }
                        }
                    }
                }
            }
            return Some(AbstractValue::Place(place.clone()));
        }
        let local = place.local()?;
        if let Some(definition) = self.forward.latest_value_definition_before(local, cursor) {
            return self.resolved_value_before(&definition.value, definition.ordinal, seen);
        }
        if let Some(value) = self.path_value_definition_before(place, cursor) {
            return self.resolved_value_before(&value, cursor, seen);
        }
        None
    }

    /// Resolve copy/cast chains for an abstract value.
    fn resolved_value(
        &self,
        value: &AbstractValue<'tcx>,
        seen: &mut TraceSeen,
    ) -> Option<AbstractValue<'tcx>> {
        self.resolved_value_before(value, self.latest_cursor(), seen)
    }

    fn resolved_value_before(
        &self,
        value: &AbstractValue<'tcx>,
        cursor: ValueCursor,
        seen: &mut TraceSeen,
    ) -> Option<AbstractValue<'tcx>> {
        match value {
            AbstractValue::Place(place) => {
                self.resolved_value_for_place_before(place, cursor, seen)
            }
            AbstractValue::Cast(inner, _) => self.resolved_value_before(inner, cursor, seen),
            _ => Some(value.clone()),
        }
    }

    /// Recover a local definition directly from the expanded MIR path.
    ///
    /// Backward relevance keeps the proof slice intentionally small. When a
    /// pure call-argument temporary is not retained in the forward visit, SMT
    /// term construction can still recover its value by replaying assignments
    /// along the already-enumerated path up to the current cursor.
    fn path_value_definition_before(
        &self,
        place: &PlaceKey,
        cursor: ValueCursor,
    ) -> Option<AbstractValue<'tcx>> {
        if !place.fields.is_empty() {
            return None;
        }
        let local = place.local()?;
        let cutoff = self.path_cursor_cutoff(cursor);
        let body = self.tcx.optimized_mir(self.forward.checkpoint.caller);
        let mut latest = None;

        for step in &self.forward.path.steps {
            let PathStep::Block(block) = step else {
                continue;
            };
            let is_cutoff_block = *block == cutoff.block;
            let block_data = &body.basic_blocks[*block];

            for (statement_index, statement) in block_data.statements.iter().enumerate() {
                if is_cutoff_block
                    && let Some(cutoff_statement) = cutoff.statement_index
                    && statement_index >= cutoff_statement
                {
                    return latest;
                }

                let rustc_middle::mir::StatementKind::Assign(assign) = &statement.kind else {
                    continue;
                };
                let (target, rvalue) = &**assign;
                if target.local == local {
                    latest = abstract_value_from_rvalue(rvalue);
                }
            }

            if is_cutoff_block {
                return latest;
            }
        }

        latest
    }

    fn path_cursor_cutoff(&self, cursor: ValueCursor) -> PathCursorCutoff {
        if let Some(definition) = self.forward.value_definitions.get(cursor) {
            return PathCursorCutoff {
                block: definition.block,
                statement_index: definition.statement_index,
            };
        }

        PathCursorCutoff {
            block: self.forward.checkpoint.block,
            statement_index: None,
        }
    }

    /// Return a stable origin key for matching `as_ptr(source)` and `len(source)`.
    fn origin_key_for_value(
        &self,
        value: &AbstractValue<'tcx>,
        seen: &mut TraceSeen,
    ) -> Option<String> {
        self.origin_key_for_value_before(value, self.latest_cursor(), seen)
    }

    fn origin_key_for_value_before(
        &self,
        value: &AbstractValue<'tcx>,
        cursor: ValueCursor,
        seen: &mut TraceSeen,
    ) -> Option<String> {
        let resolved = self
            .resolved_value_before(value, cursor, seen)
            .unwrap_or_else(|| value.clone());
        match resolved {
            AbstractValue::Ref(place) | AbstractValue::RawPtr(place) => Some(place_label(&place)),
            AbstractValue::Place(place) => self
                .source_from_points_to(&place)
                .map(|source| place_label(&source))
                .or_else(|| {
                    // Follow PointsTo(pointer→source) recursively to find
                    // the ultimate origin (e.g. _5 → _6 → _1).
                    self.forward.facts.iter().find_map(|fact| match fact {
                        StateFact::PointsTo { pointer, source } if *pointer == place => {
                            self.origin_key_for_value_before(
                                &AbstractValue::Place(source.clone()),
                                cursor,
                                seen,
                            )
                        }
                        _ => None,
                    })
                })
                .or_else(|| Some(place_label(&place))),
            AbstractValue::Cast(inner, _) => self.origin_key_for_value_before(&inner, cursor, seen),
            AbstractValue::CallResult(call) if is_as_ptr_call(&call.func) => {
                let source_arg = call.effects.iter().find_map(|effect| match effect {
                    crate::verify::call_summary::CallEffect::ReturnPointerFromArg { arg }
                    | crate::verify::call_summary::CallEffect::ReturnAliasArg { arg } => Some(*arg),
                    _ => None,
                })?;
                let call_cursor = self.call_definition_cursor(&call);
                self.origin_key_for_value_before(call.args.get(source_arg)?, call_cursor, seen)
            }
            AbstractValue::CallResult(call) => {
                if let Some(source_arg) = call.effects.iter().find_map(|effect| match effect {
                    crate::verify::call_summary::CallEffect::ReturnPointerFromArg { arg }
                    | crate::verify::call_summary::CallEffect::ReturnAliasArg { arg } => Some(*arg),
                    crate::verify::call_summary::CallEffect::ReturnPointerAdd { base_arg, .. }
                    | crate::verify::call_summary::CallEffect::ReturnPointerSub { base_arg, .. } => Some(*base_arg),
                    _ => None,
                }) {
                    let call_cursor = self.call_definition_cursor(&call);
                    return self.origin_key_for_value_before(
                        call.args.get(source_arg)?,
                        call_cursor,
                        seen,
                    );
                }
                let destination = PlaceKey {
                    base: PlaceBaseKey::Local(call.destination.as_usize()),
                    fields: Vec::new(),
                };
                Some(place_label(&destination))
            }
            _ => Some(value_label(&resolved)),
        }
    }

    /// Recover a length value from a path guard that mentions `index`.
    fn guarded_len_for_index(
        &self,
        base_origin: &str,
        index: &AbstractValue<'tcx>,
    ) -> Option<AbstractValue<'tcx>> {
        let index = self
            .resolved_value(index, &mut HashSet::new())
            .unwrap_or_else(|| index.clone());
        for fact in &self.forward.facts {
            let StateFact::BranchEq { value, equals: 1, .. } = fact else {
                continue;
            };
            let predicate = self
                .resolved_value(value, &mut HashSet::new())
                .unwrap_or_else(|| value.clone());
            let AbstractValue::Binary(op, lhs, rhs) = predicate else {
                continue;
            };
            match op {
                BinOp::Lt | BinOp::Le => {
                    if self.value_mentions(&lhs, &index)
                        && self.len_matches_origin(&rhs, base_origin)
                    {
                        return Some(*rhs);
                    }
                }
                BinOp::Gt | BinOp::Ge => {
                    if self.value_mentions(&rhs, &index)
                        && self.len_matches_origin(&lhs, base_origin)
                    {
                        return Some(*lhs);
                    }
                }
                _ => {}
            }
        }
        None
    }

    /// Return true when `haystack` contains the same resolved value as `needle`.
    fn value_mentions(&self, haystack: &AbstractValue<'tcx>, needle: &AbstractValue<'tcx>) -> bool {
        self.value_mentions_inner(haystack, needle, &mut HashSet::new())
    }

    fn value_mentions_inner(
        &self,
        haystack: &AbstractValue<'tcx>,
        needle: &AbstractValue<'tcx>,
        seen: &mut HashSet<(String, String)>,
    ) -> bool {
        let haystack = self
            .resolved_value(haystack, &mut HashSet::new())
            .unwrap_or_else(|| haystack.clone());
        let needle = self
            .resolved_value(needle, &mut HashSet::new())
            .unwrap_or_else(|| needle.clone());
        let haystack_label = value_label(&haystack);
        let needle_label = value_label(&needle);
        if haystack_label == needle_label {
            return true;
        }
        if !seen.insert((haystack_label, needle_label)) {
            return false;
        }
        match haystack {
            AbstractValue::Cast(inner, _) | AbstractValue::Unary(_, inner) => {
                self.value_mentions_inner(&inner, &needle, seen)
            }
            AbstractValue::Binary(_, lhs, rhs) => {
                self.value_mentions_inner(&lhs, &needle, seen)
                    || self.value_mentions_inner(&rhs, &needle, seen)
            }
            _ => false,
        }
    }

    /// Return true when a length-like value is the metadata/len of `base_origin`.
    fn len_matches_origin(&self, len: &AbstractValue<'tcx>, base_origin: &str) -> bool {
        self.len_matches_origin_inner(len, base_origin, &mut HashSet::new())
    }

    fn len_matches_origin_inner(
        &self,
        len: &AbstractValue<'tcx>,
        base_origin: &str,
        seen: &mut HashSet<String>,
    ) -> bool {
        let label = value_label(len);
        if !seen.insert(label) {
            return false;
        }
        let resolved = self
            .resolved_value(len, &mut HashSet::new())
            .unwrap_or_else(|| len.clone());
        match resolved {
            AbstractValue::Place(place) => value_for_place(self.forward, &place)
                .is_some_and(|value| self.len_matches_origin_inner(value, base_origin, seen)),
            AbstractValue::Unary(UnOp::PtrMetadata, inner) => self
                .origin_key_for_value(&inner, &mut HashSet::new())
                .is_some_and(|origin| origin == base_origin),
            AbstractValue::CallResult(call) => call.effects.iter().any(|effect| {
                let crate::verify::call_summary::CallEffect::ReturnLengthOfArg { arg } = effect
                else {
                    return false;
                };
                call.args
                    .get(*arg)
                    .and_then(|value| self.origin_key_for_value(value, &mut HashSet::new()))
                    .is_some_and(|origin| origin == base_origin)
            }),
            _ => false,
        }
    }

    /// Return the source place recorded by a `PointsTo(pointer, source)` fact.
    fn source_from_points_to(&self, pointer: &PlaceKey) -> Option<PlaceKey> {
        self.forward.facts.iter().find_map(|fact| match fact {
            StateFact::PointsTo {
                pointer: fact_pointer,
                source,
            } if fact_pointer == pointer => Some(source.clone()),
            _ => None,
        })
        .or_else(|| {
            if pointer.fields.is_empty() {
                return None;
            }
            let mut base = pointer.clone();
            base.fields.clear();
            self.forward.facts.iter().find_map(|fact| match fact {
                StateFact::PointsTo {
                    pointer: fact_pointer,
                    source,
                } if *fact_pointer == base => Some(source.clone()),
                _ => None,
            })
        })
    }

    /// Candidate address/value terms for an `Init` target.
    ///
    /// Pointer targets use their value term.  By-value `MaybeUninit<T>` targets
    /// may be moved into a temporary before `assume_init`; in that case the
    /// relevant initialized storage is the address of the original place.
    fn init_target_terms(&mut self, place: &PlaceKey) -> Vec<Int<'ctx>> {
        let mut terms = Vec::new();
        if let Some(term) = self.term_for_place(place) {
            terms.push(term);
        }
        if let Some(term) = self.storage_addr_for_place(place, &mut HashSet::new()) {
            if !terms.iter().any(|existing| existing == &term) {
                terms.push(term);
            }
        }
        terms
    }

    /// Candidate address/value terms for a known initialized write.
    fn init_source_terms(&mut self, place: &PlaceKey) -> Vec<Int<'ctx>> {
        let mut terms = Vec::new();
        if let Some(term) = self.term_for_place(place) {
            terms.push(term);
        }
        if let Some(source) = self.source_from_points_to(place)
            && let Some(term) = self.storage_addr_for_place(&source, &mut HashSet::new())
            && !terms.iter().any(|existing| existing == &term)
        {
            terms.push(term);
        }
        terms
    }

    /// Return the address of the storage represented by `place`.
    fn storage_addr_for_place(
        &mut self,
        place: &PlaceKey,
        seen: &mut HashSet<PlaceKey>,
    ) -> Option<Int<'ctx>> {
        if !seen.insert(place.clone()) {
            return None;
        }
        if let Some(value) = value_for_place(self.forward, place) {
            match &value {
                AbstractValue::Place(inner) => {
                    return self.storage_addr_for_place(inner, seen);
                }
                AbstractValue::Cast(inner, _) => {
                    if let AbstractValue::Place(inner_place) = inner.as_ref() {
                        return self.storage_addr_for_place(inner_place, seen);
                    }
                }
                _ => {}
            }
        }
        if let Some(source) = self.source_from_points_to(place) {
            return self.storage_addr_for_place(&source, seen);
        }
        Some(Int::new_const(
            self.ctx,
            format!("addr_{}", place_name(place)),
        ))
    }

    /// Find a retained `len(source)` call whose source matches `origin_key`.
    fn bounds_len_for_origin(
        &mut self,
        origin_key: &str,
        index: Option<&AbstractValue<'tcx>>,
    ) -> Option<(Int<'ctx>, SmtTerm)> {
        if let Some(len_place) = self.len_place_for_origin(origin_key) {
            return Some((self.term_for_place(&len_place)?, SmtTerm::Place(len_place)));
        }
        if let Some(index) = index
            && let Some(len_value) = self.guarded_len_for_index(origin_key, index)
        {
            return Some((
                self.term_for_value(&len_value, &mut HashSet::new())?,
                SmtTerm::Value(value_label(&len_value)),
            ));
        }
        let result = self.allocated_len_for_origin(origin_key)
            .filter(|&len| len > 0)
            .map(|len| (Int::from_u64(self.ctx, len), SmtTerm::Const(len)))
            .or_else(|| {
                if self.is_maybe_uninit_origin(origin_key) {
                    let len_term = Int::from_u64(self.ctx, u64::MAX / 8);
                    Some((len_term, SmtTerm::Const(u64::MAX / 8)))
                } else if self.is_slice_pointer_origin(origin_key) {
                    let len_key = format!("len({})", origin_key);
                    let len_term = self.symbolic_len_term(&len_key);
                    Some((len_term, SmtTerm::Value(len_key)))
                } else {
                    None
                }
            });
        result
    }

    /// Return true if `origin_key` is the source of an `as_ptr`-like call
    /// (suggesting it is a slice / reference whose internal pointer was
    /// extracted).  For these origins a symbolic length term is safe because
    /// the length is naturally bounded by the reference type.
    fn is_slice_pointer_origin(&self, origin_key: &str) -> bool {
        self.forward.facts.iter().any(|fact| {
            let StateFact::Call(call) = fact else { return false };
            let is_ptr_like = is_as_ptr_call(&call.func);
            let is_ptr_range = PrimitiveCall::classify(&call.func)
                .is_some_and(|p| matches!(p, PrimitiveCall::AsPtrRange | PrimitiveCall::AsMutPtrRange));
            (is_ptr_like || is_ptr_range)
                && call.effects.iter().any(|effect| {
                    matches!(
                        effect,
                        crate::verify::call_summary::CallEffect::ReturnAliasArg { .. }
                            | crate::verify::call_summary::CallEffect::ReturnPointerFromArg { .. }
                    )
                })
                && call.args.iter().any(|arg| {
                    self.origin_key_for_value(arg, &mut HashSet::new())
                        .is_some_and(|key| key == origin_key)
                })
        })
    }

    /// Return true if the allocation for `origin_key` is a `MaybeUninit`
    /// wrapper (dynamic-length array).  These have `elements == 0` in
    /// KnownAllocated and should use a symbolic/sentinel length.
    fn is_maybe_uninit_origin(&self, origin_key: &str) -> bool {
        self.forward.facts.iter().any(|fact| {
            if let StateFact::KnownAllocated { object, ty_name, elements, .. } = fact {
                *elements == 0
                    && (place_label(object) == origin_key)
                    && ty_name.contains("MaybeUninit")
            } else {
                false
            }
        })
    }

    fn len_place_for_origin(&self, origin_key: &str) -> Option<PlaceKey> {
        for fact in &self.forward.facts {
            let StateFact::Call(call) = fact else {
                continue;
            };
            let Some(source_arg) = call.effects.iter().find_map(|effect| {
                let crate::verify::call_summary::CallEffect::ReturnLengthOfArg { arg } = effect
                else {
                    return None;
                };
                Some(*arg)
            }) else {
                continue;
            };
            let Some(source) = call.args.get(source_arg) else {
                continue;
            };
            let Some(key) = self.origin_key_for_value(source, &mut HashSet::new()) else {
                continue;
            };
            if key == origin_key {
                return Some(PlaceKey {
                    base: PlaceBaseKey::Local(call.destination.as_usize()),
                    fields: Vec::new(),
                });
            }
        }
        None
    }

    fn allocated_len_for_origin(&self, origin_key: &str) -> Option<u64> {
        self.forward.facts.iter().find_map(|fact| match fact {
            StateFact::KnownAllocated {
                place,
                object,
                elements,
                ty_name,
                ..
            } if place_label(object) == origin_key || place_label(place) == origin_key => {
                // MaybeUninit<[T; N]> with const-generic N has dynamic
                // length — return None so guarded_len_for_index can
                // try the loop guard instead of using elements=1.
                if *elements == 0 || (ty_name.contains("MaybeUninit") && ty_name.contains('[')) {
                    return None;
                }
                Some(*elements)
            }
            _ => None,
        })
    }

    fn origin_is_initialized_for_ty(&self, origin_key: &str, required_ty_name: &str) -> bool {
        if self.forward.facts.iter().any(|fact| {
            let StateFact::KnownAllocated {
                place,
                object,
                ty_name,
                ..
            } = fact
            else {
                return false;
            };
            if place_label(object) != origin_key && place_label(place) != origin_key {
                return false;
            }
            if ty_name.contains("MaybeUninit") {
                return false;
            }
            init_type_compatible(ty_name, required_ty_name)
                || self
                    .initialized_element_ty_for_place(object)
                    .is_some_and(|elem| init_type_compatible(&elem, required_ty_name))
        }) {
            return true;
        }
        if let Some(local_index) = origin_key
            .strip_prefix('_')
            .and_then(|s| s.parse::<usize>().ok())
        {
            let local = rustc_middle::mir::Local::from_usize(local_index);
            let ty = self.tcx.optimized_mir(self.checkpoint.caller).local_decls[local].ty;
            if let Some(elem_ty_name) = initialized_element_ty_name(ty) {
                if init_type_compatible(&elem_ty_name, required_ty_name) {
                    return true;
                }
            }
        }
        false
    }

    fn initialized_element_ty_for_place(&self, place: &PlaceKey) -> Option<String> {
        let ty = self.place_ty(place)?;
        initialized_element_ty_name(ty)
    }
}

/// Recovered index and length terms for a first-cut in-bounds proof.
pub(crate) struct PointerBounds<'ctx> {
    index: Int<'ctx>,
    len: Int<'ctx>,
    index_term: SmtTerm,
    len_term: SmtTerm,
    origin_key: String,
}

/// Convert an operand into a place key when it names a MIR place.
fn operand_place(operand: &Operand<'_>) -> Option<PlaceKey> {
    match operand {
        Operand::Copy(place) | Operand::Move(place) => Some(PlaceKey::from_mir_place(place)),
        Operand::Constant(_) => None,
        #[cfg(rapx_rustc_ge_196)]
        Operand::RuntimeChecks(_) => None,
    }
}

fn contract_expr_from_place_key<'tcx>(place: PlaceKey) -> ContractExpr<'tcx> {
    let base = match place.base {
        PlaceBaseKey::Return => PlaceBase::Return,
        PlaceBaseKey::Local(local) => PlaceBase::Local(local),
        PlaceBaseKey::Arg(arg) => PlaceBase::Arg(arg),
    };
    let projections = place
        .fields
        .into_iter()
        .map(|index| ContractProjection::Field { index, ty: None })
        .collect();
    ContractExpr::Place(ContractPlace { base, projections })
}

/// Return the abstract value assigned to a place when it is tracked by local.
fn value_for_place<'a, 'tcx>(
    forward: &'a ForwardVisitResult<'tcx>,
    place: &PlaceKey,
) -> Option<&'a AbstractValue<'tcx>> {
    let local = place.local()?;
    forward.values.get(&local)
}

/// Return the pointee type of raw pointers and references.
fn pointee_ty<'tcx>(ty: Ty<'tcx>) -> Option<Ty<'tcx>> {
    match ty.kind() {
        TyKind::RawPtr(ty, _) | TyKind::Ref(_, ty, _) => Some(*ty),
        _ => None,
    }
}

/// Return a string label for the pointee type, for type-level alias checks.
fn pointee_ty_str<'tcx>(ty: Ty<'tcx>) -> Option<String> {
    match ty.kind() {
        TyKind::RawPtr(inner, _) | TyKind::Ref(_, inner, _) => Some(format!("{inner:?}")),
        _ => None,
    }
}

fn is_len_carrying_ty(ty: Ty<'_>) -> bool {
    match ty.kind() {
        TyKind::Ref(_, inner, _) => is_len_carrying_ty(*inner),
        TyKind::Slice(_) | TyKind::Str => true,
        _ => false,
    }
}

fn initialized_element_ty_name<'tcx>(ty: Ty<'tcx>) -> Option<String> {
    let ty_name = format!("{ty:?}");
    if ty_name.contains("MaybeUninit") {
        return None;
    }
    match ty.kind() {
        TyKind::Ref(_, inner, _) | TyKind::RawPtr(inner, _) => {
            initialized_element_ty_name(*inner).or_else(|| Some(format!("{inner:?}")))
        }
        TyKind::Array(elem, _) | TyKind::Slice(elem) => Some(format!("{elem:?}")),
        TyKind::Adt(def, args) => {
            let def_name = format!("{:?}", def.did());
            let is_vec = def_name.contains("Vec")
                || ty_name.starts_with("std::vec::Vec<")
                || ty_name.starts_with("alloc::vec::Vec<")
                || ty_name.starts_with("Vec<");
            if is_vec {
                return args.iter().find_map(|arg| match arg.kind() {
                    GenericArgKind::Type(ty) => Some(format!("{ty:?}")),
                    _ => None,
                });
            }
            Some(ty_name)
        }
        _ => Some(ty_name),
    }
}

fn is_unsigned_integral_ty(ty: Ty<'_>) -> bool {
    matches!(ty.kind(), TyKind::Uint(_))
}

/// Return true when a call summary is a typed pointer addition.
fn is_pointer_add_call(func: &str) -> bool {
    PrimitiveCall::classify(func).is_some_and(PrimitiveCall::is_pointer_add_like)
}

/// Return true when a call summary is a typed pointer subtraction.
fn is_pointer_sub_call(func: &str) -> bool {
    PrimitiveCall::classify(func).is_some_and(PrimitiveCall::is_pointer_sub_like)
}

/// Return true when a call summary extracts a pointer from a slice-like object.
pub(crate) fn is_as_ptr_call(func: &str) -> bool {
    PrimitiveCall::classify(func).is_some_and(PrimitiveCall::is_as_ptr_like)
}

/// Return true when a call summary carries pointer-add semantics.
fn call_has_pointer_add_effect(call: &CallSummary<'_>) -> bool {
    call.effects.iter().any(|effect| {
        matches!(
            effect,
            crate::verify::call_summary::CallEffect::ReturnPointerAdd { .. }
        )
    })
}

fn call_has_pointer_sub_effect(call: &CallSummary<'_>) -> bool {
    call.effects.iter().any(|effect| {
        matches!(
            effect,
            crate::verify::call_summary::CallEffect::ReturnPointerSub { .. }
        )
    })
}

fn abstract_value_from_rvalue<'tcx>(rvalue: &Rvalue<'tcx>) -> Option<AbstractValue<'tcx>> {
    Some(match rvalue {
        Rvalue::Use(operand, ..) => abstract_value_from_operand(operand),
        Rvalue::Repeat(operand, _) => {
            AbstractValue::Repeat(Box::new(abstract_value_from_operand(operand)))
        }
        Rvalue::Ref(_, _, place) => AbstractValue::Ref(PlaceKey::from_mir_place(place)),
        Rvalue::RawPtr(_, place) => AbstractValue::RawPtr(PlaceKey::from_mir_place(place)),
        Rvalue::Cast(_, operand, ty) => {
            AbstractValue::Cast(Box::new(abstract_value_from_operand(operand)), *ty)
        }
        Rvalue::BinaryOp(op, pair) => {
            let (lhs, rhs) = &**pair;
            AbstractValue::Binary(
                *op,
                Box::new(abstract_value_from_operand(lhs)),
                Box::new(abstract_value_from_operand(rhs)),
            )
        }
        Rvalue::UnaryOp(op, operand) => {
            AbstractValue::Unary(*op, Box::new(abstract_value_from_operand(operand)))
        }
        Rvalue::CopyForDeref(place) => AbstractValue::Place(PlaceKey::from_mir_place(place)),
        Rvalue::ThreadLocalRef(def_id) => AbstractValue::ThreadLocal(format!("{def_id:?}")),
        #[cfg(all(rapx_rustc_ge_193, not(rapx_rustc_ge_196)))]
        Rvalue::NullaryOp(op) => AbstractValue::Nullary(format!("{op:?}")),
        #[cfg(all(not(rapx_rustc_ge_193), not(rapx_rustc_ge_196)))]
        Rvalue::NullaryOp(op, _) => AbstractValue::Nullary(format!("{op:?}")),
        Rvalue::Discriminant(place) => AbstractValue::Discriminant(PlaceKey::from_mir_place(place)),
        Rvalue::Aggregate(kind, operands) => {
            AbstractValue::Aggregate(format!("{kind:?}"), operands.len())
        }
        #[cfg(not(rapx_rustc_ge_196))]
        Rvalue::ShallowInitBox(operand, ty) => {
            AbstractValue::ShallowInitBox(Box::new(abstract_value_from_operand(operand)), *ty)
        }
        _ => return None,
    })
}

fn infer_element_ty<'tcx>(ty: Ty<'tcx>) -> Option<Ty<'tcx>> {
    match ty.kind() {
        TyKind::Slice(elem_ty) => Some(*elem_ty),
        TyKind::Array(elem_ty, _) => Some(*elem_ty),
        TyKind::Ref(_, inner, _) => infer_element_ty(*inner),
        TyKind::RawPtr(inner_ty, _) => infer_element_ty(*inner_ty),
        _ => Some(ty),
    }
}

fn abstract_value_from_operand<'tcx>(operand: &Operand<'tcx>) -> AbstractValue<'tcx> {
    match operand {
        Operand::Copy(place) | Operand::Move(place) => {
            AbstractValue::Place(PlaceKey::from_mir_place(place))
        }
        Operand::Constant(constant) => {
            let text = format!("{:?}", constant.const_);
            const_int_from_debug(&text)
                .map(AbstractValue::ConstInt)
                .unwrap_or(AbstractValue::Const(text))
        }
        #[cfg(rapx_rustc_ge_196)]
        Operand::RuntimeChecks(_) => AbstractValue::Unknown("runtime-checks".to_string()),
    }
}

/// Stable SMT variable name for a place key.
fn place_name(place: &PlaceKey) -> String {
    let base = match place.base {
        PlaceBaseKey::Return => "return".to_string(),
        PlaceBaseKey::Local(local) => format!("local_{local}"),
        PlaceBaseKey::Arg(arg) => format!("arg_{arg}"),
    };
    if place.fields.is_empty() {
        base
    } else {
        format!(
            "{}_{}",
            base,
            place
                .fields
                .iter()
                .map(|field| field.to_string())
                .collect::<Vec<_>>()
                .join("_")
        )
    }
}

/// Compact human-readable label for a MIR place key.
pub(crate) fn place_label(place: &PlaceKey) -> String {
    let base = match place.base {
        PlaceBaseKey::Return => "return".to_string(),
        PlaceBaseKey::Local(local) => format!("_{local}"),
        PlaceBaseKey::Arg(arg) => format!("arg{arg}"),
    };
    if place.fields.is_empty() {
        base
    } else {
        format!(
            "{}.{}",
            base,
            place
                .fields
                .iter()
                .map(|field| field.to_string())
                .collect::<Vec<_>>()
                .join(".")
        )
    }
}

/// Compact human-readable label for an abstract value.
pub(crate) fn value_label(value: &AbstractValue<'_>) -> String {
    match value {
        AbstractValue::Unknown(text) => format!("unknown({text})"),
        AbstractValue::Place(place) => place_label(place),
        AbstractValue::Ref(place) => format!("&{}", place_label(place)),
        AbstractValue::RawPtr(place) => format!("raw({})", place_label(place)),
        AbstractValue::ThreadLocal(name) => format!("thread_local({name})"),
        AbstractValue::ConstInt(value) => value.to_string(),
        AbstractValue::ConstParam(name) => format!("const_{name}"),
        AbstractValue::Const(text) => const_int_from_debug(text)
            .map(|value| value.to_string())
            .unwrap_or_else(|| text.trim().to_string()),
        AbstractValue::Repeat(inner) => format!("repeat({})", value_label(inner)),
        AbstractValue::Cast(inner, ty) => format!("cast({}, {ty:?})", value_label(inner)),
        AbstractValue::Unary(op, inner) => format!("{op:?}({})", value_label(inner)),
        AbstractValue::Binary(op, lhs, rhs) => {
            format!(
                "({} {} {})",
                value_label(lhs),
                binop_label(*op),
                value_label(rhs)
            )
        }
        AbstractValue::Nullary(name) => name.clone(),
        AbstractValue::Discriminant(place) => format!("discriminant({})", place_label(place)),
        AbstractValue::Aggregate(name, len) => format!("{name}[{len}]"),
        #[cfg(not(rapx_rustc_ge_196))]
        AbstractValue::ShallowInitBox(inner, ty) => {
            format!("box({}, {ty:?})", value_label(inner))
        }
        AbstractValue::CallResult(call) if is_pointer_add_call(&call.func) => {
            let base = call
                .args
                .first()
                .map(value_label)
                .unwrap_or_else(|| "?".to_string());
            let index = call
                .args
                .get(1)
                .map(value_label)
                .unwrap_or_else(|| "?".to_string());
            format!("{base}.add({index})")
        }
        AbstractValue::CallResult(call) => {
            let destination = PlaceKey {
                base: PlaceBaseKey::Local(call.destination.as_usize()),
                fields: Vec::new(),
            };
            format!(
                "{} = call({})",
                place_label(&destination),
                short_func_name(&call.func)
            )
        }
    }
}

fn smt_term_for_value(value: &AbstractValue<'_>) -> Option<SmtTerm> {
    match value {
        AbstractValue::ConstInt(value) => u64::try_from(*value).ok().map(SmtTerm::Const),
        AbstractValue::Const(text) => const_int_from_debug(text)
            .and_then(|value| u64::try_from(value).ok())
            .map(SmtTerm::Const)
            .or_else(|| {
                let name = sanitize_smt_name(text);
                if name.is_empty() {
                    None
                } else {
                    Some(SmtTerm::Value(format!("const_{name}")))
                }
            }),
        AbstractValue::Place(place) => Some(SmtTerm::Place(place.clone())),
        AbstractValue::Cast(inner, _) => smt_term_for_value(inner),
        AbstractValue::Binary(op, lhs, rhs) => {
            let lhs = Box::new(smt_term_for_value(lhs)?);
            let rhs = Box::new(smt_term_for_value(rhs)?);
            match op {
                BinOp::Add | BinOp::AddWithOverflow => Some(SmtTerm::Add(lhs, rhs)),
                BinOp::Sub | BinOp::SubWithOverflow => Some(SmtTerm::Sub(lhs, rhs)),
                BinOp::Mul | BinOp::MulWithOverflow => Some(SmtTerm::Mul(lhs, rhs)),
                BinOp::Div => Some(SmtTerm::Div(lhs, rhs)),
                BinOp::Rem => Some(SmtTerm::Rem(lhs, rhs)),
                _ => None,
            }
        }
        _ => None,
    }
}

/// Render a compact binary operator label.
fn binop_label(op: BinOp) -> &'static str {
    match op {
        BinOp::Add => "+",
        BinOp::Sub => "-",
        BinOp::Mul => "*",
        BinOp::Div => "/",
        BinOp::Rem => "%",
        BinOp::Eq => "==",
        BinOp::Ne => "!=",
        BinOp::Lt => "<",
        BinOp::Le => "<=",
        BinOp::Gt => ">",
        BinOp::Ge => ">=",
        _ => "?",
    }
}

/// Return the final path segment of a rustc debug function name.
fn short_func_name(func: &str) -> String {
    func.rsplit("::")
        .next()
        .unwrap_or(func)
        .trim_matches('"')
        .to_string()
}

/// Extract a const generic parameter name, e.g. `Param(N)` → `"N"`.
fn const_param_name_from_debug(text: &str) -> Option<String> {
    let text = text.trim();
    // Format: Param(N)
    if let Some(rest) = text.find("Param(").map(|i| &text[i + 6..]) {
        let end = rest.find(')')?;
        let name = rest[..end].trim().to_string();
        if !name.is_empty() { return Some(name); }
    }
    // Format: Ty(usize, N/#1)  or  Ty(usize, N)
    if let Some(rest) = text.strip_prefix("Ty(") {
        let comma = rest.find(',')?;
        let after_comma = rest[comma + 1..].trim();
        let end = after_comma.find(')').unwrap_or(after_comma.len());
        let name = after_comma[..end].trim();
        // Strip trailing /#N index if present
        if let Some(slash) = name.rfind('/') {
            let name = name[..slash].trim();
            if !name.is_empty() { return Some(name.to_string()); }
        }
        if !name.is_empty() { return Some(name.to_string()); }
    }
    None
}

/// Extract a small integer constant from rustc's debug representation.
fn const_int_from_debug(text: &str) -> Option<u128> {
    let text = text.trim();
    if text == "const true" {
        return Some(1);
    }
    if text == "const false" {
        return Some(0);
    }
    if let Some(rest) = text.strip_prefix("const ") {
        let digits = rest
            .chars()
            .take_while(|ch| ch.is_ascii_digit())
            .collect::<String>();
        if digits.is_empty() {
            return None;
        }
        return digits.parse().ok();
    }

    let scalar = text.strip_prefix("Val(Scalar(0x")?;
    let digits = scalar
        .chars()
        .take_while(|ch| ch.is_ascii_hexdigit())
        .collect::<String>();
    if digits.is_empty() {
        None
    } else {
        u128::from_str_radix(&digits, 16).ok()
    }
}

fn init_type_compatible(init_ty_name: &str, required_ty_name: &str) -> bool {
    if normalize_init_ty_name(init_ty_name) == normalize_init_ty_name(required_ty_name) {
        return true;
    }
    if let Some(array_elem) = array_elem_type(required_ty_name) {
        if init_type_compatible(init_ty_name, &array_elem) {
            return true;
        }
    }
    false
}

fn allocated_type_compatible(allocated_ty_name: &str, required_ty_name: &str) -> bool {
    if normalize_init_ty_name(allocated_ty_name) == normalize_init_ty_name(required_ty_name) {
        return true;
    }
    if let Some(array_elem) = array_elem_type(required_ty_name) {
        if allocated_type_compatible(allocated_ty_name, &array_elem) {
            return true;
        }
    }
    false
}

fn array_elem_type(ty_name: &str) -> Option<String> {
    let name = ty_name.trim();
    if name.starts_with('[') && name.ends_with(']') {
        let inner = &name[1..name.len() - 1];
        if let Some(semi) = inner.rfind("; ") {
            return Some(format!(" {}", &inner[..semi]));
        }
    }
    None
}

fn allocation_object_invalidated<'tcx>(
    forward: &ForwardVisitResult<'tcx>,
    object: &PlaceKey,
) -> bool {
    forward.facts.iter().any(|fact| match fact {
        StateFact::LocalDead(local) => object.local() == Some(*local),
        StateFact::Drop(place) => place.overlaps(object) || object.overlaps(place),
        _ => false,
    })
}

fn normalize_init_ty_name(ty_name: &str) -> String {
    let ty_name = ty_name.trim();
    for prefix in [
        "std::mem::MaybeUninit<",
        "core::mem::MaybeUninit<",
        "MaybeUninit<",
    ] {
        if let Some(inner) = ty_name
            .strip_prefix(prefix)
            .and_then(|s| s.strip_suffix('>'))
        {
            return normalize_init_ty_name(inner);
        }
    }
    if let Some(rest) = ty_name.strip_prefix('[')
        && rest.ends_with(']')
    {
        let inner = &rest[..rest.len() - 1];
        if let Some(semi_pos) = inner.rfind("; ") {
            return normalize_init_ty_name(&inner[..semi_pos]);
        }
        // Slice type [T] — same alignment as T.
        return normalize_init_ty_name(inner);
    }
    let mut result = ty_name.to_string();
    while let Some(slash) = result.rfind('/')
        && slash + 1 < result.len()
        && result[slash + 1..].starts_with('#')
    {
        let trimmed = result[..slash].to_string();
        if let Some(after_hash) = result[slash + 2..].chars().next()
            && after_hash.is_ascii_digit()
        {
            result = trimmed;
            continue;
        }
        break;
    }
    result
}

/// Stable SMT identifier for diagnostic-only symbolic terms.
fn sanitize_smt_name(name: &str) -> String {
    name.chars()
        .map(|ch| {
            if ch.is_ascii_alphanumeric() || ch == '_' {
                ch
            } else {
                '_'
            }
        })
        .collect()
}

fn ptr_metadata_origin<'tcx>(
    value: &AbstractValue<'tcx>,
    model: &SmtModel<'_, '_, 'tcx>,
) -> Option<String> {
    let resolved = model.resolved_value(value, &mut TraceSeen::new())
        .unwrap_or_else(|| value.clone());
    match &resolved {
        AbstractValue::Unary(UnOp::PtrMetadata, inner) => {
            let cursor = model.latest_cursor();
            model.origin_key_for_value_before(inner, cursor, &mut TraceSeen::new())
        }
        AbstractValue::CallResult(call) => {
            if call.effects.iter().any(|e| matches!(e, crate::verify::call_summary::CallEffect::ReturnLengthOfArg { .. }))
            {
                let arg = call.effects.iter().find_map(|e| match e {
                    crate::verify::call_summary::CallEffect::ReturnLengthOfArg { arg } => Some(*arg),
                    _ => None,
                })?;
                let call_cursor = model.call_definition_cursor(call);
                let source = call.args.get(arg)?;
                model.origin_key_for_value_before(source, call_cursor, &mut TraceSeen::new())
            } else {
                None
            }
        }
        _ => None,
    }
}

fn pointee_stride_from_types<'tcx>(
    tcx: TyCtxt<'tcx>,
    src_pointee: Ty<'tcx>,
    dst_pointee: Ty<'tcx>,
) -> Option<SmtTerm> {
    use rustc_middle::ty::ConstKind;
    if src_pointee == dst_pointee {
        return Some(SmtTerm::Const(1));
    }
    if let TyKind::Array(elem, len) = src_pointee.kind()
        && *elem == dst_pointee
    {
        return len.try_to_target_usize(tcx).map(SmtTerm::Const).or_else(|| {
            if let ConstKind::Param(param) = len.kind() {
                Some(SmtTerm::ConstParam(param.name.to_string()))
            } else {
                None
            }
        });
    }
    None
}