What the name means

QF means quantifier-free. LRA means linear real arithmetic: unknown quantities are real numbers, and arithmetic uses fixed coefficients.

Quantifier-free formulas have no explicit "for every" or "there exists" binders. They can still contain unknown values that the solver must find.

Real arithmetic models quantities without floating-point rounding. A value can be fractional, and operations have their mathematical meaning. A finite decimal such as 0.1 denotes exactly one-tenth in this theory.

Expressions such as 2 × flow + reserve are linear. An unknown multiplied by another unknown is outside this fragment. The formula can use 'or' to describe alternative operating modes, each with its own linear rules.

Worked example

Split a required flow

Two pipes must supply exactly three units of flow. The first can carry at most two units, and the second at most one and a half.

  1. Let first and second be real numbers, each at least zero.
  2. Require first + second = 3, first ≤ 2, and second ≤ 3/2.
  3. Choose first = 3/2 and second = 3/2. The total is three and neither capacity is exceeded.

The query is sat. Fractions are valid values for these modeled flows.

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

Reduce both capacities to one. Their sum can then be at most two, so a total of three is unsat.

Use cases

  • Check resource balances when quantities may be divided.
  • Test linear conditions in control-system or geometric models before introducing rounding or nonlinear effects.

Modeling caution

A real-valued model does not establish the behavior of floating-point code. Use QF_FP when rounding, infinities, or signed zero can affect the result.

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.