From 8d2b9b41fdd68c73f73b4c95e7309e7fef52d6cb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 12 Jan 2025 13:39:13 -0800
Subject: [PATCH] fix compiler warnings

---
 src/math/lp/lar_solver.cpp        | 2 ++
 src/math/lp/lp_bound_propagator.h | 2 +-
 src/math/lp/var_register.h        | 4 ++--
 3 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 175fdcd01..0c458dbfa 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -2097,6 +2097,7 @@ namespace lp {
         switch (kind) {
             case LT:
                 y_of_bound = -1;
+                Z3_fallthrough;
             case LE: {
                 auto up = numeric_pair<mpq>(right_side, y_of_bound);
                 if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
@@ -2213,6 +2214,7 @@ namespace lp {
             } break;
             case GT:
                 y_of_bound = 1;
+                Z3_fallthrough;
             case GE: {
                 auto low = numeric_pair<mpq>(right_side, y_of_bound);
                 m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index daeac3b18..e2ebbfbed 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -28,7 +28,7 @@ class lp_bound_propagator {
     // works for rows of the form x - y + sum of fixed = 0    
     map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_row2index_neg;
 
-    const vector<column_type>*                         m_column_types;
+    const vector<column_type>*                         m_column_types = nullptr;
     // returns true iff there is only one non-fixed column in the row
     bool only_one_nfixed(unsigned r, unsigned& x) {
         x = UINT_MAX;
diff --git a/src/math/lp/var_register.h b/src/math/lp/var_register.h
index 84ac8236d..6e1e8f313 100644
--- a/src/math/lp/var_register.h
+++ b/src/math/lp/var_register.h
@@ -23,8 +23,8 @@ namespace lp  {
 
 
 class ext_var_info {
-    unsigned m_external_j;
-    bool m_is_integer;
+    unsigned m_external_j = 0;
+    bool m_is_integer = false;
     std::string m_name;
 public:
     ext_var_info() = default;