From 9f499055826112e9ebc8b2a06bb7576d507aee46 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 10 Jan 2017 21:05:27 +0000
Subject: [PATCH] Formatting, whitespace, and Z3_API annotations.

---
 src/api/z3_api.h | 26 ++++++++++----------------
 1 file changed, 10 insertions(+), 16 deletions(-)

diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index fcf22961c..65c155d63 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1953,7 +1953,7 @@ extern "C" {
        The datatype may be recursive. Return the datatype sort.
 
        \param c logical context.
-	   \param name name of datatype.
+       \param name name of datatype.
        \param num_constructors number of constructors passed in.
        \param constructors array of constructor containers.
 
@@ -3088,7 +3088,7 @@ extern "C" {
 
        \param c logical context.
        \param numeral A string representing the numeral value in decimal notation. The string may be of the form \code{[num]*[.[num]*][E[+|-][num]+]}.
-                      If the given sort is a real, then the numeral can be a rational, that is, a string of the form \ccode{[num]* / [num]*}.                      
+                      If the given sort is a real, then the numeral can be a rational, that is, a string of the form \ccode{[num]* / [num]*}.
        \param ty The sort of the numeral. In the current implementation, the given sort can be an int, real, finite-domain, or bit-vectors of arbitrary size.
 
        \sa Z3_mk_int
@@ -3393,7 +3393,7 @@ extern "C" {
        \c lo number of times, and with an unbounded upper bound.
 
        def_API('Z3_mk_re_loop', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in(UINT)))
-     */    
+     */
     Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi);
 
     /**
@@ -3430,7 +3430,7 @@ extern "C" {
        def_API('Z3_mk_re_full' ,AST ,(_in(CONTEXT), _in(SORT)))
      */
     Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re);
-    
+
 
     /*@}*/
 
@@ -3966,11 +3966,9 @@ extern "C" {
 
        def_API('Z3_mk_atmost', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in(UINT)))
     */
-
     Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args,
                                Z3_ast const args[], unsigned k);
 
-
     /**
        \brief Pseudo-Boolean relations.
 
@@ -3978,9 +3976,9 @@ extern "C" {
 
        def_API('Z3_mk_atleast', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in(UINT)))
     */
-
-    Z3_ast Z3_mk_atleast(Z3_context c, unsigned num_args,
+    Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args,
                                 Z3_ast const args[], unsigned k);
+
     /**
        \brief Pseudo-Boolean relations.
 
@@ -3988,12 +3986,10 @@ extern "C" {
 
        def_API('Z3_mk_pble', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in_array(1,INT), _in(INT)))
     */
-
     Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args,
                              Z3_ast const args[], int coeffs[],
                              int k);
 
-
     /**
        \brief Pseudo-Boolean relations.
 
@@ -4001,8 +3997,7 @@ extern "C" {
 
        def_API('Z3_mk_pbge', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in_array(1,INT), _in(INT)))
     */
-
-    Z3_ast Z3_mk_pbge(Z3_context c, unsigned num_args,
+    Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args,
                              Z3_ast const args[], int coeffs[],
                              int k);
 
@@ -4013,7 +4008,6 @@ extern "C" {
 
        def_API('Z3_mk_pbeq', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in_array(1,INT), _in(INT)))
     */
-
     Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args,
                              Z3_ast const args[], int coeffs[],
                              int k);
@@ -5228,7 +5222,7 @@ extern "C" {
     /*@}*/
 
     /**
-       \brief Return a string describing the given error code. 
+       \brief Return a string describing the given error code.
        Retained function name for backwards compatibility within v4.1
     */
     Z3_string Z3_API Z3_get_error_msg_ex(Z3_context c, Z3_error_code err);
@@ -6001,11 +5995,11 @@ extern "C" {
 
     /**
        \brief retrieve consequences from solver that determine values of the supplied function symbols.
-       
+
        def_API('Z3_solver_get_consequences', INT, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(AST_VECTOR), _in(AST_VECTOR)))
      */
 
-    Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, 
+    Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c,
                                                Z3_solver s,
                                                Z3_ast_vector assumptions,
                                                Z3_ast_vector variables,