Skip to main content


The z3guide was created by

  • Ruanqianqian (Lisa) Huang, UCSD, MSR Intern
  • Ayana Monroe, UNC, MSR Intern
  • Nikolaj Bjørner, Peli de Halleux, Microsoft Research

It relies on extensive help and use of the JavaScript bindings created by

  • Kevin Bakkot, Olaf Tomalka

with earlier wasm bindings by Leonardo Alt, Phillip Zucker, and Clément Pit-Claudel.

Material is based on an earlier rise4fun tutorial by Leonardo de Moura and Christoph Wintersteiger.