diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp
index 8c18df7b2..9130d628c 100644
--- a/src/ackermannization/lackr.cpp
+++ b/src/ackermannization/lackr.cpp
@@ -220,7 +220,7 @@ lbool lackr::lazy() {
     lackr_model_constructor mc(m_m, m_info);
     push_abstraction();
     unsigned ackr_head = 0;
-    while (1) {
+    while (true) {
         m_st.m_it++;
         checkpoint();
         TRACE("lackr", tout << "lazy check: " << m_st.m_it << "\n";);
diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index cdc592527..604267536 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -913,7 +913,7 @@ extern "C" {
         CHECK_VALID_AST(t, 0);
         if (sgn == nullptr) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "sign cannot be a nullpointer");
-            return 0;
+            return false;
         }
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();
@@ -922,13 +922,13 @@ extern "C" {
         expr * e = to_expr(t);
         if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
-            return 0;
+            return false;
         }
         scoped_mpf val(mpfm);
         bool r = plugin->is_numeral(to_expr(t), val);
         if (!r || mpfm.is_nan(val)) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
-            return 0;
+            return false;
         }
         *sgn = mpfm.sgn(val);
         return r;
@@ -1043,7 +1043,7 @@ extern "C" {
         CHECK_VALID_AST(t, 0);
         if (n == nullptr) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "invalid nullptr argument");
-            return 0;
+            return false;
         }
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();
@@ -1055,7 +1055,7 @@ extern "C" {
         if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
             *n = 0;
-            return 0;
+            return false;
         }
         scoped_mpf val(mpfm);
         bool r = plugin->is_numeral(e, val);
@@ -1065,10 +1065,10 @@ extern "C" {
             !mpzm.is_uint64(z)) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
             *n = 0;
-            return 0;
+            return false;
         }
         *n = mpzm.get_uint64(z);
-        return 1;
+        return true;
         Z3_CATCH_RETURN(0);
     }
 
@@ -1121,7 +1121,7 @@ extern "C" {
         CHECK_VALID_AST(t, 0);
         if (n == nullptr) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "invalid null argument");
-            return 0;
+            return false;
         }
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();
@@ -1132,14 +1132,14 @@ extern "C" {
         if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
             *n = 0;
-            return 0;
+            return false;
         }
         scoped_mpf val(mpfm);
         bool r = plugin->is_numeral(e, val);
         if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
             *n = 0;
-            return 0;
+            return false;
         }
         unsigned ebits = val.get().get_ebits();
         if (biased) {
@@ -1153,7 +1153,7 @@ extern "C" {
                   mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) :
                  mpfm.exp(val);
         }
-        return 1;
+        return true;
         Z3_CATCH_RETURN(0);
     }
 
@@ -1240,7 +1240,7 @@ extern "C" {
         fpa_util & fu = ctx->fpautil();
         if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return 0;
+            return false;
         }
         return fu.is_nan(to_expr(t));
         Z3_CATCH_RETURN(Z3_FALSE);
@@ -1254,7 +1254,7 @@ extern "C" {
         fpa_util & fu = ctx->fpautil();
         if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return 0;
+            return false;
         }
         return fu.is_inf(to_expr(t));
         Z3_CATCH_RETURN(Z3_FALSE);
@@ -1268,7 +1268,7 @@ extern "C" {
         fpa_util & fu = ctx->fpautil();
         if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return 0;
+            return false;
         }
         return fu.is_zero(to_expr(t));
         Z3_CATCH_RETURN(Z3_FALSE);
@@ -1282,7 +1282,7 @@ extern "C" {
         fpa_util & fu = ctx->fpautil();
         if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return 0;
+            return false;
         }
         return fu.is_normal(to_expr(t));
         Z3_CATCH_RETURN(Z3_FALSE);
@@ -1296,7 +1296,7 @@ extern "C" {
         fpa_util & fu = ctx->fpautil();
         if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return 0;
+            return false;
         }
         return fu.is_subnormal(to_expr(t));
         Z3_CATCH_RETURN(Z3_FALSE);
