Z3 Theorem Prover

Guest Lecture material at TU Wien October 2025

Lecture Overview

• Lecture 1 - introduction to SMT

• Lecture 2 - SMT solving fundamentals.

  • PDF.
  • Incremental Pre/in-processing for SMT
• Lecture 3-4 - Theory Solvers
  • PDF
• Lecture 4-5 - Solving Arithmetic
• Lecture 6 - Programming Z3
  • Solving Ranges
• Lecture 7 - Combining Theory Solvers
  • LIA * reduction
• Lecture 8 - Quantifiers
• Lecture 9 - Optimization Modulo Theories
  • PDF
• Lecture 10 - Topics in SMT

Project ideas