fix un-intialized variable warnings

src/math/lp/nla_core.cpp

@@ -1678,7 +1678,7 @@ bool core::is_nl_var(lpvar j) const {
 
 
 unsigned core::get_var_weight(lpvar j) const {
-    unsigned k;
+    unsigned k = 0;
     switch (lra.get_column_type(j)) {
 
     case lp::column_type::fixed:

src/muz/base/dl_context.cpp

@@ -313,7 +313,7 @@ namespace datalog {
     void context::register_finite_sort(sort * s, sort_kind k) {
         m_pinned.push_back(s);
         SASSERT(!m_sorts.contains(s));
-        sort_domain * dom;
+        sort_domain * dom = nullptr;
         switch (k) {
         case SK_SYMBOL:
             dom = alloc(symbol_sort_domain, *this, s);

src/muz/spacer/spacer_antiunify.cpp

@@ -158,7 +158,7 @@ void anti_unifier::operator()(expr *e1, expr *e2, expr_ref &res,
         m_todo.pop_back();
     }
 
-    expr *r;
+    expr *r = nullptr;
     VERIFY(m_cache.find(e1, e2, r));
     res = r;
 

src/muz/spacer/spacer_context.h

@@ -404,7 +404,7 @@ class pred_transformer {
         }
         pt_rule &mk_rule(const pt_rule &v);
         void set_tag(expr *tag, pt_rule &v) {
-            pt_rule *p;
+            pt_rule *p = nullptr;
             VERIFY(find_by_rule(v.rule(), p));
             p->set_tag(tag);
             m_tags.insert(tag, p);
@@ -569,7 +569,7 @@ class pred_transformer {
     expr *transition() const { return m_transition; }
     expr *init() const { return m_init; }
     expr *rule2tag(datalog::rule const *r) {
-        pt_rule *p;
+        pt_rule *p = nullptr;
         return m_pt_rules.find_by_rule(*r, p) ? p->tag() : nullptr;
     }
     unsigned get_num_levels() const { return m_frames.size(); }
@@ -600,7 +600,7 @@ class pred_transformer {
                                    bool_vector &reach_pred_used,
                                    unsigned &num_reuse_reach);
     expr *get_transition(datalog::rule const &r) {
-        pt_rule *p;
+        pt_rule *p = nullptr;
         return m_pt_rules.find_by_rule(r, p) ? p->trans() : nullptr;
     }
     ptr_vector<app> &get_aux_vars(datalog::rule const &r) {

src/muz/spacer/spacer_legacy_mev.cpp

@@ -569,7 +569,7 @@ void model_evaluator::eval_eq(app* e, expr* arg1, expr* arg2)
 void model_evaluator::eval_basic(app* e)
 {
     expr* arg1, *arg2;
-    expr *argCond, *argThen, *argElse, *arg;
+    expr *argCond = nullptr, *argThen = nullptr, *argElse = nullptr, *arg = nullptr;
     bool has_x = false;
     unsigned arity = e->get_num_args();
     switch (e->get_decl_kind()) {

src/sat/smt/arith_axioms.cpp

@@ -207,7 +207,7 @@ namespace arith {
 
     bool solver::check_bv_term(app* n) {
         unsigned sz;
-        expr* _x, * _y;
+        expr* _x = nullptr, * _y = nullptr;
         if (!ctx.is_relevant(expr2enode(n)))
             return true;
         expr_ref vx(m), vy(m),vn(m);

src/smt/theory_arith_int.h

@@ -360,7 +360,7 @@ namespace smt {
         for (unsigned i = 1; i < unsat_row.size(); ++i) {
             numeral c(unsat_row[i]);
             if (!c.is_zero()) {
-                theory_var var;
+                theory_var var = null_theory_var;
                 if (!index2var.find(i, var)) {
                     UNREACHABLE();
                 }

src/smt/theory_lra.cpp

@@ -1572,7 +1572,7 @@ public:
     }
 
     final_check_status eval_power(expr* e) {
-        expr* x, * y;
+        expr* x = nullptr, * y = nullptr;
         rational r;
         VERIFY(a.is_power(e, x, y));
         if (a.is_numeral(x, r) && r == 0 && a.is_numeral(y, r) && r == 0)