{"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"],"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"},"provenance":{"verified_status":"passing","verified_at":"Sun Jun 28","last_verified":"Sun Jun 28","next_check":"Tue Jul 28","install_tag":null}}