I played around with Z3 after reading the excellent tutorial at https://www.rise4fun.com/Z3/tutorial. But now I would like to get an overview over all commands available in Z3's dialect of SMTLIB2.
Unfortunately I only found reference manuals for the different languages bindings, but not for SMTLIB2 itself.
You can read all about SMTLib in http://smtlib.cs.uiowa.edu/
In particular, the document http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf is the "official" document on all SMTLib commands.
For logics, you want to browse: http://smtlib.cs.uiowa.edu/logics.shtml
Now, this document is not Z3 specific. But to a large extent, it captures all the SMT commands/logics supported by Z3, and Z3 is one of the most "compliant" solvers out there in terms of implementing the specs. There are a few differences of course: For instance, the spec never talks about optimization and Z3 does support that, likewise for set operations and a few other "extras." As Malte pointed out the documentation for these are available, but maybe not easy to navigate. My favorite links are:
https://ericpony.github.io/z3py-tutorial/guide-examples.htm (Python specific, but also tons of info on Z3 features.)
Programming in Z3: https://theory.stanford.edu/~nikolaj/programmingz3.html This is a wonderful document detailing how z3 works internally with most of its features demonstrated. Again, it uses Python, but for the most part you can find the corresponding commands in SMTLib more or less directly.
API documentation in various languages: https://z3prover.github.io/api/html/index.html Eventually you'll need these as you get to program z3; but you can keep this as a "reference" only for later use.
If there is a specific piece of info you're looking for that's not covered in one of these documents, then that's what this forum is for! Best of luck..