diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c
index ea0cd8528..980592f25 100644
--- a/examples/c/test_capi.c
+++ b/examples/c/test_capi.c
@@ -241,7 +241,7 @@ void check(Z3_context ctx, Z3_solver s, Z3_lbool expected_result)
 
    The context \c ctx is not modified by this function.
 */
-void prove(Z3_context ctx, Z3_solver s, Z3_ast f, Z3_bool is_valid)
+void prove(Z3_context ctx, Z3_solver s, Z3_ast f, bool is_valid)
 {
     Z3_model m = 0;
     Z3_ast   not_f;
@@ -639,7 +639,7 @@ void display_model(Z3_context c, FILE * out, Z3_model m)
         Z3_symbol name;
         Z3_func_decl cnst = Z3_model_get_const_decl(c, m, i);
         Z3_ast a, v;
-        Z3_bool ok;
+        bool ok;
         name = Z3_get_decl_name(c, cnst);
         display_symbol(c, out, name);
         fprintf(out, " = ");
@@ -2304,7 +2304,7 @@ typedef struct {
     // IMPORTANT: the fields m_answer_literals, m_retracted and m_num_answer_literals must be saved/restored
     // if push/pop operations are performed on m_context.
     Z3_ast     m_answer_literals[MAX_RETRACTABLE_ASSERTIONS];
-    Z3_bool    m_retracted[MAX_RETRACTABLE_ASSERTIONS]; // true if the assertion was retracted.
+    bool       m_retracted[MAX_RETRACTABLE_ASSERTIONS]; // true if the assertion was retracted.
     unsigned   m_num_answer_literals;
 } Z3_ext_context_struct;
 
@@ -2872,7 +2872,7 @@ void mk_model_example() {
                                   /*num_args=*/2,
                                   /*args=*/addArgs);
         Z3_ast aPlusBEval = NULL;
-        Z3_bool aPlusBEvalSuccess =
+        bool aPlusBEvalSuccess =
             Z3_model_eval(ctx, m, aPlusB,
                           /*model_completion=*/false, &aPlusBEval);
         if (aPlusBEvalSuccess != true) {
@@ -2882,7 +2882,7 @@ void mk_model_example() {
 
         {
             int aPlusBValue = 0;
-            Z3_bool getAPlusBValueSuccess =
+            bool getAPlusBValueSuccess =
                 Z3_get_numeral_int(ctx, aPlusBEval, &aPlusBValue);
             if (getAPlusBValueSuccess != true) {
                 printf("Failed to get integer value for a+b\n");
@@ -2906,7 +2906,7 @@ void mk_model_example() {
                                     /*num_args=*/3,
                                     /*args=*/arrayAddArgs);
         Z3_ast arrayAddEval = NULL;
-        Z3_bool arrayAddEvalSuccess =
+        bool arrayAddEvalSuccess =
             Z3_model_eval(ctx, m, arrayAdd,
                           /*model_completion=*/false, &arrayAddEval);
         if (arrayAddEvalSuccess != true) {
@@ -2915,7 +2915,7 @@ void mk_model_example() {
         }
         {
             int arrayAddValue = 0;
-            Z3_bool getArrayAddValueSuccess =
+            bool getArrayAddValueSuccess =
                 Z3_get_numeral_int(ctx, arrayAddEval, &arrayAddValue);
             if (getArrayAddValueSuccess != true) {
                 printf("Failed to get integer value for c[0] + c[1] + c[2]\n");
diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp
index 882c2bbe2..1a1e31f0a 100644
--- a/examples/tptp/tptp5.cpp
+++ b/examples/tptp/tptp5.cpp
@@ -1337,7 +1337,7 @@ public:
             }
         }
         else if (e.is_quantifier()) {
-            Z3_bool is_forall = Z3_is_quantifier_forall(ctx, e);
+            bool is_forall = Z3_is_quantifier_forall(ctx, e);
             unsigned nb = Z3_get_quantifier_num_bound(ctx, e);
 
             out << (is_forall?"!":"?") << "[";
diff --git a/scripts/update_api.py b/scripts/update_api.py
index 227d02dd2..901ea4fda 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -61,7 +61,7 @@ def is_obj(ty):
     return ty >= FIRST_OBJ_ID
 
 Type2Str = { VOID : 'void', VOID_PTR : 'void*', INT : 'int', UINT : 'unsigned', INT64 : 'int64_t', UINT64 : 'uint64_t', DOUBLE : 'double',
-             FLOAT : 'float', STRING : 'Z3_string', STRING_PTR : 'Z3_string_ptr', BOOL : 'Z3_bool', SYMBOL : 'Z3_symbol',
+             FLOAT : 'float', STRING : 'Z3_string', STRING_PTR : 'Z3_string_ptr', BOOL : 'bool', SYMBOL : 'Z3_symbol',
              PRINT_MODE : 'Z3_ast_print_mode', ERROR_CODE : 'Z3_error_code'
              }
 
@@ -1227,7 +1227,7 @@ def ml_has_plus_type(ts):
 def ml_unwrap(t, ts, s):
     if t == STRING:
         return '(' + ts + ') String_val(' + s + ')'
-    elif t == BOOL or (type2str(t) == 'Z3_bool'):
+    elif t == BOOL or (type2str(t) == 'bool'):
         return '(' + ts + ') Bool_val(' + s + ')'
     elif t == INT or t == PRINT_MODE or t == ERROR_CODE:
         return '(' + ts + ') Int_val(' + s + ')'
@@ -1248,7 +1248,7 @@ def ml_unwrap(t, ts, s):
 def ml_set_wrap(t, d, n):
     if t == VOID:
         return d + ' = Val_unit;'
-    elif t == BOOL or (type2str(t) == 'Z3_bool'):
+    elif t == BOOL or (type2str(t) == 'bool'):
         return d + ' = Val_bool(' + n + ');'
     elif t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE:
         return d + ' = Val_int(' + n + ');'
@@ -1263,7 +1263,7 @@ def ml_set_wrap(t, d, n):
         return '*(' + pts + '*)Data_custom_val(' + d + ') = ' + n + ';'
 
 def ml_alloc_and_store(t, lhs, rhs):
-    if t == VOID or t == BOOL or t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE or t == INT64 or t == UINT64 or t == DOUBLE or t == STRING or (type2str(t) == 'Z3_bool'):
+    if t == VOID or t == BOOL or t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE or t == INT64 or t == UINT64 or t == DOUBLE or t == STRING or (type2str(t) == 'bool'):
         return ml_set_wrap(t, lhs, rhs)
     else:
         pts = ml_plus_type(type2str(t))
diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp
index 4ea046f1c..7d08ade35 100644
--- a/src/api/api_algebraic.cpp
+++ b/src/api/api_algebraic.cpp
@@ -79,7 +79,7 @@ extern "C" {
              _c->autil().is_irrational_algebraic_numeral(to_expr(a)));
     }
 
-    Z3_bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a) {
+    bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a) {
         Z3_TRY;
         LOG_Z3_algebraic_is_value(c, a);
         RESET_ERROR_CODE();
@@ -87,15 +87,15 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a) {
+    bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a) {
         return Z3_algebraic_sign(c, a) > 0;
     }
 
-    Z3_bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a) {
+    bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a) {
         return Z3_algebraic_sign(c, a) < 0;
     }
 
-    Z3_bool Z3_API Z3_algebraic_is_zero(Z3_context c, Z3_ast a) {
+    bool Z3_API Z3_algebraic_is_zero(Z3_context c, Z3_ast a) {
         return Z3_algebraic_sign(c, a) == 0;
     }
 
@@ -286,7 +286,7 @@ extern "C" {
         return r;
 
 
-    Z3_bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b) {
+    bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b) {
         Z3_TRY;
         LOG_Z3_algebraic_lt(c, a, b);
         RESET_ERROR_CODE();
@@ -296,19 +296,19 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b) {
+    bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b) {
         return Z3_algebraic_lt(c, b, a);
     }
 
-    Z3_bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b) {
+    bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b) {
         return !Z3_algebraic_lt(c, b, a);
     }
 
-    Z3_bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b) {
+    bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b) {
         return !Z3_algebraic_lt(c, a, b);
     }
 
-    Z3_bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b) {
+    bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b) {
         Z3_TRY;
         LOG_Z3_algebraic_eq(c, a, b);
         RESET_ERROR_CODE();
@@ -318,7 +318,7 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
-    Z3_bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b) {
+    bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b) {
         return !Z3_algebraic_eq(c, a, b);
     }
 
diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp
index 0827fd911..69fde33a7 100644
--- a/src/api/api_arith.cpp
+++ b/src/api/api_arith.cpp
@@ -119,7 +119,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-    Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) {
+    bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) {
         LOG_Z3_is_algebraic_number(c, a);
         return mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a));
     }
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 277715950..d10da60db 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -73,7 +73,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-    Z3_bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2) {
+    bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2) {
         RESET_ERROR_CODE();
         return s1 == s2;
     }
