Contributions

• JNI bindings (Many thanks to Philippe Suter).
• Scala^Z3 (Many thanks to Philippe Suter).
• Racket API for Z3 (Many thanks to Siddharth Agarwal).
• Isabelle2009-1. Z3 is available in the Isabelle distribution as part of the smt tactic.
• Embedding of Z3 into HOL4 (Many thanks to Tjark Weber).
• Making use of F#'s math libraries together with Z3 (Many thanks to Byron Cook), F# source.
• Exploring the Z3 Theorem Prover (with a bit of LINQ) (Many thanks to Bart de Smet).
• Abstract interpretation using SMT solving (Many thanks to Ruzica Piskac).
• UTVPI solver as a Theory plugin (Many thanks to Michal Terepeta).
• The Z3 Axiom Profiler and The Z3 Inspector. The VCC system contains the Z3AxiomProfiler and Z3Inspector. These tools can be used to inspect and debug the search space covered by Z3 during long-running proofs and proof attempts.
• Sudoku Solving using Z3 (Many thanks to Dmitry Ermolov).
• Python bindings to Z3 (Many thanks to Sascha Böhme).