diff --git a/src/ast/pattern/pattern_inference.h b/src/ast/pattern/pattern_inference.h
index 09c4e333b..d35aa3d28 100644
--- a/src/ast/pattern/pattern_inference.h
+++ b/src/ast/pattern/pattern_inference.h
@@ -136,8 +136,8 @@ class pattern_inference_cfg :  public default_rewriter_cfg {
         
         ast_manager &            m;
         pattern_inference_cfg &     m_owner;
-        family_id                m_afid;
-        unsigned                 m_num_bindings;
+        family_id                m_afid = null_family_id;
+        unsigned                 m_num_bindings = 0;
         typedef map<entry, info *, obj_hash<entry>, default_eq<entry> > cache;
         cache                    m_cache;
         ptr_vector<info>         m_info;
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 44bed09c6..70824c5e4 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -105,7 +105,7 @@ bool rewriter_tpl<Config>::process_const(app * t0) {
             return true;
         }
         m_r = t;
-        // fall through
+        Z3_fallthrough;      
     case BR_DONE:
         result_stack().push_back(m_r.get());
         if (ProofGen) {
diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index a39ef5ef9..82154c961 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -26,18 +26,18 @@ namespace nla {
 class cross_nested {
     
     // fields
-    nex *                                             m_e;
+    nex *                                             m_e = nullptr;
     std::function<bool (const nex*)>                  m_call_on_result;
     std::function<bool (unsigned)>                    m_var_is_fixed;
     std::function<unsigned ()>                        m_random;    
-    bool                                              m_done;
+    bool                                              m_done = false;
     ptr_vector<nex>                                   m_b_split_vec;
-    int                                               m_reported;
-    bool                                              m_random_bit;
+    int                                               m_reported = 0;
+    bool                                              m_random_bit = false;
     std::function<nex_scalar*()>                      m_mk_scalar;
     nex_creator&                                      m_nex_creator;
 #ifdef Z3DEBUG
-    nex* m_e_clone;
+    nex* m_e_clone = nullptr;
 #endif
 public:
     
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index 0d47877c7..d0c388282 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -224,7 +224,7 @@ public:
     unsigned         limit_on_rows_for_hnf_cutter = 75;
     unsigned         limit_on_columns_for_hnf_cutter = 150;
 private:
-    unsigned         m_nlsat_delay;
+    unsigned         m_nlsat_delay = 0;
     bool             m_enable_hnf = true;
     bool             m_print_external_var_name = false;
     bool             m_propagate_eqs = false;
diff --git a/src/util/stacked_value.h b/src/util/stacked_value.h
index a3a0d933b..b92cac0a0 100644
--- a/src/util/stacked_value.h
+++ b/src/util/stacked_value.h
@@ -52,7 +52,7 @@ public:
         }
     }
 
-    stacked_value() = default;
+    stacked_value(): m_value() { }
     stacked_value(const T& m) {
         m_value = m;
     }