{"id":21088,"library":"cvc5","title":"cvc5 Python Bindings","description":"Python bindings for cvc5, an efficient automatic theorem prover for Satisfiability Modulo Theories (SMT). Current version 1.3.3. Release cadence: irregular, ~3 major versions per year.","status":"active","version":"1.3.3","language":"python","source_language":"en","source_url":"https://github.com/cvc5/cvc5","tags":["SMT","theorem prover","solver","verification","cvc5"],"install":[{"cmd":"pip install cvc5","lang":"bash","label":"Standard install"}],"dependencies":[],"imports":[{"note":"cvc5 exposes two APIs: pythonic (Z3-like) and C++-style. The common mistake is using the low-level C++-style import incorrectly.","wrong":"from cvc5 import Solver","symbol":"Solver","correct":"from cvc5.pythonic import Solver"}],"quickstart":{"code":"from cvc5.pythonic import *\ns = Solver()\ns.add(Int('x') + Int('y') == 10)\nprint(s.check())","lang":"python","description":"Minimal example using the pythonic (Z3-compatible) API."},"warnings":[{"fix":"Migrate to pythonic API: replace old 'from cvc5 import ...' with 'from cvc5.pythonic import Solver, Int, etc.'","message":"In cvc5 1.0, the Python API was completely redesigned away from the CVC4-style API. Code written for cvc5 < 1.0 will not work. Use the pythonic API (from cvc5.pythonic import *) for Z3-like syntax.","severity":"breaking","affected_versions":"< 1.0"},{"fix":"Use Unicode strings (u32string) for string literals where applicable.","message":"mkString with std::wstring is deprecated in favor of std::u32string. Python bindings may be affected indirectly.","severity":"deprecated","affected_versions":">= 1.3.1"},{"fix":"Use correct imports: from cvc5.pythonic import And, Or, Not, Implies, etc.","message":"The pythonic API uses 'And', 'Or', 'Not' (capitalized) from cvc5.pythonic, but users may try lowercase from z3. This causes NameError.","severity":"gotcha","affected_versions":"all"},{"fix":"Use s.model() directly; it returns a cvc5 pythonic model object. Or use s.model().evaluate(term).","message":"The Solver object from cvc5.pythonic does not have a 'model()' method that returns a Z3-like model. Instead, use s.model() after s.check() returns sat, but the model API is different.","severity":"gotcha","affected_versions":"all"}],"env_vars":null,"last_verified":"2026-04-27T00:00:00.000Z","next_check":"2026-07-26T00:00:00.000Z","problems":[{"fix":"Run: pip install cvc5","cause":"cvc5 package not installed or installed in wrong environment.","error":"ModuleNotFoundError: No module named 'cvc5'"},{"fix":"Use: from cvc5.pythonic import Solver","cause":"Attempted to import Solver from the low-level C++ API (which does not expose it directly).","error":"ImportError: cannot import name 'Solver' from 'cvc5'"},{"fix":"Add: from cvc5.pythonic import *   OR   from cvc5.pythonic import Int, Bool, Solver, And, Or, ...","cause":"Forgot to import sort constructors like Int, Bool, etc. from cvc5.pythonic.","error":"NameError: name 'Int' is not defined"}],"ecosystem":"pypi","meta_description":null,"install_score":null,"install_tag":null,"quickstart_score":null,"quickstart_tag":null}