It’s easy to embed the exact problem Rust has to solve for exhaustiveness checking into e.g. Lean’s pattern matching so they have the same opportunity to use SAT for such checks at least for some set of pattern matching situations (though as I said doubt it would be worthwhile). Using SMT for refinement types like F* does is mostly orthogonal to the problem this article is talking about, which arises just from structural pattern matching.