lutin --oracle-ec: Kill the ecexe process when the oracle return false.

source/Lutin/main.ml

@@ -128,7 +128,7 @@ let cov  = ref dummy_cov (* a dummy cov instead of an option type
 let check_oracle inputs outputs t = (
   match MainArg.oracle () with
     | MainArg.NoOracle -> ()
-    | MainArg.Oracle(in_decl, _, _,step_oracle) -> 
+    | MainArg.Oracle(in_decl, _, kill_oracle, step_oracle) -> 
         let all_vals = Value.OfIdent.union inputs outputs in
         let oracle_inputs = 
           List.map
@@ -143,6 +143,7 @@ let check_oracle inputs outputs t = (
                 let msg = Coverage.dump_oracle_io oracle_inputs tail !cov in
                 Printf.printf "# The oracle returned false at step %i\n" t;
                 Printf.eprintf "The oracle returned false at step %i\n%s" t msg;
+                kill_oracle();
                 flush stderr;
                 flush stdout;
                 exit 2

source/common/lustreRun.ml

@@ -29,12 +29,16 @@ let (make_ec : string -> vars * vars * (unit -> unit) *
             Printf.eprintf "*** Error when creating process with %s: %s\n" prog msg;
             exit 2
     in
+    let _ = Printf.eprintf "Process %d (ecexe) created\n" pid_oracle in
     let kill () =
       Unix.close oracle_stdin_in;
       Unix.close oracle_stdin_out;
       Unix.close oracle_stdout_in;
       Unix.close oracle_stdout_out;
-      (try Unix.kill pid_oracle Sys.sigkill with _ -> () )
+      (try 
+         Printf.eprintf "Killing process %d\n" pid_oracle;
+         Unix.kill pid_oracle Sys.sigkill 
+       with e -> (Printf.printf "Killing of ecexe process failed: %s\n" (Printexc.to_string e) ))
     in
     let step sl =
       let in_vals_str =