diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 78bab11fe..40990392c 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1484,7 +1484,7 @@ namespace nlsat {
                                   m_pm.display(tout << "  equation used: ", eq_ref, m_solver.display_proc());
                                   tout << " = 0\n";
                               });
-                        new_lit = l; // SIMP_BUG
+                        new_lit = l;
                     }
                     else {
                         literal assumption = new_lit;
@@ -1498,7 +1498,7 @@ namespace nlsat {
                                   tout << " = 0\n";
                               });
                         add_literal(assumption);
-                        new_lit = true_literal; // SIMP_BUG
+                        new_lit = true_literal;
                     }
                 }
                 else {
@@ -1517,7 +1517,6 @@ namespace nlsat {
                                   m_pm.display(tout << "  equation used: ", eq_ref, m_solver.display_proc());
                                   tout << " = 0\n";
                               });
-                        // SIMP_BUG
                     }
                 }
             }
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index b768b457f..ccf5eab8f 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -2242,7 +2242,24 @@ namespace nlsat {
                 for (var v : vars)
                     used_vars[v] = true;
             }
-            out << "(echo \"#" << m_lemma_count++ << ":assignment lemma\")\n";
+            std::ostringstream comment;            
+            bool any_var = false;
+            display_num_assignment(comment, &used_vars);
+            if (!any_var)
+                comment << " (none)";
+            comment << "; literals:";
+            if (jst.num_lits() == 0) {
+                comment << " (none)";
+            }
+            else {
+                for (unsigned i = 0; i < jst.num_lits(); ++i) {
+                    comment << " ";
+                    display(comment, jst.lit(i));
+                    if (i < jst.num_lits() - 1)
+                        comment << " /\\";
+                }
+            }
+            out << "(echo \"#" << m_lemma_count++ << ":assignment lemma " << comment.str() << "\")\n";
             out << "(set-logic ALL)\n";
             out << "(set-option :rlimit " << m_lemma_rlimit << ")\n";
             display_smt2_bool_decls(out, used_bools);