diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c
index 4ebe7c31425..a9c472f37a9 100644
--- a/examples/c/test_capi.c
+++ b/examples/c/test_capi.c
@@ -22,11 +22,11 @@ Copyright (c) 2015 Microsoft Corporation
 /**
    \defgroup capi_ex C API examples
 */
-/*@{*/
+/**@{*/
 /**
    @name Auxiliary Functions
 */
-/*@{*/
+/**@{*/
 
 /**
    \brief exit gracefully in case of error.
@@ -694,12 +694,12 @@ void display_version()
     Z3_get_version(&major, &minor, &build, &revision);
     printf("Z3 %d.%d.%d.%d\n", major, minor, build, revision);
 }
-/*@}*/
+/**@}*/
 
 /**
    @name Examples
 */
-/*@{*/
+/**@{*/
 /**
    \brief "Hello world" example: create a Z3 logical context, and delete it.
 */
@@ -2947,8 +2947,8 @@ void mk_model_example() {
     Z3_del_context(ctx);
 }
 
-/*@}*/
-/*@}*/
+/**@}*/
+/**@}*/
 
 
 
diff --git a/examples/maxsat/maxsat.c b/examples/maxsat/maxsat.c
index a0c0cfeec8b..3e8bf76a514 100644
--- a/examples/maxsat/maxsat.c
+++ b/examples/maxsat/maxsat.c
@@ -15,7 +15,7 @@ Copyright (c) 2015 Microsoft Corporation
 /** 
    \defgroup maxsat_ex MaxSAT/MaxSMT examples
 */
-/*@{*/
+/**@{*/
 
 /**
    \brief Exit gracefully in case of error.
@@ -638,5 +638,5 @@ int main(int argc, char * argv[]) {
     return 0;
 }
 
-/*@}*/
+/**@}*/
 
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index d2544361721..4847eeed52e 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -36,12 +36,12 @@ Copyright (c) 2012 Microsoft Corporation
    \defgroup cppapi C++ API
 
 */
-/*@{*/
+/**@{*/
 
 /**
    @name C++ API classes and functions
 */
-/*@{*/
+/**@{*/
 
 /**
    \brief Z3 C++ namespace
@@ -4059,7 +4059,7 @@ namespace z3 {
 
 }
 
-/*@}*/
-/*@}*/
+/**@}*/
+/**@}*/
 #undef Z3_THROW
 
diff --git a/src/api/z3_algebraic.h b/src/api/z3_algebraic.h
index 952692efac9..ee8ee21b83e 100644
--- a/src/api/z3_algebraic.h
+++ b/src/api/z3_algebraic.h
@@ -25,10 +25,10 @@ extern "C" {
 #endif // __cplusplus
 
     /** \defgroup capi C API */
-    /*@{*/
+    /**@{*/
 
     /** @name Algebraic Numbers */
-    /*@{*/
+    /**@{*/
     /**
        \brief Return \c true if \c a can be used as value in the Z3 real algebraic
        number package.
@@ -240,8 +240,8 @@ extern "C" {
     */
     unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a);
 
-    /*@}*/
-    /*@}*/
+    /**@}*/
+    /**@}*/
 
 #ifdef __cplusplus
 }
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index e6cd0a5b301..7d13663296d 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -37,11 +37,11 @@ DEFINE_TYPE(Z3_optimize);
 DEFINE_TYPE(Z3_rcf_num);
 
 /** \defgroup capi C API */
-/*@{*/
+/**@{*/
 
 /** @name Types */
 
