diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 9adf8a944..1ca8a8c69 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -388,7 +388,8 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const override {
             out << "Resolve upon " << lit << " with assignment:";
             for (pvar v : c->vars())
-                out << " " << assignment_pp(s, v, s.get_value(v), true);
+                if (s.is_assigned(v))
+                    out << " " << assignment_pp(s, v, s.get_value(v), true);
             return out;
         }
     };
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 52f2655ff..c65da431e 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1063,7 +1063,7 @@ namespace polysat {
             // it could be that such a literal has been created previously but we don't detect it when e.g. narrowing a mul_ovfl_constraint
             if (m_bvars.value(lit) == l_true) {
                 // in this case the clause is useless
-                LOG("   Clause is already true, skippping...");
+                LOG("   Clause is already true, skipping...");
                 return;
             }
         }
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 432de791d..da3921f1d 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -87,6 +87,7 @@ namespace polysat {
         friend class scoped_solverv;        
         friend class test_polysat;
         friend class test_fi;
+        friend struct inference_resolve_with_assignment;
 
         reslimit&                m_lim;
         params_ref               m_params;