A Dumb Introduction to Z3 (2025)
ar-ms.me
A Dumb Introduction to Z3 (2025)
1–10 of 29 posts
Re: A Dumb Introduction to Z3 (2025)
#2If the tutorial uses Rust, why didn't they use a solver written in Rust? Z3 was written in C++.
Re: A Dumb Introduction to Z3 (2025)
#3If the tutorial uses Rust, why didn't they use a solver written in Rust? Z3 was written in C++.
What solver would you have them use? Z3 is very mature and the Rust bindings are pretty good in my (limited) experience.
Re: A Dumb Introduction to Z3 (2025)
#4Z3 struggles with larger problems. CVC5 or Bitwuzla do a lot better once you get into anything complex.
If you're familiar with the Z3 Python API, you'll find the CVC5 one familiar.
Caveat: I mostly do logic design, maybe there are some software verification tasks where Z3 comes out ahead. I've never seen one though.
Re: A Dumb Introduction to Z3 (2025)
#5Re: A Dumb Introduction to Z3 (2025)
#6If the tutorial uses Rust, why didn't they use a solver written in Rust? Z3 was written in C++.
[deleted]
Re: A Dumb Introduction to Z3 (2025)
#7Re: A Dumb Introduction to Z3 (2025)
#8Re: A Dumb Introduction to Z3 (2025)
#9Earlier quoted context omitted.
What solver would you have them use? Z3 is very mature and the Rust bindings are pretty good in my (limited) experience.
I would write the tutorial in C++, for a more direct experience.
The author might not know C++ and you don't need to use C++ to effectively use z3.
Re: A Dumb Introduction to Z3 (2025)
#10Earlier quoted context omitted.
I personally like to avoid the “writing in C++” experience. :/
The authors of a powerful solver package thought differently.
It might have more to do with the first release of Z3 being in 2012, with the first stable Rust release being in 2015. Rather than the authors of Z3 passing some kind of judgment on Rust…