diff --git a/.Makefile.lint b/.Makefile.lint
index 4d510d832410a3d5695edb1aa766807b28ecd71a..ba3d6165fcea41dd2aac3e8913ca5d297c6064de 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -146,8 +146,6 @@ ML_LINT_KO+=src/libraries/utils/wto.mli
 ML_LINT_KO+=src/plugins/aorai/Aorai.mli
 ML_LINT_KO+=src/plugins/aorai/aorai_dataflow.ml
 ML_LINT_KO+=src/plugins/aorai/aorai_dataflow.mli
-ML_LINT_KO+=src/plugins/aorai/aorai_option.ml
-ML_LINT_KO+=src/plugins/aorai/aorai_register.ml
 ML_LINT_KO+=src/plugins/aorai/data_for_aorai.ml
 ML_LINT_KO+=src/plugins/aorai/data_for_aorai.mli
 ML_LINT_KO+=src/plugins/aorai/logic_simplification.ml
diff --git a/src/plugins/aorai/aorai_option.ml b/src/plugins/aorai/aorai_option.ml
index 2bcf7c8129b968ab205be19c4cef901c26460626..0920c5f83d1b46dff9778585a96c4b15f2b44c1d 100644
--- a/src/plugins/aorai/aorai_option.ml
+++ b/src/plugins/aorai/aorai_option.ml
@@ -24,95 +24,95 @@
 (**************************************************************************)
 
 include Plugin.Register
-  (struct
-     let name = "aorai"
-     let shortname = "aorai"
-     let help = "verification of behavioral properties (experimental)"
-   end)
+    (struct
+      let name = "aorai"
+      let shortname = "aorai"
+      let help = "verification of behavioral properties (experimental)"
+    end)
 
 module Ltl_File =
   Filepath
     (struct
-       let option_name = "-aorai-ltl"
-       let arg_name = ""
-       let file_kind = "ltl"
-       let existence = Fc_Filepath.Must_exist
-       let help = "specifies file name for LTL property"
-     end)
+      let option_name = "-aorai-ltl"
+      let arg_name = ""
+      let file_kind = "ltl"
+      let existence = Fc_Filepath.Must_exist
+      let help = "specifies file name for LTL property"
+    end)
 
 module To_Buchi =
   Filepath
     (struct
-       let option_name = "-aorai-to-buchi"
-       let arg_name = "f"
-       let file_kind = "Promela"
-       let existence = Fc_Filepath.Indifferent
-       let help =
-         "only generates the buchi automata (in Promela language) in file <s>"
-     end)
+      let option_name = "-aorai-to-buchi"
+      let arg_name = "f"
+      let file_kind = "Promela"
+      let existence = Fc_Filepath.Indifferent
+      let help =
+        "only generates the buchi automata (in Promela language) in file <s>"
+    end)
 
 module Buchi =
   Filepath
     (struct
-       let option_name = "-aorai-buchi"
-       let arg_name = "f"
-       let file_kind = "Promela"
-       let existence = Fc_Filepath.Must_exist
-       let help = "considers the property described by the buchi automata \
-                   (in Promela language) from file <f>."
-     end)
+      let option_name = "-aorai-buchi"
+      let arg_name = "f"
+      let file_kind = "Promela"
+      let existence = Fc_Filepath.Must_exist
+      let help = "considers the property described by the buchi automata \
+                  (in Promela language) from file <f>."
+    end)
 
 module Ya =
   Filepath
     (struct
-       let option_name = "-aorai-automata"
-       let arg_name = "f"
-       let file_kind = "Ya"
-       let existence = Fc_Filepath.Must_exist
-       let help = "considers the property described by the ya automata \
-                   (in Ya language) from file <f>."
-     end)
+      let option_name = "-aorai-automata"
+      let arg_name = "f"
+      let file_kind = "Ya"
+      let existence = Fc_Filepath.Must_exist
+      let help = "considers the property described by the ya automata \
+                  (in Ya language) from file <f>."
+    end)
 
 module Output_C_File =
   Filepath
     (struct
-       let option_name = "-aorai-output-c-file"
-       let arg_name = ""
-       let file_kind = "annotated C"
-       let existence = Fc_Filepath.Indifferent
-       let help = "specifies generated file name for annotated C code"
-     end)
+      let option_name = "-aorai-output-c-file"
+      let arg_name = ""
+      let file_kind = "annotated C"
+      let existence = Fc_Filepath.Indifferent
+      let help = "specifies generated file name for annotated C code"
+    end)
 
 module Dot =
   False(struct
-          let option_name = "-aorai-dot"
-          let help = "generates a dot file of the Buchi automata"
-        end)
+    let option_name = "-aorai-dot"
+    let help = "generates a dot file of the Buchi automata"
+  end)
 
 module DotSeparatedLabels =
   False(struct
-          let option_name = "-aorai-dot-sep-labels"
-          let help = "tells dot to not output guards directly over the edges"
-        end)
+    let option_name = "-aorai-dot-sep-labels"
+    let help = "tells dot to not output guards directly over the edges"
+  end)
 
 module AbstractInterpretation =
   False(struct
-          let option_name = "-aorai-simple-AI"
-          let help = "use simple abstract interpretation"
-        end)
+    let option_name = "-aorai-simple-AI"
+    let help = "use simple abstract interpretation"
+  end)
 
 module AbstractInterpretationOff  =
   False(struct
-          let option_name = "-aorai-AI-off"
-          let help = "does not use abstract interpretation"
-        end)
+    let option_name = "-aorai-AI-off"
+    let help = "does not use abstract interpretation"
+  end)
 
 let () = Parameter_customize.set_negative_option_name "-aorai-spec-off"
 module Axiomatization =
   True(struct
-         let option_name = "-aorai-spec-on"
-         let help = "if set, does not axiomatize automata"
-       end)
+    let option_name = "-aorai-spec-on"
+    let help = "if set, does not axiomatize automata"
+  end)
 
 module GenerateAnnotations =
   True
@@ -131,41 +131,34 @@ module GenerateDeterministicLemmas =
 
 module ConsiderAcceptance =
   False(struct
-         let option_name = "-aorai-acceptance"
-         let help = "if set, considers acceptation states"
-       end)
+    let option_name = "-aorai-acceptance"
+    let help = "if set, considers acceptation states"
+  end)
 
 let () = Parameter_customize.set_negative_option_name "-aorai-raw-auto"
 module AutomataSimplification=
   True
     (struct
-       let option_name = "-aorai-simplified-auto"
-       let help = "If set, does not simplify automata"
-     end)
-
-module Test =
-  Zero(struct
-         let option_name = "-aorai-test"
-         let arg_name = ""
-         let help = "Testing mode (0 = no test)"
-       end)
+      let option_name = "-aorai-simplified-auto"
+      let help = "If set, does not simplify automata"
+    end)
 
 module AddingOperationNameAndStatusInSpecification =
   False
     (struct
       let option_name = "-aorai-add-oper"
       let help = "Adding current operation name (and statut) in pre/post \
-conditions"
-     end)
+                  conditions"
+    end)
 
 module Deterministic=
   State_builder.Ref
     (Datatype.Bool)
     (struct
-        let name = "Aorai_option.Deterministic"
-        let dependencies = []
-        let default () = false
-     end)
+      let name = "Aorai_option.Deterministic"
+      let dependencies = []
+      let default () = false
+    end)
 
 module InstrumentationHistory =
   Int
@@ -187,20 +180,20 @@ let promela_file () =
 let advance_abstract_interpretation () =
   not (AbstractInterpretationOff.get ()) && not (AbstractInterpretation.get ())
 
-let emitter = 
+let emitter =
   Emitter.create
     "Aorai"
-    [ Emitter.Code_annot; Emitter.Funspec; Emitter.Global_annot ] 
+    [ Emitter.Code_annot; Emitter.Funspec; Emitter.Global_annot ]
     ~correctness:
-    [ Ltl_File.parameter; To_Buchi.parameter; Buchi.parameter;
-      Ya.parameter; Axiomatization.parameter;
-      ConsiderAcceptance.parameter;
-      AutomataSimplification.parameter ]
+      [ Ltl_File.parameter; To_Buchi.parameter; Buchi.parameter;
+        Ya.parameter; Axiomatization.parameter;
+        ConsiderAcceptance.parameter;
+        AutomataSimplification.parameter ]
     ~tuning:
-    [ AbstractInterpretation.parameter;
-      AddingOperationNameAndStatusInSpecification.parameter;
-      InstrumentationHistory.parameter;
-      GenerateAnnotations.parameter ]
+      [ AbstractInterpretation.parameter;
+        AddingOperationNameAndStatusInSpecification.parameter;
+        InstrumentationHistory.parameter;
+        GenerateAnnotations.parameter ]
 
 
 (*
diff --git a/src/plugins/aorai/aorai_option.mli b/src/plugins/aorai/aorai_option.mli
index 79482fd5f3bf793b933c95a10e4231ba42159ec8..4f8c3838eb488d2f257934861c94ba14880f09ca 100644
--- a/src/plugins/aorai/aorai_option.mli
+++ b/src/plugins/aorai/aorai_option.mli
@@ -38,7 +38,6 @@ module GenerateAnnotations: Parameter_sig.Bool
 module GenerateDeterministicLemmas: Parameter_sig.Bool
 module ConsiderAcceptance: Parameter_sig.Bool
 module AutomataSimplification: Parameter_sig.Bool
-module Test: Parameter_sig.Int
 module AddingOperationNameAndStatusInSpecification: Parameter_sig.Bool
 
 (** [true] if the user declares that its ya automaton is deterministic. *)
diff --git a/src/plugins/aorai/aorai_register.ml b/src/plugins/aorai/aorai_register.ml
index fe4775a424ced047d90ecaf96a2dd39f9b3509f6..d609113165c890b38a0cbe071952c633733fdcde 100644
--- a/src/plugins/aorai/aorai_register.ml
+++ b/src/plugins/aorai/aorai_register.ml
@@ -33,7 +33,6 @@ let output_c_file = ref Filepath.Normalized.unknown
 let ltl_tmp_file = ref Filepath.Normalized.unknown
 let ltl_file = ref Filepath.Normalized.unknown
 let dot_file = ref Filepath.Normalized.unknown
-let generatesCFile = ref true
 let ltl2ba_params = " -l -p -o "
 
 let ltl_to_promela = Hashtbl.create 7
@@ -45,15 +44,15 @@ let set_ltl_correspondence h =
 let convert_ltl_exprs t =
   let rec convert_cond cond =
     match cond with
-        POr(c1,c2) -> POr (convert_cond c1, convert_cond c2)
-      | PAnd(c1,c2) -> PAnd(convert_cond c1, convert_cond c2)
-      | PNot c -> PNot (convert_cond c)
-      | PCall _ | PReturn _ | PTrue | PFalse -> cond
-      | PRel(Neq,PVar x,PCst _) ->
-        (try
-           let (rel,t1,t2) = Hashtbl.find ltl_to_promela x in PRel(rel,t1,t2)
-         with Not_found -> cond)
-      | PRel _ -> cond
+      POr(c1,c2) -> POr (convert_cond c1, convert_cond c2)
+    | PAnd(c1,c2) -> PAnd(convert_cond c1, convert_cond c2)
+    | PNot c -> PNot (convert_cond c)
+    | PCall _ | PReturn _ | PTrue | PFalse -> cond
+    | PRel(Neq,PVar x,PCst _) ->
+      (try
+         let (rel,t1,t2) = Hashtbl.find ltl_to_promela x in PRel(rel,t1,t2)
+       with Not_found -> cond)
+    | PRel _ -> cond
   in
   let rec convert_seq_elt e =
     { e with
@@ -62,8 +61,8 @@ let convert_ltl_exprs t =
   and convert_seq s = List.map convert_seq_elt s in
   let convert_parsed c =
     match c with
-        Seq l -> Seq (convert_seq l)
-      | Otherwise -> Otherwise
+      Seq l -> Seq (convert_seq l)
+    | Otherwise -> Otherwise
   in
   let convert_trans t = { t with cross = convert_parsed t.cross } in
   List.map convert_trans t
@@ -117,7 +116,7 @@ let load_ya_file filename  =
   let channel = check_and_open_in filename "invalid Ya file" in
   let lexbuf = Lexing.from_channel channel in
   Lexing.(lexbuf.lex_curr_p <-
-    { lexbuf.lex_curr_p with pos_fname = (filename :> string) });
+            { lexbuf.lex_curr_p with pos_fname = (filename :> string) });
   try
     let automata = Yaparser.main Yalexer.token lexbuf in
     close_in channel;
@@ -136,7 +135,7 @@ let load_promela_file f  =
     let trans = convert_ltl_exprs auto.trans in
     close_in c;
     Data_for_aorai.setAutomata { auto with trans };
-  with 
+  with
   | Promelalexer.Error(loc,msg) -> syntax_error loc msg
 
 let load_promela_file_withexps f =
@@ -145,18 +144,16 @@ let load_promela_file_withexps f =
     let automata = Promelalexer_withexps.parse c  in
     close_in c;
     Data_for_aorai.setAutomata automata;
-  with 
+  with
   | Promelalexer_withexps.Error(loc,msg) -> syntax_error loc msg
 
 let display_status () =
   if Aorai_option.verbose_atleast 2 then begin
     Aorai_option.feedback "\n"  ;
     Aorai_option.feedback "C file:            '%a'\n" Filepath.Normalized.pretty !c_file ;
-    Aorai_option.feedback "Entry point:       '%a'\n" 
+    Aorai_option.feedback "Entry point:       '%a'\n"
       Kernel_function.pretty (fst (Globals.entry_point())) ;
     Aorai_option.feedback "LTL property:      '%a'\n" Filepath.Normalized.pretty !ltl_file ;
-    Aorai_option.feedback "Files to generate: '%a' (Annotated code)\n"
-      (if !generatesCFile then Filepath.Normalized.pretty else (fun fmt _ -> Format.fprintf fmt "(none)")) !output_c_file;
     if Aorai_option.Dot.get () then
       Aorai_option.feedback "Dot file:          '%a'\n" Filepath.Normalized.pretty !dot_file;
     Aorai_option.feedback "Tmp files:         '%a' (Light LTL file)\n"
@@ -167,15 +164,8 @@ let display_status () =
   end
 
 let init_file_names () =
-  (* Intermediate functions for error display or fresh name of file
-     generation *)
-  let err= ref false in
-  let dispErr mesg f =
-    Aorai_option.error "Error. File '%a' %s.\n" Filepath.Normalized.pretty f mesg;
-    err:=true
-  in
   let freshname ?opt_suf file suf =
-    let name = Filepath.Normalized.to_pretty_string file in
+    let name = (file:Filepath.Normalized.t:>string) in
     let pre = Filename.remove_extension name in
     let pre = match opt_suf with None -> pre | Some s -> pre ^ s in
     let rec fn p s n =
@@ -185,30 +175,14 @@ let init_file_names () =
     let name =
       if not (Sys.file_exists (pre^suf)) then pre^suf
       else fn pre suf 0
-    in Filepath.Normalized.of_string name
+    in
+    Filepath.Normalized.of_string name
   in
-
-  (* c_file name is given and has to point out a valid file. *)
-  c_file :=
-    (match Kernel.Files.get () with
-      | [] -> Filepath.Normalized.of_string "dummy.i"
-      | f :: _ -> f);
-  if (Filepath.Normalized.is_unknown !c_file) then dispErr ": invalid C file name" !c_file;
-
-  (* The output C file has to be a valid file name if it is used. *)
-  output_c_file := Aorai_option.Output_C_File.get ();
-  if (Filepath.Normalized.is_unknown !output_c_file) then
-    output_c_file := freshname ~opt_suf:"_annot" !c_file ".c";
-  (*   else if Sys.file_exists !output_c_file then dispErr "already exists" !output_c_file; *)
-
-  if Aorai_option.Dot.get () then
-    dot_file:= freshname !c_file ".dot";
-
   if Filepath.Normalized.is_unknown (Aorai_option.Ya.get ()) then
     if Filepath.Normalized.is_unknown (Aorai_option.Buchi.get ()) then begin
       (* ltl_file name is given and has to point out a valid file. *)
       ltl_file := Aorai_option.Ltl_File.get ();
-
+      if Aorai_option.Dot.get() then dot_file := freshname !ltl_file ".dot";
       (* The LTL file is always used. *)
       (* The promela file can be given or not. *)
       if not (Filepath.Normalized.is_unknown (Aorai_option.To_Buchi.get ())) then begin
@@ -232,26 +206,25 @@ let init_file_names () =
       if not (Filepath.Normalized.is_unknown (Aorai_option.To_Buchi.get ())) &&
          not (Filepath.Normalized.is_unknown (Aorai_option.Ltl_File.get ()))
       then begin
-        Aorai_option.error
+        Aorai_option.abort
           "Error. '-buchi' option is incompatible with '-to-buchi' and '-ltl' \
-options.";
-        err:=true
+           options."
       end;
       (* The promela file is used only if the process does not terminate after
-         LTL generation. *)
+          LTL generation. *)
       promela_file := Aorai_option.promela_file ();
+      if Aorai_option.Dot.get() then
+        dot_file := freshname !promela_file ".dot";
     end
   else begin
-   let ya_file = Aorai_option.Ya.get () in
-    if (Filepath.Normalized.is_unknown ya_file) then dispErr ": invalid Ya file name" ya_file;
+    let ya_file = Aorai_option.Ya.get () in
+    if (Filepath.Normalized.is_unknown ya_file) then
+      Aorai_option.abort
+        "invalid Ya file name %a" Filepath.Normalized.pretty ya_file;
+    if Aorai_option.Dot.get() then
+      dot_file := freshname ya_file ".dot"
   end;
-  display_status ();
-  !err
-
-let init_test () =
-  match Aorai_option.Test.get () with
-  | 1 -> generatesCFile := false;
-  | _ -> generatesCFile := true
+  display_status ()
 
 let printverb s = Aorai_option.feedback ~level:2 "%s" s
 
