I don't think it specifically states that this is z3-python (not a nitpick) which has an added bonus in that you can handle the SSA requirements if you're allocating inside a finite loop in the higher level language.
I was stuck on that at one time in the past, and then realized that not all the python code is in the scope of the solver and hence helps you automate those state additions.
These techniques aren't purely academic either, I've used them for reverse-engineering malware and software vulnerability analysis e.g. this inversion of MurmurHash3 https://www.josephkirwin.com/2018/04/07/z3-hash-inversions/
I have also used z3 to solve puzzles and toy problems, and found it magical, but can't seem to find any use case for it in practical problems :(
Personally, I have made extensive use of Z3 to find bugs in domain-specific language (DSL) compilers . You can use Z3 to encode the source code before and after a compiler optimization as a logic formula and then check whether the formulae are equivalent. If they are not, there is likely a semantic bug in the transformation pass of your compiler, meaning you have introduced a subtle logic mistake.
This style of verification really works best if your programming language is sufficiently restricted (not Turing-complete) or if you pick isolated segments in your code (e.g., functions). If that is the case, these methods can be extremely effective. We have found many semantic bugs in a short time period. In our case, Z3 was not even the bottleneck, performance-wise. It was our language interpreter. And because the language is sufficiently restricted, we can even run our tool as part of the compiler CI. So whenever a pull request is made, we can check whether it may lead to subtle issues in program translation.
Another useful aspect of using Z3 to represent a programming language is that you can also generate test cases for your programs. As far as I know, the Rosette  framework is intended to make all of this more approachable.
I remember reading an article about someone using Z3 to optimize the placement of cutout drawings on a piece of paper (kind of like a spritesheet) and optimizing for the smallest possible area in order to reduce the use of paper/materials. However, I can't seem to find the article anywhere.
One more use of z3 is as one of the available solvers for a tool called gnatprove , which is used to prove/verify the correctness of programs written in the SPARK subset of the Ada programming language. SPARK is used to program safety-critical aeronautical/military projects.
"practical uses" tends to mean whatever the speaker wants it to mean, so no guarantees, but i think it covers a number of small useful tasks, in addition to many of the common code golf type things.
Instead, Z3 is used to generate a small test data set, given the schema and the query. The core idea is to make sure the data set smokes out any mutation to the query. That is, if I use a join when the prof intended outer join to be used, or '<" instead of '<=', Z3 is used to generate a data set that will yield different results for the original and mutated queries.
Once a sufficiently robust data set is created that covers (an extensive list of) common errors, it can be used to vet student queries automatically. Interestingly, the system can award partial marks as well.
You can use it as part of your CI or during the development (there's even a neat "watch" mode, akin to auto-correct).
Fascicle 5 discusses "backtrack programming", and has some practical applications of that. Yeah yeah, you get N-Queens (probably no practical application), but also comma-free codes (obvious applications to communications / framing). Overall, Fascicle 5 builds up to the covering problem (https://en.wikipedia.org/wiki/Covering_problems) and practical applications of "covering problems with color" (a new category of problems proposed by Knuth: combining coloring problems and covering problems in one specification. Because his "Dancing Links + Algorithm X" seems to solve covering problems with color very efficiently).
Volume 4A (which contains what was formerly known as Fascicles 1 through 4) contains a huge chapter on bitwise hacks. Which while solved in Volume 4A, "could be solved" with an SMT / SAT solver like Z3.
Fascicle 6 is Knuth's dedicated section on SAT solvers. Its on my todo list... I haven't really done much with the book yet. I'll probably get to it after I finish Fascicle 5 (which seems more applicable to what I'm trying to do)
All of these "puzzles" are probably NP complete, and therefore "translate" to each other very easily. Covering problems are provably NP complete for example: and therefore can be solved with backtracking (aka: Dancing Links on Algorithm X), or an SAT solver like Z3.
SAT specifications (which Z3 solves directly) can also be converted into a covering problem, and therefore solved with Dancing Links / Algorithm X.
Having both techniques "in your pocket" so that you can pick-and-choose the right solver for the right problem (or maybe through the use of experimentation) is probably best. Unless someone solves P =/= NP any time soon, this ad-hoc methodology of "trying different techniques until something works" is our best bet at practically solving "puzzles" like traveling salesman (aka: airline travel), covering problems (aka: scheduling), integer optimization / functional equivalency of bitwise hacks (probably used in theorem proving / Verilog synthesis of circuits) or whatever else pops up in the real world.
A lot of these SAT / Backtracking problems are over graphs. Practical applications, like graph drawings (think the "dot" program: how to arrange a graph if it is planar... or if it is non-planar, how to arrange the graph such that it has the fewest number of crossings) is a combinatorics problem. So applications pop up in very unusual places: I'd argue that graph layout is a UI problem for example (a planar graph is easier to comprehend: or at least a graph with the fewest number of crossings)
A lot of these problems can be solved with "less powerful" techniques: maximum flow is itself a solved problem for example with numerous applications. Maximum-flow is "less than NP-complete" problem, but one that you might reach for Z3 unnecessarily.
Similarly: planar graph checking is solved and "less than NP-complete" IIRC. But you'll only really know that if you spend a lot of time researching graph theory.
You really want to use Z3 if you have suspicions that your problem is truly NP complete (or if you suspect is NP complete), and that the exhaustive search of all possibilities is your only option. Z3 is then useful because people have worked very, very, very hard on discovering "less-than NP complete" optimizations to subproblems, and can automatically solve these subproblems efficiently.
Some info here https://www.josephkirwin.com/2017/11/16/constraint-solver-ti...
Essentially though, you can model fixed width integers signed/unsigned using that and make assertions on things like integer overflow or change in signed-ness.
Uwaterloo did some work to abstract Strings ontop of BitVec so you can include them in your solver state too, worth a look to people that like this content https://z3string.github.io/