-///@{
+/**@{*/
 
 /**
    Most of the types in the C API are opaque pointers.
@@ -1449,7 +1449,7 @@ typedef enum
     Z3_GOAL_UNDER_OVER
 } Z3_goal_prec;
 
-///@}
+/**@}*/
 
 #ifdef __cplusplus
 extern "C" {
@@ -1514,7 +1514,7 @@ extern "C" {
     /**@}*/
 
     /** @name Create configuration */
-    /*@{*/
+    /**@{*/
 
     /**
         \brief Create a configuration object for the Z3 context object.
@@ -1569,10 +1569,10 @@ extern "C" {
     */
     void Z3_API Z3_set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value);
 
-    /*@}*/
+    /**@}*/
 
     /** @name Context and AST Reference Counting */
-    /*@{*/
+    /**@{*/
 
     /**
        \brief Create a context using the given configuration.
@@ -1678,10 +1678,10 @@ extern "C" {
     void Z3_API Z3_interrupt(Z3_context c);
 
 
-    /*@}*/
+    /**@}*/
 
     /** @name Parameters */
-    /*@{*/
+    /**@{*/
 
     /**
        \brief Create a Z3 (empty) parameter set.
@@ -1754,10 +1754,10 @@ extern "C" {
     */
     void Z3_API Z3_params_validate(Z3_context c, Z3_params p, Z3_param_descrs d);
 
-    /*@}*/
+    /**@}*/
 
     /** @name Parameter Descriptions */
-    /*@{*/
+    /**@{*/
 
     /**
        \brief Increment the reference counter of the given parameter description set.
@@ -1811,10 +1811,10 @@ extern "C" {
     */
     Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p);
 
-    /*@}*/
+    /**@}*/
 
     /** @name Symbols */
-    /*@{*/
+    /**@{*/
 
     /**
        \brief Create a Z3 symbol using an integer.
@@ -1843,10 +1843,10 @@ extern "C" {
     */
     Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s);
 
-    /*@}*/
+    /**@}*/
 
     /** @name Sorts */
-    /*@{*/
+    /**@{*/
 
     /**
        \brief Create a free (uninterpreted) type using the given name (symbol).
@@ -2150,10 +2150,10 @@ extern "C" {
                                      Z3_func_decl* tester,
                                      Z3_func_decl accessors[]);
 
-    /*@}*/
+    /**@}*/
 
     /** @name Constants and Applications */
-    /*@{*/
+    /**@{*/
 
     /**
        \brief Declare a constant or function.
@@ -2287,10 +2287,10 @@ extern "C" {
      */
     void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body);
 
-    /*@}*/
+    /**@}*/
 
     /** @name Propositional Logic and Equality */
-    /*@{*/
+    /**@{*/
     /**
         \brief Create an AST node representing \c true.
 
@@ -2397,10 +2397,10 @@ extern "C" {
        def_API('Z3_mk_or', AST, (_in(CONTEXT), _in(UINT), _in_array(1, AST)))
     */
     Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[]);
-    /*@}*/
+    /**@}*/
 
     /** @name Integers and Reals */
-    /*@{*/
+    /**@{*/
     /**
        \brief Create an AST node representing \ccode{args[0] + ... + args[num_args-1]}.
 
@@ -2573,10 +2573,10 @@ extern "C" {
         def_API('Z3_mk_is_int', AST, (_in(CONTEXT), _in(AST)))
     */
     Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1);
-    /*@}*/
+    /**@}*/
 
     /** @name Bit-vectors */
-    /*@{*/
+    /**@{*/
     /**
        \brief Bitwise negation.
 
@@ -3097,10 +3097,10 @@ extern "C" {
        def_API('Z3_mk_bvmul_no_underflow', AST, (_in(CONTEXT), _in(AST), _in(AST)))
     */
     Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2);
-    /*@}*/
+    /**@}*/
 
     /** @name Arrays */
-    /*@{*/
+    /**@{*/
     /**
        \brief Array read.
        The argument \c a is the array and \c i is the index of the array that gets read.
@@ -3212,10 +3212,10 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_set_has_size(Z3_context c, Z3_ast set, Z3_ast k);
 
-    /*@}*/
+    /**@}*/
 
     /** @name Sets */
-    /*@{*/
+    /**@{*/
     /**
        \brief Create Set type.
 
@@ -3308,10 +3308,10 @@ extern "C" {
     */
 
     Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2);
-    /*@}*/
+    /**@}*/
 
     /** @name Numerals */