@@ -88,12 +88,12 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-    Z3_bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast s1, Z3_ast s2) {
+    bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast s1, Z3_ast s2) {
         RESET_ERROR_CODE();
         return s1 == s2;
     }
 
-    Z3_bool Z3_API Z3_is_eq_func_decl(Z3_context c, Z3_func_decl s1, Z3_func_decl s2) {
+    bool Z3_API Z3_is_eq_func_decl(Z3_context c, Z3_func_decl s1, Z3_func_decl s2) {
         RESET_ERROR_CODE();
         return s1 == s2;
     }
@@ -308,7 +308,7 @@ extern "C" {
         return to_sort(s)->get_id();
     }
 
-    Z3_bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t) {
+    bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_is_well_sorted(c, t);
         RESET_ERROR_CODE();
@@ -383,7 +383,7 @@ extern "C" {
         return to_ast(a)->hash();
     }
 
-    Z3_bool Z3_API Z3_is_app(Z3_context c, Z3_ast a) {
+    bool Z3_API Z3_is_app(Z3_context c, Z3_ast a) {
         LOG_Z3_is_app(c, a);
         RESET_ERROR_CODE();
         return a != nullptr && is_app(reinterpret_cast<ast*>(a));
diff --git a/src/api/api_ast_map.cpp b/src/api/api_ast_map.cpp
index 524bd113d..aaece1621 100644
--- a/src/api/api_ast_map.cpp
+++ b/src/api/api_ast_map.cpp
@@ -57,7 +57,7 @@ extern "C" {
         Z3_CATCH;
     }
 
-    Z3_bool Z3_API Z3_ast_map_contains(Z3_context c, Z3_ast_map m, Z3_ast k) {
+    bool Z3_API Z3_ast_map_contains(Z3_context c, Z3_ast_map m, Z3_ast k) {
         Z3_TRY;
         LOG_Z3_ast_map_contains(c, m, k);
         RESET_ERROR_CODE();
diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp
index bd603aa6d..e56371bb5 100644
--- a/src/api/api_bv.cpp
+++ b/src/api/api_bv.cpp
@@ -106,7 +106,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) {                \
     MK_BV_PUNARY(Z3_mk_rotate_right, OP_ROTATE_RIGHT);
     MK_BV_PUNARY(Z3_mk_int2bv, OP_INT2BV);
 
-    Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast n, Z3_bool is_signed) {
+    Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast n, bool is_signed) {
         Z3_TRY;
         LOG_Z3_mk_bv2int(c, n, is_signed);
         RESET_ERROR_CODE();
@@ -186,7 +186,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) {                \
         return Z3_mk_int(c, -1, s);
     }
 
-    Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed) {
+    Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed) {
         Z3_TRY;
         RESET_ERROR_CODE();
         if (is_signed) {
@@ -286,7 +286,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) {                \
         Z3_CATCH_RETURN(nullptr);
     }
 
-    Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed) {
+    Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed) {
         Z3_TRY;
         RESET_ERROR_CODE();
         if (is_signed) {
@@ -311,7 +311,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) {                \
         Z3_CATCH_RETURN(nullptr);
     }
 
-    Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast n1, Z3_ast n2, Z3_bool is_signed) {
+    Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast n1, Z3_ast n2, bool is_signed) {
         LOG_Z3_mk_bvmul_no_overflow(c, n1, n2, is_signed);
         RESET_ERROR_CODE();
         if (is_signed) {
diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index c61fa9c4d..0b1bf4490 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -363,7 +363,7 @@ extern "C" {
         Z3_CATCH;
     }
 
-    void Z3_API Z3_toggle_warning_messages(Z3_bool enabled) {
+    void Z3_API Z3_toggle_warning_messages(bool enabled) {
         LOG_Z3_toggle_warning_messages(enabled);
         enable_warning_messages(enabled != 0);
     }
diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
index 0f6bd49cc..790470275 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -199,7 +199,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-    Z3_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t * out) {
+    bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t * out) {
         Z3_TRY;
         if (out) {
             *out = 0;
diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index c8a2690c6..9728cbc00 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -232,7 +232,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-    Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, Z3_bool negative) {
+    Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative) {
         Z3_TRY;
         LOG_Z3_mk_fpa_inf(c, s, negative);
         RESET_ERROR_CODE();
@@ -249,7 +249,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-    Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, Z3_bool negative) {
+    Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative) {
         Z3_TRY;
         LOG_Z3_mk_fpa_inf(c, s, negative);
         RESET_ERROR_CODE();
@@ -338,7 +338,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-    Z3_ast Z3_API Z3_mk_fpa_numeral_int_uint(Z3_context c, Z3_bool sgn, signed exp, unsigned sig, Z3_sort ty) {
+    Z3_ast Z3_API Z3_mk_fpa_numeral_int_uint(Z3_context c, bool sgn, signed exp, unsigned sig, Z3_sort ty) {
         Z3_TRY;
         LOG_Z3_mk_fpa_numeral_int64_uint64(c, sgn, exp, sig, ty);
         RESET_ERROR_CODE();
@@ -358,7 +358,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-    Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64(Z3_context c, Z3_bool sgn, int64_t exp, uint64_t sig, Z3_sort ty) {
+    Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64(Z3_context c, bool sgn, int64_t exp, uint64_t sig, Z3_sort ty) {
         Z3_TRY;
         LOG_Z3_mk_fpa_numeral_int64_uint64(c, sgn, exp, sig, ty);
         RESET_ERROR_CODE();
@@ -905,7 +905,7 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
-    Z3_bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int * sgn) {
+    bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int * sgn) {
         Z3_TRY;
         LOG_Z3_fpa_get_numeral_sign(c, t, sgn);
         RESET_ERROR_CODE();
@@ -1035,7 +1035,7 @@ extern "C" {
         Z3_CATCH_RETURN("");
     }
 
-    Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, uint64_t * n) {
+    bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, uint64_t * n) {
         Z3_TRY;
         LOG_Z3_fpa_get_numeral_significand_uint64(c, t, n);
         RESET_ERROR_CODE();
@@ -1072,7 +1072,7 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
-    Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, Z3_bool biased) {
+    Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, bool biased) {
         Z3_TRY;
         LOG_Z3_fpa_get_numeral_exponent_string(c, t, biased);
         RESET_ERROR_CODE();
@@ -1113,7 +1113,7 @@ extern "C" {
         Z3_CATCH_RETURN("");
     }
 
-    Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, int64_t * n, Z3_bool biased) {
+    bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, int64_t * n, bool biased) {
         Z3_TRY;
         LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n, biased);
         RESET_ERROR_CODE();
@@ -1157,7 +1157,7 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
-    Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, Z3_bool biased) {
+    Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, bool biased) {
         Z3_TRY;
         LOG_Z3_fpa_get_numeral_exponent_bv(c, t, biased);
         RESET_ERROR_CODE();
@@ -1232,7 +1232,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-    Z3_bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t) {
+    bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_fpa_is_numeral_nan(c, t);
         RESET_ERROR_CODE();
@@ -1246,7 +1246,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t) {
+    bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_fpa_is_numeral_inf(c, t);
         RESET_ERROR_CODE();
@@ -1260,7 +1260,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t) {
+    bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_fpa_is_numeral_zero(c, t);
         RESET_ERROR_CODE();
@@ -1274,7 +1274,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t) {
+    bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_fpa_is_numeral_normal(c, t);
         RESET_ERROR_CODE();
@@ -1288,7 +1288,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t) {
+    bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_fpa_is_numeral_subnormal(c, t);
         RESET_ERROR_CODE();
@@ -1302,7 +1302,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t) {
+    bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_fpa_is_numeral_positive(c, t);
         RESET_ERROR_CODE();
@@ -1316,7 +1316,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t) {
+    bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_fpa_is_numeral_negative(c, t);
         RESET_ERROR_CODE();
diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp
index 1a67e1061..c70d241e0 100644
--- a/src/api/api_goal.cpp
+++ b/src/api/api_goal.cpp
@@ -25,7 +25,7 @@ Revision History:
 
 extern "C" {
 
-    Z3_goal Z3_API Z3_mk_goal(Z3_context c, Z3_bool models, Z3_bool unsat_cores, Z3_bool proofs) {
+    Z3_goal Z3_API Z3_mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs) {
         Z3_TRY;
         LOG_Z3_mk_goal(c, models, unsat_cores, proofs);
         RESET_ERROR_CODE();
@@ -82,7 +82,7 @@ extern "C" {
         Z3_CATCH;
     }
 
-    Z3_bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g) {
+    bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g) {
         Z3_TRY;
         LOG_Z3_goal_inconsistent(c, g);
         RESET_ERROR_CODE();
@@ -136,7 +136,7 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
     
-    Z3_bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g) {
+    bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g) {
         Z3_TRY;
         LOG_Z3_goal_is_decided_sat(c, g);
         RESET_ERROR_CODE();
@@ -144,7 +144,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
     
-    Z3_bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g) {
+    bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g) {
         Z3_TRY;
         LOG_Z3_goal_is_decided_unsat(c, g);
         RESET_ERROR_CODE();
diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp
index dd517c82f..d338407bf 100644
--- a/src/api/api_log.cpp
+++ b/src/api/api_log.cpp
@@ -33,8 +33,8 @@ extern "C" {
         }
     }
 
-    Z3_bool Z3_API Z3_open_log(Z3_string filename) {
-        Z3_bool res = true;
+    bool Z3_API Z3_open_log(Z3_string filename) {
+        bool res = true;
 
 #ifdef Z3_LOG_SYNC
         #pragma omp critical (z3_log)
diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index 279cef673..c7347f299 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -75,7 +75,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-    Z3_bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a) {
+    bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a) {
         Z3_TRY;
         LOG_Z3_model_has_interp(c, m, a);
         CHECK_NON_NULL(m, 0);
@@ -157,7 +157,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
     
-    Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast * v) {
+    bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v) {
         Z3_TRY;
         LOG_Z3_model_eval(c, m, t, model_completion, v);
         if (v) *v = nullptr;
@@ -225,7 +225,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
     
-    Z3_bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a) {
+    bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a) {
         Z3_TRY;
         LOG_Z3_is_as_array(c, a);
         RESET_ERROR_CODE();
diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp
index 718712d61..cfa64e2c3 100644
--- a/src/api/api_numeral.cpp
+++ b/src/api/api_numeral.cpp
@@ -142,7 +142,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-    Z3_bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a) {
+    bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a) {
         Z3_TRY;
         LOG_Z3_is_numeral_ast(c, a);
         RESET_ERROR_CODE();        
@@ -157,7 +157,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_get_numeral_rational(Z3_context c, Z3_ast a, rational& r) {
+    bool Z3_API Z3_get_numeral_rational(Z3_context c, Z3_ast a, rational& r) {
         Z3_TRY;
         // This function is not part of the public API
         RESET_ERROR_CODE();
@@ -187,7 +187,7 @@ extern "C" {
         RESET_ERROR_CODE();
         CHECK_IS_EXPR(a, "");
         rational r;
-        Z3_bool ok = Z3_get_numeral_rational(c, a, r);
+        bool ok = Z3_get_numeral_rational(c, a, r);
         if (ok) {
             return mk_c(c)->mk_external_string(r.to_string());
         }
@@ -263,14 +263,14 @@ extern "C" {
         Z3_CATCH_RETURN("");
     }
 
-    Z3_bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, int64_t* num, int64_t* den) {
+    bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, int64_t* num, int64_t* den) {
         Z3_TRY;
         // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
         LOG_Z3_get_numeral_small(c, a, num, den);
         RESET_ERROR_CODE();
         CHECK_IS_EXPR(a, false);
         rational r;
-        Z3_bool ok = Z3_get_numeral_rational(c, a, r);
+        bool ok = Z3_get_numeral_rational(c, a, r);
         if (ok) {
             rational n = numerator(r);
             rational d = denominator(r);
@@ -289,7 +289,7 @@ extern "C" {
     }
 
 
-    Z3_bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int* i) {
+    bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int* i) {
         Z3_TRY;
         // This function invokes Z3_get_numeral_int64, but it is still ok to add LOG command here because it does not return a Z3 object.
         LOG_Z3_get_numeral_int(c, v, i);
@@ -308,7 +308,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned* u) {
+    bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned* u) {
         Z3_TRY;
         // This function invokes Z3_get_numeral_uint64, but it is still ok to add LOG command here because it does not return a Z3 object.
         LOG_Z3_get_numeral_uint(c, v, u);
@@ -327,7 +327,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t* u) {
+    bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t* u) {
         Z3_TRY;
         // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
         LOG_Z3_get_numeral_uint64(c, v, u);
@@ -338,7 +338,7 @@ extern "C" {
             return false;
         }
         rational r;
-        Z3_bool ok = Z3_get_numeral_rational(c, v, r);
+        bool ok = Z3_get_numeral_rational(c, v, r);
         SASSERT(u);
         if (ok && r.is_uint64()) {
             *u = r.get_uint64();
@@ -348,7 +348,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t* i) {
+    bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t* i) {
         Z3_TRY;
         // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
         LOG_Z3_get_numeral_int64(c, v, i);
@@ -359,7 +359,7 @@ extern "C" {
             return false;
         }
         rational r;
-        Z3_bool ok = Z3_get_numeral_rational(c, v, r);
+        bool ok = Z3_get_numeral_rational(c, v, r);
         if (ok && r.is_int64()) {
             *i = r.get_int64();
             return ok;
@@ -368,7 +368,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, int64_t* num, int64_t* den) {
+    bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, int64_t* num, int64_t* den) {
         Z3_TRY;
         // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
         LOG_Z3_get_numeral_rational_int64(c, v, num, den);
@@ -379,7 +379,7 @@ extern "C" {
             return false;
         }
         rational r;
-        Z3_bool ok = Z3_get_numeral_rational(c, v, r);
+        bool ok = Z3_get_numeral_rational(c, v, r);
         if (ok != true) {
             return ok;
         }
@@ -394,7 +394,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, Z3_bool const* bits) {
+    Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, bool const* bits) {
         Z3_TRY;
         LOG_Z3_mk_bv_numeral(c, sz, bits);
         RESET_ERROR_CODE();
diff --git a/src/api/api_params.cpp b/src/api/api_params.cpp
index 9d9f5157c..31a196f96 100644
--- a/src/api/api_params.cpp
+++ b/src/api/api_params.cpp
@@ -62,7 +62,7 @@ extern "C" {
     /**
        \brief Add a Boolean parameter \c k with value \c v to the parameter set \c p.
     */
-    void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, Z3_bool v) {
+    void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, bool v) {
         Z3_TRY;
         LOG_Z3_params_set_bool(c, p, k, v);
         RESET_ERROR_CODE();
diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp
index 306b422f1..546f4174a 100644
--- a/src/api/api_quant.cpp
+++ b/src/api/api_quant.cpp
@@ -26,7 +26,7 @@ extern "C" {
 
     Z3_ast Z3_API Z3_mk_quantifier(
         Z3_context c,
-        Z3_bool is_forall,
+        bool is_forall,
         unsigned weight,
         unsigned num_patterns, Z3_pattern const patterns[],
         unsigned num_decls, Z3_sort const sorts[],
@@ -50,7 +50,7 @@ extern "C" {
 
     Z3_ast mk_quantifier_ex_core(
         Z3_context c,
-        Z3_bool is_forall,
+        bool is_forall,
         unsigned weight,
         Z3_symbol quantifier_id,
         Z3_symbol skolem_id,
@@ -109,7 +109,7 @@ extern "C" {
 
     Z3_ast Z3_API Z3_mk_quantifier_ex(
         Z3_context c,
-        Z3_bool is_forall,
+        bool is_forall,
         unsigned weight,
         Z3_symbol quantifier_id,
         Z3_symbol skolem_id,
@@ -201,7 +201,7 @@ extern "C" {
 
 
     Z3_ast Z3_API Z3_mk_quantifier_const_ex(Z3_context c,
-                                            Z3_bool is_forall,
+                                            bool is_forall,
                                             unsigned weight,
                                             Z3_symbol quantifier_id,
                                             Z3_symbol skolem_id,
@@ -283,7 +283,7 @@ extern "C" {
     }
 
     Z3_ast Z3_API Z3_mk_quantifier_const(Z3_context c,
-                                         Z3_bool is_forall,
+                                         bool is_forall,
                                          unsigned weight,
                                          unsigned num_bound,
                                          Z3_app const bound[],
@@ -343,7 +343,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-    Z3_bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a) {
+    bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a) {
         Z3_TRY;
         LOG_Z3_is_quantifier_forall(c, a);
         RESET_ERROR_CODE();
@@ -351,7 +351,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a) {
+    bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a) {
         Z3_TRY;
         LOG_Z3_is_quantifier_exists(c, a);
         RESET_ERROR_CODE();
@@ -359,7 +359,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a) {
+    bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a) {
         Z3_TRY;
         LOG_Z3_is_lambda(c, a);
         RESET_ERROR_CODE();
diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp
index 0bcabf0c4..bcaf0869f 100644
--- a/src/api/api_rcf.cpp
+++ b/src/api/api_rcf.cpp
@@ -214,7 +214,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-    Z3_bool Z3_API Z3_rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
+    bool Z3_API Z3_rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
         Z3_TRY;
         LOG_Z3_rcf_lt(c, a, b);
         RESET_ERROR_CODE();
@@ -223,7 +223,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
+    bool Z3_API Z3_rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
         Z3_TRY;
         LOG_Z3_rcf_gt(c, a, b);
         RESET_ERROR_CODE();
@@ -232,7 +232,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
+    bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
         Z3_TRY;
         LOG_Z3_rcf_le(c, a, b);
         RESET_ERROR_CODE();
@@ -241,7 +241,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
+    bool Z3_API Z3_rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
         Z3_TRY;
         LOG_Z3_rcf_ge(c, a, b);
         RESET_ERROR_CODE();
@@ -250,7 +250,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
+    bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
         Z3_TRY;
         LOG_Z3_rcf_eq(c, a, b);
         RESET_ERROR_CODE();
@@ -259,7 +259,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_rcf_neq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
+    bool Z3_API Z3_rcf_neq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) {
         Z3_TRY;
         LOG_Z3_rcf_neq(c, a, b);
         RESET_ERROR_CODE();
@@ -268,7 +268,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, Z3_bool compact, Z3_bool html) {
+    Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, bool compact, bool html) {
         Z3_TRY;
         LOG_Z3_rcf_num_to_string(c, a, compact, html);
         RESET_ERROR_CODE();
diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp
index 7a9ca80a7..6b48360a3 100644
--- a/src/api/api_seq.cpp
+++ b/src/api/api_seq.cpp
@@ -65,7 +65,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-    Z3_bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s) {
+    bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s) {
         Z3_TRY;
         LOG_Z3_is_seq_sort(c, s);
         RESET_ERROR_CODE();
@@ -73,7 +73,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s) {
+    bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s) {
         Z3_TRY;
         LOG_Z3_is_re_sort(c, s);
         RESET_ERROR_CODE();
@@ -81,7 +81,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s) {
+    bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s) {
         Z3_TRY;
         LOG_Z3_is_string_sort(c, s);
         RESET_ERROR_CODE();
@@ -89,7 +89,7 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-    Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s) {
+    bool Z3_API Z3_is_string(Z3_context c, Z3_ast s) {
         Z3_TRY;
         LOG_Z3_is_string(c, s);
         RESET_ERROR_CODE();
diff --git a/src/api/api_stats.cpp b/src/api/api_stats.cpp
index 6ab18c214..3ff87039f 100644
--- a/src/api/api_stats.cpp
+++ b/src/api/api_stats.cpp
@@ -74,7 +74,7 @@ extern "C" {
         Z3_CATCH_RETURN("");
     }
 
-    Z3_bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx) {
+    bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx) {
         Z3_TRY;
         LOG_Z3_stats_is_uint(c, s, idx);
         RESET_ERROR_CODE();
@@ -86,7 +86,7 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
-    Z3_bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx) {
+    bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx) {
         Z3_TRY;
         LOG_Z3_stats_is_double(c, s, idx);
         RESET_ERROR_CODE();
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index f2cb149cb..d5d3bc1ff 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -2036,7 +2036,7 @@ namespace z3 {
         expr eval(expr const & n, bool model_completion=false) const {
             check_context(*this, n);
             Z3_ast r = 0;
-            Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
+            bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
             check_error();
             if (status == false && ctx().enable_exceptions())
                 Z3_THROW(exception("failed to evaluate expression"));
@@ -2112,8 +2112,8 @@ namespace z3 {
         }
         unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
         std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
-        bool is_uint(unsigned i) const { Z3_bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; }
-        bool is_double(unsigned i) const { Z3_bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; }
+        bool is_uint(unsigned i) const { bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; }
+        bool is_double(unsigned i) const { bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; }
         unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
         double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
         friend std::ostream & operator<<(std::ostream & out, stats const & s);
@@ -2934,7 +2934,7 @@ namespace z3 {
     inline expr context::bv_val(uint64_t n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, s); check_error(); return expr(*this, r); }
     inline expr context::bv_val(char const * n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_numeral(m_ctx, n, s); check_error(); return expr(*this, r); }
     inline expr context::bv_val(unsigned n, bool const* bits) {
-        array<Z3_bool> _bits(n);
+        array<bool> _bits(n);
         for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
         Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
     }
diff --git a/src/api/z3_algebraic.h b/src/api/z3_algebraic.h
index c3f5337c2..1ebc1ad8f 100644
--- a/src/api/z3_algebraic.h
+++ b/src/api/z3_algebraic.h
@@ -36,7 +36,7 @@ extern "C" {
 
        def_API('Z3_algebraic_is_value', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a);
+    bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a);
 
     /**
        \brief Return \c true if \c a is positive, and \c false otherwise.
@@ -45,7 +45,7 @@ extern "C" {
 
        def_API('Z3_algebraic_is_pos', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a);
+    bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a);
 
     /**
        \brief Return \c true if \c a is negative, and \c false otherwise.
@@ -54,7 +54,7 @@ extern "C" {
 
        def_API('Z3_algebraic_is_neg', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a);
+    bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a);
 
     /**
        \brief Return \c true if \c a is zero, and \c false otherwise.
@@ -63,7 +63,7 @@ extern "C" {
 
        def_API('Z3_algebraic_is_zero', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_algebraic_is_zero(Z3_context c, Z3_ast a);
+    bool Z3_API Z3_algebraic_is_zero(Z3_context c, Z3_ast a);
 
     /**
        \brief Return 1 if \c a is positive, 0 if \c a is zero, and -1 if \c a is negative.
@@ -148,7 +148,7 @@ extern "C" {
 
        def_API('Z3_algebraic_lt', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
     */
-    Z3_bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b);
+    bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b);
 
     /**
        \brief Return \c true if a > b, and \c false otherwise.
@@ -158,7 +158,7 @@ extern "C" {
 
        def_API('Z3_algebraic_gt', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
     */
-    Z3_bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b);
+    bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b);
 
     /**
        \brief Return \c true if a <= b, and \c false otherwise.
@@ -168,7 +168,7 @@ extern "C" {
 
        def_API('Z3_algebraic_le', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
     */
-    Z3_bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b);
+    bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b);
 
     /**
        \brief Return \c true if a >= b, and \c false otherwise.
@@ -178,7 +178,7 @@ extern "C" {
 
        def_API('Z3_algebraic_ge', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
     */
-    Z3_bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b);
+    bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b);
 
     /**
        \brief Return \c true if a == b, and \c false otherwise.
@@ -188,7 +188,7 @@ extern "C" {
 
        def_API('Z3_algebraic_eq', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
     */
-    Z3_bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b);
+    bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b);
 
     /**
        \brief Return \c true if a != b, and \c false otherwise.
@@ -198,7 +198,7 @@ extern "C" {
 
        def_API('Z3_algebraic_neq', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
     */
-    Z3_bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b);
+    bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b);
 
     /**
        \brief Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index a94030d22..a85413491 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1641,7 +1641,7 @@ extern "C" {
 
        def_API('Z3_params_set_bool', VOID, (_in(CONTEXT), _in(PARAMS), _in(SYMBOL), _in(BOOL)))
     */
-    void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, Z3_bool v);
+    void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, bool v);
 
     /**
        \brief Add a unsigned parameter \c k with value \c v to the parameter set \c p.
@@ -2895,7 +2895,7 @@ extern "C" {
 
        def_API('Z3_mk_bv2int', AST, (_in(CONTEXT), _in(AST), _in(BOOL)))
     */
-    Z3_ast Z3_API Z3_mk_bv2int(Z3_context c,Z3_ast t1, Z3_bool is_signed);
+    Z3_ast Z3_API Z3_mk_bv2int(Z3_context c,Z3_ast t1, bool is_signed);
 
     /**
        \brief Create a predicate that checks that the bit-wise addition
@@ -2905,7 +2905,7 @@ extern "C" {
 
        def_API('Z3_mk_bvadd_no_overflow', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(BOOL)))
     */
-    Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed);
+    Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);
 
     /**
        \brief Create a predicate that checks that the bit-wise signed addition
@@ -2935,7 +2935,7 @@ extern "C" {
 
        def_API('Z3_mk_bvsub_no_underflow', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(BOOL)))
     */
-    Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed);
+    Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);
 
     /**
        \brief Create a predicate that checks that the bit-wise signed division
@@ -2965,7 +2965,7 @@ extern "C" {
 
        def_API('Z3_mk_bvmul_no_overflow', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(BOOL)))
     */
-    Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed);
+    Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);
 
     /**
        \brief Create a predicate that checks that the bit-wise signed multiplication
@@ -3269,7 +3269,7 @@ extern "C" {
        \sa Z3_mk_numeral
        def_API('Z3_mk_bv_numeral', AST, (_in(CONTEXT), _in(UINT), _in_array(1, BOOL)))
     */
-    Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, Z3_bool const* bits);
+    Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, bool const* bits);
 
     /*@}*/
 
@@ -3288,7 +3288,7 @@ extern "C" {
 
        def_API('Z3_is_seq_sort', BOOL, (_in(CONTEXT), _in(SORT)))
      */
-    Z3_bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s);
+    bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s);
 
     /**
        \brief Create a regular expression sort out of a sequence sort.
@@ -3302,7 +3302,7 @@ extern "C" {
 
        def_API('Z3_is_re_sort', BOOL, (_in(CONTEXT), _in(SORT)))
      */
-    Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s);
+    bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s);
 
     /**
        \brief Create a sort for 8 bit strings.
@@ -3319,7 +3319,7 @@ extern "C" {
 
        def_API('Z3_is_string_sort', BOOL, (_in(CONTEXT), _in(SORT)))
      */
-    Z3_bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s);
+    bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s);
 
     /**
        \brief Create a string constant out of the string that is passed in
@@ -3332,7 +3332,7 @@ extern "C" {
 
        def_API('Z3_is_string', BOOL, (_in(CONTEXT), _in(AST)))
      */
-    Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s);
+    bool Z3_API Z3_is_string(Z3_context c, Z3_ast s);
 
     /**
        \brief Retrieve the string constant stored in \c s.
@@ -3681,7 +3681,7 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_quantifier(
         Z3_context c,
-        Z3_bool is_forall,
+        bool is_forall,
         unsigned weight,
         unsigned num_patterns, Z3_pattern const patterns[],
         unsigned num_decls, Z3_sort const sorts[],
@@ -3715,7 +3715,7 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_quantifier_ex(
         Z3_context c,
-        Z3_bool is_forall,
+        bool is_forall,
         unsigned weight,
         Z3_symbol quantifier_id,
         Z3_symbol skolem_id,
@@ -3791,7 +3791,7 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_quantifier_const(
         Z3_context c,
-        Z3_bool is_forall,
+        bool is_forall,
         unsigned weight,
         unsigned num_bound,  Z3_app const bound[],
         unsigned num_patterns, Z3_pattern const patterns[],
@@ -3806,7 +3806,7 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_quantifier_const_ex(
         Z3_context c,
-        Z3_bool is_forall,
+        bool is_forall,
         unsigned weight,
         Z3_symbol quantifier_id,
         Z3_symbol skolem_id,
@@ -3929,7 +3929,7 @@ extern "C" {
 
        def_API('Z3_is_eq_sort', BOOL, (_in(CONTEXT), _in(SORT), _in(SORT)))
     */
-    Z3_bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2);
+    bool Z3_API Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2);
 
     /**
        \brief Return the sort kind (e.g., array, tuple, int, bool, etc).
@@ -4196,7 +4196,7 @@ extern "C" {
 
        def_API('Z3_is_eq_func_decl', BOOL, (_in(CONTEXT), _in(FUNC_DECL), _in(FUNC_DECL)))
     */
-    Z3_bool Z3_API Z3_is_eq_func_decl(Z3_context c, Z3_func_decl f1, Z3_func_decl f2);
+    bool Z3_API Z3_is_eq_func_decl(Z3_context c, Z3_func_decl f1, Z3_func_decl f2);
 
     /**
         \brief Return a unique identifier for \c f.
@@ -4375,7 +4375,7 @@ extern "C" {
 
        def_API('Z3_is_eq_ast', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
     */
-    Z3_bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2);
+    bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2);
 
     /**
         \brief Return a unique identifier for \c t.
@@ -4413,7 +4413,7 @@ extern "C" {
 
        def_API('Z3_is_well_sorted', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t);
+    bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t);
 
     /**
        \brief Return Z3_L_TRUE if \c a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.
@@ -4432,19 +4432,19 @@ extern "C" {
     /**
       def_API('Z3_is_app', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_is_app(Z3_context c, Z3_ast a);
+    bool Z3_API Z3_is_app(Z3_context c, Z3_ast a);
 
     /**
       def_API('Z3_is_numeral_ast', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a);
+    bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a);
 
     /**
        \brief Return true if the given AST is a real algebraic number.
 
        def_API('Z3_is_algebraic_number', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a);
+    bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a);
 
     /**
        \brief Convert an \c ast into an \c APP_AST. This is just type casting.
@@ -4524,7 +4524,7 @@ extern "C" {
 
        def_API('Z3_get_numeral_small', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _out(INT64)))
     */
