Function z3_sys::Z3_mk_div

pub unsafe extern "C" fn Z3_mk_div(
    c: Z3_context, 
    arg1: Z3_ast, 
    arg2: Z3_ast
) -> Z3_ast

Create an AST node representing arg1 div arg2.

The arguments must either both have int type or both have real type. If the arguments have int type, then the result type is an int type, otherwise the the result type is real.