From bc6037464d4f63e7ff8721c36f9b3d7709cf924c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 19 Feb 2023 10:08:31 -0800
Subject: [PATCH] clean up build warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/spacer/spacer_convex_closure.cpp | 16 +++++++++-------
 src/sat/smt/arith_sls.cpp                |  5 ++---
 2 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/src/muz/spacer/spacer_convex_closure.cpp b/src/muz/spacer/spacer_convex_closure.cpp
index 476821643..e313c972b 100644
--- a/src/muz/spacer/spacer_convex_closure.cpp
+++ b/src/muz/spacer/spacer_convex_closure.cpp
@@ -22,21 +22,23 @@ Notes:
 #include "ast/rewriter/th_rewriter.h"
 
 namespace {
+
+#ifdef Z3DEBUG
 bool is_int_matrix(const spacer::spacer_matrix &matrix) {
-    rational val;
-    for (unsigned i = 0, rows = matrix.num_rows(); i < rows; i++) {
+    for (unsigned i = 0, rows = matrix.num_rows(); i < rows; i++) 
         for (unsigned j = 0, cols = matrix.num_cols(); j < cols; j++)
-            if (!matrix.get(i, j).is_int()) return false;
-    }
+            if (!matrix.get(i, j).is_int()) 
+                return false;
     return true;
 }
 
 bool is_sorted(const vector<rational> &data) {
-    for (unsigned i = 0; i < data.size() - 1; i++) {
-        if (!(data[i] >= data[i + 1])) return false;
-    }
+    for (unsigned i = 0; i < data.size() - 1; i++) 
+        if (!(data[i] >= data[i + 1])) 
+            return false;
     return true;
 }
+#endif
 
 /// Check whether all elements of \p data are congruent modulo \p m
 bool is_congruent_mod(const vector<rational> &data, const rational &m) {
diff --git a/src/sat/smt/arith_sls.cpp b/src/sat/smt/arith_sls.cpp
index 26358dc17..42594f043 100644
--- a/src/sat/smt/arith_sls.cpp
+++ b/src/sat/smt/arith_sls.cpp
@@ -308,10 +308,10 @@ namespace arith {
     // cached dts has to be updated when the score of literals are updated.
     // 
     double sls::dscore(var_t v, int64_t new_value) const {
-        auto const& vi = m_vars[v];
-        verbose_stream() << "dscore " << v << "\n";
         double score = 0;
 #if 0
+        auto const& vi = m_vars[v];
+        verbose_stream() << "dscore " << v << "\n";
         for (auto const& [coeff, lit] : vi.m_literals) 
             for (auto cl : m_bool_search->get_use_list(lit))              
                 score += (compute_dts(cl) - dts(cl, v, new_value)) * m_bool_search->get_weight(cl);    
@@ -530,7 +530,6 @@ namespace arith {
         if (!ineq)
             return -1;
         int64_t new_value;      
-        double result = 0;
         double max_result = -1;
         for (auto const & [coeff, x] : ineq->m_args) {
             if (!cm(!sign0, *ineq, x, coeff, new_value))