Like most languages with refinement types it uses an SMT solver (a more general problem), though I’m not sure it uses it for pattern matching. I was thinking of Coq, Agda, Lean, etc. which are full-spectrum dependently typed languages. LiquidHaskell is more specialized, though its automated proof capabilities are much stronger.