deal with compiler warnings (unused variables etc)

src/ast/rewriter/bv_rewriter.cpp

@@ -1554,7 +1554,7 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
         if (eq_args) {
             if (m.is_ite(new_args.back(), x, y, z)) {
                 ptr_buffer<expr> args1, args2;
-                for (expr* arg : new_args)
+                for (unsigned i = 0; i < new_args.size(); ++i)
                     args1.push_back(y), args2.push_back(z);
                 result = m.mk_ite(x, m_util.mk_concat(args1), m_util.mk_concat(args2));
                 return BR_REWRITE2;

src/sat/sat_ddfw.cpp

@@ -583,8 +583,7 @@ namespace sat {
     void ddfw::shift_weights() {
         ++m_shifts;
         for (unsigned to_idx : m_unsat) {
-            auto& cf = m_clauses[to_idx];
+            SASSERT(!m_clauses[to_idx].is_true());
-            SASSERT(!cf.is_true());
             unsigned from_idx = select_max_same_sign(to_idx);
             if (from_idx == UINT_MAX || disregard_neighbor())
                 from_idx = select_random_true_clause();

src/sat/smt/arith_sls.cpp

@@ -72,9 +72,6 @@ namespace arith {
                 continue;
             if (!s.lp().external_is_used(v)) 
                 continue;            
-            int64_t old_value = 0;
-            if (s.is_registered_var(v))
-                old_value = to_numeral(s.get_ivalue(v).x);
             int64_t new_value = m_vars[v].m_best_value;
             s.ensure_column(v);
             lp::column_index vj = s.lp().to_column_index(v);
@@ -535,13 +532,12 @@ namespace arith {
         int64_t new_value;      
         double result = 0;
         double max_result = -1;
-        theory_var max_var = 0;
         for (auto const & [coeff, x] : ineq->m_args) {
             if (!cm(!sign0, *ineq, x, coeff, new_value))
                 continue;
             double result = 0;
             auto old_value = m_vars[x].m_value;
-            for (auto const [coeff, bv] : m_vars[x].m_bool_vars) {
+            for (auto const& [coeff, bv] : m_vars[x].m_bool_vars) {
                 bool sign = !m_bool_search->value(bv);
                 auto dtt_old = dtt(sign, *atom(bv));
                 auto dtt_new = dtt(sign, *atom(bv), coeff, old_value, new_value);

src/sat/smt/euf_local_search.cpp

@@ -32,7 +32,7 @@ namespace euf {
         for (auto* th : m_solvers)
             th->set_bool_search(&bool_search);
 
-        lbool r = bool_search.check(0, nullptr, nullptr);        
+        bool_search.check(0, nullptr, nullptr);        
 
         auto const& mdl = bool_search.get_model();
         for (unsigned i = 0; i < mdl.size(); ++i)

src/smt/theory_pb.cpp

@@ -1604,7 +1604,7 @@ namespace smt {
             std::cout << B << "\n";
         }
 #endif
-        SASSERT(is_sat != l_true);
+        VERIFY(is_sat != l_true);
         return true;
     }
 

src/test/api.cpp

@@ -100,6 +100,7 @@ static void test_mk_distinct() {
     Z3_sort bv32 = Z3_mk_bv_sort(ctx, 32);
     Z3_ast args[] = { Z3_mk_int64(ctx, 0, bv8), Z3_mk_int64(ctx, 0, bv32) };
     Z3_ast d = Z3_mk_distinct(ctx, 2, args);
+    VERIFY(d);
     ENSURE(cb_called);
     Z3_del_config(cfg);
     Z3_del_context(ctx);    

src/test/bit_blaster.cpp

@@ -28,13 +28,9 @@ void mk_bits(ast_manager & m, char const * prefix, unsigned sz, expr_ref_vector
     sort_ref b(m);
     b = m.mk_bool_sort();
     for (unsigned i = 0; i < sz; ++i) {
-        char buffer[128];
+        std::stringstream ous;
-#ifdef _WINDOWS
+        ous << prefix << i << ".smt2";
-        sprintf_s(buffer, Z3_ARRAYSIZE(buffer), "%s%d.smt", prefix, i);
+        r.push_back(m.mk_const(symbol(ous.str()), b));
-#else
-        sprintf(buffer, "%s%d.smt", prefix, i);
-#endif
-        r.push_back(m.mk_const(symbol(buffer), b));
     }
 }
 

src/test/interval.cpp

@@ -24,6 +24,7 @@ Revision History:
 #include "util/debug.h"
 #include "util/rlimit.h"
 #include <iostream>
+#include <sstream>
 
 template class interval_manager<im_default_config>;
 typedef im_default_config::interval interval;
@@ -200,15 +201,13 @@ static void mk_random_interval(T & cfg, interval & a, unsigned magnitude) {
 #define BUFFER_SZ 256
 static int g_problem_id = 0;
 static char g_buffer[BUFFER_SZ];
+static std::stringstream ous;
 
 char const * get_next_file_name() {
-#ifdef _WINDOWS
+    ous.clear();
-    sprintf_s(g_buffer, BUFFER_SZ, "interval_lemma_%d.smt2", g_problem_id);
+    ous << "interval_lemma_" << g_problem_id << ".smt2";
-#else
-    sprintf(g_buffer, "interval_lemma_%d.smt2", g_problem_id);
-#endif
     g_problem_id++;
-    return g_buffer;
+    return ous.str().c_str();
 }
 
 static void display_lemmas(unsynch_mpq_manager & nm, char const * result_term,