rapx 0.7.40

//! Call handling for the symbolic VM.
//!
//! Bridges the existing call summary infrastructure (`call_summary`)
//! with the new symbolic VM state. The `exec_call` method is called
//! from `exec.rs` when a `Call` terminator is encountered.
//!
//! When the callee has MIR available, the VM recursively inlines the
//! callee's body to achieve context-sensitive precision, unless a
//! builtin_models summary provides more precise hand-crafted invariants.
//! Otherwise it falls back to the summary-based approach.

use rustc_hir::def_id::DefId;
use rustc_middle::mir::{BasicBlock, Local, Operand, TerminatorKind};
use rustc_middle::ty::{Ty, TyKind};
use z3::ast::{Ast, Bool, Int};

use crate::compat::{FxHashSet, Spanned};
use crate::helpers::mir_utils::operand_place;
use crate::verify::api_classify;
use crate::verify::call_summary::{self, CallEffect};
use crate::verify::def_use::{PlaceBaseKey, PlaceKey};

use super::state::{AllocId, Provenance, ValueInvariants, VmState, VmValue};

/// Classification of a call site for dispatch prioritization.
const MAX_INLINE_DEPTH: usize = 5;

impl<'ctx, 'tcx> VmState<'ctx, 'tcx> {
    /// Execute a call terminator.
    ///
    /// Dispatch priority: hand-specialized handlers first, then builtin_models
    /// summaries (whose hand-crafted invariants are more precise than inline),
    /// then inline execution of the callee's MIR (including dependency
    /// crates), then interprocedural/effect summaries, and finally an
    /// unconstrained "unsupported call" result.
    pub(crate) fn exec_call(
        &mut self,
        func: &Operand<'tcx>,
        args: &[Spanned<Operand<'tcx>>],
        destination: Local,
        _target: Option<BasicBlock>,
        _cleanup: Option<BasicBlock>,
        caller_def_id: DefId,
    ) {
        let arg_values: Vec<VmValue<'ctx, 'tcx>> = args
            .iter()
            .map(|arg| self.value_of_operand(&arg.node))
            .collect();

        let name = crate::helpers::mir_utils::call_name(self.tcx, func);
        let callee =
            crate::helpers::mir_utils::dep_callee_resolved_def_id(self.tcx, caller_def_id, func);
        let caller_arg_locals: Vec<Option<Local>> = args
            .iter()
            .map(|a| a.node.place().map(|p| p.local))
            .collect();

        // ── select_unpredictable: result ∈ {x, y} ─────────────────────
        if self.try_select_unpredictable(callee, &arg_values, args, destination) {
            return;
        }

        // Slice range indexing: `<[T]>::index(range)` / `::index_mut(range)`
        // returns a sub-slice whose length is the range's extent.
        if self.try_slice_index(callee, &arg_values, args, destination) {
            return;
        }

        // Slice range `get`: `<[T]>::get(range)` returns `Option<&[T]>` whose
        // `Some` payload is the sub-slice.
        if self.try_slice_get(callee, &arg_values, args, destination) {
            return;
        }

        // Iter::len() / Iter::is_empty(): compute from struct fields.
        if self.try_iter_len_is_empty(&name, &arg_values, args, destination) {
            return;
        }

        // Iter::next() / IterMut::next(): advance ptr by 1 and return old.
        if self.try_iter_next(&name, &arg_values, args, destination) {
            return;
        }

        // NonNull::new(ptr): the safe constructor returns Some(ptr) iff ptr is
        // non-null. Its body branches on `ptr.is_null()`, so the branch-free
        // inline path rejects it; model the null-check directly.
        if self.try_nonnull_new(callee, &arg_values, destination) {
            return;
        }

        // post_inc_start / pre_dec_end on Iter/IterMut: apply the ptr/end
        // update as a side effect, then fall through to normal handling.
        // These callees have SwitchInt (ZST branch) exceeding inline limits,
        // so the ptr update would otherwise be lost.
        if let Some(c) = callee {
            if self.tcx.is_mir_available(c) {
                if crate::helpers::mir_utils::is_iter_ptr_adj(self.tcx, c) && arg_values.len() >= 2
                {
                    self.apply_iter_ptr_update(c, &arg_values, &caller_arg_locals);
                    // Continue to normal handling (return value is () , ignored).
                }
            }
        }

        // Try inline for callees with available MIR, unless builtin_models
        // has a precise summary (memory allocation, intrinsics, known ptr
        // arithmetic, etc.). The summary path handles these with
        // hand-crafted invariants that are more precise than BFS inline.
        if let Some(c) = callee {
            if self.tcx.is_mir_available(c) {
                // MIR-derived field load (`(*self).field` getter shape, e.g.
                // `Vec::len`): recognized from the callee's MIR, not by name.
                if let Some(effect) =
                    crate::verify::call_summary::interprocedural::try_field_load_effect(self.tcx, c)
                {
                    self.apply_call_effect(&effect, &arg_values, &caller_arg_locals, destination);
                    self.last_call_name = name.clone();
                    self.last_call_callee = callee;
                    self.materialize_const_bytes_after_call(args, destination);
                    return;
                }
                if let Some(effect) =
                    crate::verify::call_summary::interprocedural::try_ptr_field_return_effect(
                        self.tcx, c,
                    )
                {
                    self.apply_call_effect(&effect, &arg_values, &caller_arg_locals, destination);
                    self.last_call_name = name.clone();
                    self.last_call_callee = callee;
                    self.materialize_const_bytes_after_call(args, destination);
                    return;
                }
                if let Some(effect) =
                    crate::verify::call_summary::interprocedural::try_branch_effect(self.tcx, c)
                {
                    self.apply_call_effect(&effect, &arg_values, &caller_arg_locals, destination);
                    self.last_call_name = name.clone();
                    self.last_call_callee = callee;
                    self.materialize_const_bytes_after_call(args, destination);
                    return;
                }
                if let Some(effect) =
                    crate::verify::call_summary::interprocedural::try_slice_bounded_return_effect(
                        self.tcx, c,
                    )
                {
                    self.apply_call_effect(&effect, &arg_values, &caller_arg_locals, destination);
                    self.last_call_name = name.clone();
                    self.last_call_callee = callee;
                    self.materialize_const_bytes_after_call(args, destination);
                    return;
                }
                if let Some(effect) =
                    crate::verify::call_summary::interprocedural::try_decode_length_return_effect(
                        self.tcx, c,
                    )
                {
                    self.apply_call_effect(&effect, &arg_values, &caller_arg_locals, destination);
                    self.last_call_name = name.clone();
                    self.last_call_callee = callee;
                    self.materialize_const_bytes_after_call(args, destination);
                    return;
                }
                let has_fn_sim = crate::verify::call_summary::builtin_models::lookup_effect(
                    self.tcx,
                    caller_def_id,
                    callee,
                    &name,
                    func,
                    destination,
                )
                .is_some();
                if !has_fn_sim {
                    if self.exec_inline_call(c, &arg_values, &caller_arg_locals, destination) {
                        self.materialize_const_bytes_after_call(args, destination);
                        return;
                    }
                }
            }
        }

        let summary = call_summary::effect_summary(self.tcx, caller_def_id, func, destination);

        self.last_call_name = summary.name.clone();
        self.last_call_callee = callee;

        if !summary.unsupported {
            for effect in &summary.effects {
                self.apply_call_effect(effect, &arg_values, &caller_arg_locals, destination);
            }
        } else {
            self.notes
                .push(format!("unsupported call: {}", summary.name));
            let dest_ty = self.body.local_decls[destination].ty;
            let term = self.fresh_int(&format!("callret_{}", destination.as_usize()));
            if let TyKind::Adt(adt_def, _) = dest_ty.kind() {
                if api_classify::is_std_ordering(adt_def.did()) {
                    let minus_one = Int::from_i64(self.ctx, -1);
                    let one = Int::from_i64(self.ctx, 1);
                    self.path_conditions.push(term.ge(&minus_one));
                    self.path_conditions.push(term.le(&one));
                }
            }
            // bool return (bool, Result::ok/err, etc.) — constrain to {0, 1}
            if dest_ty.is_bool() {
                let zero = Int::from_u64(self.ctx, 0);
                let one = Int::from_u64(self.ctx, 1);
                self.path_conditions.push(term.ge(&zero));
                self.path_conditions.push(term.le(&one));
            }
            self.set_local(
                destination,
                VmValue {
                    term,
                    ty: dest_ty,
                    provenance: None,
                    invariants: ValueInvariants::default(),
                },
            );
        }

        self.materialize_const_bytes_after_call(args, destination);
    }

    /// `select_unpredictable`: result ∈ {x, y}.
    fn try_select_unpredictable(
        &mut self,
        callee: Option<DefId>,
        arg_values: &[VmValue<'ctx, 'tcx>],
        args: &[Spanned<Operand<'tcx>>],
        destination: Local,
    ) -> bool {
        let is_select_unpredictable = callee
            .map(|c| {
                crate::def_id::contains(
                    &[
                        crate::def_id::select_unpredictable(),
                        crate::def_id::hint_select_unpredictable(),
                    ],
                    c,
                )
            })
            .unwrap_or(false);
        if !is_select_unpredictable || arg_values.len() < 3 {
            return false;
        }
        let term = self.fresh_int(&format!("selunpred_{}", destination.as_usize()));
        let dest_ty = self.body.local_decls[destination].ty;
        let eq1 = term._eq(&arg_values[1].term);
        let eq2 = term._eq(&arg_values[2].term);
        self.path_conditions.push(Bool::or(self.ctx, &[&eq1, &eq2]));
        let prov = arg_values[1]
            .provenance
            .clone()
            .or_else(|| arg_values[2].provenance.clone());
        // Track operand chain for inject_div_axioms_for_term so that
        // division axioms reachable through select_unpredictable
        // can be found even across Use / Cast chains.
        let dest_pk = PlaceKey {
            base: PlaceBaseKey::Local(destination.as_usize()),
            fields: vec![],
        };
        let lhs_pk = args.get(1).and_then(|a| operand_place(&a.node));
        let rhs_pk = args.get(2).and_then(|a| operand_place(&a.node));
        self.other_op_sources.insert(dest_pk, (lhs_pk, rhs_pk));
        self.set_local(
            destination,
            VmValue {
                term,
                ty: dest_ty,
                provenance: prov,
                invariants: ValueInvariants::default(),
            },
        );
        true
    }

    /// Slice range indexing `<[T]>::index(range)` / `::index_mut(range)`:
    /// returns a sub-slice whose length is the range's extent. Model it as a
    /// sub-allocation of the array so downstream `into_iter`/`next()` see the
    /// correct element count (empty for `..0`). Single-element indexing
    /// (`index(usize)`) has a non-slice destination and keeps the plain
    /// alias behaviour from the summary table.
    fn try_slice_index(
        &mut self,
        callee: Option<DefId>,
        arg_values: &[VmValue<'ctx, 'tcx>],
        args: &[Spanned<Operand<'tcx>>],
        destination: Local,
    ) -> bool {
        let is_index =
            callee.is_some_and(|c| crate::helpers::mir_utils::is_index_method(self.tcx, c));
        if !is_index || arg_values.len() < 2 {
            return false;
        }
        let dest_ty = self.body.local_decls[destination].ty;
        let is_slice = matches!(dest_ty.kind(), TyKind::Ref(_, inner, _)
            if matches!(inner.kind(), TyKind::Slice(_)));
        if !is_slice {
            return false;
        }
        let Some(prov) = arg_values[0].provenance.clone() else {
            return false;
        };
        let array_term = arg_values[0].term.clone();
        let (elem_ty, elem_size) = match arg_values[0].ty.kind() {
            TyKind::Ref(_, inner, _) => match inner.kind() {
                TyKind::Array(e, _) | TyKind::Slice(e) => (*e, self.size_of_ty(*e).max(1) as u64),
                _ => (arg_values[0].ty, 1),
            },
            _ => (arg_values[0].ty, 1),
        };
        let elem_align = self.align_sym(elem_ty);
        // The range argument is an aggregate whose field layout determines the
        // slice extent (start element offset and element count):
        //   RangeTo { end }        -> start = 0, len = end
        //   RangeFrom { start }    -> start,     len = total - start
        //   Range { start, end }   -> start,     len = end - start
        //   RangeInclusive { .. }  -> start,     len = end - start + 1
        //   otherwise              -> start = 0, len = total
        let range_local = args.get(1).and_then(|a| match &a.node {
            Operand::Copy(p) | Operand::Move(p) => Some(p.local),
            _ => None,
        });
        let range_field = |idx: usize| -> Option<Int<'ctx>> {
            range_local.and_then(|l| self.field_value(l, &[idx]).map(|v| v.term.clone()))
        };
        let zero = Int::from_u64(self.ctx, 0);
        let one = Int::from_u64(self.ctx, 1);
        let total_len = self
            .alloc(prov.alloc_id)
            .size
            .clone()
            .div(&Int::from_u64(self.ctx, elem_size));
        let range_kind = arg_values.get(1).and_then(|v| match v.ty.kind() {
            TyKind::Adt(adt_def, _) => Some(crate::helpers::mir_utils::range_kind(
                self.tcx,
                adt_def.did(),
            )),
            _ => None,
        });
        let (start, len) = match range_kind {
            Some(crate::helpers::mir_utils::RangeKind::RangeTo) => (
                zero.clone(),
                range_field(0).unwrap_or_else(|| total_len.clone()),
            ),
            Some(crate::helpers::mir_utils::RangeKind::RangeFrom) => {
                let s = range_field(0).unwrap_or_else(|| zero.clone());
                (s.clone(), Int::sub(self.ctx, &[&total_len, &s]))
            }
            Some(crate::helpers::mir_utils::RangeKind::Range) => {
                let s = range_field(0).unwrap_or_else(|| zero.clone());
                let e = range_field(1).unwrap_or_else(|| total_len.clone());
                (s.clone(), Int::sub(self.ctx, &[&e, &s]))
            }
            Some(crate::helpers::mir_utils::RangeKind::RangeInclusive) => {
                let s = range_field(0).unwrap_or_else(|| zero.clone());
                let e = range_field(1).unwrap_or_else(|| total_len.clone());
                let l = Int::sub(self.ctx, &[&e, &s]);
                (s.clone(), Int::add(self.ctx, &[&l, &one]))
            }
            _ => (zero.clone(), total_len.clone()),
        };
        let elem_size_term = Int::from_u64(self.ctx, elem_size);
        let start_bytes = if elem_size == 1 {
            start.clone()
        } else {
            Int::mul(self.ctx, &[&start, &elem_size_term])
        };
        let size_bytes = if elem_size == 1 {
            len.clone()
        } else {
            Int::mul(self.ctx, &[&len, &elem_size_term])
        };
        let dest_term = Int::add(self.ctx, &[&array_term, &start_bytes]);
        let (alloc_id, _) = self.allocate(size_bytes, elem_align, Some(elem_ty));
        self.alloc_mut(alloc_id).parent = Some(prov.alloc_id);
        self.set_local(
            destination,
            VmValue {
                term: dest_term,
                ty: dest_ty,
                provenance: Some(Provenance {
                    alloc_id,
                    offset: Int::from_u64(self.ctx, 0),
                    is_field_offset: false,
                }),
                invariants: ValueInvariants {
                    non_null: true,
                    aligned: true,
                    init: true,
                    in_bounds: true,
                    ..Default::default()
                },
            },
        );
        true
    }

    /// Slice range `get` `<[T]>::get(range)` / `::get_mut(range)`: returns
    /// `Option<&[T]>` whose `Some` payload is a sub-slice with the range's
    /// extent.  Mirrors [`try_slice_index`](Self::try_slice_index), but stores
    /// the sub-slice under field 0 (the `Some` payload) so a downstream
    /// `slice.len()` / `memchr(x, subslice)` sees the correct element count and
    /// provenance.
    fn try_slice_get(
        &mut self,
        callee: Option<DefId>,
        arg_values: &[VmValue<'ctx, 'tcx>],
        args: &[Spanned<Operand<'tcx>>],
        destination: Local,
    ) -> bool {
        let Some(c) = callee else {
            return false;
        };
        let Some(assoc) = self.tcx.opt_associated_item(c) else {
            return false;
        };
        if !matches!(assoc.name().as_str(), "get" | "get_mut") || arg_values.len() < 2 {
            return false;
        }
        let dest_ty = self.body.local_decls[destination].ty;
        let TyKind::Adt(adt, substs) = dest_ty.kind() else {
            return false;
        };
        if !self.tcx.is_diagnostic_item(rustc_span::sym::Option, adt.did()) {
            return false;
        }
        let payload_ty = substs.type_at(0);
        let TyKind::Ref(_, slice_ty, _) = payload_ty.kind() else {
            return false;
        };
        if !matches!(slice_ty.kind(), TyKind::Slice(_)) {
            return false;
        }
        let Some(prov) = arg_values[0].provenance.clone() else {
            return false;
        };
        let array_term = arg_values[0].term.clone();
        let (elem_ty, elem_size) = match arg_values[0].ty.kind() {
            TyKind::Ref(_, inner, _) => match inner.kind() {
                TyKind::Array(e, _) | TyKind::Slice(e) => (*e, self.size_of_ty(*e).max(1) as u64),
                _ => (arg_values[0].ty, 1),
            },
            _ => (arg_values[0].ty, 1),
        };
        let elem_align = self.align_sym(elem_ty);
        let range_local = args.get(1).and_then(|a| match &a.node {
            Operand::Copy(p) | Operand::Move(p) => Some(p.local),
            _ => None,
        });
        let range_field = |idx: usize| -> Option<Int<'ctx>> {
            range_local.and_then(|l| self.field_value(l, &[idx]).map(|v| v.term.clone()))
        };
        let zero = Int::from_u64(self.ctx, 0);
        let one = Int::from_u64(self.ctx, 1);
        let total_len = self
            .alloc(prov.alloc_id)
            .size
            .clone()
            .div(&Int::from_u64(self.ctx, elem_size));
        let range_kind = arg_values.get(1).and_then(|v| match v.ty.kind() {
            TyKind::Adt(adt_def, _) => Some(crate::helpers::mir_utils::range_kind(
                self.tcx,
                adt_def.did(),
            )),
            _ => None,
        });
        let (start, len) = match range_kind {
            Some(crate::helpers::mir_utils::RangeKind::RangeTo) => (
                zero.clone(),
                range_field(0).unwrap_or_else(|| total_len.clone()),
            ),
            Some(crate::helpers::mir_utils::RangeKind::RangeFrom) => {
                let s = range_field(0).unwrap_or_else(|| zero.clone());
                (s.clone(), Int::sub(self.ctx, &[&total_len, &s]))
            }
            Some(crate::helpers::mir_utils::RangeKind::Range) => {
                let s = range_field(0).unwrap_or_else(|| zero.clone());
                let e = range_field(1).unwrap_or_else(|| total_len.clone());
                (s.clone(), Int::sub(self.ctx, &[&e, &s]))
            }
            Some(crate::helpers::mir_utils::RangeKind::RangeInclusive) => {
                let s = range_field(0).unwrap_or_else(|| zero.clone());
                let e = range_field(1).unwrap_or_else(|| total_len.clone());
                let l = Int::sub(self.ctx, &[&e, &s]);
                (s.clone(), Int::add(self.ctx, &[&l, &one]))
            }
            _ => (zero.clone(), total_len.clone()),
        };
        let elem_size_term = Int::from_u64(self.ctx, elem_size);
        let start_bytes = if elem_size == 1 {
            start.clone()
        } else {
            Int::mul(self.ctx, &[&start, &elem_size_term])
        };
        let size_bytes = if elem_size == 1 {
            len.clone()
        } else {
            Int::mul(self.ctx, &[&len, &elem_size_term])
        };
        let dest_term = Int::add(self.ctx, &[&array_term, &start_bytes]);
        let (alloc_id, _) = self.allocate(size_bytes, elem_align, Some(elem_ty));
        self.alloc_mut(alloc_id).parent = Some(prov.alloc_id);
        self.set_field_value(
            destination,
            vec![0],
            VmValue {
                term: dest_term,
                ty: payload_ty,
                provenance: Some(Provenance {
                    alloc_id,
                    offset: Int::from_u64(self.ctx, 0),
                    is_field_offset: false,
                }),
                invariants: ValueInvariants {
                    non_null: true,
                    aligned: true,
                    init: true,
                    in_bounds: true,
                    ..Default::default()
                },
            },
        );
        true
    }

    /// `Iter::len()` / `Iter::is_empty()`: compute from struct fields
    /// (ptr + end_or_len share the same allocation with per-field offsets).
    /// The generic builtin_models would return sizeof(Iter)/sizeof(T), which is
    /// wrong for generic T.
    fn try_iter_len_is_empty(
        &mut self,
        name: &str,
        arg_values: &[VmValue<'ctx, 'tcx>],
        args: &[Spanned<Operand<'tcx>>],
        destination: Local,
    ) -> bool {
        if !((name.contains("::Iter<")
            || name.contains("::IterMut<")
            || name.ends_with("::Iter::len")
            || name.ends_with("::IterMut::len")
            || name.ends_with("::Iter::is_empty")
            || name.ends_with("::IterMut::is_empty"))
            && (name.ends_with("::len") || name.ends_with("::is_empty"))
            && arg_values.len() >= 1)
        {
            return false;
        }
        let receiver_local = args.first().and_then(|a| a.node.place()).map(|p| p.local);
        let Some(local) = receiver_local else {
            return false;
        };
        // len() = (end_or_len - ptr) / sizeof(T)   (non-ZST)
        // is_empty() = ptr == end_or_len           (non-ZST)
        let (Some(ptr), Some(end)) = (self.field_value(local, &[0]), self.field_value(local, &[1]))
        else {
            return false;
        };
        let (Some(pp), Some(ep)) = (&ptr.provenance, &end.provenance) else {
            return false;
        };
        if pp.alloc_id != ep.alloc_id {
            return false;
        }
        let dest_ty = self.body.local_decls[destination].ty;
        if name.ends_with("::len") {
            let diff = Int::sub(self.ctx, &[&ep.offset, &pp.offset]);
            let sz = self.iter_elem_size(ptr);
            let val = VmValue::new(diff.div(&sz), dest_ty);
            self.set_local(destination, val);
        } else {
            // is_empty(): ptr == end_or_len  (non-ZST branch)
            let eq = pp.offset._eq(&ep.offset);
            let zero = Int::from_u64(self.ctx, 0);
            let one = Int::from_u64(self.ctx, 1);
            let val = VmValue {
                term: eq.ite(&one, &zero),
                ty: dest_ty,
                provenance: None,
                invariants: ValueInvariants::default(),
            };
            self.set_local(destination, val);
        }
        true
    }

    /// `NonNull::<T>::new(ptr) -> Option<NonNull<T>>`: the safe constructor
    /// returns `Some` iff `ptr` is non-null. Its body branches on
    /// `ptr.is_null()`, so `exec_inline_call` (branch-free only) cannot inline
    /// it. Model the null-check directly from provenance, mirroring
    /// `check_non_null`: internal provenance or a set `non_null`/`in_bounds`
    /// invariant means the pointer is definitely non-null (`Some(ptr)`), and
    /// otherwise the `Option` is left symbolic (it may be `None`).
    fn try_nonnull_new(
        &mut self,
        callee: Option<DefId>,
        arg_values: &[VmValue<'ctx, 'tcx>],
        destination: Local,
    ) -> bool {
        if !api_classify::is_nonnull_checked_new(callee) {
            return false;
        }
        let Some(ptr) = arg_values.first() else {
            return false;
        };
        let dest_ty = self.body.local_decls[destination].ty;
        let definitely_non_null = ptr.invariants.non_null
            || ptr.invariants.in_bounds
            || ptr
                .provenance
                .as_ref()
                .is_some_and(|p| !self.alloc(p.alloc_id).is_external);
        if definitely_non_null {
            // Some(NonNull(ptr)): the Option data payload is the non-null pointer.
            let mut val = ptr.clone();
            val.ty = dest_ty;
            val.invariants.non_null = true;
            val.invariants.aligned = true;
            let zero = Int::from_u64(self.ctx, 0);
            self.path_conditions.push(ptr.term._eq(&zero).not());
            self.set_local(destination, val);
        } else {
            // ptr may be null, so the Option may be None — keep it symbolic.
            let term = self.fresh_int(&format!("nn_new_{}", destination.as_usize()));
            self.set_local(
                destination,
                VmValue {
                    term,
                    ty: dest_ty,
                    provenance: None,
                    invariants: ValueInvariants::default(),
                },
            );
        }
        true
    }

    /// `Iter::next()` / `IterMut::next()`: advance ptr by 1 and return old.
    /// The MIR calls the `Iterator::next` trait method, so also match the
    /// trait path (`std::iter::Iterator::next`) in addition to the concrete
    /// `Iter`/`IterMut` method names.
    fn try_iter_next(
        &mut self,
        name: &str,
        arg_values: &[VmValue<'ctx, 'tcx>],
        _args: &[Spanned<Operand<'tcx>>],
        destination: Local,
    ) -> bool {
        let is_next = name.ends_with("::next")
            && (name.starts_with("Iter::")
                || name.starts_with("IterMut::")
                || name.contains("::Iter::")
                || name.contains("::IterMut::")
                || name.contains("::Iter<")
                || name.contains("::IterMut<")
                || name.contains("::Iterator::next"));
        if !is_next || arg_values.len() < 1 {
            return false;
        }
        let self_val = &arg_values[0];
        let Some(local) = self.find_iter_self_local(self_val) else {
            return false;
        };
        let (Some(ptr), Some(end)) = (self.field_value(local, &[0]), self.field_value(local, &[1]))
        else {
            return false;
        };
        let (Some(pp), Some(ep)) = (&ptr.provenance, &end.provenance) else {
            return false;
        };
        if pp.alloc_id != ep.alloc_id {
            return false;
        }
        let dest_ty = self.body.local_decls[destination].ty;
        // Compute is_empty from fields/tracked offset (same as is_empty()).
        let sz = self.iter_elem_size(ptr);
        let ep_offset = ep.offset.clone();
        let remaining = if let Some(off) = self.iter_ptr_offset.get(&local) {
            let base_len = ep_offset.div(&sz);
            let zero = Int::from_u64(self.ctx, 0);
            off.gt(&base_len)
                .ite(&zero, &Int::sub(self.ctx, &[&base_len, off]))
        } else {
            let diff = Int::sub(self.ctx, &[&ep_offset, &pp.offset]);
            diff.div(&sz)
        };
        let is_empty = remaining._eq(&Int::from_u64(self.ctx, 0));
        // The returned element is the *current* position: the tracked element
        // index (iter_ptr_offset) scaled by the element stride, or the base
        // ptr offset on the first call.
        let zero = Int::from_u64(self.ctx, 0);
        let cur_off = match self.iter_ptr_offset.get(&local) {
            Some(prev) => Int::mul(self.ctx, &[prev, &sz]),
            None => pp.offset.clone(),
        };
        let old_ptr_val = VmValue {
            term: cur_off.clone(),
            ty: ptr.ty,
            provenance: Some(Provenance {
                alloc_id: pp.alloc_id,
                offset: cur_off,
                is_field_offset: false,
            }),
            invariants: ValueInvariants {
                non_null: true,
                init: true,
                ..Default::default()
            },
        };
        // Advance ptr when not empty
        let one_term = Int::from_u64(self.ctx, 1);
        let new_offset = match self.iter_ptr_offset.get(&local) {
            Some(prev) => Int::add(self.ctx, &[prev, &one_term]),
            None => one_term.clone(),
        };
        // Assert !is_empty as path condition (remaining > 0)
        self.path_conditions.push(remaining.gt(&zero));
        // Push: base_len >= tracked_offset
        let base_len = ep_offset.div(&sz);
        self.path_conditions.push(new_offset.le(&base_len));
        self.iter_ptr_offset.insert(local, new_offset);
        // Return None or old ptr
        let result_val = VmValue {
            term: is_empty.ite(&zero, &old_ptr_val.term),
            ty: dest_ty,
            provenance: if is_empty.as_bool().unwrap_or(false) {
                None
            } else {
                old_ptr_val.provenance.clone()
            },
            invariants: ValueInvariants::default(),
        };
        self.set_local(destination, result_val);
        // Tie the Option's discriminant to the emptiness condition so
        // `switchInt(discriminant(_n))` only takes the `Some` branch when the
        // iterator was non-empty (and the `None` branch when empty).
        let discr_term = is_empty.ite(&zero, &one_term);
        self.discriminant_terms.insert(destination, discr_term);
        true
    }

    fn materialize_const_bytes_after_call(
        &mut self,
        args: &[Spanned<Operand<'tcx>>],
        destination: Local,
    ) {
        if let Some(mut dv) = self.locals.get(&destination).cloned() {
            let dest_ty = dv.ty;
            let pointee_is_byte_like = match dest_ty.kind() {
                rustc_middle::ty::TyKind::RawPtr(inner, _)
                | rustc_middle::ty::TyKind::Ref(_, inner, _) => match inner.kind() {
                    rustc_middle::ty::TyKind::Uint(rustc_middle::ty::UintTy::U8)
                    | rustc_middle::ty::TyKind::Int(rustc_middle::ty::IntTy::I8) => true,
                    rustc_middle::ty::TyKind::Array(elem_ty, _)
                    | rustc_middle::ty::TyKind::Slice(elem_ty) => {
                        matches!(
                            elem_ty.kind(),
                            rustc_middle::ty::TyKind::Uint(rustc_middle::ty::UintTy::U8)
                        )
                    }
                    _ => false,
                },
                _ => false,
            };
            if pointee_is_byte_like {
                for arg in args {
                    self.try_materialize_const_bytes(&mut dv, &arg.node);
                    if dv.provenance.is_some() {
                        self.set_local(destination, dv);
                        break;
                    }
                }
            }
        }
    }

    /// Recursively execute a callee's MIR body inline.
    ///
    /// Binds the caller's argument values to the callee's parameters,
    /// executes the callee's MIR, and writes the return value to
    /// the caller's destination local. Returns `false` if inline
    /// is not possible (e.g., recursion limit reached, callee has
    /// branches, or the callee is too large).
    fn exec_inline_call(
        &mut self,
        callee_def_id: DefId,
        arg_values: &[VmValue<'ctx, 'tcx>],
        caller_arg_locals: &[Option<Local>],
        dest: Local,
    ) -> bool {
        if self.inline_depth >= MAX_INLINE_DEPTH {
            return false;
        }
        self.inline_depth += 1;

        // Only inline small, branch-free functions. `inline_execute_body`
        // follows every `SwitchInt` target without forking state, so a real
        // branch (e.g. a `match` that returns different pointers per arm)
        // would have its arms merged and lose precision — which silently marks
        // unsound callers sound. Keep rejecting `SwitchInt` bodies; branch-free
        // bodies that merely exceed a small block count are still safe to
        // inline, so the cap must cover the Box construction helpers used by
        // constructors (`from_new_internal` is 9 blocks) so the fresh heap
        // allocation's provenance reaches the returned `NonNull`.
        let callee_body = self.tcx.optimized_mir(callee_def_id);
        let n_return = callee_body
            .basic_blocks
            .iter()
            .filter(|bb| {
                matches!(
                    bb.terminator().kind,
                    rustc_middle::mir::TerminatorKind::Return
                )
            })
            .count();
        // Reject a *semantic* branch (a `SwitchInt` reachable on the normal
        // path): `inline_execute_body` merges its arms and loses precision.
        // A `SwitchInt` that only appears in a cleanup block (the drop-flag
        // dispatch) is dead on the normal path and is safe to ignore.
        // Likewise, a `debug_assert!`/`assert!`-style `SwitchInt` whose every
        // non-otherwise target leads to `panic`/`unreachable` is dead on the
        // normal path — inlining it and taking only the `otherwise` edge keeps
        // the field-level provenance of wrapper casts (`cast_to_internal_unchecked`).
        let has_switch = callee_body.basic_blocks.iter_enumerated().any(|(idx, bb)| {
            !bb.is_cleanup
                && matches!(
                    bb.terminator().kind,
                    rustc_middle::mir::TerminatorKind::SwitchInt { .. }
                )
                && !Self::switch_is_debug_assert(self.tcx, &callee_body, idx)
        });
        if arg_values.len() > 4 || callee_body.basic_blocks.len() > 16 || n_return > 1 || has_switch
        {
            self.inline_depth -= 1;
            return false;
        }

        // ── Save caller context ──
        // Resolve each arg's referent local (for `&self`/`&mut self` reborrow
        // temps) *before* the caller's address map is saved away, so that
        // `exec_assign` can resolve `(*self).field = val` writes back to the
        // caller's referent while the callee executes.
        let inline_arg_referents: Vec<Option<Local>> = arg_values
            .iter()
            .map(|v| self.find_local_by_address(&v.term))
            .collect();
        let saved_body = self.body;
        let saved_caller = self.caller_def_id;
        let saved_locals = std::mem::take(&mut self.locals);
        let saved_field_values = std::mem::take(&mut self.field_values);
        let saved_local_addresses = std::mem::take(&mut self.local_addresses);
        let saved_local_alloc_ids = std::mem::take(&mut self.local_alloc_ids);
        let saved_binary_op_sources = std::mem::take(&mut self.binary_op_sources);
        let saved_other_op_sources = std::mem::take(&mut self.other_op_sources);
        let saved_iter_ptr_offset = std::mem::take(&mut self.iter_ptr_offset);
        let saved_discriminant_terms = std::mem::take(&mut self.discriminant_terms);
        let saved_inline_arg_referents =
            std::mem::replace(&mut self.inline_arg_referents, inline_arg_referents);
        let saved_deferred_field_writes = std::mem::take(&mut self.deferred_field_writes);

        // ── Switch to callee context ──
        self.body = callee_body;
        self.caller_def_id = callee_def_id;

        // Bind args to callee locals (local_1..local_N are function params)
        for (i, arg_val) in arg_values.iter().enumerate() {
            let callee_local = Local::from_usize(i + 1);
            self.ensure_local_allocation(callee_local);
            self.set_local(callee_local, arg_val.clone());
        }

        // Propagate field_values from caller arg locals into the callee
        // context so that inline body can access struct fields (e.g.
        // Iter::ptr / end_or_len for len/is_empty computations).
        for (i, caller_arg_opt) in caller_arg_locals.iter().enumerate() {
            let callee_param = Local::from_usize(i + 1);
            let Some(caller_arg) = caller_arg_opt else {
                continue;
            };
            let caller_field_keys: Vec<Vec<usize>> = saved_field_values
                .keys()
                .filter(|(l, _)| *l == *caller_arg)
                .map(|(_, f)| f.clone())
                .collect();
            for fields in caller_field_keys {
                if let Some(fv) = saved_field_values
                    .get(&(*caller_arg, fields.clone()))
                    .cloned()
                {
                    self.set_field_value(callee_param, fields, fv);
                }
            }
        }

        // ── BFS execution of callee MIR ──
        self.inline_execute_body();

        // ── Capture return value and its per-field values ──
        let return_val = self.locals.get(&Local::from_usize(0)).cloned();
        crate::rap_debug!(
            "exec_inline_call: callee={:?} return_val={:?}",
            callee_def_id,
            return_val
                .as_ref()
                .map(|v| (v.term.to_string(), v.invariants.non_null))
        );
        let return_fields: Vec<(Vec<usize>, VmValue<'ctx, 'tcx>)> = self
            .field_values
            .iter()
            .filter(|((l, _), _)| *l == Local::from_usize(0))
            .map(|((_, path), val)| (path.clone(), val.clone()))
            .collect();

        // ── Restore caller context ──
        self.body = saved_body;
        self.caller_def_id = saved_caller;
        self.locals = saved_locals;
        self.field_values = saved_field_values;
        self.local_addresses = saved_local_addresses;
        self.local_alloc_ids = saved_local_alloc_ids;
        self.binary_op_sources = saved_binary_op_sources;
        self.other_op_sources = saved_other_op_sources;
        self.iter_ptr_offset = saved_iter_ptr_offset;
        self.discriminant_terms = saved_discriminant_terms;

        // Apply deferred field writes (`(*self).field = val` through a
        // `&mut self` reborrow) collected during the callee's execution, now
        // that the caller's `field_values` is live again.
        for (local, path, value) in std::mem::take(&mut self.deferred_field_writes) {
            self.set_field_value(local, path, value);
        }
        self.inline_arg_referents = saved_inline_arg_referents;
        self.deferred_field_writes = saved_deferred_field_writes;

        // ── Write return value to caller destination ──
        let dest_ty = self.body.local_decls[dest].ty;
        match return_val {
            Some(mut val) => {
                val.ty = dest_ty;
                // Infer invariants: a non-null provenance with offset=0
                // means the return value is valid and initialized.
                if let Some(ref prov) = val.provenance {
                    if prov.offset.as_u64() == Some(0) {
                        val.invariants.non_null = true;
                        val.invariants.init = true;
                        val.invariants.aligned = true;
                        self.alloc_mut(prov.alloc_id).initialized = true;
                    }
                }
                self.set_local(dest, val);
                // Propagate the callee's per-field return values (e.g. a
                // tuple `(NonNull<T>, A)`'s field 0) to the caller's
                // destination so subsequent field projections resolve.
                for (path, fv) in return_fields {
                    self.set_field_value(dest, path, fv);
                }
                // The callee returned a fully-constructed value, so the
                // caller's destination stack slot is initialized.  This matters
                // for ADT returns (struct/enum) whose aggregate value carries
                // no provenance: a later `&raw const (*&field)` + `ptr::read`
                // must be able to discharge `Init` against the field.
                if let Some(dest_alloc_id) = self.local_alloc_ids.get(&dest).copied() {
                    self.alloc_mut(dest_alloc_id).initialized = true;
                }
            }
            None => {
                self.inline_depth -= 1;
                return false;
            }
        }

        self.inline_depth -= 1;
        true
    }

    /// Whether a `SwitchInt`'s non-`otherwise` targets all lead straight to
    /// `panic`/`unreachable` (a `debug_assert!`/`assert!` dispatch).  Such a
    /// switch is dead on the normal path and can be inlined by following only
    /// the `otherwise` edge.
    fn switch_targets_unreachable(
        tcx: rustc_middle::ty::TyCtxt<'tcx>,
        body: &rustc_middle::mir::Body<'tcx>,
        targets: &rustc_middle::mir::SwitchTargets,
    ) -> bool {
        targets.iter().all(|(_, target)| {
            let mut cur = target;
            let mut seen = FxHashSet::default();
            loop {
                if !seen.insert(cur) {
                    return false;
                }
                let bb = &body.basic_blocks[cur];
                let term = bb.terminator();
                match &term.kind {
                    rustc_middle::mir::TerminatorKind::Unreachable => return true,
                    rustc_middle::mir::TerminatorKind::Call { func, .. } => {
                        let Some(callee) = crate::helpers::mir_utils::dep_callee_def_id(func)
                        else {
                            return false;
                        };
                        return crate::helpers::mir_utils::is_diverging_call(tcx, callee);
                    }
                    rustc_middle::mir::TerminatorKind::Goto { target: next } => {
                        cur = *next;
                    }
                    // A bare `return` with no statements is a drop-flag skip
                    // (dead on the normal path); a `return` preceded by real
                    // statements computes a different value, so it is a semantic
                    // branch and must not be ignored.
                    rustc_middle::mir::TerminatorKind::Return => return bb.statements.is_empty(),
                    _ => return false,
                }
            }
        })
    }

    /// Whether a block's `SwitchInt` is a `debug_assert!`-style dispatch (all
    /// non-`otherwise` targets are `panic`/`unreachable`).
    fn switch_is_debug_assert(
        tcx: rustc_middle::ty::TyCtxt<'tcx>,
        body: &rustc_middle::mir::Body<'tcx>,
        bb: BasicBlock,
    ) -> bool {
        let rustc_middle::mir::TerminatorKind::SwitchInt { discr, targets } =
            &body.basic_blocks[bb].terminator().kind
        else {
            return false;
        };
        // A constant discriminant (e.g. `_3 = const true` for a no-drop flag)
        // folds to a single live edge; the other edges are dead and can be
        // ignored when inlining.  This includes a `move _3` whose `_3` is
        // assigned a constant earlier in the body.
        let discr_is_const = match discr {
            rustc_middle::mir::Operand::Constant(_) => true,
            rustc_middle::mir::Operand::Copy(p) | rustc_middle::mir::Operand::Move(p) => {
                body.basic_blocks.iter().any(|bbd| {
                    bbd.statements.iter().any(|stmt| {
                        let rustc_middle::mir::StatementKind::Assign(assign) = &stmt.kind else {
                            return false;
                        };
                        let (dest, rvalue) = &**assign;
                        if dest != p {
                            return false;
                        }
                        match rvalue {
                            #[cfg(rapx_rvalue_use_with_retag)]
                            rustc_middle::mir::Rvalue::Use(
                                rustc_middle::mir::Operand::Constant(_),
                                _,
                            ) => true,
                            #[cfg(not(rapx_rvalue_use_with_retag))]
                            rustc_middle::mir::Rvalue::Use(
                                rustc_middle::mir::Operand::Constant(_),
                            ) => true,
                            _ => Self::rvalue_runtime_checks_value(tcx, rvalue).is_some(),
                        }
                    })
                })
            }
            #[allow(unreachable_patterns)]
            _ => false,
        };
        if discr_is_const {
            return true;
        }
        Self::switch_targets_unreachable(tcx, body, targets)
    }

    /// Resolve a `cfg!`-style runtime-check flag (`UbChecks`,
    /// `ContractChecks`, `OverflowChecks`) to a constant `u64`. We fold to the
    /// *no-check* edge (`0`): the check only panics on a violated precondition,
    /// and its branchy body would otherwise corrupt field/Typed propagation
    /// during inlining. Older rustc lowers these to
    /// `Rvalue::NullaryOp(NullOp::RuntimeChecks)`; newer rustc lowers them to
    /// `Operand::RuntimeChecks`.
    fn rvalue_runtime_checks_value(
        _tcx: rustc_middle::ty::TyCtxt<'tcx>,
        rvalue: &rustc_middle::mir::Rvalue<'tcx>,
    ) -> Option<u64> {
        #[cfg(rapx_rvalue_has_nullary_op)]
        {
            if let rustc_middle::mir::Rvalue::NullaryOp(rustc_middle::mir::NullOp::RuntimeChecks(
                _,
            )) = rvalue
            {
                return Some(0);
            }
        }
        #[cfg(not(rapx_rvalue_has_nullary_op))]
        {
            #[cfg(rapx_rvalue_use_with_retag)]
            if let rustc_middle::mir::Rvalue::Use(rustc_middle::mir::Operand::RuntimeChecks(_), _) =
                rvalue
            {
                return Some(0);
            }
            #[cfg(not(rapx_rvalue_use_with_retag))]
            if let rustc_middle::mir::Rvalue::Use(rustc_middle::mir::Operand::RuntimeChecks(_)) =
                rvalue
            {
                return Some(0);
            }
        }
        None
    }

    /// Resolve a `SwitchInt` discriminant to a constant `u64`, following a
    /// single local-assignment chain (a `cfg!`-style runtime-check flag).
    fn switch_discr_const(
        tcx: rustc_middle::ty::TyCtxt<'tcx>,
        body: &rustc_middle::mir::Body<'tcx>,
        discr: &Operand<'tcx>,
    ) -> Option<u64> {
        if let Some(v) = crate::helpers::mir_utils::operand_const_u64(discr) {
            return Some(v);
        }
        let (Operand::Copy(p) | Operand::Move(p)) = discr else {
            return None;
        };
        for bbd in body.basic_blocks.iter() {
            for stmt in bbd.statements.iter() {
                let rustc_middle::mir::StatementKind::Assign(assign) = &stmt.kind else {
                    continue;
                };
                let (dest, rvalue) = &**assign;
                if dest != p {
                    continue;
                }
                return Self::rvalue_runtime_checks_value(tcx, rvalue);
            }
        }
        None
    }

    /// BFS-execute the callee's MIR body.
    fn inline_execute_body(&mut self) {
        let mut visited = FxHashSet::default();
        let mut queue: Vec<BasicBlock> = Vec::new();
        queue.push(BasicBlock::from_usize(0));

        while let Some(block) = queue.pop() {
            if !visited.insert(block) {
                continue;
            }

            let bb_data = &self.body.basic_blocks[block];

            // Execute statements
            for (si, stmt) in bb_data.statements.iter().enumerate() {
                self.exec_statement(block, si, stmt);
            }

            // Process terminator
            let terminator = bb_data.terminator();

            match &terminator.kind {
                TerminatorKind::Goto { target } => {
                    queue.push(*target);
                }
                TerminatorKind::Return => {
                    // Return value captured in local_0
                }
                TerminatorKind::Assert {
                    cond,
                    expected,
                    target,
                    ..
                } => {
                    let cond_val = self.value_of_operand(cond);
                    if *expected {
                        let zero = Int::from_u64(self.ctx, 0);
                        self.path_conditions.push(cond_val.term._eq(&zero).not());
                    } else {
                        let zero = Int::from_u64(self.ctx, 0);
                        self.path_conditions.push(cond_val.term._eq(&zero));
                    }
                    // Guard inference for inline callee
                    self.infer_guard_non_null(cond, *expected);
                    self.infer_guard_align(cond, *expected);
                    queue.push(*target);
                }
                TerminatorKind::SwitchInt { discr, targets } => {
                    // A constant discriminant folds to a single live edge.
                    if let Some(v) = Self::switch_discr_const(self.tcx, &self.body, discr) {
                        let t = targets
                            .iter()
                            .find(|(val, _)| *val == v as u128)
                            .map(|(_, t)| t)
                            .unwrap_or_else(|| targets.otherwise());
                        queue.push(t);
                        continue;
                    }
                    // A `debug_assert!`/`assert!` switch or a drop-flag dispatch
                    // has its non-otherwise edges dead on the normal path, so
                    // follow only `otherwise`.
                    let trivial = Self::switch_targets_unreachable(self.tcx, &self.body, targets);
                    if trivial {
                        queue.push(targets.otherwise());
                        continue;
                    }
                    // Conservative: add path conditions for all branches,
                    // but since we don't fork state, we follow all targets.
                    // This loses precision for overwritten locals but is sound.
                    for (value, target) in targets.iter() {
                        let discr_val = self.value_of_operand(discr);
                        let val_term = Int::from_u64(self.ctx, value as u64);
                        self.path_conditions.push(discr_val.term._eq(&val_term));
                        queue.push(target);
                    }
                    let otherwise = targets.otherwise();
                    queue.push(otherwise);
                }
                TerminatorKind::Call {
                    func,
                    args,
                    destination,
                    target,
                    ..
                } => {
                    self.exec_call(
                        func,
                        args,
                        destination.local,
                        *target,
                        None,
                        self.caller_def_id,
                    );
                    if let Some(t) = target {
                        queue.push(*t);
                    }
                }
                TerminatorKind::Drop { place, target, .. } => {
                    self.exec_drop(place);
                    queue.push(*target);
                }
                TerminatorKind::Unreachable
                | TerminatorKind::UnwindResume
                | TerminatorKind::UnwindTerminate(_)
                | TerminatorKind::Yield { .. }
                | TerminatorKind::CoroutineDrop
                | TerminatorKind::FalseEdge { .. }
                | TerminatorKind::FalseUnwind { .. }
                | TerminatorKind::InlineAsm { .. }
                | TerminatorKind::TailCall { .. } => {
                    // Dead-end or unsupported — stop traversal at this block.
                }
            }
        }
    }

    /// Clone `arg_val`, retype it to `dest`'s type, mark it as a non-null,
    /// aligned, initialized pointer, and bind it to `dest`.
    fn set_dest_as_heap_ptr(&mut self, arg_val: &VmValue<'ctx, 'tcx>, dest: Local) {
        let mut val = arg_val.clone();
        val.ty = self.body.local_decls[dest].ty;
        val.invariants.non_null = true;
        val.invariants.aligned = true;
        val.invariants.init = true;
        self.set_local(dest, val);
    }

    /// Apply a single call effect to the VM state.
    fn apply_call_effect(
        &mut self,
        effect: &CallEffect,
        args: &[VmValue<'ctx, 'tcx>],
        caller_arg_locals: &[Option<Local>],
        dest: Local,
    ) {
        match effect {
            CallEffect::ReturnAliasArg { arg } => {
                if let Some(arg_val) = args.get(*arg) {
                    self.set_dest_as_heap_ptr(arg_val, dest);
                }
            }
            CallEffect::ReturnDerefArg { arg } => {
                // `mem::replace(dest, src)` returns `*dest`: the pointee value,
                // not the `&mut` reference. Prefer the materialized pointee
                // (`field_values` at the empty path, set by
                // `propagate_field_values_to_ref` for `&mut self.field`).  When
                // the borrow chain was dropped by the slicer (no pointee), model
                // the returned slice as a fresh external allocation so a
                // downstream `Allocated`/`InBound` can still match `[T]` vs `T`.
                let dest_ty = self.body.local_decls[dest].ty;
                let mut val = args.get(*arg).cloned().unwrap_or_else(|| VmValue {
                    term: self.fresh_int("replaced"),
                    ty: dest_ty,
                    provenance: None,
                    invariants: ValueInvariants::default(),
                });
                let arg_local = caller_arg_locals.get(*arg).copied().flatten();
                let pointee = arg_local
                    .and_then(|l| self.field_values.get(&(l, Vec::new())).cloned());
                if let Some(p) = pointee {
                    val = p;
                } else if let Some(elem) = crate::helpers::mir_utils::pointee_ty(dest_ty) {
                    let is_slice = matches!(
                        elem.kind(),
                        rustc_middle::ty::TyKind::Slice(_)
                    );
                    if is_slice {
                        let elem_align = self.align_sym(elem);
                        let (alloc_id, base) = self.allocate_external(
                            Int::from_u64(self.ctx, i64::MAX as u64),
                            elem_align,
                            Some(elem),
                        );
                        val = VmValue {
                            term: base,
                            ty: dest_ty,
                            provenance: Some(Provenance {
                                alloc_id,
                                offset: Int::from_u64(self.ctx, 0),
                                is_field_offset: false,
                            }),
                            invariants: ValueInvariants::default(),
                        };
                    }
                }
                val.ty = dest_ty;
                self.set_local(dest, val);
            }
            CallEffect::ReturnTransparentDeref { arg, peel } => {
                if let Some(arg_val) = args.get(*arg) {
                    self.set_dest_as_heap_ptr(arg_val, dest);
                    // Peel `peel` leading field-0 hops off the argument's
                    // pointee field values (ManuallyDrop.value → MaybeDangling.0)
                    // and expose them as the deref result's pointee fields.
                    if let Some(arg_local) = caller_arg_locals.get(*arg).copied().flatten() {
                        let keys: Vec<Vec<usize>> = self
                            .field_values
                            .keys()
                            .filter(|(l, _)| *l == arg_local)
                            .map(|(_, p)| p.clone())
                            .collect();
                        for path in keys {
                            if path.len() > *peel && path[..*peel].iter().all(|&f| f == 0) {
                                if let Some(v) =
                                    self.field_values.get(&(arg_local, path.clone())).cloned()
                                {
                                    self.set_field_value(dest, path[*peel..].to_vec(), v);
                                }
                            }
                        }
                    }
                }
            }
            CallEffect::ReturnTupleFieldLength {
                field: _field,
                from_arg: _from_arg,
            } => {
                if args.len() < 2 {
                    return;
                }
                let self_val = &args[0]; // &[T]
                let mid_val = &args[1]; // usize

                let dest_ty = self.body.local_decls[dest].ty;
                if let TyKind::Tuple(elem_tys) = dest_ty.kind() {
                    // Look up the source allocation from self's provenance.
                    let src_alloc_id = self_val.provenance.as_ref().map(|p| p.alloc_id);
                    let _src_offset = self_val
                        .provenance
                        .as_ref()
                        .map(|p| p.offset.clone())
                        .unwrap_or_else(|| Int::from_u64(self.ctx, 0));

                    let (elem_ty, elem_sz_term, alloc_size) = src_alloc_id
                        .map(|id| self.alloc(id))
                        .map(|a| {
                            let ty = a.element_ty;
                            let sz_term = self.size_sym_read(ty.unwrap_or(self_val.ty));
                            (ty, sz_term, a.size.clone())
                        })
                        .unwrap_or_else(|| {
                            // Provenance lost (e.g. `mem::replace` on a raw field
                            // whose borrow the slicer dropped): fall back to the
                            // slice pointee type so `InBound`/`Allocated` can
                            // still match `[T]` against the element `T`.
                            let pointee = crate::helpers::mir_utils::pointee_ty(self_val.ty);
                            let sz = self.size_sym_read(pointee.unwrap_or(self_val.ty));
                            (pointee, sz, Int::from_u64(self.ctx, 1))
                        });

                    let total_len = self
                        .slice_len_from_value(self_val)
                        .unwrap_or_else(|| alloc_size.div(&elem_sz_term)); // self.len()

                    let zero = Int::from_u64(self.ctx, 0);
                    self.path_conditions.push(mid_val.term.ge(&zero));
                    self.path_conditions.push(mid_val.term.le(&total_len));

                    // mid (field 0 length)
                    let mid = mid_val.term.clone();
                    // self.len() - mid (field 1 length)
                    let rest_len = Int::sub(self.ctx, &[&total_len, &mid]);

                    // mid byte offset for field 1 pointer
                    let mid_bytes = Int::mul(self.ctx, &[&mid, &elem_sz_term]);
                    let ptr1 = Int::add(self.ctx, &[&self_val.term, &mid_bytes]);

                    for f in 0..elem_tys.len() {
                        let field_ty = elem_tys[f];
                        let (field_len, field_ptr) = if f == 0 {
                            (mid.clone(), self_val.term.clone())
                        } else {
                            (rest_len.clone(), ptr1.clone())
                        };
                        let field_size = Int::mul(self.ctx, &[&field_len, &elem_sz_term]);
                        let field_alloc_align = self_val
                            .provenance
                            .as_ref()
                            .map(|p| self.alloc(p.alloc_id).align.clone())
                            .unwrap_or_else(|| Int::from_u64(self.ctx, 1));

                        let (alloc_id, _base) =
                            self.allocate(field_size.clone(), field_alloc_align.clone(), elem_ty);
                        self.alloc_mut(alloc_id).slice_len = Some(field_len.clone());
                        let src_bytes = Int::mul(self.ctx, &[&total_len, &elem_sz_term]);
                        if f == 0 {
                            self.path_conditions.push(field_size._eq(&mid_bytes));
                        } else {
                            let remaining = Int::sub(self.ctx, &[&src_bytes, &mid_bytes]);
                            self.path_conditions.push(field_size._eq(&remaining));
                        }
                        self.alloc_mut(alloc_id).initialized = true;
                        if let Some(ref source_prov) = self_val.provenance {
                            self.alloc_mut(alloc_id).parent = Some(source_prov.alloc_id);
                        }
                        if let Some(ref_dest_alloc_id) = self.local_alloc_ids.get(&dest).copied() {
                            self.alloc_mut(ref_dest_alloc_id).slice_data = Some(alloc_id);
                        }

                        let field_offset = Int::from_u64(self.ctx, 0);

                        let field_prov = Provenance {
                            alloc_id,
                            offset: field_offset,
                            is_field_offset: false,
                        };

                        let field_val = VmValue {
                            term: field_ptr,
                            ty: field_ty,
                            provenance: Some(field_prov),
                            invariants: ValueInvariants {
                                init: true,
                                non_null: true,
                                aligned: true,
                                in_bounds: true,
                                align_n: Some(field_alloc_align),
                                is_field_offset: false,
                            },
                        };
                        self.set_field_value(dest, vec![f], field_val);
                    }
                }
            }
            CallEffect::ReturnIter { receiver_arg } => {
                let Some(self_val) = args.get(*receiver_arg).cloned() else {
                    return;
                };
                let Some(src_prov) = self_val.provenance.clone() else {
                    return;
                };
                // `array[..i]` may be a `from_raw_parts` sub-allocation of the
                // array's backing storage. Follow the sub-allocation chain to the
                // root so the iterator's `ptr`/`end_or_len` fields point at live,
                // init-tracked storage (the array itself), not the transient
                // slice allocation.
                let root_alloc_id = {
                    let mut id = src_prov.alloc_id;
                    while let Some(parent) = self.alloc(id).parent {
                        id = parent;
                    }
                    id
                };
                let slice_len = self.alloc(src_prov.alloc_id).size.clone();

                // The Iter/IterMut struct has `ptr` (field 0) and `end_or_len`
                // (field 1), both raw pointers into the source slice allocation.
                // Derive the pointee type so `next()` can compute the stride.
                let field_ty = match self_val.ty.kind() {
                    TyKind::Ref(_, inner, _) => match inner.kind() {
                        TyKind::Slice(t) => *t,
                        _ => self_val.ty,
                    },
                    _ => self_val.ty,
                };

                let start_off = Int::from_u64(self.ctx, 0);
                let end_term = Int::add(self.ctx, &[&self_val.term, &slice_len]);

                let start_val = VmValue {
                    term: self_val.term.clone(),
                    ty: field_ty,
                    provenance: Some(Provenance {
                        alloc_id: root_alloc_id,
                        offset: start_off,
                        is_field_offset: false,
                    }),
                    invariants: ValueInvariants {
                        init: true,
                        non_null: true,
                        ..Default::default()
                    },
                };
                let end_val = VmValue {
                    term: end_term,
                    ty: field_ty,
                    provenance: Some(Provenance {
                        alloc_id: root_alloc_id,
                        offset: slice_len,
                        is_field_offset: false,
                    }),
                    invariants: ValueInvariants {
                        init: true,
                        non_null: true,
                        ..Default::default()
                    },
                };
                self.set_field_value(dest, vec![0], start_val);
                self.set_field_value(dest, vec![1], end_val);
            }
            CallEffect::ReturnRange { bounds_arg } => {
                self.apply_range_effect(*bounds_arg, args, caller_arg_locals, dest);
            }
            CallEffect::ReturnAlignTo { receiver_arg } => {
                let Some(self_val) = args.get(*receiver_arg).cloned() else {
                    return;
                };
                let dest_ty = self.body.local_decls[dest].ty;
                let TyKind::Tuple(elem_tys) = dest_ty.kind() else {
                    return;
                };
                if elem_tys.len() < 3 {
                    return;
                }

                // Body element type U is the pointee of field 1 (`&[U]`).
                let body_elem_ty = match elem_tys[1].kind() {
                    TyKind::Ref(_, inner, _) => match inner.kind() {
                        TyKind::Slice(u) => *u,
                        _ => return,
                    },
                    _ => return,
                };
                let size_u = self.size_of_ty(body_elem_ty).max(1) as u64;
                let align_u = self.align_sym(body_elem_ty);

                let Some(src_prov) = self_val.provenance.clone() else {
                    return;
                };
                let alloc = self.alloc(src_prov.alloc_id);
                let (elem_ty, elem_sz, len_bytes) = {
                    let ty = alloc.element_ty;
                    let sz = self.size_of_ty(ty.unwrap_or(self_val.ty)).max(1) as u64;
                    (ty, sz, alloc.size.clone())
                };

                let elem_sz_term = Int::from_u64(self.ctx, elem_sz);
                let size_u_term = Int::from_u64(self.ctx, size_u);

                // Fresh aligned offset: (ptr + offset) % align_u == 0 and
                // 0 <= offset < align_u.
                let offset = self.fresh_int(&format!("align_to_offset_{}", dest.as_usize()));
                let zero = Int::from_u64(self.ctx, 0);
                let ptr_plus_offset = Int::add(self.ctx, &[&self_val.term, &offset]);
                self.path_conditions
                    .push(ptr_plus_offset.rem(&align_u)._eq(&zero));
                self.path_conditions.push(offset.ge(&zero));
                self.path_conditions.push(offset.lt(&align_u));

                // body = len_bytes - offset bytes split into size_u chunks; the
                // remainder is the suffix. Record the Euclidean identity so that
                // `len - offset - suffix = body_len * size_u` (a multiple of
                // align_u) is derivable downstream.
                let body_bytes = Int::sub(self.ctx, &[&len_bytes, &offset]);
                let body_len = body_bytes.div(&size_u_term);
                let suffix_bytes = body_bytes.rem(&size_u_term);
                let mul_term = Int::mul(self.ctx, &[&body_len, &size_u_term]);
                let sum_term = Int::add(self.ctx, &[&mul_term, &suffix_bytes]);
                self.path_conditions.push(body_bytes._eq(&sum_term));
                self.path_conditions.push(suffix_bytes.ge(&zero));
                self.path_conditions.push(suffix_bytes.lt(&size_u_term));

                // Field lengths in elements.
                let prefix_len = offset.div(&elem_sz_term);
                let suffix_len = suffix_bytes.div(&elem_sz_term);

                let body_byte_len = Int::mul(self.ctx, &[&body_len, &size_u_term]);
                let suffix_ptr = Int::add(self.ctx, &[&ptr_plus_offset, &body_byte_len]);

                let base_align = self.alloc(src_prov.alloc_id).align.clone();

                let fields: Vec<(Int<'ctx>, Int<'ctx>, Ty<'tcx>, u64, Int<'ctx>)> = vec![
                    (
                        prefix_len,
                        self_val.term.clone(),
                        elem_tys[0],
                        elem_sz,
                        base_align.clone(),
                    ),
                    (body_len, ptr_plus_offset, elem_tys[1], size_u, align_u),
                    (suffix_len, suffix_ptr, elem_tys[2], elem_sz, base_align),
                ];

                for (f, (f_len, f_ptr, f_ty, f_elem_sz, f_align)) in fields.into_iter().enumerate()
                {
                    let f_size = Int::mul(self.ctx, &[&f_len, &Int::from_u64(self.ctx, f_elem_sz)]);
                    let f_elem_ty = if f == 1 { Some(body_elem_ty) } else { elem_ty };
                    let (alloc_id, _) = self.allocate(f_size.clone(), f_align.clone(), f_elem_ty);
                    self.alloc_mut(alloc_id).slice_len = Some(f_len.clone());
                    self.alloc_mut(alloc_id).initialized = true;
                    self.alloc_mut(alloc_id).parent = Some(src_prov.alloc_id);
                    if let Some(ref_dest_alloc_id) = self.local_alloc_ids.get(&dest).copied() {
                        self.alloc_mut(ref_dest_alloc_id).slice_data = Some(alloc_id);
                    }
                    let field_val = VmValue {
                        term: f_ptr,
                        ty: f_ty,
                        provenance: Some(Provenance {
                            alloc_id,
                            offset: Int::from_u64(self.ctx, 0),
                            is_field_offset: false,
                        }),
                        invariants: ValueInvariants {
                            init: true,
                            non_null: true,
                            aligned: true,
                            in_bounds: true,
                            align_n: if f_align.simplify().as_u64() != Some(1) {
                                Some(f_align)
                            } else {
                                None
                            },
                            is_field_offset: false,
                        },
                    };
                    self.set_field_value(dest, vec![f], field_val);
                }
            }
            CallEffect::ReturnPointerFromArg { arg } => {
                if let Some(arg_val) = args.get(*arg) {
                    let mut val = arg_val.clone();
                    let dest_ty = self.body.local_decls[dest].ty;
                    val.ty = dest_ty;
                    // The returned pointer aliases `arg`, so it is non-null
                    // exactly when the source is. The source is non-null either
                    // because its value already carries the fact, or by its
                    // *type*: a reference (`&`/`&mut`) is never null, and
                    // `NonNull` is non-null by invariant.
                    let src_non_null = arg_val.invariants.non_null
                        || matches!(arg_val.ty.kind(), rustc_middle::ty::TyKind::Ref(..))
                        || matches!(
                            arg_val.ty.kind(),
                            rustc_middle::ty::TyKind::Adt(adt, _)
                                if api_classify::is_std_nonnull(adt.did())
                        );
                    val.invariants.non_null = src_non_null;
                    val.invariants.aligned = arg_val.invariants.aligned;
                    // Pointer-returning APIs expose the backing allocation;
                    // mark it init-accessible for raw pointer types.
                    if matches!(dest_ty.kind(), rustc_middle::ty::TyKind::RawPtr(..)) {
                        val.invariants.init = true;
                    }
                    // For heap-backed containers (Vec/CString/String): redirect
                    // as_ptr() from the struct allocation to the heap data
                    // allocation. `slice_data` is the type-driven signal — only
                    // such containers set it, so no name matching is needed.
                    if let Some(ref prov) = val.provenance {
                        if let Some(data_alloc) = self.alloc(prov.alloc_id).slice_data {
                            val.term = self.allocation_base(data_alloc).clone();
                            val.provenance = Some(Provenance {
                                alloc_id: data_alloc,
                                offset: Int::from_u64(self.ctx, 0),
                                is_field_offset: false,
                            });
                        }
                    }
                    if src_non_null {
                        let zero = Int::from_u64(self.ctx, 0);
                        self.path_conditions.push(val.term._eq(&zero).not());
                    }
                    self.set_local(dest, val);
                }
            }
            CallEffect::ReturnPointerAdd {
                base_arg,
                offset_arg,
                stride,
            } => {
                let stride = *stride;
                if let (Some(base), Some(offset)) = (args.get(*base_arg), args.get(*offset_arg)) {
                    let stride_term = match stride {
                        Some(s) => Int::from_u64(self.ctx, s),
                        None => {
                            let dest_ty = self.body.local_decls[dest].ty;
                            let pointee =
                                crate::helpers::mir_utils::pointee_ty(dest_ty).unwrap_or(dest_ty);
                            self.size_sym(pointee)
                        }
                    };
                    let adjusted_offset = if stride == Some(1) {
                        offset.term.clone()
                    } else {
                        Int::mul(self.ctx, &[&offset.term, &stride_term])
                    };
                    let new_term = Int::add(self.ctx, &[&base.term, &adjusted_offset]);
                    let is_field_offset = offset.invariants.is_field_offset
                        && base
                            .provenance
                            .as_ref()
                            .is_some_and(|p| p.offset.as_u64() == Some(0));
                    let adjusted_provenance = base.provenance.as_ref().map(|prov| Provenance {
                        alloc_id: prov.alloc_id,
                        offset: Int::add(self.ctx, &[&prov.offset, &adjusted_offset]),
                        is_field_offset,
                    });
                    let align_n = match stride {
                        Some(s) => self.compute_pointer_add_align(base, offset, s),
                        None => base.invariants.align_n.clone(),
                    };
                    let val = VmValue {
                        term: new_term,
                        ty: self.body.local_decls[dest].ty,
                        provenance: adjusted_provenance,
                        invariants: ValueInvariants {
                            non_null: base.invariants.non_null,
                            aligned: align_n.is_some() && base.invariants.aligned,
                            in_bounds: base.invariants.in_bounds,
                            align_n,
                            init: base.invariants.init,
                            is_field_offset: false,
                        },
                    };
                    self.set_local(dest, val);
                }
            }
            CallEffect::ReturnPointerSub {
                base_arg,
                offset_arg,
                stride,
            } => {
                let stride = *stride;
                if let (Some(base), Some(offset)) = (args.get(*base_arg), args.get(*offset_arg)) {
                    let stride_term = match stride {
                        Some(s) => Int::from_u64(self.ctx, s),
                        None => {
                            let dest_ty = self.body.local_decls[dest].ty;
                            let pointee =
                                crate::helpers::mir_utils::pointee_ty(dest_ty).unwrap_or(dest_ty);
                            self.size_sym(pointee)
                        }
                    };
                    let scaled = if stride == Some(1) {
                        offset.term.clone()
                    } else {
                        Int::mul(self.ctx, &[&offset.term, &stride_term])
                    };
                    let new_term = Int::sub(self.ctx, &[&base.term, &scaled]);
                    let adjusted_provenance = base.provenance.as_ref().map(|prov| Provenance {
                        alloc_id: prov.alloc_id,
                        offset: Int::sub(self.ctx, &[&prov.offset, &scaled]),
                        is_field_offset: false,
                    });
                    let align_n = match stride {
                        Some(s) => self.compute_pointer_add_align(base, offset, s),
                        None => base.invariants.align_n.clone(),
                    };
                    let val = VmValue {
                        term: new_term,
                        ty: self.body.local_decls[dest].ty,
                        provenance: adjusted_provenance,
                        invariants: ValueInvariants {
                            non_null: base.invariants.non_null,
                            aligned: align_n.is_some() && base.invariants.aligned,
                            in_bounds: base.invariants.in_bounds,
                            align_n,
                            init: base.invariants.init,
                            is_field_offset: false,
                        },
                    };
                    self.set_local(dest, val);
                }
            }
            CallEffect::ReturnNonZero => {
                let zero = Int::from_u64(self.ctx, 0);
                if let Some(mut existing) = self.locals.get(&dest).cloned() {
                    existing.invariants.non_null = true;
                    // Record the non-zero fact as a path condition so that a
                    // downstream `ValidNum(result != 0)` obligation (e.g.
                    // `NonZero::new_unchecked` after a bit-preserving operation)
                    // discharges against it.
                    self.path_conditions.push(existing.term._eq(&zero).not());
                    self.set_local(dest, existing);
                } else {
                    let dest_ty = self.body.local_decls[dest].ty;
                    let term = self.fresh_int(&format!("ret_nz_{}", dest.as_usize()));
                    self.path_conditions.push(term._eq(&zero).not());
                    self.set_local(
                        dest,
                        VmValue {
                            term,
                            ty: dest_ty,
                            provenance: None,
                            invariants: ValueInvariants {
                                non_null: true,
                                ..Default::default()
                            },
                        },
                    );
                }
            }
            CallEffect::ReturnTupleFieldNonZero { field } => {
                let dest_ty = self.body.local_decls[dest].ty;
                if let TyKind::Tuple(elem_tys) = dest_ty.kind() {
                    if let Some(field_ty) = elem_tys.get(*field) {
                        let zero = Int::from_u64(self.ctx, 0);
                        let term =
                            self.fresh_int(&format!("ret_tup_nz_{}_{}", dest.as_usize(), field));
                        self.path_conditions.push(term._eq(&zero).not());
                        self.set_field_value(
                            dest,
                            vec![*field],
                            VmValue {
                                term,
                                ty: *field_ty,
                                provenance: None,
                                invariants: ValueInvariants {
                                    non_null: true,
                                    init: true,
                                    ..Default::default()
                                },
                            },
                        );
                    }
                }
            }
            CallEffect::ReturnAligned => {
                if let Some(mut existing) = self.locals.get(&dest).cloned() {
                    existing.invariants.aligned = true;
                    self.set_local(dest, existing);
                } else {
                    let dest_ty = self.body.local_decls[dest].ty;
                    let term = self.fresh_int(&format!("ret_align_{}", dest.as_usize()));
                    self.set_local(
                        dest,
                        VmValue {
                            term,
                            ty: dest_ty,
                            provenance: None,
                            invariants: ValueInvariants {
                                aligned: true,
                                ..Default::default()
                            },
                        },
                    );
                }
            }
            CallEffect::ReturnLengthOfArg { arg } => {
                if let Some(arg_val) = args.get(*arg) {
                    // For Iter / IterMut, compute len from struct fields
                    // (ptr + end_or_len with shared allocation) instead of
                    // the generic sizeof(Iter)/sizeof(T) heuristic.
                    if self.interpreter_iter_len(arg_val, dest) {
                        return;
                    }
                }
                // Field-read `len` (e.g. `Vec::len`) is handled by
                // `ReturnFieldOfArg`; here fall back to `size / elem_size`
                // (slices, `&str`, and legacy Vec values).
                if let Some(arg_val) = args.get(*arg) {
                    if self.set_len_from_alloc(arg_val, dest) {
                        return;
                    }
                }
                let dest_ty = self.body.local_decls[dest].ty;
                let term = self.fresh_int(&format!("len_{}", dest.as_usize()));
                let val = VmValue {
                    term,
                    ty: dest_ty,
                    provenance: None,
                    invariants: ValueInvariants::default(),
                };
                self.set_local(dest, val);
            }
            CallEffect::ReturnFieldOfArg { arg, field } => {
                self.apply_field_of_arg_effect(*arg, *field, None, args, caller_arg_locals, dest);
            }
            CallEffect::ReturnFieldOfArgSub { arg, field, offset } => {
                self.apply_field_of_arg_effect(
                    *arg,
                    *field,
                    Some(*offset),
                    args,
                    caller_arg_locals,
                    dest,
                );
            }
            CallEffect::ReturnConst { value } => {
                let dest_ty = self.body.local_decls[dest].ty;
                let term = Int::from_u64(self.ctx, *value);
                let val = VmValue {
                    term,
                    ty: dest_ty,
                    provenance: None,
                    invariants: ValueInvariants::default(),
                };
                self.set_local(dest, val);
            }
            CallEffect::ReturnAlignOffset { ptr_arg, align_arg } => {
                let dest_ty = self.body.local_decls[dest].ty;
                let offset = self.fresh_int(&format!("align_offset_{}", dest.as_usize()));
                if let (Some(ptr_val), Some(align_val)) = (args.get(*ptr_arg), args.get(*align_arg))
                {
                    // `ptr.align_offset(align)` guarantees `(ptr + offset) % align == 0`
                    // with `0 <= offset < align` on the success path. Record both so a
                    // downstream `*(ptr.add(offset) as *const U)` can discharge `Align`.
                    let zero = Int::from_u64(self.ctx, 0);
                    let ptr_plus_off = Int::add(self.ctx, &[&ptr_val.term, &offset]);
                    self.path_conditions
                        .push(ptr_plus_off.rem(&align_val.term)._eq(&zero));
                    self.path_conditions.push(offset.ge(&zero));
                    self.path_conditions.push(offset.lt(&align_val.term));
                }
                let val = VmValue {
                    term: offset,
                    ty: dest_ty,
                    provenance: None,
                    invariants: ValueInvariants::default(),
                };
                self.set_local(dest, val);
            }
            CallEffect::ReturnMin { lhs_arg, rhs_arg } => {
                if let (Some(lhs), Some(rhs)) = (args.get(*lhs_arg), args.get(*rhs_arg)) {
                    let dest_ty = self.body.local_decls[dest].ty;
                    // Build the min as a first-class `ite(lhs <= rhs, lhs, rhs)`
                    // term rather than a fresh variable plus disjunction facts.
                    // A fresh variable breaks downstream alignment/bounds
                    // reasoning: e.g. `ptr.align_offset(8)` guarantees
                    // `(ptr + offset) % 8 == 0`, but `offset.min(len)` would
                    // then become an unrelated symbol and the `Align`/`InBound`
                    // checks on `*(ptr.add(offset) as *const usize)` could no
                    // longer discharge.  With an `ite`, the path conditions
                    // (`offset < 8`, `len >= 16`) let the solver reduce
                    // `ite(offset <= len, offset, len)` back to `offset`.
                    let term = lhs.term.le(&rhs.term).ite(&lhs.term, &rhs.term);
                    let val = VmValue {
                        term,
                        ty: dest_ty,
                        provenance: None,
                        invariants: ValueInvariants::default(),
                    };
                    self.set_local(dest, val);
                }
            }
            CallEffect::ReturnMax { lhs_arg, rhs_arg } => {
                if let (Some(lhs), Some(rhs)) = (args.get(*lhs_arg), args.get(*rhs_arg)) {
                    let dest_ty = self.body.local_decls[dest].ty;
                    let term = lhs.term.ge(&rhs.term).ite(&lhs.term, &rhs.term);
                    let val = VmValue {
                        term,
                        ty: dest_ty,
                        provenance: None,
                        invariants: ValueInvariants::default(),
                    };
                    self.set_local(dest, val);
                }
            }
            CallEffect::ReturnClamp {
                value_arg,
                min_arg,
                max_arg,
            } => {
                if let (Some(v), Some(mn), Some(mx)) =
                    (args.get(*value_arg), args.get(*min_arg), args.get(*max_arg))
                {
                    let dest_ty = self.body.local_decls[dest].ty;
                    // clamp(v, mn, mx) = max(mn, min(v, mx))
                    let upper = v.term.gt(&mx.term).ite(&mx.term, &v.term);
                    let term = v.term.lt(&mn.term).ite(&mn.term, &upper);
                    let val = VmValue {
                        term,
                        ty: dest_ty,
                        provenance: None,
                        invariants: ValueInvariants::default(),
                    };
                    self.set_local(dest, val);
                }
            }
            CallEffect::ReturnAbs { arg } => {
                if let Some(a) = args.get(*arg) {
                    let dest_ty = self.body.local_decls[dest].ty;
                    let zero = Int::from_u64(self.ctx, 0);
                    let neg = Int::sub(self.ctx, &[&zero, &a.term]);
                    let term = a.term.ge(&zero).ite(&a.term, &neg);
                    let val = VmValue {
                        term,
                        ty: dest_ty,
                        provenance: None,
                        invariants: ValueInvariants::default(),
                    };
                    self.set_local(dest, val);
                }
            }
            CallEffect::ReturnNeg { arg } => {
                if let Some(a) = args.get(*arg) {
                    let dest_ty = self.body.local_decls[dest].ty;
                    let zero = Int::from_u64(self.ctx, 0);
                    let term = Int::sub(self.ctx, &[&zero, &a.term]);
                    let val = VmValue {
                        term,
                        ty: dest_ty,
                        provenance: None,
                        invariants: ValueInvariants::default(),
                    };
                    self.set_local(dest, val);
                }
            }
            CallEffect::ReturnAdd { lhs_arg, rhs_arg } => {
                if let (Some(lhs), Some(rhs)) = (args.get(*lhs_arg), args.get(*rhs_arg)) {
                    let dest_ty = self.body.local_decls[dest].ty;
                    let term = Int::add(self.ctx, &[&lhs.term, &rhs.term]);
                    let val = VmValue {
                        term,
                        ty: dest_ty,
                        provenance: None,
                        invariants: ValueInvariants::default(),
                    };
                    self.set_local(dest, val);
                }
            }
            CallEffect::ReturnMul { lhs_arg, rhs_arg } => {
                if let (Some(lhs), Some(rhs)) = (args.get(*lhs_arg), args.get(*rhs_arg)) {
                    let dest_ty = self.body.local_decls[dest].ty;
                    let term = Int::mul(self.ctx, &[&lhs.term, &rhs.term]);
                    let val = VmValue {
                        term,
                        ty: dest_ty,
                        provenance: None,
                        invariants: ValueInvariants::default(),
                    };
                    self.set_local(dest, val);
                }
            }
            CallEffect::ReturnOptionSomeAdd { lhs_arg, rhs_arg } => {
                if let (Some(lhs), Some(rhs)) = (args.get(*lhs_arg), args.get(*rhs_arg)) {
                    // `checked_add` returns `Option<T>`; its `Some` payload is
                    // `lhs + rhs`. Store the payload term under field 0 so the
                    // `if let Some(payload)` projection resolves to it. The
                    // discriminant is left unconstrained, so both `Some`/`None`
                    // branches remain reachable.
                    let term = Int::add(self.ctx, &[&lhs.term, &rhs.term]);
                    self.set_field_value(
                        dest,
                        vec![0],
                        VmValue {
                            term,
                            ty: lhs.ty,
                            provenance: None,
                            invariants: ValueInvariants::default(),
                        },
                    );
                }
            }
            CallEffect::ReturnOptionSomeMul { lhs_arg, rhs_arg } => {
                if let (Some(lhs), Some(rhs)) = (args.get(*lhs_arg), args.get(*rhs_arg)) {
                    let term = Int::mul(self.ctx, &[&lhs.term, &rhs.term]);
                    self.set_field_value(
                        dest,
                        vec![0],
                        VmValue {
                            term,
                            ty: lhs.ty,
                            provenance: None,
                            invariants: ValueInvariants::default(),
                        },
                    );
                }
            }
            CallEffect::ReturnOptionSomeScanIndex { self_arg } => {
                // `Iterator::position`/`find` return `Option<usize>` whose `Some`
                // payload is a scan index into the iterator, so `0 <= i < self.len()`.
                // The receiver is `&mut iter` (a reference to the Iter/IterMut
                // struct), so resolve the reference to the iterator local it
                // points at (via its provenance = the iterator's stack alloc).
                // The iterator carries `ptr` (field 0) and `end_or_len`
                // (field 1); `len = end_or_len - ptr`.
                if let Some(iter_ref) = caller_arg_locals.get(*self_arg).copied().flatten() {
                    let iter_local = self
                        .locals
                        .get(&iter_ref)
                        .and_then(|v| v.provenance_alloc_id())
                        .and_then(|alloc| {
                            self.local_alloc_ids
                                .iter()
                                .find(|(_, a)| **a == alloc)
                                .map(|(l, _)| *l)
                        });
                    let ptr_term =
                        iter_local.and_then(|l| self.field_value(l, &[0]).map(|v| v.term.clone()));
                    let end_term =
                        iter_local.and_then(|l| self.field_value(l, &[1]).map(|v| v.term.clone()));
                    if let (Some(ptr), Some(end)) = (ptr_term, end_term) {
                        let len = Int::sub(self.ctx, &[&end, &ptr]);
                        let payload = self.fresh_int(&format!("scan_idx_{}", dest.as_usize()));
                        self.path_conditions.push(payload.lt(&len));
                        let dest_ty = self.body.local_decls[dest].ty;
                        let payload_ty = match dest_ty.kind() {
                            TyKind::Adt(adt, substs) if adt.is_enum() => substs.type_at(0),
                            _ => dest_ty,
                        };
                        self.set_field_value(
                            dest,
                            vec![0],
                            VmValue {
                                term: payload,
                                ty: payload_ty,
                                provenance: None,
                                invariants: ValueInvariants::default(),
                            },
                        );
                    }
                }
            }
            CallEffect::ReturnBranchPayload { arg } => {
                // `Try::branch`: copy the `Option` arg's `Some` payload (field 0)
                // to the `ControlFlow` result's `Continue` payload (field 0),
                // preserving its provenance so a `?`-operator unwrap survives.
                let arg_local = caller_arg_locals.get(*arg).copied().flatten();
                if let Some(l) = arg_local {
                    if let Some(payload) = self.field_value(l, &[0]).cloned() {
                        self.set_field_value(dest, vec![0], payload);
                    }
                }
            }
            CallEffect::ReturnOptionSomeIndexLtArgLen { arg } => {
                // `memchr(x, bytes)`/`memrchr(x, bytes)`-style search returns
                // `Option<usize>` whose `Some(i)` payload satisfies
                // `0 <= i < bytes.len()`.  Store the payload under field 0 (so
                // `if let Some(i)` resolves to it) and record both bounds so a
                // caller can re-prove `finger <= finger_back` after
                // `finger += i + 1` (forward) or `finger_back = finger + i`
                // (reverse).
                if let Some(slice) = args.get(*arg) {
                    if let Some(len) = self.slice_len_from_value(slice) {
                        let payload =
                            self.fresh_int(&format!("scan_idx_{}", dest.as_usize()));
                        self.path_conditions.push(payload.lt(&len));
                        let zero = Int::from_u64(self.ctx, 0);
                        self.path_conditions.push(payload.ge(&zero));
                        let dest_ty = self.body.local_decls[dest].ty;
                        let payload_ty = match dest_ty.kind() {
                            TyKind::Adt(adt, substs) if adt.is_enum() => substs.type_at(0),
                            _ => dest_ty,
                        };
                        self.set_field_value(
                            dest,
                            vec![0],
                            VmValue {
                                term: payload,
                                ty: payload_ty,
                                provenance: None,
                                invariants: ValueInvariants::default(),
                            },
                        );
                    }
                }
            }
            CallEffect::ReturnOptionSomeTupleFieldLeArgLen { field, arg } => {
                // UTF-8 decoder returns `Option<(.., len, ..)>` whose length
                // field satisfies `len <= slice.len()`.  Store the length under
                // `[0, field]` (the `Some` payload tuple's field) and record
                // `len <= arg.len()` so a caller can re-prove
                // `finger <= finger_back` after `finger += len`.
                if let Some(slice) = args.get(*arg) {
                    if let Some(arg_len) = self.slice_len_from_value(slice) {
                        let len = self.fresh_int(&format!("decode_len_{}", dest.as_usize()));
                        self.path_conditions.push(len.le(&arg_len));
                        let dest_ty = self.body.local_decls[dest].ty;
                        let payload_ty = match dest_ty.kind() {
                            TyKind::Adt(adt, substs) if adt.is_enum() => substs.type_at(0),
                            _ => dest_ty,
                        };
                        let field_ty = match payload_ty.kind() {
                            TyKind::Tuple(tys) => tys.get(*field).copied().unwrap_or(payload_ty),
                            _ => payload_ty,
                        };
                        self.set_field_value(
                            dest,
                            vec![0, *field],
                            VmValue {
                                term: len,
                                ty: field_ty,
                                provenance: None,
                                invariants: ValueInvariants::default(),
                            },
                        );
                    }
                }
            }
            CallEffect::ReturnScanLength => {
                // `strlen(ptr)` returns the byte length before the NUL
                // terminator. The `ValidCStr` invariant guarantees the NUL is
                // within `isize::MAX` bytes, so `len < isize::MAX`, and
                // `len + 1` (the length with the terminator) fits in
                // `isize::MAX` — discharging `from_raw_parts`'s
                // `ValidNum(size_of(T)*(len+1) <= isize::MAX)`.
                let len = self.fresh_int(&format!("strlen_{}", dest.as_usize()));
                let max = Int::from_i64(self.ctx, i64::MAX);
                self.path_conditions.push(len.lt(&max));
                let dest_ty = self.body.local_decls[dest].ty;
                self.set_local(
                    dest,
                    VmValue {
                        term: len,
                        ty: dest_ty,
                        provenance: None,
                        invariants: ValueInvariants::default(),
                    },
                );
            }
            CallEffect::ReturnNonZeroIff { arg } => {
                if let Some(a) = args.get(*arg) {
                    let dest_ty = self.body.local_decls[dest].ty;
                    let zero = Int::from_u64(self.ctx, 0);
                    let term = self.fresh_int(&format!("ret_nz_iff_{}", dest.as_usize()));
                    // `result == 0` iff `arg == 0`, i.e. non-zero is preserved
                    // exactly (bit-preserving ops map 0 -> 0, non-zero -> non-zero).
                    self.path_conditions
                        .push(term._eq(&zero)._eq(&a.term._eq(&zero)));
                    self.set_local(
                        dest,
                        VmValue {
                            term,
                            ty: dest_ty,
                            provenance: None,
                            invariants: ValueInvariants::default(),
                        },
                    );
                }
            }
            CallEffect::ReturnOptionSomeNonZeroIff { arg } => {
                if let Some(a) = args.get(*arg) {
                    let zero = Int::from_u64(self.ctx, 0);
                    let term = self.fresh_int(&format!("ret_opt_nz_iff_{}", dest.as_usize()));
                    self.path_conditions
                        .push(term._eq(&zero)._eq(&a.term._eq(&zero)));
                    self.set_field_value(
                        dest,
                        vec![0],
                        VmValue {
                            term,
                            ty: a.ty,
                            provenance: None,
                            invariants: ValueInvariants::default(),
                        },
                    );
                }
            }
            CallEffect::ReturnOptionSomeNonZero => {
                // `Some` payload is unconditionally non-zero (e.g.
                // `checked_next_power_of_two`).
                let zero = Int::from_u64(self.ctx, 0);
                let term = self.fresh_int(&format!("ret_opt_nz_{}", dest.as_usize()));
                self.path_conditions.push(term._eq(&zero).not());
                let payload_ty = args
                    .first()
                    .map(|a| a.ty)
                    .unwrap_or(self.body.local_decls[dest].ty);
                self.set_field_value(
                    dest,
                    vec![0],
                    VmValue {
                        term,
                        ty: payload_ty,
                        provenance: None,
                        invariants: ValueInvariants::default(),
                    },
                );
            }
            CallEffect::WriteMemory { pointer_arg } => {
                if let Some(arg_val) = args.get(*pointer_arg) {
                    if let Some(prov) = &arg_val.provenance {
                        // Writing a non-`u8` value through a byte buffer reinterprets
                        // it (e.g. `*mut FreeBlock` cast from a `Vec<u8>` buffer):
                        // update the allocation's element type so a later `Typed`
                        // invariant matches the written type.
                        if let rustc_middle::ty::TyKind::RawPtr(inner, _)
                        | rustc_middle::ty::TyKind::Ref(_, inner, _) = arg_val.ty.kind()
                        {
                            let cur = self.alloc(prov.alloc_id).element_ty;
                            let is_u8 = |t: rustc_middle::ty::Ty<'_>| {
                                matches!(
                                    t.kind(),
                                    rustc_middle::ty::TyKind::Uint(rustc_middle::ty::UintTy::U8)
                                )
                            };
                            if let Some(c) = cur {
                                if is_u8(c) && !is_u8(*inner) {
                                    self.alloc_mut(prov.alloc_id).element_ty = Some(*inner);
                                }
                            }
                        }
                        // For locally-created Vec-like types: create a heap data
                        // allocation on first mutation. (Param Vecs already have
                        // an external allocation set by init_parameters.)
                        let is_vec = crate::verify::api_classify::is_vec_push_or_reserve(
                            self.last_call_callee,
                        );
                        let is_external = self.alloc(prov.alloc_id).is_external;
                        if is_vec && !is_external {
                            let elem_ty = match arg_val.ty.kind() {
                                TyKind::Ref(_, inner, _) | TyKind::RawPtr(inner, _) => {
                                    crate::verify::call_summary::vec_elem_ty(self.tcx, *inner)
                                }
                                _ => crate::verify::call_summary::vec_elem_ty(self.tcx, arg_val.ty),
                            };
                            let heap_align =
                                elem_ty.map(|ty| self.align_sym(ty)).unwrap_or_else(|| Int::from_u64(self.ctx, 1));
                            if let Some(old_data) = self.alloc(prov.alloc_id).slice_data {
                                // Subsequent mutation: invalidate old heap data.
                                self.alloc_mut(old_data).dead = true;
                                let max_size = Int::from_u64(self.ctx, i64::MAX as u64);
                                let (data_alloc, _) =
                                    self.allocate_external(max_size, heap_align, elem_ty);
                                self.alloc_mut(prov.alloc_id).slice_data = Some(data_alloc);
                            } else {
                                // First mutation: create heap data allocation.
                                let max_size = Int::from_u64(self.ctx, i64::MAX as u64);
                                let (data_alloc, _) =
                                    self.allocate_external(max_size, heap_align, elem_ty);
                                self.alloc_mut(prov.alloc_id).slice_data = Some(data_alloc);
                            }
                        }
                        // When offset is concrete, only mark the bytes actually
                        // written. For symbolic offsets, mark entire allocation.
                        let off_u64 = prov
                            .offset
                            .as_u64()
                            .or_else(|| prov.offset.simplify().as_u64());
                        if let Some(off) = off_u64 {
                            if off == 0 {
                                self.alloc_mut(prov.alloc_id).initialized = true;
                            }
                            let elem_size = match arg_val.ty.kind() {
                                rustc_middle::ty::TyKind::Ref(_, inner, _) => {
                                    self.size_of_ty(*inner) as usize
                                }
                                _ => 0,
                            };
                            let write_size = if elem_size > 0 {
                                elem_size
                            } else {
                                self.allocation_size(prov.alloc_id).as_u64().unwrap_or(0) as usize
                            };
                            let end = (off as usize + write_size).min(4096);
                            for byte_off in (off as usize)..end {
                                self.mark_byte_init(prov.alloc_id, byte_off);
                            }
                        } else {
                            // Symbolic write offset: the exact written element
                            // can't be tracked per-byte. For concrete allocation
                            // sizes, mark every byte (as before). For unknown /
                            // zero sizes — generic element types such as
                            // `MaybeUninit<T>` inside `[MaybeUninit<T>; N]` —
                            // mark the whole allocation initialized so a later
                            // `assume_init_read`/`assume_init_drop` can discharge
                            // `Init` on those (fully initialized) elements.
                            let size_val = self.allocation_size(prov.alloc_id).as_u64();
                            match size_val {
                                Some(sz) if sz > 0 => {
                                    for off in 0..(sz as usize).min(1024) {
                                        self.mark_byte_init(prov.alloc_id, off);
                                    }
                                }
                                _ => {
                                    self.alloc_mut(prov.alloc_id).initialized = true;
                                }
                            }
                        }
                    }
                }
            }
            CallEffect::ReturnFreshAllocation {
                pointer_arg,
                size_arg,
                elem_size,
            } => {
                if let (Some(ptr_val), Some(size_val)) =
                    (args.get(*pointer_arg), args.get(*size_arg))
                {
                    let dest_ty = self.body.local_decls[dest].ty;
                    let elem_ty = crate::verify::call_summary::from_raw_parts_elem_ty(
                        self.tcx,
                        self.caller_def_id,
                        Some(dest),
                    );
                    // A generic element type uses the shared symbolic `sizeof_T`
                    // so the fresh allocation's size stays consistent with ptr
                    // strides and `InBound` cancels the factor.
                    let elem_sz_term = if *elem_size == 0 {
                        self.size_sym(elem_ty.unwrap_or(dest_ty))
                    } else {
                        Int::from_u64(self.ctx, *elem_size)
                    };
                    let total = Int::mul(self.ctx, &[&size_val.term, &elem_sz_term]);
                    let heap_align = elem_ty.map(|ty| self.align_sym(ty)).unwrap_or_else(|| Int::from_u64(self.ctx, 1));
                    let (alloc_id, base) = self.allocate(total, heap_align, elem_ty);
                    self.alloc_mut(alloc_id).slice_len = Some(size_val.term.clone());
                    let prov = Provenance {
                        alloc_id,
                        offset: Int::from_u64(self.ctx, 0),
                        is_field_offset: false,
                    };
                    // If return is a reference, register slice/pointee data
                    if let Some(ref dest_alloc_id) = self.local_alloc_ids.get(&dest).copied() {
                        self.alloc_mut(*dest_alloc_id).slice_data = Some(alloc_id);
                    }
                    // Propagate init status and byte-level tracking from the source pointer
                    // For fresh allocations, the init status is inherited from the source.
                    let is_external = self.alloc(alloc_id).is_external;
                    if is_external {
                        self.alloc_mut(alloc_id).initialized = true;
                    }
                    if let Some(ref source_prov) = ptr_val.provenance {
                        if !self.alloc(source_prov.alloc_id).dead {
                            self.alloc_mut(alloc_id).initialized = true;
                            self.alloc_mut(alloc_id).parent = Some(source_prov.alloc_id);
                        }
                        // Copy byte-level tracking (value, init, NUL knowledge).
                        self.copy_byte_tracking(source_prov.alloc_id, alloc_id);
                    }
                    let result_align_n = ptr_val.invariants.align_n.clone().or_else(|| {
                        ptr_val
                            .provenance
                            .as_ref()
                            .map(|p| self.alloc(p.alloc_id).align.clone())
                    });
                    let vec_base = base.clone();
                    let vec_prov = prov.clone();
                    let vec_len = size_val.term.clone();
                    self.set_local(
                        dest,
                        VmValue {
                            term: base,
                            ty: dest_ty,
                            provenance: Some(prov),
                            invariants: ValueInvariants {
                                non_null: true,
                                init: true,
                                in_bounds: true,
                                aligned: true,
                                align_n: result_align_n.clone(),
                                ..ValueInvariants::default()
                            },
                        },
                    );
                    // Materialize `{ptr, cap, len}` fields for a Vec destination
                    // (`from_raw_parts` sets cap == len).
                    if let rustc_middle::ty::TyKind::Adt(adt_def, _) = dest_ty.kind() {
                        if api_classify::is_std_vec(adt_def.did()) {
                            let ptr_field = VmValue {
                                term: vec_base,
                                ty: ptr_val.ty,
                                provenance: Some(vec_prov),
                                invariants: ValueInvariants {
                                    non_null: true,
                                    init: true,
                                    aligned: true,
                                    in_bounds: true,
                                    align_n: result_align_n,
                                    ..ValueInvariants::default()
                                },
                            };
                            self.materialize_vec_fields(dest, ptr_field, vec_len.clone(), vec_len);
                        }
                    }
                }
            }
            CallEffect::ReturnNewAllocation {
                size_arg,
                elem_size,
            } => {
                if let Some(size_val) = args.get(*size_arg) {
                    let elem_sz = Int::from_u64(self.ctx, *elem_size);
                    let total = Int::mul(self.ctx, &[&size_val.term, &elem_sz]);
                    let dest_ty = self.body.local_decls[dest].ty;
                    let elem_ty = crate::verify::call_summary::vec_elem_ty(self.tcx, dest_ty);
                    let heap_align = elem_ty.map(|ty| self.align_sym(ty)).unwrap_or_else(|| Int::from_u64(self.ctx, 1));
                    let (alloc_id, base) = self.allocate_external(total, heap_align, elem_ty);
                    let dest_alloc_id = self.local_alloc_ids.get(&dest).copied();
                    if let Some(dest_alloc_id) = dest_alloc_id {
                        self.alloc_mut(dest_alloc_id).slice_data = Some(alloc_id);
                    }
                    self.alloc_mut(alloc_id).initialized = true;
                    let vec_base = base.clone();
                    let vec_len = size_val.term.clone();
                    self.set_local(
                        dest,
                        VmValue {
                            term: base,
                            ty: dest_ty,
                            provenance: dest_alloc_id.map(|stack_id| Provenance {
                                alloc_id: stack_id,
                                offset: Int::from_u64(self.ctx, 0),
                                is_field_offset: false,
                            }),
                            invariants: ValueInvariants {
                                non_null: true,
                                init: true,
                                in_bounds: true,
                                aligned: true,
                                ..ValueInvariants::default()
                            },
                        },
                    );
                    // `Vec::from_elem`/`from_elem`-style constructors set
                    // len == cap == count.
                    if let rustc_middle::ty::TyKind::Adt(adt_def, _) = dest_ty.kind() {
                        if api_classify::is_std_vec(adt_def.did()) {
                            let ptr_field = VmValue {
                                term: vec_base,
                                ty: elem_ty.unwrap_or(dest_ty),
                                provenance: Some(Provenance {
                                    alloc_id,
                                    offset: Int::from_u64(self.ctx, 0),
                                    is_field_offset: false,
                                }),
                                invariants: ValueInvariants {
                                    non_null: true,
                                    init: true,
                                    aligned: true,
                                    in_bounds: true,
                                    ..ValueInvariants::default()
                                },
                            };
                            self.materialize_vec_fields(dest, ptr_field, vec_len.clone(), vec_len);
                        }
                    }
                }
            }
            CallEffect::ReturnNewAllocationFromCap { cap_arg, elem_size } => {
                if let Some(cap_val) = args.get(*cap_arg) {
                    let elem_sz = Int::from_u64(self.ctx, *elem_size);
                    let total = Int::mul(self.ctx, &[&cap_val.term, &elem_sz]);
                    let dest_ty = self.body.local_decls[dest].ty;
                    let elem_ty = crate::verify::call_summary::vec_elem_ty(self.tcx, dest_ty);
                    let heap_align = elem_ty.map(|ty| self.align_sym(ty)).unwrap_or_else(|| Int::from_u64(self.ctx, 1));
                    let (alloc_id, base) = self.allocate_external(total, heap_align, elem_ty);
                    let dest_alloc_id = self.local_alloc_ids.get(&dest).copied();
                    if let Some(dest_alloc_id) = dest_alloc_id {
                        self.alloc_mut(dest_alloc_id).slice_data = Some(alloc_id);
                    }
                    self.alloc_mut(alloc_id).initialized = true;
                    let vec_base = base.clone();
                    let vec_cap = cap_val.term.clone();
                    self.set_local(
                        dest,
                        VmValue {
                            term: base,
                            ty: dest_ty,
                            provenance: dest_alloc_id.map(|stack_id| Provenance {
                                alloc_id: stack_id,
                                offset: Int::from_u64(self.ctx, 0),
                                is_field_offset: false,
                            }),
                            invariants: ValueInvariants {
                                non_null: true,
                                init: true,
                                in_bounds: true,
                                aligned: true,
                                ..ValueInvariants::default()
                            },
                        },
                    );
                    // `Vec::with_capacity(n)`: len == 0, cap == n.
                    if let rustc_middle::ty::TyKind::Adt(adt_def, _) = dest_ty.kind() {
                        if api_classify::is_std_vec(adt_def.did()) {
                            let ptr_field = VmValue {
                                term: vec_base,
                                ty: elem_ty.unwrap_or(dest_ty),
                                provenance: Some(Provenance {
                                    alloc_id,
                                    offset: Int::from_u64(self.ctx, 0),
                                    is_field_offset: false,
                                }),
                                invariants: ValueInvariants {
                                    non_null: true,
                                    init: true,
                                    aligned: true,
                                    in_bounds: true,
                                    ..ValueInvariants::default()
                                },
                            };
                            let zero = Int::from_u64(self.ctx, 0);
                            self.materialize_vec_fields(dest, ptr_field, vec_cap, zero);
                        }
                    }
                }
            }
            CallEffect::ReturnNewAllocationFromBox => {
                // Box→Vec conversion (into_vec, box_assume_init_into_vec_unsafe).
                self.ensure_local_allocation(dest);
                let dest_ty = self.body.local_decls[dest].ty;
                let elem_ty = crate::verify::call_summary::vec_elem_ty(self.tcx, dest_ty);
                let heap_align = elem_ty.map(|ty| self.align_sym(ty)).unwrap_or_else(|| Int::from_u64(self.ctx, 1));
                let max = Int::from_u64(self.ctx, i64::MAX as u64);
                let (alloc_id, base) = self.allocate_external(max, heap_align, elem_ty);
                let dest_alloc_id = self.local_alloc_ids.get(&dest).copied();
                if let Some(ref dest_alloc_id) = dest_alloc_id {
                    self.alloc_mut(*dest_alloc_id).slice_data = Some(alloc_id);
                }
                self.alloc_mut(alloc_id).initialized = true;
                let vec_base = base.clone();
                self.set_local(
                    dest,
                    VmValue {
                        term: base,
                        ty: dest_ty,
                        provenance: dest_alloc_id.map(|stack_id| Provenance {
                            alloc_id: stack_id,
                            offset: Int::from_u64(self.ctx, 0),
                            is_field_offset: false,
                        }),
                        invariants: ValueInvariants {
                            non_null: true,
                            init: true,
                            in_bounds: true,
                            aligned: true,
                            ..ValueInvariants::default()
                        },
                    },
                );
                // `into_vec` / `box_assume_init_into_vec_unsafe`: the Vec's
                // length equals the source boxed slice's length (symbolic);
                // cap == len (no spare capacity).
                if let rustc_middle::ty::TyKind::Adt(adt_def, _) = dest_ty.kind() {
                    if api_classify::is_std_vec(adt_def.did()) {
                        let ptr_field = VmValue {
                            term: vec_base,
                            ty: elem_ty.unwrap_or(dest_ty),
                            provenance: Some(Provenance {
                                alloc_id,
                                offset: Int::from_u64(self.ctx, 0),
                                is_field_offset: false,
                            }),
                            invariants: ValueInvariants {
                                non_null: true,
                                init: true,
                                aligned: true,
                                in_bounds: true,
                                ..ValueInvariants::default()
                            },
                        };
                        let len_term = self.fresh_int(&format!("vec_len_{}", dest.as_usize()));
                        self.materialize_vec_fields(dest, ptr_field, len_term.clone(), len_term);
                    }
                }
            }
            CallEffect::ReturnBoxFromVec { arg } => {
                if let Some(vec_val) = args.get(*arg) {
                    if let Some(ref prov) = vec_val.provenance {
                        if let Some(heap_alloc_id) = self.alloc(prov.alloc_id).slice_data {
                            let heap_base = self.allocation_base(heap_alloc_id).clone();
                            let dest_ty = self.body.local_decls[dest].ty;
                            self.set_local(
                                dest,
                                VmValue {
                                    term: heap_base,
                                    ty: dest_ty,
                                    provenance: Some(Provenance {
                                        alloc_id: heap_alloc_id,
                                        offset: Int::from_u64(self.ctx, 0),
                                        is_field_offset: false,
                                    }),
                                    invariants: ValueInvariants {
                                        non_null: true,
                                        init: true,
                                        in_bounds: true,
                                        aligned: true,
                                        ..ValueInvariants::default()
                                    },
                                },
                            );
                        }
                    }
                }
            }
            CallEffect::OwnsInitMemory { arg } => {
                if let Some(arg_val) = args.get(*arg) {
                    if let Some(prov) = &arg_val.provenance {
                        self.alloc_mut(prov.alloc_id).initialized = true;
                    }
                    let mut val = arg_val.clone();
                    val.ty = self.body.local_decls[dest].ty;
                    val.invariants.init = true;
                    val.invariants.non_null = true;
                    self.set_local(dest, val);
                }
            }
            CallEffect::ReturnPowerOfTwo => {
                // `Layout::align()` returns the layout's alignment, which is a
                // non-zero power of two. `Layout::align` inlines to
                // `self.align.as_usize()`, whose transmute-based body drops the
                // `NonZero` provenance; re-establish the non-zero fact (and the
                // power-of-two fact) with a fresh symbol so downstream
                // `from_size_align_unchecked` can discharge `align != 0` (its
                // `(align & (align - 1)) == 0` check is otherwise vacuously
                // proved, since contract-level `BitAnd` is unsupported).
                let dest_ty = self.body.local_decls[dest].ty;
                let term = self.fresh_int(&format!("layout_align_{}", dest.as_usize()));
                let zero = Int::from_u64(self.ctx, 0);
                self.path_conditions.push(term.gt(&zero));
                self.set_local(
                    dest,
                    VmValue {
                        term,
                        ty: dest_ty,
                        provenance: None,
                        invariants: ValueInvariants::default(),
                    },
                );
            }
            CallEffect::ChecksIndexBoundsDisjoint {
                indices_arg,
                len_arg,
            } => {
                let indices = args.get(*indices_arg);
                let len_val = args.get(*len_arg);
                if let (Some(indices_val), Some(len_val)) = (indices, len_val) {
                    let arr_ty = match indices_val.ty.kind() {
                        rustc_middle::ty::TyKind::Ref(_, inner, _) => *inner,
                        _ => indices_val.ty,
                    };
                    if let rustc_middle::ty::TyKind::Array(_elem_ty, _const_len) = arr_ty.kind() {
                        let alloc_id = indices_val.provenance_alloc_id().or_else(|| {
                            // Slicer may have dropped the &indices
                            // assignment, losing provenance.  Fall back
                            let fallback = self.locals.values().find_map(|v| {
                                if v.ty == arr_ty {
                                    v.provenance_alloc_id()
                                } else {
                                    None
                                }
                            });
                            fallback
                        });
                        if let Some(alloc_id) = alloc_id {
                            self.contract_flags.has_checked_bounds = true;
                            let zero = Int::from_u64(self.ctx, 0);
                            let mut byte_offsets: Vec<(usize, Int)> = self
                                .alloc_byte_values(alloc_id)
                                .into_iter()
                                .map(|(off, term)| (off, term.clone()))
                                .collect();
                            byte_offsets.sort_by_key(|(off, _)| *off);
                            for (_, term) in &byte_offsets {
                                self.path_conditions.push(term.ge(&zero));
                                self.path_conditions.push(term.lt(&len_val.term));
                            }
                            for i in 0..byte_offsets.len() {
                                for j in (i + 1)..byte_offsets.len() {
                                    let ti = &byte_offsets[i].1;
                                    let tj = &byte_offsets[j].1;
                                    self.path_conditions.push(ti._eq(tj).not());
                                }
                            }
                        }
                    }
                }
                let dest_ty = self.body.local_decls[dest].ty;
                let term = self.fresh_int(&format!("ck_ok_{}", dest.as_usize()));
                self.set_local(
                    dest,
                    VmValue {
                        term,
                        ty: dest_ty,
                        provenance: None,
                        invariants: ValueInvariants::default(),
                    },
                );
            }
        }
    }

    /// Compute the preserved alignment when doing `base + offset * stride`.
    /// Pointer arithmetic only ever *preserves* the base's alignment; it never
    /// creates it. When the base's alignment is unknown, we cannot conclude
    /// anything about the result (a `wrapping_add` over misaligned storage does
    /// not become aligned just because the stride is a power of two).
    fn compute_pointer_add_align(
        &self,
        base: &VmValue<'ctx, 'tcx>,
        _offset: &VmValue<'ctx, 'tcx>,
        stride_bytes: u64,
    ) -> Option<Int<'ctx>> {
        let base_align = base.invariants.align_n.as_ref()?;
        // Concrete alignment: the result stays n-aligned only if the stride is
        // a multiple of n.  A symbolic alignment can't be decided against a
        // concrete stride, so drop it here (the `check_align` SMT query
        // re-derives alignment from the allocation's align and the
        // `sizeof_T % align_T == 0` layout constraint).
        let Some(n) = base_align.simplify().as_u64() else {
            return None;
        };
        if stride_bytes > 0 && stride_bytes % n == 0 {
            return Some(base_align.clone());
        }
        None
    }

    pub(crate) fn propagate_const_bytes_to_tracked(&mut self, args: &[Spanned<Operand<'tcx>>]) {
        let mut const_bytes: Option<(Vec<u8>, usize)> = None;
        let mut tracked_alloc: Option<AllocId> = None;
        let mut tracked_offset: usize = 0;

        for (i, arg) in args.iter().enumerate() {
            let arg_val = self.value_of_operand(&arg.node);
            if const_bytes.is_none() {
                let bytes_opt = crate::helpers::mir_utils::const_operand_bytes(self.tcx, &arg.node)
                    .or_else(|| self.trace_to_const_bytes(&arg.node));
                if let Some(bytes) = bytes_opt {
                    const_bytes = Some((bytes, i));
                }
            }
            if tracked_alloc.is_none() {
                if let Some(alloc_id) = arg_val.provenance_alloc_id() {
                    tracked_alloc = Some(alloc_id);
                    if let Some(ref prov) = arg_val.provenance {
                        tracked_offset = prov.offset.as_u64().map(|v| v as usize).unwrap_or(0);
                    }
                }
            }
        }

        if let (Some((bytes, _)), Some(alloc_id)) = (const_bytes, tracked_alloc) {
            for (j, &b) in bytes.iter().enumerate() {
                let off = tracked_offset + j;
                self.record_byte_value(alloc_id, off, Int::from_u64(self.ctx, b as u64));
                if b == 0 {
                    self.mark_byte_nul(alloc_id, off);
                } else {
                    self.mark_byte_non_nul(alloc_id, off);
                }
            }
            self.alloc_mut(alloc_id).initialized = true;
        }
    }

    /// Element size of the type iterated by an Iter/IterMut pointer, symbolic
    /// (`sizeof_T`) for a generic element type so `size / elem_size` cancels.
    pub(crate) fn iter_elem_size(&self, ptr: &VmValue<'ctx, 'tcx>) -> Int<'ctx> {
        let elem_ty = match ptr.ty.kind() {
            TyKind::Adt(_, substs) => substs.first().and_then(|s| s.as_type()),
            _ => None,
        };
        match elem_ty {
            Some(t) => self.size_sym_read(t),
            None => Int::from_u64(self.ctx, 1),
        }
    }

    /// Element count from two pointer fields sharing the same allocation:
    /// `(end.offset - ptr.offset) / elem_size`.
    pub(crate) fn iter_len_from_ptrs(
        &self,
        ptr: &VmValue<'ctx, 'tcx>,
        end: &VmValue<'ctx, 'tcx>,
    ) -> Option<Int<'ctx>> {
        let pp = ptr.provenance.as_ref()?;
        let ep = end.provenance.as_ref()?;
        if pp.alloc_id != ep.alloc_id {
            return None;
        }
        let diff = Int::sub(self.ctx, &[&ep.offset, &pp.offset]);
        let sz = self.iter_elem_size(ptr);
        Some(diff.div(&sz))
    }

    /// Remaining element count of the Iter/IterMut backed by `local`
    /// (fields `[0]` = ptr, `[1]` = end_or_len).  When a tracked pointer
    /// offset exists (`iter_ptr_offset`), prefers the compact
    /// `base_len - offset` form; otherwise falls back to
    /// `(end.offset - ptr.offset) / elem_size`.
    fn iter_remaining_len(&self, local: Local) -> Option<Int<'ctx>> {
        let ptr = self.field_value(local, &[0])?;
        let end = self.field_value(local, &[1])?;
        let ep = end.provenance.as_ref()?;
        if ptr.provenance.as_ref().map(|p| p.alloc_id) != Some(ep.alloc_id) {
            return None;
        }
        let sz = self.iter_elem_size(&ptr);
        if let Some(offset) = self.iter_ptr_offset.get(&local) {
            let base_len = ep.offset.div(&sz);
            let zero = Int::from_u64(self.ctx, 0);
            Some(
                offset
                    .gt(&base_len)
                    .ite(&zero, &Int::sub(self.ctx, &[&base_len, offset])),
            )
        } else {
            self.iter_len_from_ptrs(&ptr, &end)
        }
    }

    /// For Iter/IterMut types, compute len from struct fields directly
    /// instead of the generic allocation-size heuristic. Returns true
    /// if handled (value set to dest).
    fn interpreter_iter_len(&mut self, arg_val: &VmValue<'ctx, 'tcx>, dest: Local) -> bool {
        let Some(l) = self.find_iter_self_local(arg_val) else {
            return false;
        };
        let Some(len_term) = self.iter_remaining_len(l) else {
            return false;
        };
        let dest_ty = self.body.local_decls[dest].ty;
        self.set_local(dest, VmValue::new(len_term, dest_ty));
        true
    }

    /// Apply the side effect of post_inc_start / pre_dec_end on Iter/IterMut.
    /// Only updates the tracked offset (not field values), so that the
    /// precondition check (which runs before the call executes) sees the
    /// pre-update state, while subsequent len()/is_empty() calls use
    /// `base_len - offset` via interpreter_iter_len.
    fn apply_iter_ptr_update(
        &mut self,
        callee: DefId,
        arg_values: &[VmValue<'ctx, 'tcx>],
        _caller_arg_locals: &[Option<Local>],
    ) {
        let is_inc = crate::helpers::mir_utils::is_post_inc_start(self.tcx, callee);
        if !is_inc {
            return;
        } // pre_dec_end not yet supported
        let self_val = &arg_values[0];
        let some_local = self.find_iter_self_local(self_val);
        let Some(local) = some_local else { return };
        let offset_term = arg_values
            .get(1)
            .map(|v| v.term.clone())
            .unwrap_or_else(|| Int::from_u64(self.ctx, 1));
        let new_offset = match self.iter_ptr_offset.get(&local) {
            Some(prev) => Int::add(self.ctx, &[prev, &offset_term]),
            None => offset_term,
        };
        self.iter_ptr_offset.insert(local, new_offset);
    }

    /// Find the local whose symbolic address matches `term` (the address a
    /// reference value points at). Used to resolve a `&self`/`&mut self`
    /// receiver (often a reborrow temp) back to the referent local that carries
    /// the materialized field values.
    pub(crate) fn find_local_by_address(&self, term: &Int<'ctx>) -> Option<Local> {
        for (local, addr) in &self.local_addresses {
            if addr == term {
                return Some(*local);
            }
        }
        None
    }

    /// If arg_val is a reference to an Iter or IterMut struct, return the
    /// local index of the referent (so field values can be looked up).
    /// Since len()/is_empty() always take &self, local 1 is the receiver.
    fn find_iter_self_local(&self, arg_val: &VmValue<'ctx, 'tcx>) -> Option<Local> {
        match arg_val.ty.kind() {
            TyKind::Ref(_, pointee, _) => match pointee.kind() {
                TyKind::Adt(adt_def, _) => {
                    if api_classify::is_std_iter_or_itermut(adt_def.did()) {
                        // Find the local holding the iterator by matching the
                        // reference's address term against known local addresses
                        // (`&mut _iter` has term `addr__iter`).  A hardcoded
                        // `Local(1)` only holds for inlined `next` bodies where
                        // the iterator is the first argument; direct trait
                        // `Iterator::next` calls keep the iterator at an
                        // arbitrary local.
                        if let Some(local) = self.find_local_by_address(&arg_val.term) {
                            return Some(local);
                        }
                        // Fallback for inlined `next` bodies (iter bound to arg 1).
                        return Some(Local::from_usize(1));
                    }
                    None
                }
                _ => None,
            },
            _ => None,
        }
    }

    /// Derive an element count from the backing allocation (`size / elem_size`).
    /// Used by `ReturnLengthOfArg` and the fallback in `ReturnFieldOfArg`
    /// (slices, `&str`, and Vec values whose `{buf{ptr,cap}, len}` field was not
    /// materialized). Returns true when a value was produced.
    fn set_len_from_alloc(&mut self, arg_val: &VmValue<'ctx, 'tcx>, dest: Local) -> bool {
        let effective_alloc_id = arg_val
            .provenance_alloc_id()
            .and_then(|pid| self.alloc(pid).slice_data)
            .or_else(|| arg_val.provenance_alloc_id());
        let Some(alloc_id) = effective_alloc_id else {
            return false;
        };
        let dest_ty = self.body.local_decls[dest].ty;
        // Prefer the materialized slice length.
        if let Some(len) = self.alloc(alloc_id).slice_len.clone() {
            let val = VmValue::new(len, dest_ty);
            self.set_local(dest, val);
            return true;
        }
        if let Some(elem_ty) = self.alloc(alloc_id).element_ty {
            let elem_term = self.size_sym_read(elem_ty);
            let size = self.allocation_size(alloc_id);
            if elem_term.simplify().as_u64() == Some(1) {
                let val = VmValue::new(size.clone(), dest_ty);
                self.set_local(dest, val);
                return true;
            }
            let val = VmValue::new(size.div(&elem_term), dest_ty);
            self.set_local(dest, val);
            return true;
        }
        let size = self.allocation_size(alloc_id);
        let val = VmValue::new(size.clone(), dest_ty);
        self.set_local(dest, val);
        true
    }

    /// Apply a `ReturnFieldOfArg`/`ReturnFieldOfArgSub` effect: read the
    /// materialized field `field` of the receiver's pointee and return it,
    /// preserving the field's own type/provenance. For `ReturnFieldOfArgSub`,
    /// subtract `sub_offset` elements from the field pointer (`next_back_unchecked`
    /// after `pre_dec_end`).
    ///
    /// The receiver of a `&self` getter is a reborrow temp (`_t = &data`) whose
    /// local carries no field values, while the fields were materialized on the
    /// referent (`data`). Resolve the referent by matching the receiver value's
    /// address term against the known local addresses; fall back to the direct
    /// arg local.
    fn apply_field_of_arg_effect(
        &mut self,
        arg: usize,
        field: usize,
        sub_offset: Option<u64>,
        args: &[VmValue<'ctx, 'tcx>],
        caller_arg_locals: &[Option<Local>],
        dest: Local,
    ) {
        // Candidate locals that may carry the materialized field, in order of
        // preference. A `&mut self` receiver is often a mutable reborrow
        // (`_t = &mut (*self)`) whose local does not carry the field values,
        // while the parameter and the shared reborrow (`_t = &(*self)`) do.
        let mut candidates: Vec<Local> = Vec::new();
        if let Some(l) = args.get(arg).and_then(|v| self.find_local_by_address(&v.term)) {
            candidates.push(l);
        }
        if let Some(l) = caller_arg_locals.get(arg).copied().flatten() {
            candidates.push(l);
        }
        // Any local that already materializes the field (covers the receiver
        // parameter / shared reborrow that the mutable reborrow does not copy).
        for (l, _) in self.field_values.keys() {
            candidates.push(*l);
        }
        let mut found: Option<VmValue<'ctx, 'tcx>> = None;
        for l in candidates {
            if let Some(fv) = self.field_value(l, &[field]) {
                found = Some(fv.clone());
                break;
            }
        }
        if let Some(mut v) = found {
            if let Some(offset) = sub_offset {
                // `field - offset` elements: subtract the element stride from
                // both the address term and the provenance offset.
                let stride = self.pointee_elem_size(v.ty).max(1) as u64;
                let scaled = Int::from_u64(self.ctx, offset * stride);
                v.term = Int::sub(self.ctx, &[&v.term, &scaled]);
                if let Some(prov) = &v.provenance {
                    v.provenance = Some(Provenance {
                        alloc_id: prov.alloc_id,
                        offset: Int::sub(self.ctx, &[&prov.offset, &scaled]),
                        is_field_offset: false,
                    });
                }
            }
            v.ty = self.body.local_decls[dest].ty;
            self.set_local(dest, v);
            return;
        }
        // Fallback: for an integer result (e.g. `len`/`capacity`), the
        // receiver is often a reborrow temp whose referent carries no field
        // values; reconstruct the length from the backing allocation
        // (`size / elem_size`), as `ReturnLengthOfArg` does.
        let dest_ty = self.body.local_decls[dest].ty;
        if matches!(dest_ty.kind(), TyKind::Uint(_) | TyKind::Int(_)) {
            if let Some(arg_val) = args.get(arg) {
                if self.set_len_from_alloc(arg_val, dest) {
                    return;
                }
            }
        }
        let term = self.fresh_int(&format!("field_{}", dest.as_usize()));
        let val = VmValue {
            term,
            ty: dest_ty,
            provenance: None,
            invariants: ValueInvariants::default(),
        };
        self.set_local(dest, val);
    }

    /// Apply a `ReturnRange` effect: model `slice::range(range, bounds)`
    /// returning `Range { start, end }` with `0 <= start <= end <= bounds.end`.
    /// The `bounds` argument is a `RangeTo<usize>` whose field 0 carries the
    /// slice length; the returned `Range<usize>` fields are fresh symbols bound
    /// by the range invariant.
    fn apply_range_effect(
        &mut self,
        bounds_arg: usize,
        args: &[VmValue<'ctx, 'tcx>],
        caller_arg_locals: &[Option<Local>],
        dest: Local,
    ) {
        let dest_ty = self.body.local_decls[dest].ty;
        let TyKind::Adt(adt, substs) = dest_ty.kind() else {
            return;
        };
        let variant = adt.non_enum_variant();
        let field_ty = |idx: usize| -> Ty<'tcx> {
            variant
                .fields
                .iter()
                .nth(idx)
                .map(|f| crate::helpers::mir_utils::field_ty(self.tcx, f, substs))
                .unwrap_or(dest_ty)
        };

        // Resolve `bounds.end` (the slice length): prefer the materialized
        // field 0 of the `RangeTo<usize>` argument, falling back to the
        // argument's own term.
        let mut len_term = None;
        if let Some(l) = caller_arg_locals.get(bounds_arg).copied().flatten() {
            if let Some(fv) = self.field_value(l, &[0]) {
                len_term = Some(fv.term.clone());
            }
        }
        let len_term = len_term.or_else(|| args.get(bounds_arg).map(|v| v.term.clone()));
        let Some(len_term) = len_term else {
            return;
        };

        let start = self.fresh_int(&format!("range_start_{}", dest.as_usize()));
        let end = self.fresh_int(&format!("range_end_{}", dest.as_usize()));
        let zero = Int::from_u64(self.ctx, 0);
        self.path_conditions.push(start.ge(&zero));
        self.path_conditions.push(start.le(&end));
        self.path_conditions.push(end.le(&len_term));

        let start_val = VmValue {
            term: start,
            ty: field_ty(0),
            provenance: None,
            invariants: ValueInvariants::default(),
        };
        let end_val = VmValue {
            term: end,
            ty: field_ty(1),
            provenance: None,
            invariants: ValueInvariants::default(),
        };
        self.set_field_value(dest, vec![0], start_val);
        self.set_field_value(dest, vec![1], end_val);
    }

