add comments

src/mcsat/nra/nra_plugin.c

@@ -2184,6 +2184,7 @@ void nra_plugin_learn(plugin_t* plugin, trail_token_t* prop) {
             ctx_trace_printf(nra->ctx, "nra: hinting variable = %d\n", constraint_var);
           }
           nra->ctx->hint_next_decision(nra->ctx, constraint_var);
+	  // update the trail value cache
           nra->ctx->hint_value(nra->ctx, constraint_var, constraint_value);
         }
       }

src/mcsat/solver.c

@@ -707,11 +707,18 @@ void mcsat_plugin_context_hint_next_decision(plugin_context_t* self, variable_t
   mcsat_add_decision_hint(mctx->mcsat, x);
 }
 
+/*
+ * Provide hint to the trail cache.
+ */
 static
 void mcsat_plugin_context_hint_value(plugin_context_t* self, variable_t x, const mcsat_value_t* val) {
   mcsat_plugin_context_t* mctx;
   mctx = (mcsat_plugin_context_t*) self;
+  // update only if the x value is not set in the trail
   if (!trail_has_value(mctx->mcsat->trail, x)) {
+    // we set the value in the model of the trail.
+    // Remark: This is not making a decision in the trail. The model
+    // in the trail is used as a cache for unassigned variables.
     mcsat_model_set_value(&mctx->mcsat->trail->model, x, val);
   }
 }