@@ -263,26 +236,8 @@ let output () =
         (!dot_file:>string);
       printverb "Generating dot file    : done\n"
     end;
-
-  (* C file *)
-  if (not !generatesCFile) then
-    printverb "C file generation      : skipped\n"
-  else
-    begin
-      let cout = open_out (!output_c_file:>string) in
-      let fmt = Format.formatter_of_out_channel cout in
-      Kernel.Unicode.without_unicode
-        (fun () ->
-          File.pretty_ast ~fmt ();
-          close_out cout;
-          printverb "C file generation      : done\n";
-        ) ()
-    end;
-
-  printverb "Finished.\n";
   (* Some test traces. *)
-  Data_for_aorai.debug_computed_state ();
-  if !generatesCFile then Kernel.Files.set [ !output_c_file ]
+  Data_for_aorai.debug_computed_state ()
 
 let work () =
   let file = Ast.get () in
@@ -297,15 +252,15 @@ let work () =
           Filepath.Normalized.pretty !ltl_tmp_file
           Filepath.Normalized.pretty !promela_file
       in if Sys.command cmd <> 0 then
-          Aorai_option.abort "failed to run: %s" cmd ;
+        Aorai_option.abort "failed to run: %s" cmd ;
       printverb "LTL ~> Promela (ltl2ba): done\n"
     end;
   if not (Filepath.Normalized.is_unknown (Aorai_option.To_Buchi.get ())) then
     printverb ("Finished.\nGenerated file: '"^(Filepath.Normalized.to_pretty_string !promela_file)^"'\n")
   else
     begin
-        (* Step 3 : Loading promela_file and checking the consistency between informations from C code and LTL property *)
-        (*          Such as functions name and global variables. *)
+      (* Step 3 : Loading promela_file and checking the consistency between informations from C code and LTL property *)
+      (*          Such as functions name and global variables. *)
 
       if not (Filepath.Normalized.is_unknown (Aorai_option.Buchi.get ())) then
         load_promela_file_withexps !promela_file
@@ -314,23 +269,23 @@ let work () =
       else
         load_promela_file !promela_file;
       printverb "Loading promela        : done\n";
-        (* Computing the list of ignored functions *)
-        (*      Aorai_visitors.compute_ignored_functions file; *)
+      (* Computing the list of ignored functions *)
+      (*      Aorai_visitors.compute_ignored_functions file; *)
 
 
-        (* Promelaoutput.print_raw_automata (Data_for_aorai.getAutomata());  *)
-        (* Data_for_aorai.debug_ltl_expressions (); *)
+      (* Promelaoutput.print_raw_automata (Data_for_aorai.getAutomata());  *)
+      (* Data_for_aorai.debug_ltl_expressions (); *)
 
       (*let _ = Path_analysis.test (Data_for_aorai.getAutomata())in*)
       let root = fst (Globals.entry_point ()) in
       let axiomatization = Aorai_option.Axiomatization.get() in
       if axiomatization then
         begin
-            (* Step 5 : incrementing pre/post
-               conditions with states and transitions information *)
+          (* Step 5 : incrementing pre/post
+             conditions with states and transitions information *)
           printverb "Refining pre/post      : \n";
           Aorai_dataflow.compute ();
-            (* Step 6 : Removing transitions never crossed *)
+          (* Step 6 : Removing transitions never crossed *)
           let automaton_has_states =
             if (Aorai_option.AutomataSimplification.get()) then
               begin
@@ -362,19 +317,19 @@ let work () =
         end
       else
         begin