@@ -1310,7 +1310,7 @@ extern "C" {
         fpa_util & fu = ctx->fpautil();
         if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return 0;
+            return false;
         }
         return fu.is_positive(to_expr(t));
         Z3_CATCH_RETURN(Z3_FALSE);
@@ -1324,7 +1324,7 @@ extern "C" {
         fpa_util & fu = ctx->fpautil();
         if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return 0;
+            return false;
         }
         return fu.is_negative(to_expr(t));
         Z3_CATCH_RETURN(Z3_FALSE);
diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp
index 49aa09727..fe9faa2a5 100644
--- a/src/api/api_quant.cpp
+++ b/src/api/api_quant.cpp
@@ -132,7 +132,7 @@ extern "C" {
                                unsigned num_decls, Z3_sort const types[],
                                Z3_symbol const decl_names[],
                                Z3_ast body) {
-        return Z3_mk_quantifier(c, 1, weight, num_patterns, patterns, num_decls, types, decl_names, body);
+        return Z3_mk_quantifier(c, true, weight, num_patterns, patterns, num_decls, types, decl_names, body);
     }
 
     Z3_ast Z3_API Z3_mk_exists(Z3_context c,
@@ -141,7 +141,7 @@ extern "C" {
                                unsigned num_decls, Z3_sort const types[],
                                Z3_symbol const decl_names[],
                                Z3_ast body) {
-        return Z3_mk_quantifier(c, 0, weight, num_patterns, patterns, num_decls, types, decl_names, body);
+        return Z3_mk_quantifier(c, false, weight, num_patterns, patterns, num_decls, types, decl_names, body);
     }
 
     Z3_ast Z3_API Z3_mk_lambda(Z3_context c,
diff --git a/src/ast/rewriter/bv_bounds.cpp b/src/ast/rewriter/bv_bounds.cpp
index f337ca638..f30df7890 100644
--- a/src/ast/rewriter/bv_bounds.cpp
+++ b/src/ast/rewriter/bv_bounds.cpp
@@ -111,7 +111,7 @@ bv_bounds::conv_res bv_bounds::convert(expr * e, vector<ninterval>& nis, bool ne
     numeral val, val1;
     unsigned bv_sz1;
 
-    if (0) {
+    if (false) {
         if (m_m.is_eq(e, lhs, rhs) && to_bound(lhs) && m_bv_util.is_numeral(rhs, val, bv_sz1)) {
             return record(to_app(lhs), val, val, negated, nis);
         }
@@ -125,7 +125,7 @@ bv_bounds::conv_res bv_bounds::convert(expr * e, vector<ninterval>& nis, bool ne
         return record(to_app(lhs), numeral::zero(), val, negated, nis);
     }
 
-    if (1) {
+    if (true) {
         numeral rhs_val;
         unsigned rhs_sz;
         if (m_m.is_eq(e, lhs, rhs)
@@ -343,7 +343,7 @@ bool bv_bounds::add_constraint(expr* e) {
     numeral val, val1;
     unsigned bv_sz1;
 
-    if (0) {
+    if (false) {
         if (m_m.is_eq(e, lhs, rhs) && to_bound(lhs) && m_bv_util.is_numeral(rhs, val, bv_sz1)) {
             return add_bound_unsigned(to_app(lhs), val, val, negated);
         }
diff --git a/src/muz/transforms/dl_mk_array_instantiation.cpp b/src/muz/transforms/dl_mk_array_instantiation.cpp
index 6a8f0ce81..626109528 100644
--- a/src/muz/transforms/dl_mk_array_instantiation.cpp
+++ b/src/muz/transforms/dl_mk_array_instantiation.cpp
@@ -300,7 +300,7 @@ namespace datalog {
     expr_ref_vector res(m);
 
     svector<unsigned> chosen(arg_correspondance.size(), 0u);
-    while(1)
+    while(true)
     {
       expr_ref_vector new_args(m);
       for(unsigned i=0;i<chosen.size();i++)