-    Z3_bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, int64_t* num, int64_t* den);
+    bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, int64_t* num, int64_t* den);
 
     /**
        \brief Similar to #Z3_get_numeral_string, but only succeeds if
@@ -4536,7 +4536,7 @@ extern "C" {
 
        def_API('Z3_get_numeral_int', BOOL, (_in(CONTEXT), _in(AST), _out(INT)))
     */
-    Z3_bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int* i);
+    bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int* i);
 
     /**
        \brief Similar to #Z3_get_numeral_string, but only succeeds if
@@ -4548,7 +4548,7 @@ extern "C" {
 
        def_API('Z3_get_numeral_uint', BOOL, (_in(CONTEXT), _in(AST), _out(UINT)))
     */
-    Z3_bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned* u);
+    bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned* u);
 
     /**
        \brief Similar to #Z3_get_numeral_string, but only succeeds if
@@ -4560,7 +4560,7 @@ extern "C" {
 
        def_API('Z3_get_numeral_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64)))
     */
-    Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t* u);
+    bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t* u);
 
     /**
        \brief Similar to #Z3_get_numeral_string, but only succeeds if
@@ -4572,7 +4572,7 @@ extern "C" {
 
        def_API('Z3_get_numeral_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64)))
     */
-    Z3_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t* i);
+    bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t* i);
 
     /**
        \brief Similar to #Z3_get_numeral_string, but only succeeds if
@@ -4584,7 +4584,7 @@ extern "C" {
 
        def_API('Z3_get_numeral_rational_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _out(INT64)))
     */
