Function verify 

pub fn verify(
    path: &str,
    rules: &[Rule],
    model: &Model,
    solver: &Solver,
) -> Result<Report, Vec<Error>>

Ask about every rule.

A rule that the solver settles at its own width is discharged and that is the end of it. A rule it gives up on is asked again at BOUNDED_WIDTHS, but only if the rule carries a written reason for taking narrow widths as enough, because a bounded proof is a judgement somebody makes and not a fallback a tool takes on its own.

Errors

Anything the model cannot write out, and anything that stops the solver from running.