SMT solving
QF_BV
The quantifier-free SMT-LIB logic for fixed-width bit-vectors.
Definition
QF_BV
QF_BV contains quantifier-free formulas whose main data values are fixed-width bit-vectors.
The logic is useful for hardware, machine arithmetic, and bounded program behavior. Solvers often decide it by rewriting and bit-blasting the terms into SAT.
01
Example
An eight-bit overflow check can ask whether x + 1 is smaller than x under unsigned comparison.
02
Important distinction
QF_BV models bounded machine values, not mathematical integers of unlimited size.
After reading this article, you should be able to
- Define QF_BV in the sense used on this site.
- Explain why a QF_BV result may differ from the corresponding integer equation.