diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index ae9c060e9..e2d480664 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -61,7 +61,7 @@ namespace recfun {
         expr_ref_vector     m_guards; //<! conjunction that is equivalent to this case
         expr_ref            m_rhs; //<! if guard is true, `f(t1...tn) = rhs` holds
         def *               m_def; //<! definition this is a part of
-        bool                m_immediate; //<! does `rhs` contain no defined_fun/case_pred?
+        bool                m_immediate = false; //<! does `rhs` contain no defined_fun/case_pred?
 
         case_def(ast_manager& m):
             m_pred(m),
diff --git a/src/ast/rewriter/macro_replacer.cpp b/src/ast/rewriter/macro_replacer.cpp
index d8389ae6a..1cbcc14c6 100644
--- a/src/ast/rewriter/macro_replacer.cpp
+++ b/src/ast/rewriter/macro_replacer.cpp
@@ -78,8 +78,7 @@ struct macro_replacer::macro_replacer_cfg : public default_rewriter_cfg {
             return false;
         p = nullptr;
         app* n = to_app(_n);
-        quantifier* q = nullptr;
-        func_decl* d = n->get_decl(), * d2 = nullptr;
+        func_decl* d = n->get_decl();
         app_ref head(m);
         expr_ref def(m);
         expr_dependency_ref dep(m);
diff --git a/src/ast/simplifiers/bound_simplifier.h b/src/ast/simplifiers/bound_simplifier.h
index c7739715e..06e25920c 100644
--- a/src/ast/simplifiers/bound_simplifier.h
+++ b/src/ast/simplifiers/bound_simplifier.h
@@ -27,9 +27,9 @@ Description:
 
 
 class bound_simplifier : public dependent_expr_simplifier {
-    typedef interval_manager<im_default_config> interval_manager;
-    typedef interval_manager::interval interval;
-    typedef _scoped_interval<interval_manager> scoped_interval;
+    typedef interval_manager<im_default_config> _interval_manager;
+    typedef _interval_manager::interval interval;
+    typedef _scoped_interval<_interval_manager> scoped_interval;
 
     arith_util              a;
     th_rewriter             m_rewriter;
@@ -37,7 +37,7 @@ class bound_simplifier : public dependent_expr_simplifier {
     small_object_allocator  m_alloc;
     bound_propagator        bp;
     im_default_config       i_cfg;
-    interval_manager        i_manager;
+    _interval_manager       i_manager;
     unsigned                m_num_vars = 0;
     ptr_vector<expr>        m_var2expr;
     unsigned_vector         m_expr2var;
diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h
index 7b5dec945..3818b589a 100644
--- a/src/math/lp/lp_primal_core_solver_def.h
+++ b/src/math/lp/lp_primal_core_solver_def.h
@@ -480,7 +480,7 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_
 template <typename T, typename X>    int lp_primal_core_solver<T, X>::find_leaving_and_t(unsigned entering, X & t) {
     if (this->m_settings.use_breakpoints_in_feasibility_search && !this->current_x_is_feasible())
         return find_leaving_and_t_with_breakpoints(entering, t);
-    X theta;
+    X theta = zero_of_type<X>();
     bool unlimited = get_harris_theta(theta);
     lp_assert(unlimited || theta >= zero_of_type<X>());
     if (try_jump_to_another_bound_on_entering(entering, theta, t, unlimited)) return entering;