Function z3_sys::Z3_mk_bvsdiv

source · 
pub unsafe extern "C" fn Z3_mk_bvsdiv(
    c: Z3_context,
    t1: Z3_ast,
    t2: Z3_ast
) -> Z3_ast
Expand description

Two’s complement signed division.

It is defined in the following way:

  • The floor of t1/t2 if t2 is different from zero, and t1*t2 >= 0.

  • The ceiling of t1/t2 if t2 is different from zero, and t1*t2 < 0.

If t2 is zero, then the result is undefined.

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