From 328616b8b28feddca2fdb55b2865ca525d584e91 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 30 Sep 2024 17:25:19 -0700
Subject: [PATCH] fix build warnings

---
 src/ast/fpa/fpa2bv_converter.cpp     | 2 +-
 src/muz/spacer/spacer_legacy_mev.cpp | 2 +-
 src/sat/smt/arith_axioms.cpp         | 2 +-
 src/smt/mam.cpp                      | 6 +++---
 src/smt/theory_str.cpp               | 2 +-
 src/test/dlist.cpp                   | 1 +
 6 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 25a0e77ad..d138cc082 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -2692,7 +2692,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
         SASSERT(tmp_rat.is_int32());
         SASSERT(sz == 3);
 
-        mpf_rounding_mode mrm;
+        mpf_rounding_mode mrm = MPF_ROUND_TOWARD_ZERO;
         switch ((BV_RM_VAL)tmp_rat.get_unsigned()) {
         case BV_RM_TIES_TO_AWAY: mrm = MPF_ROUND_NEAREST_TAWAY; break;
         case BV_RM_TIES_TO_EVEN: mrm = MPF_ROUND_NEAREST_TEVEN; break;
diff --git a/src/muz/spacer/spacer_legacy_mev.cpp b/src/muz/spacer/spacer_legacy_mev.cpp
index 86ee731d8..57f249274 100644
--- a/src/muz/spacer/spacer_legacy_mev.cpp
+++ b/src/muz/spacer/spacer_legacy_mev.cpp
@@ -568,7 +568,7 @@ void model_evaluator::eval_eq(app* e, expr* arg1, expr* arg2)
 
 void model_evaluator::eval_basic(app* e)
 {
-    expr* arg1, *arg2;
+    expr* arg1 = nullptr, *arg2 = nullptr;
     expr *argCond = nullptr, *argThen = nullptr, *argElse = nullptr, *arg = nullptr;
     bool has_x = false;
     unsigned arity = e->get_num_args();
diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index 508a6d805..97a8ee563 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -206,7 +206,7 @@ namespace arith {
     }
 
     bool solver::check_bv_term(app* n) {
-        unsigned sz;
+        unsigned sz = 0;
         expr* _x = nullptr, * _y = nullptr;
         if (!ctx.is_relevant(expr2enode(n)))
             return true;
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index b9ac45039..a10c243f8 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -906,9 +906,9 @@ namespace {
         void linearise_core() {
             m_aux.reset();
             app *         first_app = nullptr;
-            unsigned      first_app_reg;
-            unsigned      first_app_sz;
-            unsigned      first_app_num_unbound_vars;
+            unsigned      first_app_reg = 0;
+            unsigned      first_app_sz = 0;
+            unsigned      first_app_num_unbound_vars = 0;
             // generate first the non-BIND operations
             for (unsigned reg : m_todo) {
                 expr *  p    = m_registers[reg];
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 61f6ec644..f88887feb 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1089,7 +1089,7 @@ namespace smt {
 
     void theory_str::instantiate_axiom_CharAt(enode * e) {
         ast_manager & m = get_manager();
-        expr* arg0, *arg1;
+        expr* arg0 = nullptr, *arg1 = nullptr;
         app * expr = e->get_expr();
         if (axiomatized_terms.contains(expr)) {
             TRACE("str", tout << "already set up CharAt axiom for " << mk_pp(expr, m) << std::endl;);
diff --git a/src/test/dlist.cpp b/src/test/dlist.cpp
index 32a54f9ff..9ad04d6b2 100644
--- a/src/test/dlist.cpp
+++ b/src/test/dlist.cpp
@@ -179,5 +179,6 @@ void tst_dlist() {
     test_detach();
     test_invariant();
     test_contains();
+    (void)test_remove_from;
     std::cout << "All tests passed." << std::endl;
 }