fix build warnings

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;

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();

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;

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];

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;);

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;
 }