Two years ago I found the sources for that in my garage and put them on Github. The section "CPC4" is the modified (by Derek Oppen) Oppen-Nelson simplifier. This was originally in Franz LISP, and I converted them to Common LISP in 2017. It's not fully debugged, but it will run the basic solvers - add, subtract, multiply by constant, equality, inequality, theory of arrays, theory of structures, booleans, conditionals. That theory is completely decidable, and it covers most of the problems that cause range and subscript errors.
In our experience we haven't really seen it hang or do anything out of the ordinary - unsat problems on average seem to take longer than sat problems (it probably needs to scan a lot more).
We've pushed it to about a million variables or so and it has handled it well thought we might only be a the lower end of workloads.
: http://vmcaischool19.tecnico.ulisboa.pt/~vmcaischool19.daemo... (PowerPoint slides)
"Automated Verification of a Type-Safe Operating System"
Back in the day, I was foolish enough to implement my own (bitvector) solver. Hoping to outcompete with the assumption that I could encode heuristics informed by the domain (i.e., synthesis-specific). Turned out Z3's "general" heuristics were just faster. You could say, I let Nikolaj and Leonardo take it from there. For completeness, I also did experiment with a bunch of other solvers that were considered good at the time . (Have to caveat with the fact that CVC3, now CVC4, has always been on my list of future-to-try.)
 VS3: QF_BV (bitvector benchmarks) https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_B... -- apologies for the unimaginative name. VS3 stands for "(V)erification and (S)ynthesis using (S)MT (S)olvers"
 Example SMT instance: https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_B...
 Engineering for synthesis using SMT solvers: Chapter 6 of PhD: http://saurabh-srivastava.com/pubs/saurabh-srivastava-thesis...
Its facilities for program construction over the integers, sets, bitvectors, and reals make it an ideal candidate for this, especially when leveraging nu-Z3 for optimization over these.
With Z3, we’re able to construct optimized routes for robots extremely fast (especially with extensions over the techniques described in ), and as a direct result, derive value for our customers as execution time is important when dealing with expensive equipment.
A couple of my friends over at trail of bits do the work that saurabh does at synthetic minds, and their code is open source so you can take a look at it. 
It’s a decently active field of research, with solvers trading blows in the annual SMT-COMP . check out their instances to see how people really use them.
* Program synthesis overview: https://medium.com/@vidiborskiy/software-writes-software-pro...
* Program synthesis to make smart contract security more accessible: https://medium.com/@vidiborskiy/program-synthesis-smart-cont...
* Synthetic Minds (that is us): https://synthetic-minds.com/
You can help by telling me what questions would be most informative to answer. Promise to write a post addressing them directly.
(I suspect just because optimising 26! permutations is HARD.)
E.g. consider a window of (say) 6 keys and ask if any of the 6! permutations of them are better, for each possible window over the keyboard. This is similar to n-opt in TSP.
Make N as big as you can before your search falls down. Also try making a random move and local searching the region around the random move. Try all ~n^2 pairs of n/2 windows to jointly optimize. etc.
You can also make the local searches small by grouping keys and then search for the best permutation of whole group rather than single keys. Then alternate to windows of single keys.
I imagined something similar - since we can reasonably assume that XJQZKV are doing to be at the outer edges, we can take it from 26! to 6!20!. But even constraining it as much as possible, we still end up with 6!6!6!8! and 29 years of searching.
But I'll definitely give the sliding window approach a go, yeah.
Appears to be useful for static analysis and verification of a program.
A case study/glowing review from a programmer at Microsoft is here:
What do Z3 and other SMT solvers do if you ask them about undecidable questions? Do they potentially run forever?
You can use it to answer questions like "I want to reach this statement in this C# method, what values this method's inputs have to have for the execution to pass all the if checks and so on to reach this statement?".
More broadly speaking, you can use Z3 as a solver for Dynamic Symbolic Execution engine, where DSE is described in:
Source: I am the first author of "Generating Test Suites with Augmented Dynamic Symbolic Execution" leveraging Z3: https://www.microsoft.com/en-us/research/wp-content/uploads/...
Unless you're implementing solvers or caught up on the particulars of a solver's implementation, the best way to gauge this is to try it.
Try contacting the authors?
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.