Z3 Rust Guide

[mehrad31415]

Hi all,

While working on a somewhat related research project, I encountered some rough edges in the high-level Rust API for Z3. So I decided to put some time into it, and I've submitted a few PRs to address specific issues. Also, to document and maybe to help others who might be new to using Z3 from Rust, I’ve written a guide. The guide includes:

• When and how to use various methods in the high-level API
• Differences between sorts (e.g. Int, Real, Float, BitVec, etc.)
• Common pitfalls and when not to use certain constructs
• Many concrete, runnable examples.

📎 z3_rust_guide.pdf

Note: Some sections are adapted directly from Z3’s official documentation and are not original contributions. The guide reflects the state of the API as of July 2025. Also, some of the responses and content in this document were developed with the assistance of LLMs. Overall, this document is not intended to introduce novel material. The primary goal was to centralize
information and provide illustrative examples to create a beginner-friendly practical guide in using the
Rust bindings for Z3. I hope it’s helpful!

[toolCHAINZ]

Hello, thanks for the many PRs!

I appreciate the desire to document and centralize information about both Z3 and z3.rs. It's important that libraries be understandable and discoverable.

I'm not sure, however, if an LLM-generated/enhanced 100-page LaTeX document is the way to go about that, for a few reasons:

• As you mention, this information already (canonically, authoritatively) exists in the Z3 Guide or as comments in Z3 or z3.rs. Putting it all in a PDF is the opposite of centralizing it.
• PDFs get out of date. That PDF is already out of date in its build instructions due to changes in this repo 2 weeks ago.
• The PDF also has inaccuracies (e.g. no Ast types in z3.rs own the context as the PDF claims).

I'd argue that the right mix of documentation for this project is:

• docs.rs: https://docs.rs/z3/latest/z3/
• The Z3 Guide: https://microsoft.github.io/z3guide/
• Programming Z3: https://z3prover.github.io/papers/programmingz3.html
• Decision Procedures (An excellent primer in SMT): https://link.springer.com/book/10.1007/978-3-662-50497-0

If there are specific docs you feel are missing on any types or functions in this library, please feel free to contribute them; I think that will be much more discoverable than a PDF.

As for usage examples I can think of three good places for them:

• Unit tests and Documentation Tests (https://doc.rust-lang.org/rustdoc/write-documentation/documentation-tests.html)
• We could make an /examples/ directory in the workspace to make code snippets discoverable by Scraped Examples whenever that stablizes
• We could use the Wiki feature on this repository if there's specific topics that need to be covered in more depth (though I would want evidence that there's actually a question worth answering in any wiki page).