SAT/SMT hardness regression has come a long way, especially if you can insert profiling information for real instances.

If this is a production model for the cloud, the engineer should have put some thought into the encoding as to express sat/unsat clearly, if possible.

In the general case, sure, to some extent one can construct an adversarial example just as with NN (random 3-sat hardness cliff). Real world formulations of problems are either nice or atrocious IME, discoverable at dev time.