Z3-Owl

SMT Solver
Z3-Owl is an SMT solver built on top of Z3. It supports quantifier-free theories commonly used in verification and synthesis tasks.

Supported Theories

QF_BV Bit-vectors
QF_UFBV Uninterpreted functions + Bit-vectors
QF_ABV Arrays + Bit-vectors
QF_AUFBV Arrays + UF + Bit-vectors
QF_FP Floating-point arithmetic
QF_BVFP Bit-vectors + Floating-point
QF_LIA Linear integer arithmetic
QF_LRA Linear real arithmetic
QF_UFLIA UF + Linear integer arithmetic
QF_UFLRA UF + Linear real arithmetic

Research Group

Actively developed by the Programming Languages and Automated Reasoning Group
Zhejiang University, Hangzhou, China

Contact

For questions or collaboration inquiries:

rainoftime@gmail.com