Module smt_check 

SMT checking package for the staged verifier.

The package is split into:

• common: the shared SMT entry point, query/result types, and term model.
• one SP-specific module per safety property family, such as align.

SP-specific modules should only lower verifier properties into common SMT obligations. They should not construct independent solver APIs.

Modules

alias 🔒

Alias hazard checks for unsafe view-producing APIs.

align 🔒

SMT lowering for the Align safety property.

alive 🔒

Lifetime anchoring checks for the Alive safety property.

allocated 🔒

SMT lowering for the Allocated safety property.

common 🔒

Common SMT checking backend for the staged verifier.

deref 🔒

SMT lowering for the Deref safety property.

in_bound 🔒

SMT lowering for the InBound safety property.

init 🔒

SMT lowering for the Init safety property.

non_null 🔒

SMT lowering for the NonNull safety property.

non_overlap 🔒

SMT lowering for the NonOverlap safety property.

non_volatile 🔒

SMT lowering for the NonVolatile safety property.

typed 🔒

Path-local checking for the Typed safety property.

valid_num 🔒

SMT lowering for the ValidNum safety property.

valid_ptr 🔒

SMT lowering for the composite ValidPtr safety property.

Structs

SmtCheckResult

Result of one SMT check.

SmtChecker

SMT backend for verifier properties.

SmtQuery

Solver query built from path facts plus one negated obligation.

Enums

SmtObligation

General SMT obligation produced by an SP-specific lowering.