> Gurobi solved the new model to optimality (i.e., the bound became equal to the value of the best solution found).

Ah, I was not aware that that's what this language indicated. Thanks for helping me understand more!

I've used Gurobi (and other solvers) in the past, but always in situations where we just needed to find a solution that was way better than what we were going to find with, say, a heuristic... I've never needed to find a provably optimal solution...