Commenting out unused variables

src/tools/seal/seal_extract.ml

@@ -1117,7 +1117,7 @@ let node_as_switched_sys consts (mems:var_decl list) nd =
            
       in
       check_dup_up [] sw_sys;
-      let sw_sys =
+      let _ (* sw_sys *) =
         List.sort (fun (gl1, _) (gl2, _) ->
             let glid gl = List.map (fun (e,_) -> e.expr_tag) gl in
             

src/tools/zustre/zustre_cex.ml

@@ -153,7 +153,7 @@ let build_cex machine machines decl_err =
   (*   if !debug then *)
   (*     Format.eprintf "FP help: %s@." (Z3.Fixedpoint.get_help !fp); *)
 
-  let stats_entries =   Z3.Statistics.get_entries stats in
+  (*  let _ (*stats_entries*) =   Z3.Statistics.get_entries stats in *)
   (* List.iter (fun e -> Format.eprintf "%s@.@?" *)
   (*   (Z3.Statistics.Entry.to_string e) *)
     

src/tools/zustre/zustre_common.ml

@@ -650,7 +650,8 @@ let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.e
     List.fold_left (fun (instrs, resets) b ->
       let b_instrs, b_resets = branch_to_expr b in
       instrs@b_instrs, resets@b_resets 
-    ) ([], reset_instances) hl 
+      ) ([], reset_instances) hl
+  | MSpec _ -> assert false
 
 and instrs_to_expr machines reset_instances m instrs = 
   let instr_to_exprs rs i = instr_to_exprs machines rs m i in
@@ -728,10 +729,11 @@ let add_rule ?(dont_touch=[]) vars  expr =
 	(fun accu e ->  FDSet.union accu (get_expr_vars e))
 	FDSet.empty (Z3.Expr.get_args e)
   in
+  (* Unsed variable. Coul;d be reintroduced 
   let extracted_vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in
   let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in
   let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in
-
+   *)
   if !debug then (
     Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @."
       (Z3.Expr.to_string expr)
@@ -939,7 +941,7 @@ let decl_machine machines m =
 
 
 (* Debug functions *)
-
+(*
 let rec extract_expr_fds e =
   (* Format.eprintf "@[<v 2>Extracting fundecls from expr %s@ " *)
   (*   (Z3.Expr.to_string e); *)
@@ -984,7 +986,7 @@ let rec extract_expr_fds e =
   in
   (* Format.eprintf "@]@ " *)
   ()      
-
+ *)
 (* Local Variables: *)
 (* compile-command:"make -C ../.." *)
 (* End: *)

src/tools/zustre/zustre_verifier.ml

@@ -167,7 +167,7 @@ module Verifier =
       (* TODO
 	 load deps: cf print_dep in horn_backend.ml
 
-      *)
+      
       if false then (
 	
 	let queries = Z3.Fixedpoint.parse_file !fp "nstep.smt2" in
@@ -232,7 +232,11 @@ module Verifier =
 
 	()	
       )
-      else (
+      else 
+
+       *)
+
+      (
 	
 	
 	decl_sorts ();