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