LOVE Spring School 2016

SMT Solvers

Martina Seidl

Software

• Z3 (online version)
• Lingeling (SAT Solver)
• Limboole (SAT Solver with Infix Format)
• Boolector

Examples

• bool.smt2
• middle.smt2
• middle2.smt2
• middle32.smt2
• ackbitblasted.limboole
• ack.smt2
• EUF.smt2
• UFNIA_EUF.smt2
• dpllt.smt2