diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 0898c640d..87714da22 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1012,7 +1012,7 @@ namespace polysat {
 
     /// Deactivate constraint
     void solver::deactivate_constraint(signed_constraint c) {
-        LOG("Deactivating constraint: " << c.blit());
+        LOG_V("Deactivating constraint: " << c.blit());
         c->set_active(false);
     }
 
@@ -1023,7 +1023,7 @@ namespace polysat {
         }
     }
 
-    // Add lemma to storage
+    // Add clause to storage
     void solver::add_clause(clause& clause) {
         LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause);
         for (sat::literal lit : clause) {
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 8cf3c9a1a..3ddb95ccb 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -17,7 +17,6 @@ Author:
 --*/
 #pragma once
 
-#include <limits>
 #include "util/statistics.h"
 #include "util/params.h"
 #include "math/polysat/boolean.h"
@@ -35,6 +34,8 @@ Author:
 #include "math/polysat/trail.h"
 #include "math/polysat/viable.h"
 #include "math/polysat/log.h"
+#include <limits>
+#include <optional>
 
 namespace polysat {
 
@@ -222,7 +223,7 @@ namespace polysat {
         void report_unsat();
         void learn_lemma(clause& lemma);
         void backjump(unsigned new_level);
-        void add_clause(clause& lemma);
+        void add_clause(clause& clause);
         void add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant);
         void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, bool is_redundant);
         void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant);
diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp
index 341335a7a..a7a9a7b13 100644
--- a/src/sat/smt/bv_polysat.cpp
+++ b/src/sat/smt/bv_polysat.cpp
@@ -273,8 +273,8 @@ namespace bv {
             pdd p = m_polysat.var(pv);
             polysat_set(v, p);
 #ifndef NDEBUG
-            expr* e = var2enode(v)->get_expr();
-            std::cerr << "var2pdd:     " << mk_ismt2_pp(e, m) << " -> " << p << std::endl;
+            // expr* e = var2enode(v)->get_expr();
+            // std::cerr << "var2pdd:     " << mk_ismt2_pp(e, m) << " -> " << p << std::endl;
 #endif
             return p;
         }
@@ -303,8 +303,8 @@ namespace bv {
         ctx.push(set_bitvector_trail(m_var2pdd_valid, v));
         m_var2pdd[v] = p;
 #ifndef NDEBUG
-        expr* e = var2enode(v)->get_expr();
-        std::cerr << "polysat_set: " << mk_ismt2_pp(e, m) << " -> " << p << std::endl;
+        // expr* e = var2enode(v)->get_expr();
+        // std::cerr << "polysat_set: " << mk_ismt2_pp(e, m) << " -> " << p << std::endl;
 #endif
     }