The nonlinear solver #

Methods of invocation #

By assertion. The nonlinear_arith solver can be invoked via an assert-by statement:

assert(Q) by(nonlinear_arith);

Proves Q via the nonlinear_arith solver.

assert(Q) by(nonlinear_arith) requires P;

Proves P ==> Q via the nonlinear_arith solver.

As a proof function. The nonlinear_arith solver can be invoked with a by(nonlinear_arith) on a proof function.

proof fn example(...) by(nonlinear_arith)
    requires P
    ensures Q
{ }

This proves P ==> Q via the nonlinear_arith solver.

Solver operation #

The solver uses Z3's theory of nonlinear arithmetic. This can often solve problems that involve multiplication or division of symbolic values. For example, commutativity axioms like a * b == b * a are accessible in this mode.