diff --git a/src/sat/smt/polysat/constraints.cpp b/src/sat/smt/polysat/constraints.cpp
index fe577ef8c..b351ff8e1 100644
--- a/src/sat/smt/polysat/constraints.cpp
+++ b/src/sat/smt/polysat/constraints.cpp
@@ -1,4 +1,4 @@
-/*++
+/*++
 Copyright (c) 2021 Microsoft Corporation
 
 Module Name:
@@ -131,7 +131,7 @@ namespace polysat {
         if (l.lo().val() == 0)
             val = 0;
         else 
-            val = l.manager().max_value() + 1 - l.lo().val();
+            val = l.manager().two_to_N() - l.lo().val();
         return true;
     }
 
diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h
index 316d47ed2..d3290dedc 100644
--- a/src/sat/smt/polysat/core.h
+++ b/src/sat/smt/polysat/core.h
@@ -146,7 +146,7 @@ namespace polysat {
 
 
         /*
-        * Add a named clause. Dependencies are assumed, signed constraints are guaranteeed.
+        * Add a named clause. Dependencies are assumed, signed constraints are guaranteed.
         * In other words, the clause represents the formula /\ d_i -> \/ sc_j
         * Where d_i are logical interpretations of dependencies and sc_j are signed constraints.
         */
diff --git a/src/sat/smt/polysat/ule_constraint.cpp b/src/sat/smt/polysat/ule_constraint.cpp
index 806f823fb..c0c64ee2a 100644
--- a/src/sat/smt/polysat/ule_constraint.cpp
+++ b/src/sat/smt/polysat/ule_constraint.cpp
@@ -175,7 +175,6 @@ namespace polysat {
         //          3. now the reference returned from lhs.offset() may be invalid
         pdd const rhs_plus_one = rhs + 1;
 
-        // TODO: potential bug here: first call offset(), then rhs+1 has to reallocate pdd_manager::m_values, then the reference to offset is broken.
         if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs_plus_one.val()) {
             TRACE("bv", tout << "p - k <= -k - 1  -->  k <= p\n");
             pdd k = -(rhs + 1);
diff --git a/src/sat/smt/polysat_model.cpp b/src/sat/smt/polysat_model.cpp
index f630a47cc..815f6df51 100644
--- a/src/sat/smt/polysat_model.cpp
+++ b/src/sat/smt/polysat_model.cpp
@@ -89,9 +89,9 @@ namespace polysat {
     }
 
     std::ostream& solver::display(std::ostream& out) const {
-        for (unsigned v = 0; v < get_num_vars(); ++v)
+        for (theory_var v = 0; v < get_num_vars(); ++v)
             if (m_var2pdd_valid.get(v, false))
-                out << ctx.bpp(var2enode(v)) << " := " << m_var2pdd[v] << "\n";
+                out << "tv" << v << " is " << ctx.bpp(var2enode(v)) << " := " << m_var2pdd[v] << "\n";
         m_core.display(out);
         m_intblast.display(out);
         return out;
diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp
index 8cfd9dba4..7ae6c99ef 100644
--- a/src/sat/smt/polysat_solver.cpp
+++ b/src/sat/smt/polysat_solver.cpp
@@ -495,16 +495,16 @@ namespace polysat {
         
         expr_ref_vector args(m);
         for (auto const& mon : p) {
-            auto c = mon.coeff;
+            rational const& c = mon.coeff;
             if (mon.vars.empty())
                 args.push_back(mk_num(c));
-            else if (mon.coeff == 1 && mon.vars.size() == 1)
+            else if (c == 1 && mon.vars.size() == 1)
                 args.push_back(mk_var(mon.vars[0]));
             else if (mon.vars.size() == 1)
                 args.push_back(bv.mk_bv_mul(mk_num(c), mk_var(mon.vars[0])));
             else {
                 expr_ref_vector args2(m);
-                for (auto v : mon.vars)
+                for (pvar v : mon.vars)
                     args2.push_back(mk_var(v));
                 if (c == 1)
                     args.push_back(bv.mk_bv_mul(args2));
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index e226566b8..430f41ca2 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -177,8 +177,6 @@ namespace euf {
         void add_equiv(sat::literal a, sat::literal b);
         void add_equiv_and(sat::literal a, sat::literal_vector const& bs);
         bool add_redundant(sat::literal_vector const& lits, th_proof_hint const* ps) { return add_clause(lits.size(), lits.data(), ps, true); }
-        bool add_redundant(unsigned n, sat::literal* lits, th_proof_hint const* ps);
-
 
         bool is_true(sat::literal lit);
         bool is_true(sat::literal a, sat::literal b) { return is_true(a) || is_true(b); }