-    Z3_bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, int64_t* num, int64_t* den);
+    bool Z3_API Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, int64_t* num, int64_t* den);
 
     /**
        \brief Return a lower bound for the given real algebraic number.
@@ -4643,7 +4643,7 @@ extern "C" {
 
        def_API('Z3_is_quantifier_forall', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a);
+    bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a);
 
     /**
        \brief Determine if ast is an existential quantifier.
@@ -4651,7 +4651,7 @@ extern "C" {
 
        def_API('Z3_is_quantifier_exists', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a);
+    bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a);
 
     /**
        \brief Determine if ast is a lambda expression.
@@ -4660,7 +4660,7 @@ extern "C" {
 
        def_API('Z3_is_lambda', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a);
+    bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a);
 
     /**
        \brief Obtain weight of quantifier.
@@ -4874,7 +4874,7 @@ extern "C" {
 
        def_API('Z3_model_eval', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _in(BOOL), _out(AST)))
     */
-    Z3_bool_opt Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast * v);
+    Z3_bool_opt Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v);
 
     /**
        \brief Return the interpretation (i.e., assignment) of constant \c a in the model \c m.
@@ -4892,7 +4892,7 @@ extern "C" {
 
        def_API('Z3_model_has_interp', BOOL, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL)))
     */
-    Z3_bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a);
+    bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a);
 
     /**
        \brief Return the interpretation of the function \c f in the model \c m.
@@ -5003,7 +5003,7 @@ extern "C" {
 
        def_API('Z3_is_as_array', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a);
+    bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a);
 
     /**
        \brief Return the function declaration \c f associated with a \ccode{(_ as_array f)} node.
@@ -5168,7 +5168,7 @@ extern "C" {
 
        extra_API('Z3_open_log', INT, (_in(STRING),))
     */
