stp.BVAddNoOverflow¶

stp.BVAddNoOverflow(a, b, signed)¶: z3py: the addition does not overflow (unsigned: no wrap; signed: not beyond the maximum).

STP

The Simple Theorem Prover

Overview

Building STP
Architecture

Running STP

The 3.x API (C++, C and Python)
API reference
- C++ API
- C API
- Python API
2.x C API handle lifetime
Array extensionality
Uninterpreted functions
Incremental solving
Bit-vector abstraction
Floating-point abstraction
Linear real arithmetic
SMT-LIB 2.7 compatibility

Source code layout
Testing
Developer tools
Making a release

Benchmarks

Source code on GitHub

©2018-2026, The STP Project. | Page source