micro cleanup

src/jimplefront/jstar.ml

@@ -136,14 +136,12 @@ let make_logic_for_one_program spec_list logic program =
        (*let _ = Prover.pprint_sequent_rules logic in*)
        (* End of axioms clause treatment *)
 
-
 let main () =
   let usage_msg =
     Printf.sprintf "usage: %s [options] <jimple_programs>" Sys.argv.(0) in
   Arg.parse arg_list set_file usage_msg;
   if !Config.verbosity >= 2 then
     printf "@[Files to analyze: %a@." (pp_list_sep " " pp_string) !jimple_files;
-
   prof_phase "parse_program jimple";
   let programs = List.map parse_program !jimple_files in
   prof_phase "preprocess_jimple";

src/topl/toplSpecs.ml

@@ -267,7 +267,7 @@ let pDeQu n pv el =
 let pDeQu_modifies n pv el =
   var_of_term pv.size :: logical_deque_modifies pv.queue el n
 
-(* The last argument is the previous vertex. It is used in irder to decide whether the
+(* The last argument is the previous vertex. It is used in order to decide whether the
    transition modifies pv.state *)
 let trans_pre_and_post pv el l_sr0 v j t =
    let st = t.TM.steps in
@@ -329,7 +329,10 @@ let get_specs_for_vertex t pv v s =
     ( fun k ->
       let pSats = ListH.mapi (fun i (x,y) -> if IntSet.mem i k then x else y)
         (List.combine pAllSats pAllSats_neg) in
-      let pre = Expr.mk_big_star ( pAt :: pInit @ pQud @ pSats ) |> Prover.normalize in
+      let pre = Expr.mk_big_star ( pAt :: pInit @ pQud @ pSats ) in
+(*      (* debug *) Format.printf "@\npre for {%a} before normalization:@,%a" (pp_list (fun f -> Format.fprintf f "%d")) (IntSet.elements k) Expr.pp pre; *)
+      let pre = Prover.normalize pre in
+(*      (* debug *) Format.printf "@\npre after normalization:@,%a" Expr.pp pre; *)
       let post = Expr.mk_big_or (select_subset k pAllPosts) |> Prover.normalize in
       let modifies = List.concat (select_subset k allModifies) in
       { Core.pre; post; modifies }) subs in