diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h
index aaec6f93a..878661362 100644
--- a/src/math/polysat/fixplex_def.h
+++ b/src/math/polysat/fixplex_def.h
@@ -748,11 +748,9 @@ namespace polysat {
         unsigned tz_b,    
         numeral const& old_value_y) {
 
-        var_t y = row2base(r_y);
         numeral b = row2base_coeff(r_y);
         auto z = row2base(r_z);
         auto& row_z = m_rows[r_z.id()];
-        var_info& zI = m_vars[z];
         unsigned tz_c = m.trailing_zeros(c);
         numeral b1, c1;
         if (tz_b <= tz_c) {
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index e838fbbba..db11bf379 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -200,6 +200,7 @@ namespace polysat {
     void solver::propagate(sat::literal lit) {
         LOG_H2("Propagate boolean literal " << lit);
         constraint* c = m_constraints.lookup(lit.var());
+        (void)c;
         SASSERT(c);
         SASSERT(!c->is_undef());
         // c->narrow(*this);
@@ -238,6 +239,7 @@ namespace polysat {
     void solver::pop_levels(unsigned num_levels) {
         SASSERT(m_level >= num_levels);
         unsigned const target_level = m_level - num_levels;
+        (void)target_level;
         LOG("Pop " << num_levels << " levels (lvl " << m_level << " -> " << target_level << ")");
 #if ENABLE_LINEAR_SOLVER
         m_linear_solver.pop(num_levels);
@@ -853,8 +855,7 @@ namespace polysat {
                 lits.push_back(~lit);
                 reason = clause::from_literals(reason->level(), {reason->dep(), m_dm}, lits, reason->new_constraints());
             }
-            bool contains_opp = std::any_of(reason->begin(), reason->end(), [lit](sat::literal reason_lit) { return reason_lit == ~lit; });
-            SASSERT(contains_opp);
+            SASSERT(std::any_of(reason->begin(), reason->end(), [lit](sat::literal reason_lit) { return reason_lit == ~lit; }));
         }
         else {
             LOG_H3("Empty reason");