If the tutorial uses Rust, why didn't they use a solver written in Rust? Z3 was written in C++.
I'm not sure I understand your argument. Z3's API is canonically C. There's a C++ wrapper that works pretty well. I don't have experience with the Rust wrapper, but I'd imagine that works pretty well too.
What solver would you have them use? Z3 is very mature and the Rust bindings are pretty good in my (limited) experience.
I'm not sure I understand your argument. Z3's API is canonically C. There's a C++ wrapper that works pretty well. I don't have experience with the Rust wrapper, but I'd imagine that works pretty well too.