Expand description
Shared verification engine for the staged verifier pipeline.
This module extracts the common backward-visit → forward-visit → SMT-check flow that is shared between unsafe-checkpoint verification and struct-invariant verification, keeping both pipelines thin and focused on their own path-preparation logic.
Structs§
- Invariant
Check Result - Result of checking one invariant along one reachability path.
- Verify
Engine - Thin wrapper around the three-stage verification pipeline.