-    /*@{*/
+    /**@{*/
     /**
        \brief Create a numeral of a given sort.
 
@@ -3400,10 +3400,10 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, bool const* bits);
 
-    /*@}*/
+    /**@}*/
 
     /** @name Sequences and regular expressions */
-    /*@{*/
+    /**@{*/
 
     /**
        \brief Create a sequence sort out of the sort for the elements.
@@ -3859,11 +3859,11 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch);
 
-    /*@}*/
+    /**@}*/
 
 
     /** @name Special relations */
-    /*@{*/
+    /**@{*/
     /**
        \brief create a linear ordering relation over signature \c a.
        The relation is identified by the index \c id.
@@ -3904,10 +3904,10 @@ extern "C" {
      */
     Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f);
 
-    /*@}*/
+    /**@}*/
 
     /** @name Quantifiers */
-    /*@{*/
+    /**@{*/
     /**
        \brief Create a pattern for quantifier instantiation.
 
@@ -4212,10 +4212,10 @@ extern "C" {
                                      Z3_ast body);
 
 
-    /*@}*/
+    /**@}*/
 
     /** @name Accessors */
-    /*@{*/
+    /**@{*/
     /**
        \brief Return \c Z3_INT_SYMBOL if the symbol was constructed
        using #Z3_mk_int_symbol, and \c Z3_STRING_SYMBOL if the symbol
@@ -5150,10 +5150,10 @@ extern "C" {
        def_API('Z3_simplify_get_param_descrs', PARAM_DESCRS, (_in(CONTEXT),))
     */
     Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c);
-    /*@}*/
+    /**@}*/
 
     /** @name Modifiers */
-    /*@{*/
+    /**@{*/
     /**
        \brief Update the arguments of term \c a using the arguments \c args.
        The number of arguments \c num_args should coincide
@@ -5196,10 +5196,10 @@ extern "C" {
        def_API('Z3_translate', AST, (_in(CONTEXT), _in(AST), _in(CONTEXT)))
     */
     Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target);
-    /*@}*/
+    /**@}*/
 
     /** @name Models */
-    /*@{*/
+    /**@{*/
 
     /**
        \brief Create a fresh model object. It has reference count 0.
@@ -5534,10 +5534,10 @@ extern "C" {
        def_API('Z3_func_entry_get_arg', AST, (_in(CONTEXT), _in(FUNC_ENTRY), _in(UINT)))
     */
     Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i);
-    /*@}*/
+    /**@}*/
 
     /** @name Interaction logging */
-    /*@{*/
+    /**@{*/
     /**
        \brief Log interaction to a file.
 
@@ -5572,10 +5572,10 @@ extern "C" {
        def_API('Z3_toggle_warning_messages', VOID, (_in(BOOL),))
     */
     void Z3_API Z3_toggle_warning_messages(bool enabled);
-    /*@}*/
+    /**@}*/
 
     /** @name String conversion */
-    /*@{*/
+    /**@{*/
     /**
        \brief Select mode for the format used for pretty-printing AST nodes.
 
@@ -5662,10 +5662,10 @@ extern "C" {
                                                    Z3_ast const assumptions[],
                                                    Z3_ast formula);
 
-    /*@}*/
+    /**@}*/
 
     /** @name Parser interface */
-    /*@{*/
+    /**@{*/
     /**
        \brief Parse the given string using the SMT-LIB2 parser.
 
@@ -5709,10 +5709,10 @@ extern "C" {
 
     Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context, Z3_string str);
 
-    /*@}*/
+    /**@}*/
 
     /** @name Error Handling */
-    /*@{*/
+    /**@{*/
 #ifndef SAFE_ERRORS
     /**
        \brief Return the error code for the last API call.
@@ -5755,10 +5755,10 @@ extern "C" {
     */
     Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err);
 
-    /*@}*/
+    /**@}*/
 
     /** @name Miscellaneous */
-    /*@{*/
+    /**@{*/
 
     /**
        \brief Return Z3 version number information.
@@ -5819,10 +5819,10 @@ extern "C" {
        def_API('Z3_finalize_memory', VOID, ())
     */
     void Z3_API Z3_finalize_memory(void);
