A Dumb Introduction to z3
Summary
An approachable, hands-on tour of using Z3 for constraint solving, with Rust bindings. It covers basic equations, real vs int types, multiple solutions, optimization (coin change), push/pop, and a Sudoku example, highlighting modeling constraints and interpreting solver output.