cvc5

library1.3.4pypypi✓ verified 87d ago

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.

data ai-ml

pip install cvc5

github ↗package ↗homepage ↗docs ↗changelog ↗

INSTALL

IMPORT

SIG · CVC5

cvc5

datapythonv1.3.4

Install

2.0s avg

Import

100ms

Disk

58MB

Pass rate

5/ 10

Env Coverage5 / 10

glibc

3.9–3.13

musl

3.9–3.13

Install & Compatibility

Where this runs

tested against v1.3.4 · 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

build_error

glibc

py 3.10–3.95 runs

installs and imports cleanly · install 2.0s · import 0.100s · 60MB

58MB installed

● package 58MB

Code

Verified usage

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

Solver

✓ from cvc5.pythonic import Solver

✗ from cvc5 import Solver

cvc5 exposes two APIs: pythonic (Z3-like) and C++-style. The common mistake is using the low-level C++-style import incorrectly.

Minimal example using the pythonic (Z3-compatible) API.

from cvc5.pythonic import * s = Solver() s.add(Int('x') + Int('y') == 10) print(s.check())

cvc5 --version

Debug

Known issues

breakingIn 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.

fix

Migrate to pythonic API: replace old 'from cvc5 import ...' with 'from cvc5.pythonic import Solver, Int, etc.'

affects: < 1.0

deprecatedmkString with std::wstring is deprecated in favor of std::u32string. Python bindings may be affected indirectly.

fix

Use Unicode strings (u32string) for string literals where applicable.

affects: >= 1.3.1

gotchaThe pythonic API uses 'And', 'Or', 'Not' (capitalized) from cvc5.pythonic, but users may try lowercase from z3. This causes NameError.

fix

Use correct imports: from cvc5.pythonic import And, Or, Not, Implies, etc.

affects: all

gotchaThe 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.

fix

Use s.model() directly; it returns a cvc5 pythonic model object. Or use s.model().evaluate(term).

affects: all

Errors

Common errors & fixes

ModuleNotFoundError: No module named 'cvc5'

cvc5 package not installed or installed in wrong environment.

fix

Run: pip install cvc5

ImportError: cannot import name 'Solver' from 'cvc5'

Attempted to import Solver from the low-level C++ API (which does not expose it directly).

fix

Use: from cvc5.pythonic import Solver

NameError: name 'Int' is not defined

Forgot to import sort constructors like Int, Bool, etc. from cvc5.pythonic.

fix

Add: from cvc5.pythonic import *   OR   from cvc5.pythonic import Int, Bool, Solver, And, Or, ...

Upgrade

Version history

1.3.4latest on PyPI · released May 7, 2026

Audit

Dependencies

No dependency data recorded yet.

Agent activity

14 hits · last 30 days

node

OpenAI (training)

Resources

githubhttps://github.com/cvc5/cvc5 ↗

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

homepagehttps://cvc5.github.io/ ↗

docshttps://cvc5.github.io/docs/ ↗

changeloghttps://github.com/cvc5/cvc5/blob/main/NEWS.md ↗