{"id":21837,"library":"pyvcg","title":"PyVCG - Verification Condition Generator","description":"A Python library for generating verification conditions (VCs) from an intermediate language (IL) and emitting SMTLIB or interacting with solvers like CVC5 and Z3. Current version 1.0.10, supports Python 3.8+. Release cadence: irregular, with several minor releases in 2023-2024.","status":"active","version":"1.0.10","language":"python","source_language":"en","source_url":"https://github.com/florianschanda/PyVCG","tags":["verification","smt","vcg","cvc5","formal-methods"],"install":[{"cmd":"pip install pyvcg","lang":"bash","label":"Install from PyPI"}],"dependencies":[{"reason":"Required for the default CVC5 solver driver","package":"cvc5","optional":false},{"reason":"Required for the Z3 solver driver","package":"z3-solver","optional":true}],"imports":[{"note":"Solver is directly exported from pyvcg, not a submodule","wrong":"from pyvcg.solver import Solver","symbol":"Solver","correct":"from pyvcg import Solver"},{"note":"Literal is a top-level export","wrong":"from pyvcg.literal import Literal","symbol":"Literal","correct":"from pyvcg import Literal"},{"note":"Sort is directly available","wrong":null,"symbol":"Sort","correct":"from pyvcg import Sort"},{"note":"Top-level export","wrong":null,"symbol":"Record","correct":"from pyvcg import Record"}],"quickstart":{"code":"from pyvcg import Solver, Literal, Sort\n\nsolver = Solver()\n# Create a boolean constant\np = Literal('p', Sort.Bool)\nsolver.assert_formula(p)\nresult = solver.check()\nprint(result)","lang":"python","description":"Create a solver, add a boolean assertion, and check satisfiability."},"warnings":[{"fix":"Ensure your AST is a DAG; reuse nodes only without cycles.","message":"Recursive trees are rejected since version 1.0.9. Attempting to create a cyclic AST raises pyvcg.Recursion.","severity":"breaking","affected_versions":">=1.0.9"},{"fix":"Use the SMTLIB driver: set driver='smtlib' when creating Solver.","message":"The CVC5 API driver is being phased out in favor of SMTLIB-based driver. The CVC5 API driver may stop working in future releases.","severity":"deprecated","affected_versions":"all"},{"fix":"Use pip install 'cvc5==1.0.5' with PyVCG 1.0.3 or upgrade to a newer PyVCG.","message":"CVC5 version 1.0.7 is broken. PyVCG 1.0.3 pins to CVC5 1.0.5. Always match PyVCG's cvc5 dependency version.","severity":"gotcha","affected_versions":"1.0.3"},{"fix":"Upgrade to pyvcg >=1.0.2.","message":"String literals in SMTLIB output are escaped incorrectly in versions <1.0.2. Non-printable characters and quotes may cause solver parsing errors.","severity":"gotcha","affected_versions":"<1.0.2"}],"env_vars":null,"last_verified":"2026-04-27T00:00:00.000Z","next_check":"2026-07-26T00:00:00.000Z","problems":[{"fix":"Use: from pyvcg import Solver","cause":"Old versions or wrong import path; Solver is in the top-level __init__.py.","error":"ImportError: cannot import name 'Solver' from 'pyvcg'"},{"fix":"Ensure the AST is a DAG. For self-recursive records, use the add_component method with the record sort itself.","cause":"You constructed a recursive tree (cycle) which is forbidden since version 1.0.9.","error":"pyvcg.exceptions.Recursion: Cycle detected in AST"},{"fix":"Upgrade to pyvcg >=1.0.8 which supports Python 3.11+.","cause":"Old versions of pyvcg (<1.0.8) relied on CVC5 with limited Python support.","error":"ValueError: Unsupported Python version. Only Python 3.8 to 3.10 are supported."},{"fix":"Install cvc5: pip install cvc5 (ensure version matches PyVCG requirements). On Windows, use pyvcg >=1.0.7.","cause":"Missing CVC5 native library or incompatible version.","error":"OSError: libcvc5.so: cannot open shared object file"}],"ecosystem":"pypi","meta_description":null,"install_score":null,"install_tag":null,"quickstart_score":null,"quickstart_tag":null}