Just some simple examples of using this tool from fasmg. The API is all pointers, so it's very easy to use from asm. There is a little bit of a learning curve to constructing model ASTs, but it's totally worth the effort to learn.

The intro tutorial online is quite a good overview of Z3:
https://rise4fun.com/z3/tutorial

Project is active on GitHub:
https://github.com/Z3Prover/z3
(Will need libz3.dll to run the examples. Since the DLL is dependent on UCRT, I've also used it for console output.)

It's really fun tool - will probably be posting more uses of it.

Software Modeling and Verification Lecture playlist (advanced course).
Prof. Joost-Pieter Katoen at RWTH Aachen University