Function itp_model_check 

pub fn itp_model_check(
    init: &VerifyExpr,
    transition: &VerifyExpr,
    property: &VerifyExpr,
    bound: u32,
) -> InterpolationResult

Interpolation-based model checking.

Iteratively computes over-approximations of reachable states:

1. Start with init as R_0
2. Compute R_{i+1} = image(R_i, transition)
3. Check if R_{i+1} ⊆ R_i (fixpoint)
4. Check if R_i AND NOT(property) is UNSAT (safety)