From 91a9feb5a879e65337353ff92fa157810425308b Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 20 Mar 2024 12:16:24 +0100
Subject: [PATCH] warnings

---
 src/sat/smt/polysat/fixed_bits.cpp | 2 +-
 src/sat/smt/polysat/monomials.cpp  | 2 +-
 src/sat/smt/polysat/saturation.cpp | 5 +++--
 src/sat/smt/polysat_model.cpp      | 2 +-
 4 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/sat/smt/polysat/fixed_bits.cpp b/src/sat/smt/polysat/fixed_bits.cpp
index 3c745e315..24b5e4c8d 100644
--- a/src/sat/smt/polysat/fixed_bits.cpp
+++ b/src/sat/smt/polysat/fixed_bits.cpp
@@ -47,7 +47,7 @@ namespace polysat {
 
                 SASSERT(s.offset + s.length <= sz);
                 unsigned bw = s.length + s.offset;
-                unsigned K = sz - bw;
+                // unsigned K = sz - bw;
                 pdd lo = c.value(rational::power_of_two(sz - s.length) * (s.value + 1), sz);
                 pdd hi = c.value(rational::power_of_two(sz - s.length) * s.value, sz);
                 rational hi_val = rational::power_of_two(s.offset) * s.value;
diff --git a/src/sat/smt/polysat/monomials.cpp b/src/sat/smt/polysat/monomials.cpp
index 6f4f9c18c..860b9be40 100644
--- a/src/sat/smt/polysat/monomials.cpp
+++ b/src/sat/smt/polysat/monomials.cpp
@@ -142,7 +142,7 @@ namespace polysat {
 
     bool monomials::mul(monomial const& mon, std::function<bool(rational const&)> const& p) {
         unsigned free_index = UINT_MAX;
-        auto& m = mon.args[0].manager();
+        // auto& m = mon.args[0].manager();
         for (unsigned j = mon.size(); j-- > 0; ) {
             auto const& arg_val = mon.arg_vals[j];
             if (p(arg_val))
diff --git a/src/sat/smt/polysat/saturation.cpp b/src/sat/smt/polysat/saturation.cpp
index 2e805fccf..eaea9c04d 100644
--- a/src/sat/smt/polysat/saturation.cpp
+++ b/src/sat/smt/polysat/saturation.cpp
@@ -38,13 +38,14 @@ namespace polysat {
             if (l_false == operator()(idx))
                 return l_false;
         }
+        // found conflict but no applicable saturation -> give up
         if (has_conflict)
             return l_undef;
         return l_true;
     }
 
     lbool saturation::operator()(constraint_id idx) {
-        auto sc = c.get_constraint(idx);
+        // auto sc = c.get_constraint(idx);
         auto vars = c.find_conflict_variables(idx);
         for (auto v : vars)
             if (resolve(v, idx))
@@ -95,7 +96,7 @@ namespace polysat {
             }
             else
                 UNREACHABLE();
-        }        
+        }
         c.add_axiom(name, lemma.begin(), lemma.end(), is_redundant);
         SASSERT(c.inconsistent());
     }
diff --git a/src/sat/smt/polysat_model.cpp b/src/sat/smt/polysat_model.cpp
index 8f68ede0a..9e21815d7 100644
--- a/src/sat/smt/polysat_model.cpp
+++ b/src/sat/smt/polysat_model.cpp
@@ -89,7 +89,7 @@ namespace polysat {
     }
 
     std::ostream& solver::display(std::ostream& out) const {
-        for (theory_var v = 0; v < get_num_vars(); ++v)
+        for (theory_var v = 0; v < (int)get_num_vars(); ++v)
             if (m_var2pdd_valid.get(v, false))
                 out << "tv" << v << " is " << ctx.bpp(var2enode(v)) << " := " << m_var2pdd[v] << "\n";
         m_core.display(out);