-            (* Step 4': Computing the set of possible pre-states and post-states of each function *)
-            (*          And so for pre/post transitions *)
+          (* Step 4': Computing the set of possible pre-states and post-states of each function *)
+          (*          And so for pre/post transitions *)
           printverb "Abstracting pre/post   : skipped\n";
 
-            (* Step 5': incrementing pre/post conditions with states and transitions information *)
+          (* Step 5': incrementing pre/post conditions with states and transitions information *)
           printverb "Refining pre/post      : skipped\n";
 
 
-            (* Step 6 : Removing transitions never crossed *)
+          (* Step 6 : Removing transitions never crossed *)
           printverb "Removing unused trans  : skipped\n";
 
-            (* Step 7 : Labeling abstract file *)
-            (* Finally the information is added into the Cil automata. *)
+          (* Step 7 : Labeling abstract file *)
+          (* Finally the information is added into the Cil automata. *)
           Aorai_utils.initGlobals root axiomatization;
           Aorai_visitors.add_sync_with_buch file;
           printverb "Annotation of Cil      : partial\n"
@@ -392,24 +347,16 @@ let work () =
     end
 
 let run () =
-  Aorai_option.result "Welcome to the Aorai plugin@.";
-  init_test ();
-
   (* Step 1 : Capture files names *)
-  let error_status = init_file_names () in
-  (* Treatment is done only if parameters are valid *)
-  if error_status then
-    Aorai_option.error "Generation stopped."
-  else
-
-    (* Step 2 : Work in our own project, initialized by a copy of the main
-       one. *)
-    let work_prj =
-      File.create_project_from_visitor "aorai"
-        (fun prj -> new Visitor.frama_c_copy prj)
-    in
-    Project.copy ~selection:(Parameter_state.get_selection ()) work_prj;
-    Project.on work_prj work ()
+  init_file_names ();
+  (* Step 2 : Work in our own project, initialized by a copy of the main
+     one. *)
+  let work_prj =
+    File.create_project_from_visitor "aorai"
+      (fun prj -> new Visitor.frama_c_copy prj)
+  in
+  Project.copy ~selection:(Parameter_state.get_selection ()) work_prj;
+  Project.on work_prj work ()
 
 (* Plugin registration *)
 
@@ -426,9 +373,9 @@ let run, _ =
     "Aorai"
     (let module O = Aorai_option in
      [ O.Ltl_File.self; O.To_Buchi.self; O.Buchi.self;
-      O.Ya.self; O.Axiomatization.self; O.ConsiderAcceptance.self;
-      O.AutomataSimplification.self; O.AbstractInterpretation.self;
-      O.AddingOperationNameAndStatusInSpecification.self ])
+       O.Ya.self; O.Axiomatization.self; O.ConsiderAcceptance.self;
+       O.AutomataSimplification.self; O.AbstractInterpretation.self;
+       O.AddingOperationNameAndStatusInSpecification.self ])
     run
 
 let main () = if Aorai_option.is_on () then run ()
diff --git a/src/plugins/aorai/tests/ltl/goto.c b/src/plugins/aorai/tests/ltl/goto.c
index ccd31e28dbe2344aa5c4fee8254898945fcfa29c..8cbd56c0842494483bbbf423b8f28eeb7853a751 100644
--- a/src/plugins/aorai/tests/ltl/goto.c
+++ b/src/plugins/aorai/tests/ltl/goto.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 int status=0;
diff --git a/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle b/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle
index e06220b829a21490d9e731597629a8af15419041..e8fddab9facef7d0257db700af4d9007d123051f 100644
--- a/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/goto.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [aorai] tests/ltl/goto.c:28: Warning: 
   Call to opc does not follow automaton's specification. This path is assumed to be dead
 [kernel] Parsing TMPDIR/aorai_goto_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
index 7504f14db91b1210fc241a88b6d3aef23383d3d8..04174d4018a865d5e854376f9bd0a5aca035c5fe 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
@@ -1,7 +1,6 @@
 [kernel] Parsing tests/ltl/test_boucle.c (with preprocessing)
 [kernel:typing:implicit-function-declaration] tests/ltl/test_boucle.c:16: Warning: 
   Calling undeclared function call_to_an_undefined_function. Old style K&R code?
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_boucle_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
index 810cc3f996f1b162ac7c9e9a6b1f0d509853d2f1..aed1c6cbbf0e5f8c0333d3b2038f72c2d1e6412f 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_boucle1.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_boucle1_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
index bf069fb7cfce5612379c5a2c80540bb07db94e31..9ab4d87d9cc4fec37cb7161c6985fbba348376e2 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_boucle2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_boucle2_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
index bbf09f7914af37ccd19f0eeb02e56ce59f3853e2..8b2d1dbb5f25e9a5e7ce4f93d939320ceff7e03c 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_boucle3.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_boucle3_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
index d434d1ddf705c3dbd33831dba0827d3c4a8ba00c..4a0a9031b26157edb32bc4646da67494a4734c6d 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_factorial.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_factorial_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle
index 28c0b50dbab69fcc8cd831e6791f43ace8439798..a377f6f727cf1145d02b2f0e5277e23d68f5c293 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle
@@ -5,7 +5,6 @@
   parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
 [kernel] tests/ltl/test_recursion1.c:54: Warning: 
   parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_recursion1_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
index 0c38acfaa75591b7f30ff5ef1c54ebe2446995e6..6dda5c9d85b5c4ff6209a1347863c8efd0b1838b 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_recursion2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_recursion2_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
index 97d6decf1f8df3d0daf2acb49b6edd6e7cb53558..aabed966d5a0f114ae66bb87c5b263bab35d8e27 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_recursion2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_recursion2_1.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle
index b3c85addc01c55afdd11746420fba2f62361f199..88e19cf5f590edfaa350bdeef336969f7cf3149b 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_switch2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [aorai] tests/ltl/test_switch2.c:34: Warning: 
   Call to opc not conforming to automaton (post-cond). Assuming it is on a dead path
 [aorai] tests/ltl/test_switch2.c:23: Warning: 
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
index 4d74ec69aeb2cae08b4b990cf52e83e37258604c..3b0822025db85b3f78f088c4147467d42c4385fc 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_switch3.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_switch3_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle
index 96b9dc90c1e354c849080815cb015ba467bb2397..94652a4ad7343682dfdb2329d514d27232c24ff6 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_switch3_et_recursion.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [aorai] tests/ltl/test_switch3_et_recursion.c:26: Warning: 
   Call to countOne does not follow automaton's specification. This path is assumed to be dead
 [kernel] Parsing TMPDIR/aorai_test_switch3_et_recursion_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
index 23495bc09b5a1c69662a183e5eb5fddcecc16787..74f48874eb313e191b4918e670f2126e8843de58 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_switch3_if.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_switch3_if_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
index 1c04d032f84346569b3c9b803fdc19c3048314f3..e4f973d66d554a0ac72c98aca30e5600442a4cc3 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_switch3_return.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_switch3_return_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/goto.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/goto.res.oracle
index a0b1d8ed006dcc5ea0ee140a4ffe963e975d0e90..8e07b35953f76a889c06c6b94390006f13565928 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/goto.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/goto.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/goto.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [aorai] tests/ltl/goto.c:28: Warning: 
   Call to opc does not follow automaton's specification. This path is assumed to be dead
 [kernel] Parsing TMPDIR/aorai_goto_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
index 2d27926df0c01f67d7cd6e6aab08effa8a00c3af..e3d5ec00773c630fcd03a506eaec86aa0b0777ee 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
@@ -1,7 +1,6 @@
 [kernel] Parsing tests/ltl/test_boucle.c (with preprocessing)
 [kernel:typing:implicit-function-declaration] tests/ltl/test_boucle.c:16: Warning: 
   Calling undeclared function call_to_an_undefined_function. Old style K&R code?
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_boucle_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
 [kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0.i:86: Warning: 
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle1.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle1.res.oracle
index 1569a5b398d4faf17bcd738ec5e59ba3470a7d8f..c7334dc7d0e47e4f03ab43e11ff87faab1c583af 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle1.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_boucle1.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_boucle1_0.i (no preprocessing)
 [wp] TMPDIR/aorai_test_boucle1_0.i:3: Warning: 
   Global invariant not handled yet ('inv_cpt' ignored)
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle2.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle2.res.oracle
index 6aff87fc8f04cb57fafbcfab6e1693e21a6112c8..1da39e22bb3f77b68bdfd9a967e3448f141d13e1 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle2.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_boucle2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_boucle2_0.i (no preprocessing)
 [wp] TMPDIR/aorai_test_boucle2_0.i:4: Warning: 
   Global invariant not handled yet ('inv' ignored)
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle3.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle3.res.oracle
index d42c00524da292d300baf6eb1c8465fca0a1de88..8f6717a1e318e6976e9ba28deca3fd2c64bc2cdd 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle3.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_boucle3.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_boucle3_0.i (no preprocessing)
 [wp] TMPDIR/aorai_test_boucle3_0.i:4: Warning: 
   Global invariant not handled yet ('inv' ignored)
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_factorial.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_factorial.res.oracle
index 6e1e98b96475e950de103887600795bebb7f75c7..0a52966e046dc1fb9d3add5f07e55b9c93b13ab2 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_factorial.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ltl/test_factorial.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_factorial_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion1.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion1.res.oracle
index b41e5fc1a018d973abfb9b98ecb0739dc439b879..b5e9aba20ed217ff7340c60ba5f738a388ba80e9 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion1.res.oracle
@@ -5,7 +5,6 @@
   parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
 [kernel] tests/ltl/test_recursion1.c:54: Warning: 
   parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_recursion1_0.i (no preprocessing)
 [wp] Warning: No definition for 'string_len' interpreted as reads nothing
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.0.res.oracle
index ccdb613ba7df3a6e4cf3d433a986b71f550e4501..9891c035100b93d2c7f9dfda512688613a83d126 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.0.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.0.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_recursion2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_recursion2_0.i (no preprocessing)
 [wp] Warning: No definition for 'string_len' interpreted as reads nothing
 [wp] Warning: No definition for 'sum_tab' interpreted as reads nothing
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.1.res.oracle
index 8e71caf0debca2dc610c47ca48fbce0d3983eb82..904f906300cd765dbc82900fc04a8f861e28e484 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.1.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_recursion2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_recursion2_1.i (no preprocessing)
 [wp] Warning: No definition for 'string_len' interpreted as reads nothing
 [wp] Warning: No definition for 'sum_tab' interpreted as reads nothing
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch2.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch2.res.oracle
index 9964a15c39c0df3664931de857618178351c0552..5e6c56778cf99c15ab7fd72ef63105540588b23c 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch2.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_switch2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [aorai] tests/ltl/test_switch2.c:34: Warning: 
   Call to opc not conforming to automaton (post-cond). Assuming it is on a dead path
 [aorai] tests/ltl/test_switch2.c:23: Warning: 
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3.res.oracle
index bfe46c01065891f3dc5d9c074dfc8a316e494409..1370ce59a991ba6eb4b392edde15f855451b98c5 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ltl/test_switch3.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_switch3_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_et_recursion.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_et_recursion.res.oracle
index f13072d1a65cb42361f1cb18532fbc21dba5c80a..0c3127bafe547fb808d547145daf183e709e4f3a 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_et_recursion.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_et_recursion.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ltl/test_switch3_et_recursion.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [aorai] tests/ltl/test_switch3_et_recursion.c:26: Warning: 
   Call to countOne does not follow automaton's specification. This path is assumed to be dead
 [kernel] Parsing TMPDIR/aorai_test_switch3_et_recursion_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_if.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_if.res.oracle
index 68de03d1b30d2be55649d7e8c0139bd9668a380e..bf53ddf15baf64391dbcc15a5a67b6dd579f9445 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_if.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_if.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ltl/test_switch3_if.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_switch3_if_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_return.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_return.res.oracle
index 2bfc5074656abd0609d096003396b2d396dbdce4..eb8fb8e27b51954dd4935997e25b24735c7302b3 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_return.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_return.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ltl/test_switch3_return.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_switch3_return_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/test_boucle.c b/src/plugins/aorai/tests/ltl/test_boucle.c
index 72cf5e78ac931fa05a5a21be18a1777112e6e8e2..db2f6bc0c3f18408ea163acbdaacffdaaeac8ac3 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 /*@ requires \true;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle1.c b/src/plugins/aorai/tests/ltl/test_boucle1.c
index 0245ffedcfdfe67aad9a8d9610159c9a3313b0e8..7b091c51b7614a411c3afdb521561a4785ffcf16 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle1.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle1.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 int cpt=3;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle2.c b/src/plugins/aorai/tests/ltl/test_boucle2.c
index 9d4cf3a9aff3c018e3739a253578cdcfb92eea5e..8aa77e6f8b0589e2f53869d76fb00adba6abd76a 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle2.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle2.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 int status=0;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle3.c b/src/plugins/aorai/tests/ltl/test_boucle3.c
index 6c93a4202649a24dff714ef33906252a84b74704..6da17de07b287db5befa2b3bcd350672f128f03d 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle3.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle3.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 
diff --git a/src/plugins/aorai/tests/ltl/test_factorial.c b/src/plugins/aorai/tests/ltl/test_factorial.c
index 6a429a55e31de0a06be227ffd9ca72d1fb4770ea..0ad6476002658f8a1bedc42146f14f3229b42427 100644
--- a/src/plugins/aorai/tests/ltl/test_factorial.c
+++ b/src/plugins/aorai/tests/ltl/test_factorial.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 
diff --git a/src/plugins/aorai/tests/ltl/test_recursion1.c b/src/plugins/aorai/tests/ltl/test_recursion1.c
index ee0968101b1a776f5b232d5740d4ae4e2c568f7e..14be685a47bcdfbaf534712834e6a69acc2de9fb 100644
--- a/src/plugins/aorai/tests/ltl/test_recursion1.c
+++ b/src/plugins/aorai/tests/ltl/test_recursion1.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 
diff --git a/src/plugins/aorai/tests/ltl/test_recursion2.c b/src/plugins/aorai/tests/ltl/test_recursion2.c
index a13c39b9f887df7af32c52fa0f2a142e992478cd..7d93ab3fa3a3e28e205517b56bc795ad2b427ebf 100644
--- a/src/plugins/aorai/tests/ltl/test_recursion2.c
+++ b/src/plugins/aorai/tests/ltl/test_recursion2.c
@@ -1,6 +1,6 @@
 /* run.config*
-   OPT: -aorai-buchi @PTEST_DIR@/@PTEST_NAME@.promela -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
-   OPT: -aorai-buchi @PTEST_DIR@/test_recursion3.promela -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-buchi @PTEST_DIR@/@PTEST_NAME@.promela -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-buchi @PTEST_DIR@/test_recursion3.promela -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 /* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ltl/test_switch2.c b/src/plugins/aorai/tests/ltl/test_switch2.c
index f411cec23dcd459cbfe1bdb5d3d33b05ad6e3ee2..2bb7284fbbd78e3c7d6455efbceaac54213338b6 100644
--- a/src/plugins/aorai/tests/ltl/test_switch2.c
+++ b/src/plugins/aorai/tests/ltl/test_switch2.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 int status=0;
diff --git a/src/plugins/aorai/tests/ltl/test_switch3.c b/src/plugins/aorai/tests/ltl/test_switch3.c
index 42e5fc6ba9aebb0bf7be62ec776e3a969f250d4a..5d9e8582f493e3d9d10f5343e8eeff8e4897b048 100644
--- a/src/plugins/aorai/tests/ltl/test_switch3.c
+++ b/src/plugins/aorai/tests/ltl/test_switch3.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 /* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c b/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c
index 00caa9826bb96e63a099b54204d1e1d5e9c3aeab..352725ef98403e943292dd701851020dd9450331 100644
--- a/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c
+++ b/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 /* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ltl/test_switch3_if.c b/src/plugins/aorai/tests/ltl/test_switch3_if.c
index f6375d4d859a018e4349cbcbdca037d48298de40..93dd122636eb69e79de4ed04781fa4528a261027 100644
--- a/src/plugins/aorai/tests/ltl/test_switch3_if.c
+++ b/src/plugins/aorai/tests/ltl/test_switch3_if.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 /* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ltl/test_switch3_return.c b/src/plugins/aorai/tests/ltl/test_switch3_return.c
index a105540b9829ff3d2cdb2a7c12b4f7b056c8ece2..8df70979968ab549179cf70011105ac4083f0001 100644
--- a/src/plugins/aorai/tests/ltl/test_switch3_return.c
+++ b/src/plugins/aorai/tests/ltl/test_switch3_return.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 /* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ya/assigns.c b/src/plugins/aorai/tests/ya/assigns.c
index ce6fe159678db8d14bddb1119d020f3b6362b14b..c760aa1537ec7d120bb213e1eeab4c0df7da9ef0 100644
--- a/src/plugins/aorai/tests/ya/assigns.c
+++ b/src/plugins/aorai/tests/ya/assigns.c
@@ -1,8 +1,8 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya  -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
-   OPT: -aorai-automata @PTEST_DIR@/assigns_det.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/assigns_det.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
    MODULE: @PTEST_DIR@/name_projects.cmxs
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -then -print
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -then -print
 */
 
 int X;
diff --git a/src/plugins/aorai/tests/ya/bts1289.i b/src/plugins/aorai/tests/ya/bts1289.i
index 2c6c8f9aa59097ab9cd9f8dd9aa63d1ffcf62900..93cf50233c6de580a502d09ec0ebb9e0710a3fd4 100644
--- a/src/plugins/aorai/tests/ya/bts1289.i
+++ b/src/plugins/aorai/tests/ya/bts1289.i
@@ -1,6 +1,6 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@-2.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@-2.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
  */
 
 void a(void) {}
diff --git a/src/plugins/aorai/tests/ya/declared_function.i b/src/plugins/aorai/tests/ya/declared_function.i
index 53bcdfd71ad5fdf29b39d44acc444dd4a29d5c79..12f50538eb389c40452004dcae442b80e72800c5 100644
--- a/src/plugins/aorai/tests/ya/declared_function.i
+++ b/src/plugins/aorai/tests/ya/declared_function.i
@@ -1,5 +1,5 @@
 /* run.config*
-OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 int f(void);
diff --git a/src/plugins/aorai/tests/ya/deterministic.i b/src/plugins/aorai/tests/ya/deterministic.i
index b92271127e264c85e2578be4fbdc86a1e7ac8a9e..d892d8913785cf908250be51ee907aea92bd59fe 100644
--- a/src/plugins/aorai/tests/ya/deterministic.i
+++ b/src/plugins/aorai/tests/ya/deterministic.i
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 int X;
diff --git a/src/plugins/aorai/tests/ya/formals.i b/src/plugins/aorai/tests/ya/formals.i
index 4a32df49b67be992c14ceb88e3541d05c638992d..a463e4f7d372e66081bacb8a83c6c1fbc799a62e 100644
--- a/src/plugins/aorai/tests/ya/formals.i
+++ b/src/plugins/aorai/tests/ya/formals.i
@@ -1,5 +1,5 @@
 /* run.config*
-OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 int f(int x) { return x; }
diff --git a/src/plugins/aorai/tests/ya/generate_assigns_bts1290.i b/src/plugins/aorai/tests/ya/generate_assigns_bts1290.i
index 2e92796ec0655d2ae0977566205fc1072e275a60..d9333d415f6a9e4a266b9b4e4ee0fffb0157aeec 100644
--- a/src/plugins/aorai/tests/ya/generate_assigns_bts1290.i
+++ b/src/plugins/aorai/tests/ya/generate_assigns_bts1290.i
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
  */
 void main(void)
 {
diff --git a/src/plugins/aorai/tests/ya/hoare_seq.i b/src/plugins/aorai/tests/ya/hoare_seq.i
index cc7e148477430589b00c142325c5a4baf3a32531..b60ae6082da68af639a7419bd7b8fcc06c1dbfcc 100644
--- a/src/plugins/aorai/tests/ya/hoare_seq.i
+++ b/src/plugins/aorai/tests/ya/hoare_seq.i
@@ -1,5 +1,5 @@
 /* run.config*
-OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 void f(void) { }
diff --git a/src/plugins/aorai/tests/ya/incorrect.i b/src/plugins/aorai/tests/ya/incorrect.i
index fae082d3120aa4fd80c2354bcc318c71e43a689d..01f702808601302f85949d38f64b69b4f79c8ab7 100644
--- a/src/plugins/aorai/tests/ya/incorrect.i
+++ b/src/plugins/aorai/tests/ya/incorrect.i
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 int f(void);
diff --git a/src/plugins/aorai/tests/ya/loop_bts1050.i b/src/plugins/aorai/tests/ya/loop_bts1050.i
index fdec741b7b32ef14be4756afd8847a9ac21ccb27..86fe369e9f793b991fd0e3f4510b1ea5111b1c55 100644
--- a/src/plugins/aorai/tests/ya/loop_bts1050.i
+++ b/src/plugins/aorai/tests/ya/loop_bts1050.i
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 void f(){};
 
diff --git a/src/plugins/aorai/tests/ya/metavariables-incompatible.i b/src/plugins/aorai/tests/ya/metavariables-incompatible.i
index 26744167705ea93e49e38818c96dcb32d17b623b..a32cefe9e95a077a549e747e0231200ad48c4a5b 100644
--- a/src/plugins/aorai/tests/ya/metavariables-incompatible.i
+++ b/src/plugins/aorai/tests/ya/metavariables-incompatible.i
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 void main(void) {}
diff --git a/src/plugins/aorai/tests/ya/metavariables-right.i b/src/plugins/aorai/tests/ya/metavariables-right.i
index cff3994c1017f532d1d44db092abb5be27d1dcb8..9d88e67323f1579b8cb9ff96e0713ab2652fbb67 100644
--- a/src/plugins/aorai/tests/ya/metavariables-right.i
+++ b/src/plugins/aorai/tests/ya/metavariables-right.i
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 void f(int x) {}
diff --git a/src/plugins/aorai/tests/ya/metavariables-wrong.i b/src/plugins/aorai/tests/ya/metavariables-wrong.i
index 09ea4b6c4bcfc15e83ef2c2a676be84c00ca294b..a0542d200213bae00dd447ca74e59ef7a0c15f08 100644
--- a/src/plugins/aorai/tests/ya/metavariables-wrong.i
+++ b/src/plugins/aorai/tests/ya/metavariables-wrong.i
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 void f(int x) {}
diff --git a/src/plugins/aorai/tests/ya/monostate.i b/src/plugins/aorai/tests/ya/monostate.i
index 9dade69c092b118f482686eaa918ee2e878a692c..0d72d9a431caaf166b2bcdbf4cdbceca3e231244 100644
--- a/src/plugins/aorai/tests/ya/monostate.i
+++ b/src/plugins/aorai/tests/ya/monostate.i
@@ -1,5 +1,5 @@
 /* run.config
-OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 void f(void) {}
diff --git a/src/plugins/aorai/tests/ya/not_prm.i b/src/plugins/aorai/tests/ya/not_prm.i
index d96e123d6e6a367565597f0cce0df942b23a2ba5..8b5c4281608d86fbed207d2f056fcb22f6513953 100644
--- a/src/plugins/aorai/tests/ya/not_prm.i
+++ b/src/plugins/aorai/tests/ya/not_prm.i
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test -main f -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test -main f -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 int f(int x) {
diff --git a/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle b/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
index 8c31757f7be947f639da13da388b5d61d1d18e71..a0d1e8e9805cb518ef7dd64fe057fdc454603cd6 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/assigns.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_assigns_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
index cdb19dd27629019910814cbdfed089f7feadc3ee..067dda49b4da26140d890bff0562197c4771c561 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/assigns.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_assigns_1.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_States {
diff --git a/src/plugins/aorai/tests/ya/oracle/assigns.2.res.oracle b/src/plugins/aorai/tests/ya/oracle/assigns.2.res.oracle
index f5a60a3aac12f9e6f74b645b97c97125445d9996..5a761e8ca86775a91718ded77e107d61a8a15aa6 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.2.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.2.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/assigns.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 /* Generated by Frama-C */
 int X;
 void f(void)
diff --git a/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle b/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
index d694fc99a038a4c55017d6a0dc095bbab7196059..15f90358d6d80d076d3bbc1d5037100798bf47c2 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/bts1289.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
 [kernel] Parsing TMPDIR/aorai_bts1289_0.i (no preprocessing)
 /* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
index 3c96ba015886f3598f2289bba6a35a46309f64e2..6fb3035c21ae0f523e25c9b83807cdce7675ee74 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/bts1289.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_bts1289_1.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
index 162c17c6430a0c7f9ed5cc669a949fd117ba2452..038d8c1a87087eae5fdcc7596b0515b6f7265d70 100644
--- a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/declared_function.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_declared_function_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_States {
diff --git a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
index 7d3f5aa88777d3c1fac64715ff6ac126db4cb1b5..72d480289360a25c758af89999a1d516a13bc578 100644
--- a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/deterministic.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_deterministic_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_States {
diff --git a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
index cbe2ba005bef80cd8401bcc3d5b36f696d3281b7..e93f5561f0807a14d00498c42c24d8ba4ff50589 100644
--- a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/formals.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_formals_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_States {
diff --git a/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle b/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
index 818442d76187088f2978e417638c446b9864c827..6dba7900323402dcd732a3b81604b6ece4b4f1cb 100644
--- a/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/generate_assigns_bts1290.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_generate_assigns_bts1290_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
index 6095d7964e2c4d7526faf4862ec8ac8bfd787e35..29ffb1ff422b6b31e10952122c05b1f1ff1d650c 100644
--- a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/hoare_seq.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_hoare_seq_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
index 21a5cd9feb5329782519856617e4e888d6221448..22596de4c18a3aa77dbb683b11aa7707bfd7e550 100644
--- a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/incorrect.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
 [kernel] Parsing TMPDIR/aorai_incorrect_0.i (no preprocessing)
 /* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
index 14b24d45cddfb0f1d2d147e149127967c148440c..6569b67175a8280471a8c3cb305840c14053e5e4 100644
--- a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/loop_bts1050.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_loop_bts1050_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle
index 1a257aa76d2a867a0ef61196a96d7618541bd606..a682bee8a270311ec22d7a3b33999a452ac306bf 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/metavariables-incompatible.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [aorai] User Error: The use of metavariables is incompatible with non-deterministic automata, such as automata using extended transitions.
 [kernel] Plug-in aorai aborted: invalid user input.
diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
index e753f6649c43947b761c5fa9a1eff8975e595692..ee94f69b3848bbc6b9b26950a0b9736b328bbe99 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/metavariables-right.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_metavariables-right_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_States {
diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-wrong.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-wrong.res.oracle
index 44c1487fcf7693e627a38f17cea95e7cd8e7b492..7aca51a51b2a805049c34693029c51f4dbd8a369 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-wrong.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-wrong.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/metavariables-wrong.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [aorai] User Error: The metavariables aorai_x may not be initialized before the transition from e to f_0:
   { (Call(h)) and ((aorai_x) > (0)) }
 [kernel] Plug-in aorai aborted: invalid user input.
diff --git a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
index 4b5d328fbbea498c667ace7217cc15b157eddb34..984890928fa440a12a69183ee4d138aae1306960 100644
--- a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/monostate.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
 [aorai] tests/ya/monostate.i:8: Warning: 
   Call to main not conforming to automaton (pre-cond). Assuming it is on a dead path
diff --git a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
index a1315a44ec98d6077751b08104bd3115eeb5f930..79d8cc18058df72e85381c46d1d59f80ff09f81d 100644
--- a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/not_prm.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_not_prm_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/other.res.oracle b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
index ea8efc3984f7b9c7adbe61320f4b9b41950efeeb..d7146144fdf2901adb66b6a09f4c2a019c0cd8fb 100644
--- a/src/plugins/aorai/tests/ya/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/other.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_other_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
index 8a68e3c289489ec4062c5eaf9d9234965b337bb9..92b8136c6f9ff6db57d75f729389cec00afcbff5 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/seq.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_seq_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
index 241908d1ee501a201e2240ecfb5484099cd40652..ea66b1d2bf754868b2a05efbd8b9c8dc413a61bc 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/seq_loop.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_seq_loop_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
index 5f1197b44ca72486f0810f627d81a87e6e568c7a..6cc4d3484ec9a67a1f3d4798d4bb24761cd46cc0 100644
--- a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/serial.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel:annot:missing-spec] tests/ya/serial.c:43: Warning: 
   Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
 [eva] Analyzing a complete application starting at main
diff --git a/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle b/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
index ea9bdd5f8c44f4e60ea26e0cf2d916169aa44109..6264eea6c56d38291d3d6007ccec7b1702a4c7df 100644
--- a/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/single_call.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_single_call_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
index e76ec6fc3ca67bd677079f2888024f1a34b471f0..311412524b5009aba4debf1e643b10fbb91dc723 100644
--- a/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/singleassignment-right.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_singleassignment-right_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_States {
diff --git a/src/plugins/aorai/tests/ya/oracle/singleassignment-wrong.res.oracle b/src/plugins/aorai/tests/ya/oracle/singleassignment-wrong.res.oracle
index a24943fca9867c96902f607deaafe3a12f1a2e71..9eca9305b90905e2fe0c03ebb470b6b321956636 100644
--- a/src/plugins/aorai/tests/ya/oracle/singleassignment-wrong.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/singleassignment-wrong.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/singleassignment-wrong.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [aorai] User Error: The metavariable aorai_x is assigned several times during the transition from a to b:
   { Call(main) } aorai_x <- x
                  aorai_x <- aorai_x + 1
diff --git a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
index b20f875ba1400ef04b46722a6d248482175a1437..7bb7948a156df11a03f6795a73ed979157a58b1e 100644
--- a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/stack.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_stack_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_States {
diff --git a/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
index 960ccd88bee0e98436f8b49004060cdfd70d4e36..72d1dbd1b7087f20168713e8811b6529fe5047c3 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/test_acces_params.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_acces_params_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
index 0527f8f7b592cc272a2d1b250c1d61c71211b75a..f20db94ee5b3eb2af611286e49d3866b42e02735 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/test_acces_params2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_acces_params2_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
index 3e9c2f9103d143b98528450a2e512548da46841e..d9e7db7f8036d21031746b26ee84b19aa5ffcf14 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
@@ -3,7 +3,6 @@
   parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
 [kernel] tests/ya/test_boucle_rechercheTableau.c:7: Warning: 
   parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_boucle_rechercheTableau_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
index 70c686c2f89ed0d6e6a7211bb6a348fd81cae358..ed5f20033adfc02c42e59041a6d3fc7548e8ef8d 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/test_factorial.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_factorial_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
index 968521d3ad2ecef832776490a9f78c5345c5543d..3f9a007d77696b6178c88a55def1baf568004e5c 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/test_recursion4.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_recursion4_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
index 1a84302afcdb9689c16739c356a1c26601259dee..b3d197570e702e04d0d7730ca993dd6fa5d6faa1 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
@@ -3,7 +3,6 @@
   parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
 [kernel] tests/ya/test_recursion5.c:28: Warning: 
   parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_recursion5_0.i (no preprocessing)
 /* Generated by Frama-C */
 enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
index e0b06bd1c0f3829ba53195545620d8f0f478680d..fa0bb669fc7a5d68255e8ce6fc8d1bd8aabd11f6 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/test_struct.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_struct_0.i (no preprocessing)
 /* Generated by Frama-C */
 struct People {
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/assigns.0.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/assigns.0.res.oracle
index 6e42468e3ad6fb56d5cfecda01abf90d858bcfe2..982103df2daf7ea1a089a36951f686d4c9a1ad59 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/assigns.0.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/assigns.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_assigns_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/assigns.1.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/assigns.1.res.oracle
index bfa57eb1f306974f472def9cf44e9cb20c224eb2..19922b414f8a559fe85fd825037f7154ba64f231 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/assigns.1.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/assigns.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_assigns_1.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/assigns.2.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/assigns.2.res.oracle
index f5a60a3aac12f9e6f74b645b97c97125445d9996..5a761e8ca86775a91718ded77e107d61a8a15aa6 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/assigns.2.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/assigns.2.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/assigns.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 /* Generated by Frama-C */
 int X;
 void f(void)
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/bts1289.0.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/bts1289.0.res.oracle
index 8a21ce6dc7cc4ae686a93943b42b1a52a4ecf689..9e49047ac776ff21695ad39cf63803a0e8c0aa67 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/bts1289.0.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/bts1289.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
 [kernel] Parsing TMPDIR/aorai_bts1289_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/bts1289.1.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/bts1289.1.res.oracle
index 7455ed9f29ad0d766b44878cabe2cf61ab7e0a98..09d835e87402e3767aef3dca97a0ef21ea085a87 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/bts1289.1.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/bts1289.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_bts1289_1.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
index e961cfa00b2c702983e5a54ba2f3c9f44d55d313..dda7d91ed57dc422451bd64176a91eecefad7558 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/declared_function.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_declared_function_0.i (no preprocessing)
 [kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0.i:48: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/deterministic.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/deterministic.res.oracle
index da8094d3368a5686310a2aff3d01b936866ceb30..8b53a748afa1149d700e7f74203ad0bb37c35a04 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/deterministic.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/deterministic.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_deterministic_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/formals.res.oracle
index 203e6f02f62136e70e652d204f160ecb34450cde..fbd3997a5e7e5d298aefcc9b3f03b2bbbd2b00ca 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/formals.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/formals.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_formals_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/generate_assigns_bts1290.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/generate_assigns_bts1290.res.oracle
index 8c689f78567e5268a9ff9b5e916b7ee948bb47ab..55b4a9433c8e88bcb17b22bb5bb7485f7747e270 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/generate_assigns_bts1290.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/generate_assigns_bts1290.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/generate_assigns_bts1290.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_generate_assigns_bts1290_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/hoare_seq.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/hoare_seq.res.oracle
index 25f11ffa4fd49a20ff9441ac586602ccffb8bfa8..5f917f2df5c7f9b6bb104d8d8afc525bce69d14e 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/hoare_seq.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/hoare_seq.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_hoare_seq_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
index 16d8f0409c53ff0280dd7978f240fe94cc7edda0..b8e7296acf003802517f2ff5211e7afc68b42a11 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/incorrect.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
 [kernel] Parsing TMPDIR/aorai_incorrect_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/loop_bts1050.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/loop_bts1050.res.oracle
index 8830b5bd606bd9d84295fe6287d86194126227e3..49b40bd6a118b65a30760349ede69b4d669ee30e 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/loop_bts1050.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/loop_bts1050.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_loop_bts1050_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-incompatible.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-incompatible.res.oracle
index 57c2d7eed1ca61046277d1cbf5d005a9fde10a52..a682bee8a270311ec22d7a3b33999a452ac306bf 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-incompatible.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-incompatible.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/metavariables-incompatible.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
-[aorai] User Error: The use of metavariables is incompatible with non-deterministic automata, such as automa using extended transitions.
+[aorai] User Error: The use of metavariables is incompatible with non-deterministic automata, such as automata using extended transitions.
 [kernel] Plug-in aorai aborted: invalid user input.
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-right.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-right.res.oracle
index 6803c149a7b942ab01ffcff164c2ae40bf6aca0d..54e1691625c95c6428570c38d5f776886b469f60 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-right.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/metavariables-right.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_metavariables-right_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-wrong.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-wrong.res.oracle
index 44c1487fcf7693e627a38f17cea95e7cd8e7b492..7aca51a51b2a805049c34693029c51f4dbd8a369 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-wrong.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-wrong.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/metavariables-wrong.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [aorai] User Error: The metavariables aorai_x may not be initialized before the transition from e to f_0:
   { (Call(h)) and ((aorai_x) > (0)) }
 [kernel] Plug-in aorai aborted: invalid user input.
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/not_prm.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/not_prm.res.oracle
index fd02e38e18a3bbf64d83f462bb12b7d3f1b5bc04..9921e92ae87197c4147f52ecfbff12b30d2fea70 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/not_prm.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/not_prm.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_not_prm_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/other.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/other.res.oracle
index 470d9d475b7189d3ad2178ee95013cc97bdc81f5..67ad5163c35ce47843920767d47f50ca90c19b6f 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/other.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/other.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/other.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_other_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/seq.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/seq.res.oracle
index 750146c1ae60528b0c2e8ad46caf226758da9106..7c0f0ef38ef39f16d8dd3704f753bea8042bf337 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/seq.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/seq.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_seq_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/seq_loop.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/seq_loop.res.oracle
index 37849cdec351ef0d0ac0a23bd999d16c95507974..aaa9705b556710ed07a4fa154c06b82d02874836 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/seq_loop.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/seq_loop.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_seq_loop_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
index 2572e58edadb63b68bd1688485edc30674b54cbd..cc4a6cd6b2b2590e30319455bebfe284661c82fc 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
@@ -1,8 +1,5 @@
 [kernel] Parsing tests/ya/serial.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/ya/serial.c:81: Warning: 
-  Calling undeclared function Frama_C_show_aorai_state. Old style K&R code?
-[aorai] Welcome to the Aorai plugin
-[kernel:annot:missing-spec] tests/ya/serial.c:45: Warning: 
+[kernel:annot:missing-spec] tests/ya/serial.c:43: Warning: 
   Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
@@ -21,28 +18,36 @@
   aorai_StatesHistory_1 ∈ {19}
   aorai_StatesHistory_2 ∈ {19}
 [eva] using specification for function Frama_C_interval
-[eva] tests/ya/serial.c:47: starting to merge loop iterations
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 100 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 300 states
-[aorai] tests/ya/serial.c:81: Wait1 <- Wait1 <- Complete
-[aorai] tests/ya/serial.c:81: Error <- Error <- Complete
-[aorai] tests/ya/serial.c:81: Complete <- Complete <- Complete
-[aorai] tests/ya/serial.c:81: Wait1 <- Wait1 <- Complete
-[aorai] tests/ya/serial.c:81: Error <- Error <- Complete
-[aorai] tests/ya/serial.c:81: Complete <- Complete <- Complete
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 500 states
-[eva:alarm] tests/ya/serial.c:54: Warning: 
+[eva] tests/ya/serial.c:45: starting to merge loop iterations
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 100 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 300 states
+[aorai] tests/ya/serial.c:79: Wait1 <- Wait1 <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
+[aorai] tests/ya/serial.c:79: Error <- Error <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
+[aorai] tests/ya/serial.c:79: Complete <- Complete <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
+[aorai] tests/ya/serial.c:79: Wait1 <- Wait1 <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
+[aorai] tests/ya/serial.c:79: Error <- Error <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
+[aorai] tests/ya/serial.c:79: Complete <- Complete <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 500 states
+[eva:alarm] tests/ya/serial.c:52: Warning: 
   accessing uninitialized left-value. assert \initialized(&status);
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 700 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 900 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1200 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1500 states
-[aorai] tests/ya/serial.c:81: Error <- Error <- Error
-[aorai] tests/ya/serial.c:81: Error <- Error <- Error
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1700 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1900 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 2000 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 2100 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 700 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 900 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1200 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1500 states
+[aorai] tests/ya/serial.c:79: Error <- Error <- Error
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
+[aorai] tests/ya/serial.c:79: Error <- Error <- Error
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1700 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1900 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 2000 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 2100 states
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function input_data_post_func:
@@ -299,7 +304,7 @@
   100% of the logical properties reached have been proven.
   ----------------------------------------------------------------------------
 [kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
-[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:176: Warning: 
+[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:174: Warning: 
   Calling undeclared function Frama_C_interval. Old style K&R code?
 [wp] Warning: Missing RTE guards
 [wp] Warning: No goal generated
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/single_call.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/single_call.res.oracle
index dbd60dc8fb54dbf01fb849c02ef8a49365e03b57..ecbefc2abff8eb03290a35b61fc23cd191fe0e48 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/single_call.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/single_call.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/single_call.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_single_call_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-right.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-right.res.oracle
index 79c1ae490e64e6a010e1842eec97bd6062a2cf0d..46c7832cef04833d9e3c5c2c7b367a8c4bf70d0c 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-right.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/singleassignment-right.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_singleassignment-right_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-wrong.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-wrong.res.oracle
index a24943fca9867c96902f607deaafe3a12f1a2e71..9eca9305b90905e2fe0c03ebb470b6b321956636 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-wrong.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-wrong.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/singleassignment-wrong.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [aorai] User Error: The metavariable aorai_x is assigned several times during the transition from a to b:
   { Call(main) } aorai_x <- x
                  aorai_x <- aorai_x + 1
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle
index ad8ddcef2ca5c41625a8a4dec207a6a71cdf6be6..e56f27fc2b989aca361e326f8f48dbf18daef36b 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/stack.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_stack_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle
index a20fbf3e28dfbe78c2e6e38549ae116e82d50117..0bf1b088bf5ade07b4cd849c3aec445cb17b41ef 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/test_acces_params.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_acces_params_0.i (no preprocessing)
 [wp] TMPDIR/aorai_test_acces_params_0.i:4: Warning: 
   Global invariant not handled yet ('inv' ignored)
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle
index c45f6f03706d1f2f3f8b0c0ea9771e9bca8aa970..82a83a9128b6065cf9c1cddf718442da4c93d7d1 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle
@@ -1,5 +1,4 @@
 [kernel] Parsing tests/ya/test_acces_params2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_acces_params2_0.i (no preprocessing)
 [wp] TMPDIR/aorai_test_acces_params2_0.i:3: Warning: 
   Global invariant not handled yet ('inv' ignored)
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
index d303821150962269a00d47dd2e504fcea9944db9..8cab8fa7b812e4fb8decee97420467e6fd790c5b 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
@@ -3,6 +3,5 @@
   parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
 [kernel] tests/ya/test_boucle_rechercheTableau.c:7: Warning: 
   parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_boucle_rechercheTableau_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_factorial.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_factorial.res.oracle
index 533a909e627c6e37bef7e29d3cf59dfd1a159e28..0a55ec0fe94f5ad8b0d702a2202938a4b848c915 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_factorial.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/test_factorial.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_factorial_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_recursion4.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_recursion4.res.oracle
index 5ca3ac392fdd4b832d8ddadfb0116c1e1e74530b..c87a3ebe4e904d75261e70724144576db3cd5b96 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_recursion4.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/test_recursion4.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_recursion4_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_recursion5.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_recursion5.res.oracle
index 6d11db5117d25a5e722e0f3d7601bd33b5908fe3..2cc98760865bd5e4cdda8a2f355a993384137333 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_recursion5.res.oracle
@@ -3,6 +3,5 @@
   parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
 [kernel] tests/ya/test_recursion5.c:28: Warning: 
   parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_recursion5_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_struct.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_struct.res.oracle
index fe4190800bde83f284a0788579d355d2a84ed468..4c72fb29ede0839691a5f3174338e5fc10fa2bb6 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_struct.res.oracle
@@ -1,4 +1,3 @@
 [kernel] Parsing tests/ya/test_struct.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
 [kernel] Parsing TMPDIR/aorai_test_struct_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/other.c b/src/plugins/aorai/tests/ya/other.c
index 4e13872dbf2b5ae2c6f44bb887577bfa91d3402e..c4977e2a37d1bd55cf58ded7ffe03019fe0d6f5e 100644
--- a/src/plugins/aorai/tests/ya/other.c
+++ b/src/plugins/aorai/tests/ya/other.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 int x=0;
diff --git a/src/plugins/aorai/tests/ya/seq.i b/src/plugins/aorai/tests/ya/seq.i
index f573a5491b319de72d6072634e78f3ebc33d5381..1ba54569e1265a39feb5116465e75c7547c1fb61 100644
--- a/src/plugins/aorai/tests/ya/seq.i
+++ b/src/plugins/aorai/tests/ya/seq.i
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
  */
 
 void f() { }
diff --git a/src/plugins/aorai/tests/ya/seq_loop.i b/src/plugins/aorai/tests/ya/seq_loop.i
index 07cc7cf2a9b9593684429bbd6d0a1950f97818c1..bee4d37d3cf6133cb65ca4bb52f1beb98e427bbb 100644
--- a/src/plugins/aorai/tests/ya/seq_loop.i
+++ b/src/plugins/aorai/tests/ya/seq_loop.i
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 void f() {}
diff --git a/src/plugins/aorai/tests/ya/serial.c b/src/plugins/aorai/tests/ya/serial.c
index 43d67d6540f64dea2e4b36b1dc03203095ec9694..8e9624c36c46c5f314a99566ccfdf8a968cf8046 100644
--- a/src/plugins/aorai/tests/ya/serial.c
+++ b/src/plugins/aorai/tests/ya/serial.c
@@ -1,5 +1,5 @@
 /* run.config*
-  OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ -aorai-no-acceptance -aorai-instrumentation-history 2 -aorai-no-generate-annotations -aorai-no-generate-deterministic-lemmas -then-last -eva -eva-partition-value n -eva-ilevel 256
+  OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ -aorai-no-acceptance -aorai-instrumentation-history 2 -aorai-no-generate-annotations -aorai-no-generate-deterministic-lemmas -then-last -eva -eva-partition-value n -eva-ilevel 256
 */
 
 #include "__fc_builtin.h"
diff --git a/src/plugins/aorai/tests/ya/single_call.i b/src/plugins/aorai/tests/ya/single_call.i
index 257ce2b2c7a4493ee42953dcff3b29bed8d29643..51abf5a7ef33870f78f6a029de9e3ebbb3330e69 100644
--- a/src/plugins/aorai/tests/ya/single_call.i
+++ b/src/plugins/aorai/tests/ya/single_call.i
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 int main () {}
diff --git a/src/plugins/aorai/tests/ya/singleassignment-right.i b/src/plugins/aorai/tests/ya/singleassignment-right.i
index 943c3e5e67cf9c02fde3be2c6dc73b2fbaa07b7d..4c5612f51075bcfe936814e8492beb88f67935c4 100644
--- a/src/plugins/aorai/tests/ya/singleassignment-right.i
+++ b/src/plugins/aorai/tests/ya/singleassignment-right.i
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 void main(int *x, int *y)
diff --git a/src/plugins/aorai/tests/ya/singleassignment-wrong.i b/src/plugins/aorai/tests/ya/singleassignment-wrong.i
index c983ce03e455dd3ac55c8baa1c76fc0785a8028f..4a88230c1c71bc1958ba3a68ca1a473d28633b66 100644
--- a/src/plugins/aorai/tests/ya/singleassignment-wrong.i
+++ b/src/plugins/aorai/tests/ya/singleassignment-wrong.i
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 int main(int x)
diff --git a/src/plugins/aorai/tests/ya/stack.i b/src/plugins/aorai/tests/ya/stack.i
index b3a734178295ace67bf450f577e757095db612b1..d911301c6860deccbbf88ee8e2cecaf097232e3a 100644
--- a/src/plugins/aorai/tests/ya/stack.i
+++ b/src/plugins/aorai/tests/ya/stack.i
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 
diff --git a/src/plugins/aorai/tests/ya/test_acces_params.c b/src/plugins/aorai/tests/ya/test_acces_params.c
index 884140ce9cab8b66952394937c1595f7a31dd37a..dc673f9bc593429faf4c8cadd396389fa5c115a7 100644
--- a/src/plugins/aorai/tests/ya/test_acces_params.c
+++ b/src/plugins/aorai/tests/ya/test_acces_params.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 int status=0;
diff --git a/src/plugins/aorai/tests/ya/test_acces_params2.c b/src/plugins/aorai/tests/ya/test_acces_params2.c
index 86092179e3f19e4041f7d3f3b5b2623d073edf51..7f25f23facbb6f7de9782534fb2dc42e0e0515f0 100644
--- a/src/plugins/aorai/tests/ya/test_acces_params2.c
+++ b/src/plugins/aorai/tests/ya/test_acces_params2.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 
diff --git a/src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c b/src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c
index 7dcf436cfe3bc7a95f03bb57faf63c8cca87b1b9..da220198440138b3924dddc99a92b9ea53794f5d 100644
--- a/src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c
+++ b/src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 
diff --git a/src/plugins/aorai/tests/ya/test_factorial.c b/src/plugins/aorai/tests/ya/test_factorial.c
index 9cb2213b68d6e23abeaed004b89d16e8b7a8d67e..fbb9762854cd43b3ef4c17245f2919486f58d4b8 100644
--- a/src/plugins/aorai/tests/ya/test_factorial.c
+++ b/src/plugins/aorai/tests/ya/test_factorial.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 
diff --git a/src/plugins/aorai/tests/ya/test_recursion4.c b/src/plugins/aorai/tests/ya/test_recursion4.c
index cf4c5d8523a6c123692f77b03bb2a129b9e3c20c..e88b8471fb74d57f267b879b89fe4b2c3bdc803a 100644
--- a/src/plugins/aorai/tests/ya/test_recursion4.c
+++ b/src/plugins/aorai/tests/ya/test_recursion4.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 # pragma JessieIntegerModel(math)
diff --git a/src/plugins/aorai/tests/ya/test_recursion5.c b/src/plugins/aorai/tests/ya/test_recursion5.c
index 241030e711241484c0f829e0a16101618649f832..0f902c0071f25495d236c849b770836a8b227ee4 100644
--- a/src/plugins/aorai/tests/ya/test_recursion5.c
+++ b/src/plugins/aorai/tests/ya/test_recursion5.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 
diff --git a/src/plugins/aorai/tests/ya/test_struct.c b/src/plugins/aorai/tests/ya/test_struct.c
index 1b8ff3ec2ff039f6a94506b149db7d128961e656..d94c75970eb6a1897bc2cb560147174f73452bf3 100644
--- a/src/plugins/aorai/tests/ya/test_struct.c
+++ b/src/plugins/aorai/tests/ya/test_struct.c
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
 */
 
 struct People{