{"library":"z3-solver","type":"library","category":null,"description":"Z3 is a high-performance theorem prover developed by Microsoft Research, primarily used for Satisfiability Modulo Theories (SMT) problems. It supports various data types including bitvectors, booleans, arrays, floating point numbers, and strings, making it a versatile tool for formal verification, software/hardware testing, and constraint solving. The library is actively maintained with frequent minor releases and is currently on version 4.16.0.0.","language":"python","status":"active","version":"4.16.0.0","tags":["smt","solver","verification","logic","constraint-solving","formal-methods"],"last_verified":"Thu May 21","install":[{"cmd":"pip install z3-solver","imports":["from z3 import *","import z3"]}],"homepage":null,"github":"https://github.com/Z3Prover/z3","docs":null,"changelog":null,"pypi":"https://pypi.org/project/z3-solver/","npm":null,"openapi_spec":null,"status_page":null,"smithery":null,"compatibility":{"summary":{"python_range":"3.10–3.9","success_rate":50,"avg_install_s":2.4,"avg_import_s":0.47,"wheel_type":"wheel"},"url":"https://checklist.day/v1/registry/z3-solver/compatibility"}}