Function varisat::proof::solve_finished

pub fn solve_finished<'a>(
    ctx: Mut<SolverStateP, Mut<ProofP<'a>, Ref<Context<'a>>>>
)

Called before solve returns to flush buffers and to trigger delayed unit conflict processing.

We flush buffers before solve returns to ensure that we can pass IO errors to the user.