Module ic3 

IC3/PDR (Property-Directed Reachability)

The gold standard for unbounded safety verification (Bradley 2011).

Maintains frame sequence F_0, F_1, …, F_k where each frame over-approximates reachable states at step i. Converges when F_i = F_{i+1} (fixpoint = inductive invariant).

Core operations:

1. Counterexample to Induction (CTI): Find state in F_i AND T AND NOT P
2. Blocking: Add clause to prevent CTI state (generalized)
3. Propagation: Push clauses forward through frames
4. Convergence: Check if F_i == F_{i+1}

Enums

Ic3Result

Result of IC3/PDR verification.

Functions

check_sat

Check if a formula is satisfiable (public, creates its own Z3 context).

ic3

Run IC3/PDR on a safety property.