diff --git a/lib/z3_api.h b/lib/z3_api.h index 8573d8b45..f3e33ff21 100644 --- a/lib/z3_api.h +++ b/lib/z3_api.h @@ -3725,6 +3725,13 @@ END_MLAPI_EXCLUDE */ Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(__in Z3_context c, __in Z3_ast a, unsigned i); + /** + \brief Return number of bound variables of quantifier. + + \pre Z3_get_ast_kind(a) == Z3_QUANTIFIER_AST + */ + unsigned Z3_API Z3_get_quantifier_num_bound(__in Z3_context c, __in Z3_ast a); + /** \brief Return symbol of the i'th bound variable. @@ -3746,13 +3753,6 @@ END_MLAPI_EXCLUDE */ Z3_ast Z3_API Z3_get_quantifier_body(__in Z3_context c, __in Z3_ast a); - /** - \brief Return number of bound variables of quantifier. - - \pre Z3_get_ast_kind(a) == Z3_QUANTIFIER_AST - */ - unsigned Z3_API Z3_get_quantifier_num_bound(__in Z3_context c, __in Z3_ast a); - /** \mlonly {3 {L Simplification}} \endmlonly