diff --git a/src/sat/smt/polysat_core.cpp b/src/sat/smt/polysat_core.cpp
index 27d6ee731..931a92992 100644
--- a/src/sat/smt/polysat_core.cpp
+++ b/src/sat/smt/polysat_core.cpp
@@ -225,7 +225,7 @@ namespace polysat {
 
             // constraint is unitary, add to viable set 
             if (vars.size() >= 2 && is_assigned(vars[0]) && !is_assigned(vars[1])) {
-                // m_viable.add_unitary(vars[1], idx);
+                m_viable.add_unitary(vars[1], idx);
             }
         }
         m_watch[v].shrink(j);
diff --git a/src/sat/smt/polysat_core.h b/src/sat/smt/polysat_core.h
index 7fdf8c88c..075840a48 100644
--- a/src/sat/smt/polysat_core.h
+++ b/src/sat/smt/polysat_core.h
@@ -59,8 +59,6 @@ namespace polysat {
         var_queue<activity>     m_var_queue;                 // priority queue of variables to assign
         vector<unsigned_vector> m_watch;                     // watch lists for variables for constraints on m_prop_queue where they occur
 
-        vector<pdd>             m_subst;            // substitution, one for each size.
-
         // values to split on
         rational    m_value;
         pvar        m_var = 0;
diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp
index 80c2fb19b..dd761fdc3 100644
--- a/src/sat/smt/polysat_internalize.cpp
+++ b/src/sat/smt/polysat_internalize.cpp
@@ -3,11 +3,11 @@ Copyright (c) 2022 Microsoft Corporation
 
 Module Name:
 
-    polysat_model.cpp
+    polysat_internalize.cpp
 
 Abstract:
 
-    PolySAT model generation
+    PolySAT internalize
     
 Author:
 
diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp
index cee129327..58b2c97d1 100644
--- a/src/sat/smt/polysat_solver.cpp
+++ b/src/sat/smt/polysat_solver.cpp
@@ -3,7 +3,7 @@ Copyright (c 2022 Microsoft Corporation
 
 Module Name:
 
-    polysat_internalize.cpp
+    polysat_solver.cpp
 
 Abstract: