What the name means

LIA means linear integer arithmetic. Unlike QF_LIA, it permits explicit quantifiers over integer values.

A quantified variable can range over all integers, including negative ones. A universal statement must hold throughout that domain. An existential statement needs a suitable integer, possibly depending on a variable bound earlier.

The arithmetic remains linear: a fixed coefficient can multiply a variable, but two unknowns cannot be multiplied together. Linear integer arithmetic with quantifiers has decision methods, though quantifier structure can make solving expensive.

Worked example

Every integer has a larger integer

Assert that for every integer x there exists an integer y with y > x.

  1. Let x be any integer, without imposing an upper bound.
  2. Choose y = x + 1. The result is an integer and is strictly greater than x.
  3. The rule works for negative and positive values alike, so it covers the full quantified domain.

The formula is true and the asserted query is sat. Each choice of x can have its own y.

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

There exists one integer y greater than every integer x is unsat. Choosing x = y violates the required strict inequality.

Use cases

  • State linear relations that must hold for every integer input, with an integer response chosen afterward.
  • Express integer specifications before eliminating bound variables to obtain a simpler condition.

Modeling caution

A theorem about mathematical integers may fail for bounded machine integers. The successor of the largest unsigned machine value wraps, so it is not greater under unsigned order.

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.

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.