pyvcg

library1.0.10pypypi✓ verified 82d ago

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.

data ai-ml

pip install pyvcg

github ↗package ↗docs ↗

INSTALL

IMPORT

SIG · PYVCG

pyvcg

datapythonv1.0.10

Install

1.7s avg

Import

—

Disk

16MB

Pass rate

10/ 10

Env Coverage10 / 10

glibc

3.9–3.13

musl

3.9–3.13

Install & Compatibility

Where this runs

tested against v1.0.10 · pip install

no network on importno background threads

Install × environment matrix

Each cell = how many times install + import succeeded across repeated harness runs. Partial = flaky.
glibc = Debian/Ubuntu slim · musl = Alpine Linux

musl

py 3.10–3.95 runs

installs and imports cleanly · install 0.0s · import 0.000s · 18.1MB

glibc

py 3.10–3.95 runs

installs and imports cleanly · install 1.7s · import 0.000s · 19MB

16MB installed

● package 16MB

Code

Verified usage

Verified import paths — ran on the pinned version, not inferred.

Solver

✓ import pyvcg

✗ from pyvcg import Solver

Create a solver, add a boolean assertion, and check satisfiability.

from pyvcg import Solver, Literal, Sort solver = Solver() # Create a boolean constant p = Literal('p', Sort.Bool) solver.assert_formula(p) result = solver.check() print(result)

Debug

Known issues

breakingRecursive trees are rejected since version 1.0.9. Attempting to create a cyclic AST raises pyvcg.Recursion.

fix

Ensure your AST is a DAG; reuse nodes only without cycles.

affects: >=1.0.9

deprecatedThe CVC5 API driver is being phased out in favor of SMTLIB-based driver. The CVC5 API driver may stop working in future releases.

fix

Use the SMTLIB driver: set driver='smtlib' when creating Solver.

affects: all

gotchaCVC5 version 1.0.7 is broken. PyVCG 1.0.3 pins to CVC5 1.0.5. Always match PyVCG's cvc5 dependency version.

fix

Use pip install 'cvc5==1.0.5' with PyVCG 1.0.3 or upgrade to a newer PyVCG.

affects: 1.0.3

gotchaString literals in SMTLIB output are escaped incorrectly in versions <1.0.2. Non-printable characters and quotes may cause solver parsing errors.

fix

Upgrade to pyvcg >=1.0.2.

affects: <1.0.2

Upgrade

Version history

1.0.10latest on PyPI · released Jan 9, 2026

Audit

Dependencies

cvc5requiredRequired for the default CVC5 solver driver

z3-solveroptionalRequired for the Z3 solver driver

Agent activity

15 hits · last 30 days

node

OpenAI (training)

Resources

githubhttps://github.com/florianschanda/PyVCG ↗

packagehttps://pypi.org/project/pyvcg/ ↗

docshttps://github.com/pages/florianschanda/PyVCG/ ↗