Function Z3_mk_bvsrem 

pub unsafe extern "C" fn Z3_mk_bvsrem(
    c: Z3_context,
    t1: Z3_ast,
    t2: Z3_ast,
) -> Option<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