SMT solvers have been getting better and better, but they still fail at relatively simple things. I often use them to prove certain low-level optimizations are correct, and sometimes simple things completely choke the solver.

The following is a simple example of a popcount implementation, relatively easy to prove correct by a human, but that Z3 (and presumably others, but I haven't tried) is unable to solve in a reasonable amount of time. Using z3py for convenience:

  from z3 import *

  def popcount1(x):
    return Sum([ ZeroExt(6, Extract(i,i,x)) for i in range(64) ])

  def popcount2(x):
    return Extract(6, 0, -Sum([ RotateLeft(x, i) for i in range(64) ]))

  x = BitVec("x", 64)
  prove(popcount1(x) == popcount2(x))