I'm disappointed. I thought I was going to see the solver generates code that finds the largest palindrome. I recall how mini-Kanren was used to generate quines. Z3 should be capable of similar feats.
Yeah, that was my first thought, too, but the article is still inspirational. Could code generation ever be fast enough for practical problems? I'm wondering how far we could get if the generated code for each problem is cached between compiles (so we build up a huge database of solutions over time) and also reused, based on the satisfied constraints, when searching for solutions to more complex problems (much like developers reuse existing functions).
I good start might be getting RSpec and generating the correct scaffolds for it in Rails. It would only work for a tiny subset of problems but it would be a start, and also produce something many web developers could see the real world use for.
Well, as benjamincburns says in another comment, Z3 is basically equivalent to the finite domain solver of a Prolog. Since mini-Kanren is a Prolog, it is not surprising that it is more powerful. Otherwise Z3 would also be a Prolog :).