Agreed. I don't know if I would be shocked, but I would be surprised.

This is one that is hard for people to really internalize, I think? The SAT solvers many are likely to use today are not at all the same as the ones they would have used 20 years ago. They have made some amazing advances in how to approach those problems.

There are also probably some very poorly conceived models that people use to adapt a problem to some of these solvers.