What the name means
QF means quantifier-free. A adds arrays; BV gives their indices and elements fixed-width bit-vector values.
Quantifier-free formulas have no explicit "for every" or "there exists" binders. They can still contain unknown values that the solver must find.
A bit-vector array can model byte-addressed memory: addresses are bit patterns and each read returns a byte. The array covers every address in its index sort. A store changes one value and produces a new array.
Address arithmetic wraps at its declared width. Two different-looking address expressions can therefore identify the same cell. The read and write rules must respect that equality.
Worked example
Read through a wrapped address
Use eight-bit addresses and eight-bit elements. Store the byte 7 at address zero, then read at the eight-bit sum 255 + 1.
- Define updated = store(memory, 0, 7), with all constants at eight-bit width.
- The address 255 + 1 wraps to zero.
- Ask whether the read at that address differs from 7. It reads the same location the store changed.
The query is unsat. Address wraparound makes the read return 7.
This is an authored mathematical example, not captured Axeyum output. Here, sat means the constraints can all hold; unsat means they cannot.
A contrasting case
Reading address one can return a different byte. The write at zero leaves address one unchanged.
Use cases
- Check memory operations in bounded program paths.
- Analyze address wraparound, aliasing, and byte updates in hardware or firmware models.
Modeling caution
The theory does not decide which addresses a real program may legally access. Allocation, pointer validity, and byte order need explicit rules in the encoding.
Axeyum coverage
The examples explain the logic's meaning. They do not establish complete Axeyum support for this division. Acceptance, solving, and evidence coverage depend on the input and the solver route.
This division appears in the site's retained regression scoreboard. Read the individual slices and their source records for the tested scope.
The results page also includes a retained comparison for this division. Its figures apply to the named benchmark list and resource budget.
A solver may return unknown if it cannot settle a query. That result establishes
neither sat nor unsat. Parsing a declared logic name alone does not prove support for every
formula in it.
Engine support documentation at the site's recorded snapshot, 03ae4a3c9, 2026-10-05.
Definitions and references
Definitions consulted September 6, 2026. The worked examples and use-case explanations are authored for this guide.