{"id":68364,"library":"z3-sys","title":"Z3 Sys","description":"Low-level bindings for the Z3 SMT solver from Microsoft Research.","status":"active","version":"0.11.0","language":"rust","source_language":null,"source_url":"https://github.com/prove-rs/z3.rs","tags":["z3","smt","solver","bindings","formal-verification"],"install":[{"cmd":"# Cargo.toml\n[dependencies]\nz3-sys = \"0.11.0\"","lang":"toml","label":"Cargo.toml"},{"cmd":"cargo add z3-sys","lang":"bash","label":"cargo add"}],"dependencies":[],"imports":[{"symbol":"Z3_context","correct":"use z3_sys::Z3_context;"}],"quickstart":{"code":"use z3_sys::Z3_context;\n\nfn main() {\n    let cfg = unsafe { z3_sys::Z3_mk_config() };\n    let ctx = unsafe { z3_sys::Z3_mk_context(cfg) };\n    println!(\"Z3 context created\");\n}","lang":"rust","description":"Create a Z3 context using low-level bindings."},"warnings":[{"fix":"Install Z3 via your package manager or build from source.","message":"Requires the Z3 library installed on the system.","severity":"gotcha","affected_versions":">=0.11.0"}],"env_vars":null,"search_vec":"'bind':6,18 'formal':20 'formal-verif':19 'level':5 'low':4 'low-level':3 'microsoft':13 'research':14 'smt':10,16 'solver':11,17 'sys':2 'verif':21 'z3':1,9,15","created_at":"2026-06-17T17:48:48.610575+00:00","updated_at":"2026-06-17T17:48:48.610575+00:00","problems":[],"ecosystem":"crates","meta_description":null,"install_score":null,"quickstart_score":null,"quickstart_tag":null,"pypi_latest":null,"cli_name":null,"cli_version":null,"type":"library","homepage":"https://github.com/prove-rs/z3.rs","github":"https://github.com/prove-rs/z3.rs","docs":"https://docs.rs/z3-sys/","changelog":null,"pypi":null,"npm":null,"openapi_spec":null,"status_page":null,"smithery":null,"categories":["other"],"base_url":null,"auth_type":null,"provenance":{"verified_status":null,"verified_at":null,"last_verified":"2026-06-17","next_check":"2026-12-14","install_tag":null}}