z3 Microsoft’s Automated Theorem Prover based on SAT solving and Satisfiability Modulo Theories. Resources Solving puzzles using z3 More puzzles with z3 Modelling TLA in z3py Build script for OS X and Linux Author: Alcides Fonseca Language: English