diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index c4c1cc05b..8e548e678 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -192,11 +192,13 @@ namespace smt {
         svector<bool_var_data>      m_bdata;       //!< mapping bool_var -> data
         svector<double>             m_activity;
         updatable_priority_queue::priority_queue<bool_var, double> m_pq_scores;
+
         struct lit_node : dll_base<lit_node> {
             literal lit;
             lit_node(literal l) : lit(l) { init(this); }
         };
         lit_node* m_dll_lits;
+
         svector<std::array<double, 2>> m_lit_scores; 
 
         clause_vector               m_aux_clauses;
diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 0913f498f..ce8b699aa 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -109,6 +109,7 @@ namespace smt {
 
         auto cube_pq = [&](context& ctx, expr_ref_vector& lasms, expr_ref& c) {
             unsigned k = 3; // Number of top literals you want
+
             ast_manager& m = ctx.get_manager();
 
             // Get the entire fixed-size priority queue (it's not that big)
@@ -302,7 +303,7 @@ namespace smt {
                         finished_id = i;
                         result = r;                        
                     }
-                    else if (!first) return;
+                    else if (!first) return; // nothing new to contribute
                 }
 
                 // Cancel limits on other threads now that a result is known