Struct Constraints 

pub(crate) struct Constraints<'z3, 'tcx> {
    pub(crate) assertions: Vec<Bool<'z3>>,
    pub(crate) term_caches: TermCaches<'z3, 'tcx>,
}

Accumulated solver state for the current path.

assertions is the assertion stream fed to Z3; term_caches holds the per-phenomenon term-provenance caches that keep expressions compact and linear. Everything is path-scoped and monotonic: it accumulates as the VM steps and is never reset within a path (or across inlined frames).

Fields

assertions: Vec<Bool<'z3>>

Accumulated solver constraints along the current path: branch/guard constraints (SwitchInt/Assert), API preconditions, and symbolic layout facts (sizeof_T, align_T). Asserted into the solver by VmState::assert_all and by the property checker’s feasibility queries.

term_caches: TermCaches<'z3, 'tcx>

Term-provenance caches that shape terms into a form Z3 can solve.

Trait Implementations

impl<'z3, 'tcx> Default for Constraints<'z3, 'tcx>

fn default() -> Self

Returns the “default value” for a type.