A translation of a Z3 example from Python to Rust

This post is a translation of a Z3 example from Python to Rust. It is not very inspired: Please read the original Python article 1 for more background. However, at the bottom of this page, I provide a few more links and resources with a few notes.

The Z3 crate does not have any examples, so it makes it a bit tough to get started. I found one article that explains how to use Z3 for scheduling tasks in Python.

Last week there were two posts on the reputation of C++. In a noble effort, Jussi Pakkanen showcased modern C++. Nothing fancy, just clean and readable code. Unfortunately, around ten years after C++11, the news that simple (and safe) C++ code is now the default has not spread everywhere.

Jason Moiron answered with Go code doing the same (article). Both programs find the ten most common words in all txt files, which can be recursively found in the current directory.