diff --git a/src/tools/tiny/tiny_utils.ml b/src/tools/tiny/tiny_utils.ml
index c5b3730d59d0233b846616c91c2dc272cdaba981..4f34a89caa67b32adb30f46c74d9815f11927e02 100644
--- a/src/tools/tiny/tiny_utils.ml
+++ b/src/tools/tiny/tiny_utils.ml
@@ -1,4 +1,6 @@
+let report = Log.report ~plugin:"tiny"
 
+           
 module Ast = Tiny.Ast
 
 let gen_loc () = Tiny.Location.dummy ()
@@ -163,8 +165,14 @@ let machine_body_to_ast init m =
                                 over-approximate behavior *)
        in
        if (match init_var, te.Ast.expr_desc with
-           | Some v, Var v2 -> Format.eprintf "Building init (possibly if %b)@." (v=v2); v = v2
-           | _ -> Format.eprintf "Building if init def? %b @." (match init_var with None -> false | _ -> true); false) then 
+           | Some v, Var v2 ->
+              (* Format.eprintf "Building init (possibly if %b)@." (v=v2);  *)v = v2
+           | _ ->
+              (* Format.eprintf "Building if init def? %b @." (match init_var with None -> false | _ -> true);
+               *)
+              false
+          )
+       then 
          instrl_to_stm (
              if init then
                (List.assoc "true" guarded_instrs)
@@ -267,11 +275,11 @@ let machine_to_ast bounds_input m =
   
 let machine_to_env m =
   List.fold_left (fun accu v ->
-      Format.eprintf "Adding variable %a to env@." Printers.pp_var v;
+      report ~level:3 (fun fmt -> Format.fprintf fmt "Adding variable %a to env@." Printers.pp_var v);
       let typ =
         ltyp_to_ttyp (v.Lustre_types.var_type)
       in
-      Ast.VarSet.add (v.var_id, typ) accu)
-    Ast.VarSet.empty
+      Ast.Var.Set.add (v.var_id, typ) accu)
+    Ast.Var.Set.empty
     (Machine_code_common.machine_vars m)
 
diff --git a/src/tools/tiny/tiny_verifier.ml b/src/tools/tiny/tiny_verifier.ml
index 66b3a535e381155b6e3537a2f3e0b73e7f5e1f7c..f590d0a21c9c63ed54e6bb581281c306f9bebd27 100644
--- a/src/tools/tiny/tiny_verifier.ml
+++ b/src/tools/tiny/tiny_verifier.ml
@@ -8,7 +8,8 @@ let output = ref false
 
               
 let quiet () = Tiny.Report.verbosity := 0
-             
+let report = Tiny_utils.report
+               
 let print_tiny_help () =
   let open Format in
   Format.eprintf "@[Tiny verifier plugin produces a simple imperative code \
@@ -57,16 +58,16 @@ let tiny_run ~basename prog machines =
   let mems = m.mmemory in
   if !output then (
     let destname = !Options.dest_dir ^ "/" ^ basename ^ "_" ^ node_name ^ ".tiny" in
-    Log.report ~plugin:"tiny" ~level:1 (fun fmt -> Format.fprintf fmt "Exporting resulting tiny source as %s@ " destname);
+    report ~level:2 (fun fmt -> Format.fprintf fmt "Exporting resulting tiny source as %s@ " destname);
     let out = open_out destname in
     let fmt = Format.formatter_of_out_channel out in
-    Format.fprintf fmt "%a@." Tiny.Ast.VarSet.pp env; 
+    Format.fprintf fmt "%a@." Tiny.Ast.Var.Set.pp env; 
     Format.fprintf fmt "%a@." Tiny.Ast.fprint_stm ast; 
     close_out out;
   
   
   );
-  Format.printf "%a@." Tiny.Ast.fprint_stm ast; 
+  report ~level:1 (fun fmt -> Format.fprintf fmt "%a@." Tiny.Ast.fprint_stm ast); 
   
   let dom =
      let open Tiny.Load_domains in
@@ -78,7 +79,8 @@ let tiny_run ~basename prog machines =
    let module PrintResults = Tiny.PrintResults.Make (Dom) in
    let m = Results.results in
    (* if !Tiny.Report.verbosity > 1 then *)
-   PrintResults.print m env ast None (* no !output_file *);
+   report ~level:1 (PrintResults.print m env ast)
+   (* no !output_file *);
         (* else PrintResults.print_invariants m ast !output_file *)
 
    ()