address compiler warnings gcc-13

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/proofs/proof_utils.h

@@ -230,7 +230,7 @@ public:
                    << "New pf: " << mk_pp(newp, m) << "\n";);
         }
 
-        proof *r;
+        proof *r = nullptr;
         VERIFY(cache.find(pr, r));
 
         DEBUG_CODE(

src/ast/simplifiers/dominator_simplifier.cpp

@@ -187,8 +187,8 @@ expr_ref dominator_simplifier::simplify_and_or(bool is_and, app * e) {
 }
 
 expr_ref dominator_simplifier::simplify_not(app * e) {
-    expr *ee;
+    expr *ee = nullptr;
-    ENSURE(m.is_not(e, ee));
+    VERIFY(m.is_not(e, ee));
     unsigned old_lvl = scope_level();
     expr_ref t = simplify_rec(ee);
     local_pop(scope_level() - old_lvl);

src/ast/sls/bv_sls_eval.cpp

@@ -145,7 +145,6 @@ namespace bv {
         SASSERT(m.is_bool(e));
         SASSERT(e->get_family_id() == basic_family_id);
 
-        auto id = e->get_id();
         switch (e->get_decl_kind()) {
         case OP_TRUE:
             return true;

src/muz/spacer/spacer_concretize.cpp

@@ -27,7 +27,7 @@ struct proc {
     void operator()(var *n) const {}
     void operator()(quantifier *q) const {}
     void operator()(app const *n) const {
-        expr *e1, *e2;
+        expr *e1 = nullptr, *e2 = nullptr;
         if (m_arith.is_mul(n, e1, e2)) {
             if (is_var(e1) && !is_var(e2))
                 m_marks.mark(e2);
@@ -71,7 +71,7 @@ bool pob_concretizer::apply(const expr_ref_vector &cube, expr_ref_vector &out) {
 }
 
 bool pob_concretizer::is_split_var(expr *e, expr *&var, bool &pos) {
-    expr *e1, *e2;
+    expr *e1 = nullptr, *e2 = nullptr;
     rational n;
 
     if (m_var_marks.is_marked(e)) {
@@ -89,7 +89,7 @@ bool pob_concretizer::is_split_var(expr *e, expr *&var, bool &pos) {
 }
 
 void pob_concretizer::split_lit_le_lt(expr *_lit, expr_ref_vector &out) {
-    expr *e1, *e2;
+    expr *e1 = nullptr, *e2 = nullptr;
 
     expr *lit = _lit;
     m.is_not(_lit, lit);
@@ -133,7 +133,7 @@ void pob_concretizer::split_lit_le_lt(expr *_lit, expr_ref_vector &out) {
 }
 
 void pob_concretizer::split_lit_ge_gt(expr *_lit, expr_ref_vector &out) {
-    expr *e1, *e2;
+    expr *e1 = nullptr, *e2 = nullptr;
 
     expr *lit = _lit;
     m.is_not(_lit, lit);
@@ -182,7 +182,7 @@ bool pob_concretizer::apply_lit(expr *_lit, expr_ref_vector &out) {
 
     // split literals of the form a1*x1 + ... + an*xn ~ c, where c is a
     // constant, ~ is <, <=, >, or >=, and the top level operator of LHS is +
-    expr *e1, *e2;
+    expr *e1 = nullptr, *e2 = nullptr;
     if ((m_arith.is_lt(lit, e1, e2) || m_arith.is_le(lit, e1, e2)) &&
         m_arith.is_add(e1)) {
         SASSERT(m_arith.is_numeral(e2));

src/nlsat/nlsat_explain.cpp

@@ -126,7 +126,7 @@ namespace nlsat {
         scoped_literal_vector   m_core2;
 
         // temporary fields for storing the result
-        scoped_literal_vector * m_result;
+        scoped_literal_vector * m_result = nullptr;
         svector<char>           m_already_added_literal;
 
         evaluator &             m_evaluator;
@@ -149,8 +149,6 @@ namespace nlsat {
             m_todo(u),
             m_core1(s),
             m_core2(s),
-            m_result(nullptr),
-
             m_cell_sample(is_sample),
 
             m_evaluator(ev) {

src/nlsat/nlsat_simplify.cpp

@@ -93,7 +93,6 @@ namespace nlsat {
         }
 
         void update_clauses(u_map<literal> const& b2l) {
-            bool is_sat = true;
             literal_vector lits;
             unsigned n = m_clauses.size();
 

src/nlsat/nlsat_solver.cpp

@@ -634,7 +634,7 @@ namespace nlsat {
                     if (sign < 0)
                         k = atom::flip(k);
                     sign = 1;
-                    polynomial::manager::ineq_type t;
+                    polynomial::manager::ineq_type t = polynomial::manager::ineq_type::EQ;
                     switch (k) {
                     case atom::EQ: t = polynomial::manager::ineq_type::EQ; break;
                     case atom::LT: t = polynomial::manager::ineq_type::LT; break;

src/qe/mbp/mbp_arrays_tg.cpp

@@ -116,7 +116,7 @@ struct mbp_array_tg::impl {
     bool is_rd_wr(expr* t, expr*& wr_ind, expr*& rd_ind, expr*& b, expr*& v) {
         if (!is_rd_wr(t))
             return false;
-        expr* a;
+        expr* a = nullptr;
         VERIFY(m_array_util.is_select1(t, a, rd_ind));
         VERIFY(m_array_util.is_store1(a, b, wr_ind, v));
         return true;
@@ -185,7 +185,7 @@ struct mbp_array_tg::impl {
     // or              &&_{i \in indices} j \neq i &&
     //                        !(select(y, j) = elem)
     void elimwreq(peq p, bool is_neg) {
-        expr* a, *j, *elem;
+        expr* a = nullptr, *j = nullptr, *elem = nullptr;
         VERIFY(is_arr_write(p.lhs(), a, j, elem));
         TRACE("mbp_tg",
               tout << "applying elimwreq on " << expr_ref(p.mk_peq(), m) << " is neg: " << is_neg;);
@@ -279,7 +279,7 @@ struct mbp_array_tg::impl {
     // rewrite select(store(a, i, k), j) into either select(a, j) or k
     void elimrdwr(expr *term) {
         TRACE("mbp_tg", tout << "applying elimrdwr on " << expr_ref(term, m););
-        expr* wr_ind, *rd_ind, *b, *v;
+        expr* wr_ind = nullptr, *rd_ind = nullptr, *b = nullptr, *v = nullptr;
         VERIFY(is_rd_wr(term, wr_ind, rd_ind, b, v));
         if (m_mdl.are_equal(wr_ind, rd_ind)) 
             m_tg.add_eq(wr_ind, rd_ind);

src/sat/sat_aig_cuts.cpp

@@ -534,7 +534,7 @@ namespace sat {
     }
 
     cut_val aig_cuts::eval(node const& n, cut_eval const& env) const {
-        uint64_t result;
+        uint64_t result = 0;
         switch (n.op()) {
         case var_op:
             UNREACHABLE();