    /// Materialize the `{ptr, cap, len}` field values of a `Vec<T>` aggregate
    /// at `local`, using the real `Vec` layout `{ buf: RawVec<T>, len }` /
    /// `RawVec { ptr, cap }`:
    ///   * field `[0, 0]` = backing-buffer pointer (`buf.ptr`),
    ///   * field `[0, 1]` = capacity (`buf.cap`),
    ///   * field `[1]`   = length (`len`).
    ///
    /// The symbolic invariant `0 <= len <= cap` and `cap * elem_size <=
    /// isize::MAX` is asserted as a path condition so downstream `len()` /
    /// `capacity()` / `InBound` / `ValidNum` queries agree. This is the
    /// internalized counterpart of a user `#[rapx::invariant]` for the `Vec`
    /// layout — the length/capacity are tracked as named fields (read back by
    /// `ReturnFieldOfArg` for `len()`) instead of being recomputed from
    /// `alloc.size`.
    pub(crate) fn materialize_vec_fields(
        &mut self,
        local: Local,
        ptr: VmValue<'ctx, 'tcx>,
        cap: Int<'ctx>,
        len: Int<'ctx>,
    ) {
        let elem_size = self.size_of_ty(ptr.ty).max(1) as u64;
        self.set_field_value(local, vec![0, 0], ptr);
        self.materialize_vec_len_cap(local, cap, len, elem_size);
    }

