Expand description
Interpolation-Based Model Checking
Craig interpolation provides over-approximations of reachable states. Given A AND B is UNSAT, interpolant I satisfies: A → I, and I AND B is UNSAT. The interpolant uses only variables shared between A and B.
Since Z3’s Rust bindings don’t directly expose interpolation, we approximate using variable-restricted weakening: project A onto shared variables.
Enums§
- Interpolation
Result - Result of interpolation-based model checking.
Functions§
- interpolate
- Compute a Craig interpolant approximation.
- itp_
model_ check - Interpolation-based model checking.