Z3 supports arithmetic, fixed-size bit-vectors, extensional arrays, datatypes, uninterpreted functions, and quantifiers.

[4] The solver can be built using Visual Studio, a makefile or using CMake and runs on Windows, FreeBSD, Linux, and macOS.

The following script solves the two given equations, finding suitable values for the variables a and b: Result: In 2015, Z3 received the Programming Languages Software Award from ACM SIGPLAN.

[6][7] In 2018, Z3 received the Test of Time Award from the European Joint Conferences on Theory and Practice of Software (ETAPS).

[8] Microsoft researchers Nikolaj Bjørner and Leonardo de Moura received the 2019 Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of their work in advancing theorem proving with Z3.