    /// Materialize a Vec's `cap` field (`[0, 1]`) and `len` field (`[1]`) as
    /// fresh symbolic values, together with the invariants `0 <= len <= cap`
    /// and `cap * elem_size <= isize::MAX`.
    pub(crate) fn materialize_vec_len_cap(
        &mut self,
        local: Local,
        cap: Int<'ctx>,
        len: Int<'ctx>,
        elem_size: u64,
    ) {
        let usize_ty = self.tcx.types.usize;
        self.set_field_value(local, vec![0, 1], VmValue::new(cap.clone(), usize_ty));
        self.set_field_value(local, vec![1], VmValue::new(len.clone(), usize_ty));
        let zero = Int::from_u64(self.ctx, 0);
        self.path_conditions.push(len.ge(&zero));
        self.path_conditions.push(len.le(&cap));
        self.path_conditions.push(cap.ge(&zero));
        // Language invariant: a Vec's byte length fits in `isize::MAX`, so the
        // `from_raw_parts`/`from_raw_parts_mut` precondition
        // `size_of(T) * len <= isize::MAX` is provable from the materialized
        // fields (`len <= cap` and `cap * elem_size <= isize::MAX`).
        let isize_max = Int::from_u64(self.ctx, isize::MAX as u64);
        let elem_term = Int::from_u64(self.ctx, elem_size.max(1));
        self.path_conditions
            .push(Int::mul(self.ctx, &[&cap, &elem_term]).le(&isize_max));
    }
}