diff --git a/lib/licDump.ml b/lib/licDump.ml
index e22b8cb7fc4a7cc48e3deab42027effe3e8aa20a..1b9a8161feccf9f35e6c9141a786ef79cb67eb63 100644
--- a/lib/licDump.ml
+++ b/lib/licDump.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 26/02/2024 (at 17:54) by Erwan Jahier> *)
+(* Time-stamp: <modified the 27/02/2024 (at 16:20) by Erwan Jahier> *)
 (*
 
 This module is used both for
@@ -834,7 +834,7 @@ and (const_decl: bool -> Lv6Id.long -> Lic.const -> string) =
   )
 
 (* exported *)
-and node_of_node_exp_eff forprint (neff: Lic.node_exp): string =
+and node_of_node_exp_eff is_main_node forprint (neff: Lic.node_exp): string =
   wrap_long_profile (
     (
       if neff.is_safe_eff then "" else "unsafe "
@@ -886,7 +886,11 @@ and node_of_node_exp_eff forprint (neff: Lic.node_exp): string =
 	    ("var\n   " ^ (string_of_type_decl_list forprint l ";\n   ") ^ ";\n")
          )
          ^  (if global_opt.assert_in_contract then
-               Printf.sprintf "let\n    %s" eqs_str
+               Printf.sprintf "let\n    %s%s" eqs_str
+                 (if is_main_node then "
+--%MAIN ;
+--%PROPERTY "^ (List.hd neff.outlist_eff).var_name_eff ^";
+" else "")
               else
 	        ("let\n   " ^ ass_str ^ eqs_str)
              ) ^
diff --git a/lib/licPrg.ml b/lib/licPrg.ml
index 4fcf5e0fed1194f7d69eb43046dd3ead0aa4501f..7e09a05e58009ae3b86c58bfbacceb2b275ac930 100644
--- a/lib/licPrg.ml
+++ b/lib/licPrg.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 08/06/2023 (at 10:49) by Erwan Jahier> *)
+(* Time-stamp: <modified the 27/02/2024 (at 15:56) by Erwan Jahier> *)
 open Lv6MainArgs
 
 module ItemKeyMap = struct
@@ -307,7 +307,7 @@ let to_file (opt: Lv6MainArgs.t) (this:t) (main_node: Lv6Id.idref option) =
        Hence we print the first one (if no main node is set).
     *)
     let nexp = get_main_node_exp this main_node in
-    output_string opt.Lv6MainArgs.oc (LicDump.node_of_node_exp_eff true nexp);
+    output_string opt.Lv6MainArgs.oc (LicDump.node_of_node_exp_eff true true nexp);
     flush opt.Lv6MainArgs.oc;
   ) else (
     (* Pour les noeuds, pas sur que ça marche tant qu'on n'a
@@ -320,12 +320,13 @@ let to_file (opt: Lv6MainArgs.t) (this:t) (main_node: Lv6Id.idref option) =
        On n'affiche PAS les extern Lustre::...
      *)
 
+    let nexp_main = get_main_node_exp this main_node in
     NodeKeyMap.iter (
         fun _ nexp ->
         match nexp.Lic.node_key_eff with
         (* inutile d'écrire les noeuds predefs *)
         | (("Lustre",_),[]) -> ()
-        | _ -> output_string opt.Lv6MainArgs.oc (LicDump.node_of_node_exp_eff true nexp)
+        | _ -> output_string opt.Lv6MainArgs.oc (LicDump.node_of_node_exp_eff (nexp_main = nexp) true nexp)
       )
                     this.nodes
   )