Provedor automático de teoremas SMT
