Function z3_sys::Z3_mk_bvsrem

pub unsafe extern "C" fn Z3_mk_bvsrem(
    c: Z3_context,
    t1: Z3_ast,
    t2: Z3_ast
) -> Z3_ast

Two’s complement signed remainder (sign follows dividend).

It is defined as t1 - (t1 /s t2) * t2, where /s represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of t1.

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector sort.

See also:

• Z3_mk_bvsmod