[Simplex] add comment about the reason of a restriction

colibri2/theories/LRA/simplex.ml

@@ -177,6 +177,8 @@ let make_equations d (eqs, vars) n =
     let sign = Dom_product.SolveSign.get_repr d n in
     match (abs, sign) with
     | Some abs, Some sign ->
+        (* The restriction is not for soundness, any node can be added as
+           equation using {!addition} since it uses the domains of the node *)
         Debug.dprintf6 debug "[Simplex] %a: %a --- %a" Node.pp n Product.pp abs
           Sign_product.pp sign;
         if Sign_product.(equal one sign) then