-    Z3_bool Z3_API Z3_open_log(Z3_string filename);
+    bool Z3_API Z3_open_log(Z3_string filename);
 
     /**
        \brief Append user-defined string to interaction log.
@@ -5196,7 +5196,7 @@ extern "C" {
 
        def_API('Z3_toggle_warning_messages', VOID, (_in(BOOL),))
     */
-    void Z3_API Z3_toggle_warning_messages(Z3_bool enabled);
+    void Z3_API Z3_toggle_warning_messages(bool enabled);
     /*@}*/
 
     /** @name String conversion */
@@ -5457,7 +5457,7 @@ extern "C" {
 
        def_API('Z3_mk_goal', GOAL, (_in(CONTEXT), _in(BOOL), _in(BOOL), _in(BOOL)))
     */
-    Z3_goal Z3_API Z3_mk_goal(Z3_context c, Z3_bool models, Z3_bool unsat_cores, Z3_bool proofs);
+    Z3_goal Z3_API Z3_mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs);
 
     /**
        \brief Increment the reference counter of the given goal.
@@ -5501,7 +5501,7 @@ extern "C" {
 
        def_API('Z3_goal_inconsistent', BOOL, (_in(CONTEXT), _in(GOAL)))
     */
-    Z3_bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g);
+    bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g);
 
     /**
        \brief Return the depth of the given goal. It tracks how many transformations were applied to it.
@@ -5545,14 +5545,14 @@ extern "C" {
 
        def_API('Z3_goal_is_decided_sat', BOOL, (_in(CONTEXT), _in(GOAL)))
     */
