Difference between Z3 and coq

I am wondering if someone can tell me the difference between Z3 and coq? Seems to me that coq is a proof assistant in that it requires the user to fill in the proof steps, whereas Z3 does not have that requirement. But seems like coq also has auto tactic that is similar to what Z3 does? Or maybe the proof search ability in coq is not as powerful as Z3?