This is an example of title that could benefit from a simple, non-editorialized, and purely factual change: "Programming the Z3 SMT solver".
I am sure I was not the first to think it was related to Konrad Zuse's Z3.
I am sure I was not the first to think it was related to Konrad Zuse's Z3.
The Zuse Z3 is literally the only thing I know of which hooks up with the abbreviation "Z3" in the context of computers.