-    Z3_bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g);
+    bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g);
 
     /**
        \brief Return true if the goal contains false, and it is precise or the product of an over approximation.
 
        def_API('Z3_goal_is_decided_unsat', BOOL, (_in(CONTEXT), _in(GOAL)))
     */
-    Z3_bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g);
+    bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g);
 
     /**
        \brief Copy a goal \c g from the context \c source to the context \c target.
@@ -6376,7 +6376,7 @@ extern "C" {
 
        def_API('Z3_stats_is_uint', BOOL, (_in(CONTEXT), _in(STATS), _in(UINT)))
     */
-    Z3_bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx);
+    bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx);
 
     /**
        \brief Return \c true if the given statistical data is a double.
@@ -6385,7 +6385,7 @@ extern "C" {
 
        def_API('Z3_stats_is_double', BOOL, (_in(CONTEXT), _in(STATS), _in(UINT)))
     */
-    Z3_bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx);
+    bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx);
 
     /**
        \brief Return the unsigned value of the given statistical data.
diff --git a/src/api/z3_ast_containers.h b/src/api/z3_ast_containers.h
index c423a3286..c8438a2ad 100644
--- a/src/api/z3_ast_containers.h
+++ b/src/api/z3_ast_containers.h
@@ -138,7 +138,7 @@ extern "C" {
 
     def_API('Z3_ast_map_contains', BOOL, (_in(CONTEXT), _in(AST_MAP), _in(AST)))
     */
