What the name means

QF means quantifier-free. BV means bit-vectors: values made of a fixed number of bits, each zero or one.

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 has a declared width. Eight bits have 256 possible patterns. Addition keeps only the low eight bits, so the unsigned value 255 plus one becomes zero. This wraparound is part of the meaning of the operation.

The same pattern can be read as signed or unsigned. The comparison operator chooses the interpretation. A solver can also reason about individual bits, shifts, joined bit patterns, and extracted ranges of bits.

Worked example

Find an increment that wraps

A counter is an eight-bit value. Find a starting value whose increment is zero.

  1. Declare counter as an eight-bit vector.
  2. Require its eight-bit sum with one to equal zero.
  3. Set every counter bit to one. Its unsigned value is 255; adding one produces 256, whose low eight bits are zero.

The query is sat. The all-ones pattern supplies the requested counter value.

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

Add the condition that counter is unsigned-less-than 255. The query becomes unsat because the all-ones pattern was the only value that wrapped to zero.

Use cases

  • Find overflow and mask errors in machine-integer code.
  • Check whether two combinational hardware circuits produce different outputs for any input.

Modeling caution

Signed comparison, unsigned comparison, and the source language's overflow rules are separate choices. Fixed-width wrapping arithmetic does not by itself model every rule of C or Rust.

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.