From 62126fd6e26102e814b73a71cca424c9f821b23d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 10 Feb 2025 11:51:21 -0800
Subject: [PATCH] fix build warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/sls_arith_base.cpp      |  4 +---
 src/ast/sls/sls_arith_clausal.cpp   |  5 ++++-
 src/ast/sls/sls_datatype_plugin.cpp |  3 ++-
 src/ast/sls/sls_seq_plugin.cpp      | 12 ++++++------
 4 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index ebc9f08e3..479134eae 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -497,7 +497,7 @@ namespace sls {
         else if (is_op(v) && m_allow_recursive_delta) 
             add_update(get_op(v), delta_out);        
         else if (vi.is_if_op() && m_allow_recursive_delta) {
-            expr* c, * t, * e;
+            expr* c = nullptr, * t = nullptr, * e = nullptr;
             VERIFY(m.is_ite(vi.m_expr, c, t, e));
             bool cond = ctx.is_true(c);
             if (cond)
@@ -540,7 +540,6 @@ namespace sls {
         num_t arg2 = value(od.m_arg2);
 
         if (arg2 != 0) {
-            num_t val = div(arg1, arg2);
             if (arg2 > 0)
                 add_update(od.m_arg1, delta * arg2);
             else if (arg2 < 0)
@@ -550,7 +549,6 @@ namespace sls {
 
     template<typename num_t>
     void arith_base<num_t>::add_update_mod(op_def const& od, num_t const& delta) {
-        num_t val = value(od.m_var);
         num_t arg1 = value(od.m_arg1);
         num_t arg2 = value(od.m_arg2);
         if (arg1 + delta >= 0 && arg1 + delta < arg2)
diff --git a/src/ast/sls/sls_arith_clausal.cpp b/src/ast/sls/sls_arith_clausal.cpp
index f42796419..d1cb01bcb 100644
--- a/src/ast/sls/sls_arith_clausal.cpp
+++ b/src/ast/sls/sls_arith_clausal.cpp
@@ -60,7 +60,8 @@ namespace sls {
             else if ((!m_bool_mode && bool_in_unsat > 0 && time_up_arith) || vars_in_unsat == bool_in_unsat)
                 enter_bool_mode();
             if (m_bool_mode) {
-                bv = ctx.bool_flip();                 
+                bv = ctx.bool_flip();        
+
                 m_no_improve_bool = update_outer_best_solution() ? 0 : m_no_improve_bool + 1;
             }
             else {
@@ -69,6 +70,8 @@ namespace sls {
             }
             m_no_improve = update_best_solution() ? 0 : m_no_improve + 1;
 
+            (void)bv;
+            (void)v;
             TRACE("arith", 
                 if (bv != sat::null_bool_var) tout << "bool flip " << bv << "\n";
                 else if (v != null_arith_var) tout << "arith flip v" << v << "\n";
diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp
index 938b65d06..7df9dee6a 100644
--- a/src/ast/sls/sls_datatype_plugin.cpp
+++ b/src/ast/sls/sls_datatype_plugin.cpp
@@ -310,6 +310,7 @@ namespace sls {
                 out << g->bpp(sib) << " ";
             out << " <- " << mk_bounded_pp(m_values.get(n->get_id()), m) << "\n";
         };
+        (void)trace_assignment;
         deps.topological_sort();
         expr_ref_vector args(m);
         euf::enode_vector leaves, worklist;
@@ -943,7 +944,7 @@ namespace sls {
         for (expr* b : m_occurs[f]) {
             if (b == e)
                 continue;
-            expr* a;
+            expr* a = nullptr;
             VERIFY(dt.is_accessor(b, a));
             auto v_a = eval0(a);
             if (v_a.get() == t) {
diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp
index 8ae6eda01..1e14a6932 100644
--- a/src/ast/sls/sls_seq_plugin.cpp
+++ b/src/ast/sls/sls_seq_plugin.cpp
@@ -575,7 +575,7 @@ namespace sls {
     }
 
     bool seq_plugin::repair_down_str_length(app* e) {
-        expr* x;
+        expr* x = nullptr;
         VERIFY(seq.str.is_length(e, x));
         expr_ref len = ctx.get_value(e);
         rational r;
@@ -603,7 +603,7 @@ namespace sls {
     }
 
     void seq_plugin::repair_up_str_stoi(app* e) {
-        expr* x;
+        expr* x = nullptr;
         VERIFY(seq.str.is_stoi(e, x));
 
         rational val_e;
@@ -622,7 +622,7 @@ namespace sls {
     }
 
     void seq_plugin::repair_up_str_itos(app* e) {
-        expr* x;
+        expr* x = nullptr;
         VERIFY(seq.str.is_itos(e, x));
         rational val_x;
         VERIFY(a.is_numeral(ctx.get_value(x), val_x));
@@ -670,7 +670,7 @@ namespace sls {
 
     bool seq_plugin::repair_down_str_eq(app* e) {
         bool is_true = ctx.is_true(e);
-        expr* x, * y;
+        expr* x = nullptr, * y = nullptr;
         VERIFY(m.is_eq(e, x, y));
         IF_VERBOSE(3, verbose_stream() << is_true << ": " << mk_bounded_pp(e, m, 3) << "\n");
         if (ctx.is_true(e)) {
@@ -1830,7 +1830,7 @@ namespace sls {
         expr_ref val(m);
         for (auto lit : ctx.unit_literals()) {
             auto e = ctx.atom(lit.var());
-            expr* x, * y, * z;
+            expr* x = nullptr, * y = nullptr, * z = nullptr;
             rational r;
             if (!lit.sign() && (a.is_le(e, x, y) || a.is_ge(e, y, x))) {
                 if (a.is_numeral(x, r) && r.is_unsigned() && seq.str.is_length(y, z)) {
@@ -2029,7 +2029,7 @@ namespace sls {
             if (m.is_eq(x, ))
         }
 #endif
-        expr* x, * y;
+        expr* x = nullptr, * y = nullptr;
         zstring s;
         if (seq.re.is_concat(r, x, y)) {
             auto info = seq.re.get_info(x);