Function debug_z3_solver_state 

fn debug_z3_solver_state<'ctx>(
    solver: &Solver<'ctx>,
    result: SatResult,
    z3_vars: &HashMap<usize, BV<'ctx>>,
)