Expand description
Verification Intermediate Representation for relevant types, eventually to be lowered to SMT. The goal is to leave some freedom to change term encodings or the specific solver backend.
Note: annotations use the higher-level IR in annotation_ir.rs.
Modules§
Structs§
- Bound
Var - A bound variable, including the VIR type
- Concrete
Input - Concrete
Test - Counterexample
- To-be-flushed-out verification counterexample for failures
- Term
Signature - Type
Context