diff --git a/src/api/z3_api.h b/src/api/z3_api.h index e8306bfb6..98bde7bcf 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6924,12 +6924,15 @@ END_MLAPI_EXCLUDE ); /*@}*/ - +#endif + + /** @name Deprecated Constraints API */ /*@{*/ +#ifdef CorML3 /** \brief Set the SMTLIB logic to be used in the given logical context. It is incorrect to invoke this function after invoking @@ -7111,7 +7114,9 @@ END_MLAPI_EXCLUDE __out Z3_model * m, __out Z3_ast* proof, __inout unsigned* core_size, __inout_ecount(num_assumptions) Z3_ast core[] ); +#endif +#ifdef CorML4 /** \brief Retrieve congruence class representatives for terms. @@ -7142,7 +7147,9 @@ END_MLAPI_EXCLUDE __in_ecount(num_terms) Z3_ast const terms[], __out_ecount(num_terms) unsigned class_ids[] ); +#endif +#ifdef CorML3 /** \brief Delete a model object.