-    /*@}*/
+    /**@}*/
 
     /** @name Goals */
-    /*@{*/
+    /**@{*/
     /**
        \brief Create a goal (aka problem). A goal is essentially a set
        of formulas, that can be solved and/or transformed using
@@ -5972,10 +5972,10 @@ extern "C" {
     */
     Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names);
 
-    /*@}*/
+    /**@}*/
 
     /** @name Tactics and Probes */
-    /*@{*/
+    /**@{*/
     /**
        \brief Return a tactic associated with the given name.
        The complete list of tactics may be obtained using the procedures #Z3_get_num_tactics and #Z3_get_tactic_name.
@@ -6324,10 +6324,10 @@ extern "C" {
     */
     Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i);
 
-    /*@}*/
+    /**@}*/
 
     /** @name Solvers*/
-    /*@{*/
+    /**@{*/
     /**
        \brief Create a new solver. This solver is a "combined solver" (see
        combined_solver module) that internally uses a non-incremental (solver1) and an
@@ -6850,10 +6850,10 @@ extern "C" {
     */
     Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names);
 
-    /*@}*/
+    /**@}*/
 
     /** @name Statistics */
-    /*@{*/
+    /**@{*/
 
     /**
        \brief Convert a statistics into a string.
@@ -6935,11 +6935,11 @@ extern "C" {
     */
     uint64_t Z3_API Z3_get_estimated_alloc_size(void);
 
-    /*@}*/
+    /**@}*/
 
 #ifdef __cplusplus
 }
 #endif // __cplusplus
 
-/*@}*/
+/**@}*/
 
diff --git a/src/api/z3_ast_containers.h b/src/api/z3_ast_containers.h
index e317460f894..1db7bf4ce38 100644
--- a/src/api/z3_ast_containers.h
+++ b/src/api/z3_ast_containers.h
@@ -23,10 +23,10 @@ extern "C" {
 #endif // __cplusplus
 
     /** \defgroup capi C API */
-    /*@{*/
+    /**@{*/
 
     /** @name AST vectors */
-    /*@{*/
+    /**@{*/
     /**
        \brief Return an empty AST vector.
 
@@ -104,10 +104,10 @@ extern "C" {
     */
     Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v);
 
-    /*@}*/
+    /**@}*/
 
     /** @name AST maps */
-    /*@{*/
+    /**@{*/
     /**
     \brief Return an empty mapping from AST to AST
 
@@ -189,8 +189,8 @@ extern "C" {
     def_API('Z3_ast_map_to_string', STRING, (_in(CONTEXT), _in(AST_MAP)))
     */
     Z3_string Z3_API Z3_ast_map_to_string(Z3_context c, Z3_ast_map m);
-    /*@}*/
-    /*@}*/
+    /**@}*/
+    /**@}*/
 
 #ifdef __cplusplus
 }
diff --git a/src/api/z3_fixedpoint.h b/src/api/z3_fixedpoint.h
index b9fada51d23..5eadaaf467e 100644
--- a/src/api/z3_fixedpoint.h
+++ b/src/api/z3_fixedpoint.h
@@ -23,10 +23,10 @@ extern "C" {
 #endif // __cplusplus
 
     /** \defgroup capi C API */
-    /*@{*/
+    /**@{*/
 
     /** @name Fixedpoint facilities */
-    /*@{*/
+    /**@{*/
     /**
        \brief Create a new fixedpoint context.
 
@@ -373,8 +373,8 @@ extern "C" {
 
     void Z3_API Z3_fixedpoint_add_constraint (Z3_context c, Z3_fixedpoint d, Z3_ast e, unsigned lvl);
 
-    /*@}*/
-    /*@}*/
+    /**@}*/
+    /**@}*/
 
 #ifdef __cplusplus
 }
diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h
index fe85e702e64..4ab0d91775b 100644
--- a/src/api/z3_fpa.h
+++ b/src/api/z3_fpa.h
@@ -23,10 +23,10 @@ extern "C" {
 #endif // __cplusplus
 
     /** \defgroup capi C API */
-    /*@{*/
+    /**@{*/
 
     /** @name Floating-Point Arithmetic */
-    /*@{*/
+    /**@{*/
     /**
         \brief Create the RoundingMode sort.
 
@@ -841,7 +841,7 @@ extern "C" {
 
 
     /** @name Z3-specific floating-point extensions */
-    /*@{*/
+    /**@{*/
     /**
         \brief Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.
 
@@ -1080,9 +1080,9 @@ extern "C" {
         def_API('Z3_mk_fpa_to_fp_int_real', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(SORT)))
     */
     Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s);
-    /*@}*/
-    /*@}*/
-    /*@}*/
+    /**@}*/
+    /**@}*/
+    /**@}*/
 
 #ifdef __cplusplus
 }
diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h
index 51d8853e0d1..3cdacc46d53 100644
--- a/src/api/z3_optimization.h
+++ b/src/api/z3_optimization.h
@@ -28,10 +28,10 @@ extern "C" {
 #endif // __cplusplus
 
     /** \defgroup capi C API */
-    /*@{*/
+    /**@{*/
 
     /** @name Optimization facilities */
-    /*@{*/
+    /**@{*/
     /**
        \brief Create a new optimize context.
 
@@ -368,8 +368,8 @@ extern "C" {
         Z3_model_eh  model_eh);
 
 
-    /*@}*/
-    /*@}*/
+    /**@}*/
+    /**@}*/
 
 #ifdef __cplusplus
 }
diff --git a/src/api/z3_polynomial.h b/src/api/z3_polynomial.h
index 47979fc87cb..6e7a72df366 100644
--- a/src/api/z3_polynomial.h
+++ b/src/api/z3_polynomial.h
@@ -24,11 +24,11 @@ extern "C" {
 #endif // __cplusplus
 
     /** \defgroup capi C API */
-    /*@{*/
+    /**@{*/
 
 
     /** @name Polynomials */
-    /*@{*/
+    /**@{*/
 
     /**
        \brief Return the nonzero subresultants of \c p and \c q with respect to the "variable" \c x.
@@ -43,8 +43,8 @@ extern "C" {
     Z3_ast_vector Z3_API Z3_polynomial_subresultants(Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x);
 
 
-    /*@}*/
-    /*@}*/
+    /**@}*/
+    /**@}*/
 
 #ifdef __cplusplus
 }
diff --git a/src/api/z3_rcf.h b/src/api/z3_rcf.h
index f61da20c5e5..88c27db61f1 100644
--- a/src/api/z3_rcf.h
+++ b/src/api/z3_rcf.h
@@ -26,10 +26,10 @@ extern "C" {
 #endif // __cplusplus
 
     /** \defgroup capi C API */
-    /*@{*/
+    /**@{*/
 
     /** @name Real Closed Fields */
-    /*@{*/
+    /**@{*/
     /**
        \brief Delete a RCF numeral created using the RCF API.
 
@@ -196,8 +196,8 @@ extern "C" {
     */
     void Z3_API Z3_rcf_get_numerator_denominator(Z3_context c, Z3_rcf_num a, Z3_rcf_num * n, Z3_rcf_num * d);
 
-    /*@}*/
-    /*@}*/
+    /**@}*/
+    /**@}*/
 
 #ifdef __cplusplus
 }
diff --git a/src/api/z3_spacer.h b/src/api/z3_spacer.h
index fe4086e5a53..dd102843372 100644
--- a/src/api/z3_spacer.h
+++ b/src/api/z3_spacer.h
@@ -23,10 +23,10 @@ extern "C" {
 #endif // __cplusplus
 
     /** \defgroup capi C API */
-    /*@{*/
+    /**@{*/
 
     /** @name Spacer facilities */
-    /*@{*/
+    /**@{*/
     /**
         \brief Pose a query against the asserted rules at the given level.
 
@@ -132,8 +132,8 @@ extern "C" {
        Z3_ast_vector vars,
        Z3_ast body);
 
-    /*@}*/
-    /*@}*/
+    /**@}*/
+    /**@}*/
 
 #ifdef __cplusplus
 }