diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp
index f29bfa16b..59784ac06 100644
--- a/src/math/polysat/constraint_manager.cpp
+++ b/src/math/polysat/constraint_manager.cpp
@@ -613,7 +613,6 @@ namespace polysat {
         // v[|q|:] = q
         unsigned const p_sz = p.power_of_2();
         unsigned const q_sz = q.power_of_2();
-        unsigned const v_sz = p_sz + q_sz;
         if (p.is_val() || q.is_val())
             return zero_ext(p, q_sz) * rational::power_of_two(q_sz) + zero_ext(q, p_sz);
         pvar const v = s.m_slicing.mk_concat({s.m_names.mk_name(p), s.m_names.mk_name(q)});
diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp
index 9f24b6a0b..84021548e 100644
--- a/src/math/polysat/op_constraint.cpp
+++ b/src/math/polysat/op_constraint.cpp
@@ -629,7 +629,6 @@ namespace polysat {
      * q = 1   ==>  r = p
      */
     clause_ref op_constraint::lemma_udiv(solver& s, assignment const& a) {
-        auto& m = p().manager();
         auto pv = a.apply_to(p());
         auto qv = a.apply_to(q());
         auto rv = a.apply_to(r());
@@ -679,7 +678,6 @@ namespace polysat {
      * q = 0   ==>  r = p
      */
     clause_ref op_constraint::lemma_urem(solver& s, assignment const& a) {
-        auto& m = p().manager();
         auto pv = a.apply_to(p());
         auto qv = a.apply_to(q());
         auto rv = a.apply_to(r());
diff --git a/src/math/polysat/polysat_ast.cpp b/src/math/polysat/polysat_ast.cpp
index ad808a0e3..bbcf0e199 100644
--- a/src/math/polysat/polysat_ast.cpp
+++ b/src/math/polysat/polysat_ast.cpp
@@ -165,7 +165,6 @@ namespace polysat {
 
     template <typename Fn>
     expr* polysat_ast::mk_bin(char const* name, pdd const& p, pdd const& q, pdd const& r, Fn mk_bin_expr) {
-        unsigned const N = p.power_of_2();
         // r = p OP q
         expr* definition = m().mk_eq(mk_poly(r), mk_bin_expr(mk_poly(p), mk_poly(q)));
         // b <=> definition
diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index dc658113e..e89b63e76 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -1359,11 +1359,9 @@ namespace polysat {
         if (!is_AxB_eq_0(x, a_l_b, a, b, y)) // TODO: Is the restriction to linear "x" too restrictive?
             return false;
         
-        bool change = false;
         bool prop = false;
         
         for (auto c : core) {
-            change = false;
             if (c == a_l_b)
                 continue;
             LOG("Trying to eliminate v" << x << " in " << c << " by using equation " << a_l_b.as_signed_constraint());
@@ -1448,7 +1446,6 @@ namespace polysat {
      * -x <  -x - y
      */
     bool saturation::is_add_overflow(pvar x, inequality const& i, pdd& y, bool& is_minus) {
-        auto& m = s.var2pdd(x);
         pdd const X = s.var(x);
         pdd a = X;
         if (i.lhs().degree(x) != 1 || i.rhs().degree(x) != 1)
@@ -1950,7 +1947,7 @@ namespace polysat {
      * Values of x1, y1, q1 have to be available for the rule to apply.
      * If not all values are present, the rule isn't going to be used.
      * The arithmetic solver uses complete assignments because it 
-     * builds on top of an integer feasiable state (or feasible over rationals)
+     * builds on top of an integer feasible state (or feasible over rationals)
      * Lemmas are false under that assignment. They don't necessarily propagate, though.
      * PolySAT isn't (yet) set up to work with complete assignments and thereforce misses such lemmas.
      * - should we force complete assignments by computing first a model that is feasible modulo linear constraints