Most state-of-the-art branch-and-bound solvers for mixed-integer linear programming rely on limited-precision floating-point arithmetic and use numerical tolerances when reasoning about feasibility and optimality during their search. While the practical success of floating-point MIP solvers bears witness to their overall numerical robustness, it is well-known that numerically challenging input can lead them into producing incorrect results. Even when their final answer is correct, one critical question remains: Was the reasoning of the branch-and-bound solver justified, i.e., can its individual decisions be post-processed to yield a certificate that is valid in exact arithmetic?

In this talk I will present results from a first such a posteriori analysis of an LP-based branch-and-bound method, where we check all intermediate decisions critical to the correctness of the result: accepting solutions as integer feasible, declaring the LP relaxation infeasible, and pruning subtrees as suboptimal. Our computational study in the academic MIP solver SCIP confirms the expectation that in the overwhelming majority of cases, all decisions are correct. When errors do occur on numerically challenging instances, they typically affect only a small, typically single-digit, amount of leaf nodes that would require further processing.