mk_divides method

Z3_ast mk_divides(
  1. Z3_context c,
  2. Z3_ast t1,
  3. Z3_ast t2
)

\brief Create division predicate.

The nodes \c t1 and \c t2 must be of integer sort. The predicate is true when \c t1 divides \c t2. For the predicate to be part of linear integer arithmetic, the first argument \c t1 must be a non-zero integer.

def_API('Z3_mk_divides', AST, (_in(CONTEXT), _in(AST), _in(AST)))

Implementation

Z3_ast mk_divides(
  Z3_context c,
  Z3_ast t1,
  Z3_ast t2,
) {
  return _mk_divides(
    c,
    t1,
    t2,
  );
}