-    Z3_bool Z3_API Z3_ast_map_contains(Z3_context c, Z3_ast_map m, Z3_ast k);
+    bool Z3_API Z3_ast_map_contains(Z3_context c, Z3_ast_map m, Z3_ast k);
 
     /**
     \brief Return the value associated with the key \c k.
diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h
index 544d9372b..cc2091caa 100644
--- a/src/api/z3_fpa.h
+++ b/src/api/z3_fpa.h
@@ -233,7 +233,7 @@ extern "C" {
 
         def_API('Z3_mk_fpa_inf', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
     */
-    Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, Z3_bool negative);
+    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.
@@ -246,7 +246,7 @@ extern "C" {
 
         def_API('Z3_mk_fpa_zero', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
     */
-    Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, Z3_bool negative);
+    Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative);
 
     /**
         \brief Create an expression of FloatingPoint sort from three bit-vector expressions.
@@ -332,7 +332,7 @@ extern "C" {
 
         def_API('Z3_mk_fpa_numeral_int_uint', AST, (_in(CONTEXT), _in(BOOL), _in(INT), _in(UINT), _in(SORT)))
     */
-    Z3_ast Z3_API Z3_mk_fpa_numeral_int_uint(Z3_context c, Z3_bool sgn, signed exp, unsigned sig, Z3_sort ty);
+    Z3_ast Z3_API Z3_mk_fpa_numeral_int_uint(Z3_context c, bool sgn, signed exp, unsigned sig, Z3_sort ty);
 
     /**
         \brief Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
@@ -349,7 +349,7 @@ extern "C" {
 
         def_API('Z3_mk_fpa_numeral_int64_uint64', AST, (_in(CONTEXT), _in(BOOL), _in(INT64), _in(UINT64), _in(SORT)))
     */
-    Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64(Z3_context c, Z3_bool sgn, int64_t exp, uint64_t sig, Z3_sort ty);
+    Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64(Z3_context c, bool sgn, int64_t exp, uint64_t sig, Z3_sort ty);
 
     /**
         \brief Floating-point absolute value
@@ -830,7 +830,7 @@ extern "C" {
 
         def_API('Z3_fpa_is_numeral_nan', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t);
+    bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t);
 
     /**
         \brief Checks whether a given floating-point numeral is a +oo or -oo.
@@ -840,7 +840,7 @@ extern "C" {
 
         def_API('Z3_fpa_is_numeral_inf', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t);
+    bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t);
 
     /**
         \brief Checks whether a given floating-point numeral is +zero or -zero.
@@ -850,7 +850,7 @@ extern "C" {
 
         def_API('Z3_fpa_is_numeral_zero', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t);
+    bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t);
 
     /**
         \brief Checks whether a given floating-point numeral is normal.
@@ -860,7 +860,7 @@ extern "C" {
 
         def_API('Z3_fpa_is_numeral_normal', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t);
+    bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t);
 
     /**
         \brief Checks whether a given floating-point numeral is subnormal.
@@ -870,7 +870,7 @@ extern "C" {
 
         def_API('Z3_fpa_is_numeral_subnormal', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t);
+    bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t);
 
     /**
         \brief Checks whether a given floating-point numeral is positive.
@@ -880,7 +880,7 @@ extern "C" {
 
         def_API('Z3_fpa_is_numeral_positive', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t);
+    bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t);
 
     /**
         \brief Checks whether a given floating-point numeral is negative.
@@ -890,7 +890,7 @@ extern "C" {
 
         def_API('Z3_fpa_is_numeral_negative', BOOL, (_in(CONTEXT), _in(AST)))
     */
-    Z3_bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t);
+    bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t);
 
     /**
         \brief Retrieves the sign of a floating-point literal as a bit-vector expression.
@@ -928,7 +928,7 @@ extern "C" {
 
         def_API('Z3_fpa_get_numeral_sign', BOOL, (_in(CONTEXT), _in(AST), _out(INT)))
     */
