Adventures in solving regex crosswords using the SMT solver, Z3. Further adventures and misadventures in making the solver fast, in which I learn about far more Z3 features than I knew existed. Some reflections on Z3 and SMT solvers more broadly.