diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 7ba88a92d..f3d61c1cf 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1515,19 +1515,19 @@ extern "C" {
        although some parameters can be changed using #Z3_update_param_value.
        All main interaction with Z3 happens in the context of a \c Z3_context.
 
-       In contrast to #Z3_mk_context_rc, the life time of Z3_ast objects
+       In contrast to #Z3_mk_context_rc, the life time of \c Z3_ast objects
        are determined by the scope level of #Z3_solver_push and #Z3_solver_pop.
-       In other words, a Z3_ast object remains valid until there is a
-       call to Z3_solver_pop that takes the current scope below the level where
+       In other words, a \c Z3_ast object remains valid until there is a
+       call to #Z3_solver_pop that takes the current scope below the level where
        the object was created.
 
-       Note that all other reference counted objects, including Z3_model,
-       Z3_solver, Z3_func_interp have to be managed by the caller.
+       Note that all other reference counted objects, including \c Z3_model,
+       \c Z3_solver, \c Z3_func_interp have to be managed by the caller.
        Their reference counts are not handled by the context.
 
        Further remarks:
-       - Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are Z3_ast's.
-       - Z3 uses hash-consing, i.e., when the same Z3_ast is created twice,
+       - \c Z3_sort, \c Z3_func_decl, \c Z3_app, \c Z3_pattern are \c Z3_ast's.
+       - Z3 uses hash-consing, i.e., when the same \c Z3_ast is created twice,
          Z3 will return the same pointer twice.
 
        \sa Z3_del_context
@@ -1540,20 +1540,20 @@ extern "C" {
        \brief Create a context using the given configuration.
        This function is similar to #Z3_mk_context. However,
        in the context returned by this function, the user
-       is responsible for managing Z3_ast reference counters.
+       is responsible for managing \c Z3_ast reference counters.
        Managing reference counters is a burden and error-prone,
        but allows the user to use the memory more efficiently.
-       The user must invoke #Z3_inc_ref for any Z3_ast returned
-       by Z3, and #Z3_dec_ref whenever the Z3_ast is not needed
+       The user must invoke #Z3_inc_ref for any \c Z3_ast returned
+       by Z3, and #Z3_dec_ref whenever the \c Z3_ast is not needed
        anymore. This idiom is similar to the one used in
        BDD (binary decision diagrams) packages such as CUDD.
 
        Remarks:
 
-       - Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are Z3_ast's.
+       - \c Z3_sort, \c Z3_func_decl, \c Z3_app, \c Z3_pattern are \c Z3_ast's.
        - After a context is created, the configuration cannot be changed.
        - All main interaction with Z3 happens in the context of a \c Z3_context.
-       - Z3 uses hash-consing, i.e., when the same Z3_ast is created twice,
+       - Z3 uses hash-consing, i.e., when the same \c Z3_ast is created twice,
          Z3 will return the same pointer twice.
 
        def_API('Z3_mk_context_rc', CONTEXT, (_in(CONFIG),))
@@ -1615,7 +1615,7 @@ extern "C" {
        Starting at Z3 4.0, parameter sets are used to configure many components such as:
        simplifiers, tactics, solvers, etc.
 
-       \remark Reference counting must be used to manage parameter sets, even when the Z3_context was
+       \remark Reference counting must be used to manage parameter sets, even when the \c Z3_context was
        created using #Z3_mk_context instead of #Z3_mk_context_rc.
 
        def_API('Z3_mk_params', PARAMS, (_in(CONTEXT),))
@@ -4998,7 +4998,7 @@ extern "C" {
     Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s);
 
     /**
-       \brief translate model from context c to context \c dst.
+       \brief translate model from context \c c to context \c dst.
 
        def_API('Z3_model_translate', MODEL, (_in(CONTEXT), _in(MODEL), _in(CONTEXT)))
     */
diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h
index cc2091caa..1eaa1f64e 100644
--- a/src/api/z3_fpa.h
+++ b/src/api/z3_fpa.h
@@ -134,7 +134,7 @@ extern "C" {
         \param ebits number of exponent bits
         \param sbits number of significand bits
 
-        \remark ebits must be larger than 1 and sbits must be larger than 2.
+        \remark \c ebits must be larger than 1 and \c sbits must be larger than 2.
 
         def_API('Z3_mk_fpa_sort', SORT, (_in(CONTEXT), _in(UINT), _in(UINT)))
     */
@@ -213,7 +213,7 @@ extern "C" {
     Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c);
 
     /**
-        \brief Create a floating-point NaN of sort s.
+        \brief Create a floating-point NaN of sort \c s.
 
         \param c logical context
         \param s target sort
@@ -223,7 +223,7 @@ extern "C" {
     Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s);
 
     /**
-        \brief Create a floating-point infinity of sort s.
+        \brief Create a floating-point infinity of sort \c s.
 
         \param c logical context
         \param s target sort
@@ -236,7 +236,7 @@ extern "C" {
     Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative);
 
     /**
-        \brief Create a floating-point zero of sort s.
+        \brief Create a floating-point zero of sort \c s.
 
         \param c logical context
         \param s target sort
@@ -252,7 +252,7 @@ extern "C" {
         \brief Create an expression of FloatingPoint sort from three bit-vector expressions.
 
         This is the operator named `fp' in the SMT FP theory definition.
-        Note that \c sign is required to be a bit-vector of size 1. Significand and exponent
+        Note that \c sgn is required to be a bit-vector of size 1. Significand and exponent
         are required to be longer than 1 and 2 respectively. The FloatingPoint sort
         of the resulting expression is automatically determined from the bit-vector sizes
         of the arguments. The exponent is assumed to be in IEEE-754 biased representation.
@@ -276,7 +276,7 @@ extern "C" {
         \param v value
         \param ty sort
 
-        ty must be a FloatingPoint sort
+        \c ty must be a FloatingPoint sort
 
         \sa Z3_mk_numeral
 
@@ -294,7 +294,7 @@ extern "C" {
         \param v value
         \param ty sort
 
-        ty must be a FloatingPoint sort
+        \c ty must be a FloatingPoint sort
 
         \sa Z3_mk_numeral
 
@@ -309,7 +309,7 @@ extern "C" {
         \param v value
         \param ty result sort
 
-        ty must be a FloatingPoint sort
+        \c ty must be a FloatingPoint sort
 
         \sa Z3_mk_numeral
 
@@ -326,7 +326,7 @@ extern "C" {
         \param exp exponent
         \param ty result sort
 
-        ty must be a FloatingPoint sort
+        \c ty must be a FloatingPoint sort
 
         \sa Z3_mk_numeral
 
@@ -343,7 +343,7 @@ extern "C" {
         \param exp exponent
         \param ty result sort
 
-        ty must be a FloatingPoint sort
+        \c ty must be a FloatingPoint sort
 
         \sa Z3_mk_numeral
 
@@ -379,7 +379,7 @@ extern "C" {
         \param t1 term of FloatingPoint sort
         \param t2 term of FloatingPoint sort
 
-        rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.
+        \c rm must be of RoundingMode sort, \c t1 and \c t2 must have the same FloatingPoint sort.
 
         def_API('Z3_mk_fpa_add', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
     */
@@ -393,7 +393,7 @@ extern "C" {
         \param t1 term of FloatingPoint sort
         \param t2 term of FloatingPoint sort
 
-        rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.
+        \c rm must be of RoundingMode sort, \c t1 and \c t2 must have the same FloatingPoint sort.
 
         def_API('Z3_mk_fpa_sub', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
     */
@@ -407,7 +407,7 @@ extern "C" {
         \param t1 term of FloatingPoint sort
         \param t2 term of FloatingPoint sort
 
-        rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.
+        \c rm must be of RoundingMode sort, \c t1 and \c t2 must have the same FloatingPoint sort.
 
         def_API('Z3_mk_fpa_mul', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
     */
@@ -421,7 +421,7 @@ extern "C" {
         \param t1 term of FloatingPoint sort.
         \param t2 term of FloatingPoint sort
 
-        The nodes rm must be of RoundingMode sort t1 and t2 must have the same FloatingPoint sort.
+        The nodes \c rm must be of RoundingMode sort, \c t1 and \c t2 must have the same FloatingPoint sort.
 
         def_API('Z3_mk_fpa_div', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
     */
@@ -436,9 +436,9 @@ extern "C" {
         \param t2 term of FloatingPoint sort
         \param t3 term of FloatingPoint sort
 
-        The result is round((t1 * t2) + t3)
+        The result is \ccode{round((t1 * t2) + t3)}.
 
-        rm must be of RoundingMode sort, t1, t2, and t3 must have the same FloatingPoint sort.
+        \c rm must be of RoundingMode sort, \c t1, \c t2, and \c t3 must have the same FloatingPoint sort.
 
         def_API('Z3_mk_fpa_fma', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(AST)))
     */
@@ -451,7 +451,7 @@ extern "C" {
         \param rm term of RoundingMode sort
         \param t term of FloatingPoint sort
 
-        rm must be of RoundingMode sort, t must have FloatingPoint sort.
+        \c rm must be of RoundingMode sort, \c t must have FloatingPoint sort.
 
         def_API('Z3_mk_fpa_sqrt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
@@ -464,7 +464,7 @@ extern "C" {
         \param t1 term of FloatingPoint sort
         \param t2 term of FloatingPoint sort
 
-        t1 and t2 must have the same FloatingPoint sort.
+        \c t1 and \c t2 must have the same FloatingPoint sort.
 
         def_API('Z3_mk_fpa_rem', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
@@ -478,7 +478,7 @@ extern "C" {
         \param rm term of RoundingMode sort
         \param t term of FloatingPoint sort
 
-        t must be of FloatingPoint sort.
+        \c t must be of FloatingPoint sort.
 
         def_API('Z3_mk_fpa_round_to_integral', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
@@ -491,7 +491,7 @@ extern "C" {
         \param t1 term of FloatingPoint sort
         \param t2 term of FloatingPoint sort
 
-        t1, t2 must have the same FloatingPoint sort.
+        \c t1, \c t2 must have the same FloatingPoint sort.
 
         def_API('Z3_mk_fpa_min', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
@@ -504,7 +504,7 @@ extern "C" {
         \param t1 term of FloatingPoint sort
         \param t2 term of FloatingPoint sort
 
-        t1, t2 must have the same FloatingPoint sort.
+        \c t1, \c t2 must have the same FloatingPoint sort.
 
         def_API('Z3_mk_fpa_max', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
@@ -517,7 +517,7 @@ extern "C" {
         \param t1 term of FloatingPoint sort
         \param t2 term of FloatingPoint sort
 
-        t1 and t2 must have the same FloatingPoint sort.
+        \c t1 and \c t2 must have the same FloatingPoint sort.
 
         def_API('Z3_mk_fpa_leq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
@@ -530,7 +530,7 @@ extern "C" {
         \param t1 term of FloatingPoint sort
         \param t2 term of FloatingPoint sort
 
-        t1 and t2 must have the same FloatingPoint sort.
+        \c t1 and \c t2 must have the same FloatingPoint sort.
 
         def_API('Z3_mk_fpa_lt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
@@ -543,7 +543,7 @@ extern "C" {
         \param t1 term of FloatingPoint sort
         \param t2 term of FloatingPoint sort
 
-        t1 and t2 must have the same FloatingPoint sort.
+        \c t1 and \c t2 must have the same FloatingPoint sort.
 
         def_API('Z3_mk_fpa_geq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
@@ -556,7 +556,7 @@ extern "C" {
         \param t1 term of FloatingPoint sort
         \param t2 term of FloatingPoint sort
 
-        t1 and t2 must have the same FloatingPoint sort.
+        \c t1 and \c t2 must have the same FloatingPoint sort.
 
         def_API('Z3_mk_fpa_gt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
@@ -569,93 +569,93 @@ extern "C" {
         \param t1 term of FloatingPoint sort
         \param t2 term of FloatingPoint sort
 
-        Note that this is IEEE 754 equality (as opposed to SMT-LIB =).
+        Note that this is IEEE 754 equality (as opposed to SMT-LIB \ccode{=}).
 
-        t1 and t2 must have the same FloatingPoint sort.
+        \c t1 and \c t2 must have the same FloatingPoint sort.
 
         def_API('Z3_mk_fpa_eq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2);
 
     /**
-        \brief Predicate indicating whether t is a normal floating-point number.
+        \brief Predicate indicating whether \c t is a normal floating-point number.
 
         \param c logical context
         \param t term of FloatingPoint sort
 
-        t must have FloatingPoint sort.
+        \c t must have FloatingPoint sort.
 
         def_API('Z3_mk_fpa_is_normal', AST, (_in(CONTEXT),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t);
 
     /**
-        \brief Predicate indicating whether t is a subnormal floating-point number.
+        \brief Predicate indicating whether \c t is a subnormal floating-point number.
 
         \param c logical context
         \param t term of FloatingPoint sort
 
-        t must have FloatingPoint sort.
+        \c t must have FloatingPoint sort.
 
         def_API('Z3_mk_fpa_is_subnormal', AST, (_in(CONTEXT),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t);
 
     /**
-        \brief Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero.
+        \brief Predicate indicating whether \c t is a floating-point number with zero value, i.e., +zero or -zero.
 
         \param c logical context
         \param t term of FloatingPoint sort
 
-        t must have FloatingPoint sort.
+        \c t must have FloatingPoint sort.
 
         def_API('Z3_mk_fpa_is_zero', AST, (_in(CONTEXT),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t);
 
    /**
-        \brief Predicate indicating whether t is a floating-point number representing +oo or -oo.
+        \brief Predicate indicating whether \c t is a floating-point number representing +oo or -oo.
 
         \param c logical context
         \param t term of FloatingPoint sort
 
-        t must have FloatingPoint sort.
+        \c t must have FloatingPoint sort.
 
         def_API('Z3_mk_fpa_is_infinite', AST, (_in(CONTEXT),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t);
 
     /**
-        \brief Predicate indicating whether t is a NaN.
+        \brief Predicate indicating whether \c t is a NaN.
 
         \param c logical context
         \param t term of FloatingPoint sort
 
-        t must have FloatingPoint sort.
+        \c t must have FloatingPoint sort.
 
         def_API('Z3_mk_fpa_is_nan', AST, (_in(CONTEXT),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t);
 
     /**
-        \brief Predicate indicating whether t is a negative floating-point number.
+        \brief Predicate indicating whether \c t is a negative floating-point number.
 
         \param c logical context
         \param t term of FloatingPoint sort
 
-        t must have FloatingPoint sort.
+        \c t must have FloatingPoint sort.
 
         def_API('Z3_mk_fpa_is_negative', AST, (_in(CONTEXT),_in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_is_negative(Z3_context c, Z3_ast t);
 
     /**
-        \brief Predicate indicating whether t is a positive floating-point number.
+        \brief Predicate indicating whether \c t is a positive floating-point number.
 
         \param c logical context
         \param t term of FloatingPoint sort
 
-        t must have FloatingPoint sort.
+        \c t must have FloatingPoint sort.
 
         def_API('Z3_mk_fpa_is_positive', AST, (_in(CONTEXT),_in(AST)))
     */
@@ -664,15 +664,15 @@ extern "C" {
     /**
         \brief Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
 
-        Produces a term that represents the conversion of a bit-vector term bv to a
-        floating-point term of sort s.
+        Produces a term that represents the conversion of a bit-vector term \c bv to a
+        floating-point term of sort \c s.
 
         \param c logical context
         \param bv a bit-vector term
         \param s floating-point sort
 
-        s must be a FloatingPoint sort, t must be of bit-vector sort, and the bit-vector
-        size of bv must be equal to ebits+sbits of s. The format of the bit-vector is
+        \c s must be a FloatingPoint sort, \c t must be of bit-vector sort, and the bit-vector
+        size of \c bv must be equal to \ccode{ebits+sbits} of \c s. The format of the bit-vector is
         as defined by the IEEE 754-2008 interchange format.
 
         def_API('Z3_mk_fpa_to_fp_bv', AST, (_in(CONTEXT),_in(AST),_in(SORT)))
@@ -682,16 +682,16 @@ extern "C" {
     /**
         \brief Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
 
-        Produces a term that represents the conversion of a floating-point term t to a
-        floating-point term of sort s. If necessary, the result will be rounded according
-        to rounding mode rm.
+        Produces a term that represents the conversion of a floating-point term \c t to a
+        floating-point term of sort \c s. If necessary, the result will be rounded according
+        to rounding mode \c rm.
 
         \param c logical context
         \param rm term of RoundingMode sort
         \param t term of FloatingPoint sort
         \param s floating-point sort
 
-        s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of floating-point sort.
+        \c s must be a FloatingPoint sort, \c rm must be of RoundingMode sort, \c t must be of floating-point sort.
 
         def_API('Z3_mk_fpa_to_fp_float', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
     */
@@ -700,16 +700,16 @@ extern "C" {
     /**
         \brief Conversion of a term of real sort into a term of FloatingPoint sort.
 
-        Produces a term that represents the conversion of term t of real sort into a
-        floating-point term of sort s. If necessary, the result will be rounded according
-        to rounding mode rm.
+        Produces a term that represents the conversion of term \c t of real sort into a
+        floating-point term of sort \c s. If necessary, the result will be rounded according
+        to rounding mode \c rm.
 
         \param c logical context
         \param rm term of RoundingMode sort
         \param t term of Real sort
         \param s floating-point sort
 
-        s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of real sort.
+        \c s must be a FloatingPoint sort, \c rm must be of RoundingMode sort, \c t must be of real sort.
 
         def_API('Z3_mk_fpa_to_fp_real', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
     */
@@ -718,17 +718,17 @@ extern "C" {
     /**
         \brief Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
 
-        Produces a term that represents the conversion of the bit-vector term t into a
-        floating-point term of sort s. The bit-vector t is taken to be in signed
+        Produces a term that represents the conversion of the bit-vector term \c t into a
+        floating-point term of sort \c s. The bit-vector \c t is taken to be in signed
         2's complement format. If necessary, the result will be rounded according
-        to rounding mode rm.
+        to rounding mode \c rm.
 
         \param c logical context
         \param rm term of RoundingMode sort
         \param t term of bit-vector sort
         \param s floating-point sort
 
-        s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of bit-vector sort.
+        \c s must be a FloatingPoint sort, \c rm must be of RoundingMode sort, \c t must be of bit-vector sort.
 
         def_API('Z3_mk_fpa_to_fp_signed', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
     */
@@ -737,17 +737,17 @@ extern "C" {
     /**
         \brief Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.
 
-        Produces a term that represents the conversion of the bit-vector term t into a
-        floating-point term of sort s. The bit-vector t is taken to be in unsigned
+        Produces a term that represents the conversion of the bit-vector term \c t into a
+        floating-point term of sort \c s. The bit-vector \c t is taken to be in unsigned
         2's complement format. If necessary, the result will be rounded according
-        to rounding mode rm.
+        to rounding mode \c rm.
 
         \param c logical context
         \param rm term of RoundingMode sort
         \param t term of bit-vector sort
         \param s floating-point sort
 
-        s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of bit-vector sort.
+        \c s must be a FloatingPoint sort, \c rm must be of RoundingMode sort, \c t must be of bit-vector sort.
 
         def_API('Z3_mk_fpa_to_fp_unsigned', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
     */
@@ -756,9 +756,9 @@ extern "C" {
     /**
         \brief Conversion of a floating-point term into an unsigned bit-vector.
 
-        Produces a term that represents the conversion of the floating-point term t into a
-        bit-vector term of size sz in unsigned 2's complement format. If necessary, the result
-        will be rounded according to rounding mode rm.
+        Produces a term that represents the conversion of the floating-point term \c t into a
+        bit-vector term of size \c sz in unsigned 2's complement format. If necessary, the result
+        will be rounded according to rounding mode \c rm.
 
         \param c logical context
         \param rm term of RoundingMode sort
@@ -772,9 +772,9 @@ extern "C" {
     /**
         \brief Conversion of a floating-point term into a signed bit-vector.
 
-        Produces a term that represents the conversion of the floating-point term t into a
-        bit-vector term of size sz in signed 2's complement format. If necessary, the result
-        will be rounded according to rounding mode rm.
+        Produces a term that represents the conversion of the floating-point term \c t into a
+        bit-vector term of size \c sz in signed 2's complement format. If necessary, the result
+        will be rounded according to rounding mode \c rm.
 
         \param c logical context
         \param rm term of RoundingMode sort
@@ -788,7 +788,7 @@ extern "C" {
     /**
         \brief Conversion of a floating-point term into a real-numbered term.
 
-        Produces a term that represents the conversion of the floating-point term t into a
+        Produces a term that represents the conversion of the floating-point term \c t into a
         real number. Note that this type of conversion will often result in non-linear
         constraints over real terms.
 
@@ -936,7 +936,7 @@ extern "C" {
         \param c logical context
         \param t a floating-point numeral
 
-        Remarks: The significand s is always 0.0 <= s < 2.0; the resulting string is long
+        Remarks: The significand \c s is always \ccode{0.0 <= s < 2.0}; the resulting string is long
         enough to represent the real significand precisely.
 
         def_API('Z3_fpa_get_numeral_significand_string', STRING, (_in(CONTEXT), _in(AST)))
@@ -951,8 +951,8 @@ extern "C" {
         \param n pointer to output uint64
 
         Remarks: This function extracts the significand bits in `t`, without the
-        hidden bit or normalization. Sets the Z3_INVALID_ARG error code if the
-        significand does not fit into a uint64. NaN is an invalid argument.
+        hidden bit or normalization. Sets the \c Z3_INVALID_ARG error code if the
+        significand does not fit into a \c uint64. NaN is an invalid argument.
 
         def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64)))
     */
@@ -1007,7 +1007,7 @@ extern "C" {
         \param c logical context
         \param t term of FloatingPoint sort
 
-        t must have FloatingPoint sort. The size of the resulting bit-vector is automatically
+        \c t must have FloatingPoint sort. The size of the resulting bit-vector is automatically
         determined.
 
         Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
@@ -1021,9 +1021,9 @@ extern "C" {
     /**
         \brief Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
 
-        Produces a term that represents the conversion of sig * 2^exp into a
-        floating-point term of sort s. If necessary, the result will be rounded
-        according to rounding mode rm.
+        Produces a term that represents the conversion of \ccode{sig * 2^exp} into a
+        floating-point term of sort \c s. If necessary, the result will be rounded
+        according to rounding mode \c rm.
 
         \param c logical context
         \param rm term of RoundingMode sort
@@ -1031,7 +1031,7 @@ extern "C" {
         \param sig significand term of Real sort
         \param s FloatingPoint sort
 
-        s must be a FloatingPoint sort, rm must be of RoundingMode sort, exp must be of int sort, sig must be of real sort.
+        \c s must be a FloatingPoint sort, \c rm must be of RoundingMode sort, \c exp must be of int sort, \c sig must be of real sort.
 
         def_API('Z3_mk_fpa_to_fp_int_real', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(SORT)))
     */
diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h
index 8f1275774..a8ffd45ab 100644
--- a/src/api/z3_optimization.h
+++ b/src/api/z3_optimization.h
@@ -228,8 +228,8 @@ extern "C" {
     /**
        \brief Retrieve lower bound value or approximation for the i'th optimization objective.
               The returned vector is of length 3. It always contains numerals.
-              The three numerals are coefficients a, b, c and encode the result of \c Z3_optimize_get_lower
-              a * infinity + b + c * epsilon.
+              The three numerals are coefficients \c a, \c b, \c c and encode the result of
+              #Z3_optimize_get_lower \ccode{a * infinity + b + c * epsilon}.
               
        \param c - context
        \param o - optimization context
@@ -330,7 +330,7 @@ extern "C" {
     /**
        \brief Return objectives on the optimization context.
        If the objective function is a max-sat objective it is returned
-       as a Pseudo-Boolean (minimization) sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...)
+       as a Pseudo-Boolean (minimization) sum of the form \ccode{(+ (if f1 w1 0) (if f2 w2 0) ...)}
        If the objective function is entered as a maximization objective, then return
        the corresponding minimization objective. In this way the resulting objective
        function is always returned as a minimization objective.
diff --git a/src/api/z3_polynomial.h b/src/api/z3_polynomial.h
index 0561bfd9c..5f4815d02 100644
--- a/src/api/z3_polynomial.h
+++ b/src/api/z3_polynomial.h
@@ -36,9 +36,8 @@ extern "C" {
 
        \pre \c p, \c q and \c x are Z3 expressions where \c p and \c q are arithmetic terms.
        Note that, any subterm that cannot be viewed as a polynomial is assumed to be a variable.
-       Example: f(a) is a considered to be a variable in the polynomial
-
-       f(a)*f(a) + 2*f(a) + 1
+       Example: \ccode{f(a)} is a considered to be a variable in the polynomial \ccode{
+       f(a)*f(a) + 2*f(a) + 1}
 
        def_API('Z3_polynomial_subresultants', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
     */
diff --git a/src/api/z3_rcf.h b/src/api/z3_rcf.h
index dc025bddd..4e4ecbd15 100644
--- a/src/api/z3_rcf.h
+++ b/src/api/z3_rcf.h
@@ -74,7 +74,7 @@ extern "C" {
     Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c);
 
     /**
-       \brief Store in roots the roots of the polynomial <tt>a[n-1]*x^{n-1} + ... + a[0]</tt>.
+       \brief Store in roots the roots of the polynomial \ccode{a[n-1]*x^{n-1} + ... + a[0]}.
        The output vector \c roots must have size \c n.
        It returns the number of roots of the polynomial.
 
@@ -85,91 +85,91 @@ extern "C" {
     unsigned Z3_API Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]);
 
     /**
-       \brief Return the value a + b.
+       \brief Return the value \ccode{a + b}.
 
        def_API('Z3_rcf_add', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
     */
     Z3_rcf_num Z3_API Z3_rcf_add(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
     /**
-       \brief Return the value a - b.
+       \brief Return the value \ccode{a - b}.
 
        def_API('Z3_rcf_sub', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
     */
     Z3_rcf_num Z3_API Z3_rcf_sub(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
     /**
-       \brief Return the value a * b.
+       \brief Return the value \ccode{a * b}.
 
        def_API('Z3_rcf_mul', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
     */
     Z3_rcf_num Z3_API Z3_rcf_mul(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
     /**
-       \brief Return the value a / b.
+       \brief Return the value \ccode{a / b}.
 
        def_API('Z3_rcf_div', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
     */
     Z3_rcf_num Z3_API Z3_rcf_div(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
     /**
-       \brief Return the value -a
+       \brief Return the value \ccode{-a}.
 
        def_API('Z3_rcf_neg', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM)))
     */
     Z3_rcf_num Z3_API Z3_rcf_neg(Z3_context c, Z3_rcf_num a);
 
     /**
-       \brief Return the value 1/a
+       \brief Return the value \ccode{1/a}.
 
        def_API('Z3_rcf_inv', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM)))
     */
     Z3_rcf_num Z3_API Z3_rcf_inv(Z3_context c, Z3_rcf_num a);
 
     /**
-       \brief Return the value a^k
+       \brief Return the value \ccode{a^k}.
 
        def_API('Z3_rcf_power', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(UINT)))
     */
     Z3_rcf_num Z3_API Z3_rcf_power(Z3_context c, Z3_rcf_num a, unsigned k);
 
     /**
-       \brief Return \c true if a < b
+       \brief Return \c true if \ccode{a < b}.
 
        def_API('Z3_rcf_lt', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
     */
     bool Z3_API Z3_rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
     /**
-       \brief Return \c true if a > b
+       \brief Return \c true if \ccode{a > b}.
 
        def_API('Z3_rcf_gt', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
     */
     bool Z3_API Z3_rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
     /**
-       \brief Return \c true if a <= b
+       \brief Return \c true if \ccode{a <= b}.
 
        def_API('Z3_rcf_le', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
     */
     bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
     /**
-       \brief Return \c true if a >= b
+       \brief Return \c true if \ccode{a >= b}.
 
        def_API('Z3_rcf_ge', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
     */
     bool Z3_API Z3_rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
     /**
-       \brief Return \c true if a == b
+       \brief Return \c true if \ccode{a == b}.
 
        def_API('Z3_rcf_eq', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
     */
     bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
     /**
-       \brief Return \c true if a != b
+       \brief Return \c true if \ccode{a != b}.
 
        def_API('Z3_rcf_neq', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
     */
@@ -191,7 +191,7 @@ extern "C" {
 
     /**
        \brief Extract the "numerator" and "denominator" of the given RCF numeral.
-       We have that a = n/d, moreover n and d are not represented using rational functions.
+       We have that \ccode{a = n/d}, moreover \c n and \c d are not represented using rational functions.
 
        def_API('Z3_rcf_get_numerator_denominator', VOID, (_in(CONTEXT), _in(RCF_NUM), _out(RCF_NUM), _out(RCF_NUM)))
     */
diff --git a/src/api/z3_spacer.h b/src/api/z3_spacer.h
index bd6b7d01d..09cbe6a51 100644
--- a/src/api/z3_spacer.h
+++ b/src/api/z3_spacer.h
@@ -48,7 +48,7 @@ extern "C" {
      /**
        \brief Retrieve a bottom-up (from query) sequence of ground facts
 
-       The previous call to Z3_fixedpoint_query must have returned \c Z3_L_TRUE.
+       The previous call to #Z3_fixedpoint_query must have returned \c Z3_L_TRUE.
 
        def_API('Z3_fixedpoint_get_ground_sat_answer', AST, (_in(CONTEXT), _in(FIXEDPOINT)))
     */