diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index d3dfe2812..1e4b3554d 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -236,7 +236,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
 
     unsigned sz = buffer.size();
 
-    switch(sz) {
+    switch (sz) {
     case 0:
         result = m().mk_false();
         return BR_DONE;
@@ -298,7 +298,7 @@ br_status bool_rewriter::mk_flat_or_core(unsigned num_args, expr * const * args,
 }
 
 expr * bool_rewriter::mk_or_app(unsigned num_args, expr * const * args) {
-    switch(num_args) {
+    switch (num_args) {
     case 0: return m().mk_false();
     case 1: return args[0];
     default: return m().mk_or(num_args, args);
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index c2a5e1d16..64955ad4b 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -205,7 +205,7 @@ public:
     void try_add_equation_with_val_table(const vertex *v) {
         SASSERT(m_fixed_vertex);
         unsigned v_j = v->column();
-        vertex *u;
+        vertex *u = nullptr;
         if (!m_vals_to_verts.find(val(v_j), u)) {
             m_vals_to_verts.insert(val(v_j), u);
             return;