-    Z3_bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int * sgn);
+    bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int * sgn);
 
     /**
         \brief Return the significand value of a floating-point numeral as a string.
@@ -956,7 +956,7 @@ extern "C" {
 
         def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64)))
     */
-    Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, uint64_t * n);
+    bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, uint64_t * n);
 
     /**
         \brief Return the exponent value of a floating-point numeral as a string.
@@ -970,7 +970,7 @@ extern "C" {
 
     def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST), _in(BOOL)))
     */
-    Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, Z3_bool biased);
+    Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, bool biased);
 
     /**
         \brief Return the exponent value of a floating-point numeral as a signed 64-bit integer
@@ -985,7 +985,7 @@ extern "C" {
 
         def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _in(BOOL)))
     */
-    Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, int64_t * n, Z3_bool biased);
+    bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, int64_t * n, bool biased);
 
     /**
         \brief Retrieves the exponent of a floating-point literal as a bit-vector expression.
@@ -999,7 +999,7 @@ extern "C" {
 
         def_API('Z3_fpa_get_numeral_exponent_bv', AST, (_in(CONTEXT), _in(AST), _in(BOOL)))
     */
-    Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, Z3_bool biased);
+    Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, bool biased);
 
     /**
         \brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
diff --git a/src/api/z3_private.h b/src/api/z3_private.h
index 7b60a6ab9..4d5e2d3bd 100644
--- a/src/api/z3_private.h
+++ b/src/api/z3_private.h
@@ -29,7 +29,7 @@ Notes:
 extern "C" {
 #endif // __cplusplus
 
-    Z3_bool Z3_API Z3_get_numeral_rational(Z3_context c, Z3_ast a, rational& r);
+    bool Z3_API Z3_get_numeral_rational(Z3_context c, Z3_ast a, rational& r);
 
 #ifdef __cplusplus
 };
diff --git a/src/api/z3_rcf.h b/src/api/z3_rcf.h
index cc8e5a525..dc025bddd 100644
--- a/src/api/z3_rcf.h
+++ b/src/api/z3_rcf.h
@@ -138,49 +138,49 @@ extern "C" {
 
        def_API('Z3_rcf_lt', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
     */
-    Z3_bool Z3_API Z3_rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
+    bool Z3_API Z3_rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
     /**
        \brief Return \c true if a > b
 
        def_API('Z3_rcf_gt', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
     */
-    Z3_bool Z3_API Z3_rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
+    bool Z3_API Z3_rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
     /**
        \brief Return \c true if a <= b
 
        def_API('Z3_rcf_le', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
     */
-    Z3_bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
+    bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
     /**
        \brief Return \c true if a >= b
 
        def_API('Z3_rcf_ge', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
     */
-    Z3_bool Z3_API Z3_rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
+    bool Z3_API Z3_rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
     /**
        \brief Return \c true if a == b
 
        def_API('Z3_rcf_eq', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
     */
-    Z3_bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
+    bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
     /**
        \brief Return \c true if a != b
 
        def_API('Z3_rcf_neq', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
     */
-    Z3_bool Z3_API Z3_rcf_neq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
+    bool Z3_API Z3_rcf_neq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
     /**
        \brief Convert the RCF numeral into a string.
 
        def_API('Z3_rcf_num_to_string', STRING, (_in(CONTEXT), _in(RCF_NUM), _in(BOOL), _in(BOOL)))
     */
-    Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, Z3_bool compact, Z3_bool html);
+    Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, bool compact, bool html);
 
     /**
        \brief Convert the RCF numeral into a string in decimal notation.
diff --git a/src/test/no_overflow.cpp b/src/test/no_overflow.cpp
index 9ad629383..eb26866a5 100644
--- a/src/test/no_overflow.cpp
+++ b/src/test/no_overflow.cpp
@@ -530,7 +530,7 @@ void test_div(unsigned bvsize) {
     Z3_del_context(ctx);
 }
 
-typedef Z3_ast (Z3_API *NO_OVFL_ARITH_FUNC)(Z3_context ctx, Z3_ast t1, Z3_ast t2, Z3_bool is_signed);
+typedef Z3_ast (Z3_API *NO_OVFL_ARITH_FUNC)(Z3_context ctx, Z3_ast t1, Z3_ast t2, bool is_signed);
 typedef Z3_ast (Z3_API *ARITH_FUNC)(Z3_context ctx, Z3_ast t1, Z3_ast t2);
 
 typedef enum { OVFL_FUNC, UDFL_FUNC } overflow_type;
@@ -546,11 +546,11 @@ typedef struct {
     bool               sign_compar; // whether signed comparison should be used even for unsigned operation
 } Equivalence_params;
 
-Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow_wrapper(Z3_context ctx, Z3_ast t1, Z3_ast t2, Z3_bool is_signed) {
+Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow_wrapper(Z3_context ctx, Z3_ast t1, Z3_ast t2, bool is_signed) {
     return Z3_mk_bvsdiv_no_overflow(ctx, t1, t2);
 }
 
-Z3_ast Z3_API Z3_mk_bvneg_no_overflow_wrapper(Z3_context ctx, Z3_ast t1, Z3_ast t2, Z3_bool is_signed) {
+Z3_ast Z3_API Z3_mk_bvneg_no_overflow_wrapper(Z3_context ctx, Z3_ast t1, Z3_ast t2, bool is_signed) {
     return Z3_mk_bvneg_no_overflow(ctx, t1);
 }
 
@@ -558,15 +558,15 @@ Z3_ast Z3_API Z3_mk_bvneg_wrapper(Z3_context ctx, Z3_ast t1, Z3_ast t2) {
     return Z3_mk_bvneg(ctx, t1);
 }
 
-Z3_ast Z3_API Z3_mk_bvadd_no_underflow_wrapper(Z3_context ctx, Z3_ast t1, Z3_ast t2, Z3_bool is_signed) {
+Z3_ast Z3_API Z3_mk_bvadd_no_underflow_wrapper(Z3_context ctx, Z3_ast t1, Z3_ast t2, bool is_signed) {
     return Z3_mk_bvadd_no_underflow(ctx, t1, t2);
 }
 
-Z3_ast Z3_API Z3_mk_bvsub_no_overflow_wrapper(Z3_context ctx, Z3_ast t1, Z3_ast t2, Z3_bool is_signed) {
+Z3_ast Z3_API Z3_mk_bvsub_no_overflow_wrapper(Z3_context ctx, Z3_ast t1, Z3_ast t2, bool is_signed) {
     return Z3_mk_bvsub_no_overflow(ctx, t1, t2);
 }
 
-Z3_ast Z3_API Z3_mk_bvmul_no_underflow_wrapper(Z3_context ctx, Z3_ast t1, Z3_ast t2, Z3_bool is_signed) {
+Z3_ast Z3_API Z3_mk_bvmul_no_underflow_wrapper(Z3_context ctx, Z3_ast t1, Z3_ast t2, bool is_signed) {
     return Z3_mk_bvmul_no_underflow(ctx, t1, t2);
 }