Style

src/bin/common/solving_loop.ml

@@ -1389,14 +1389,15 @@ let main () =
             aux named_map st tl
           | {contents = `Pop n; _} ->
             let pushed_paths = get_pushed_paths st in
-            Format.eprintf "Vec size: %i@." pushed_paths.sz;
             let rec pop_until until res =
-              if until = 0 then res else pop_until (until - 1) (Vec.pop pushed_paths)
+              if until = 0 then
+                res
+              else
+                pop_until (until - 1) (Vec.pop pushed_paths)
             in
             let prefix = pop_until (n - 1) (Vec.pop pushed_paths) in
             let st = handle_reset st in
             let whole_path = List.rev_append prefix tl in
-            Format.eprintf "Restarting with %i instructions@." (List.length whole_path);
             aux Util.MS.empty st whole_path
           | {contents; _ } ->
             let st =

src/lib/frontend/d_cnf.ml

@@ -213,7 +213,9 @@ let builtin_enum = function
     let add_cstrs map =
       List.fold_left (fun map ((c : DE.term_cst), _) ->
           let name = get_basename c.path in
-          DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } (fun env _ ->
+          DStd.Id.Map.add
+            { name = DStd.Name.simple name; ns = Term }
+            (fun env _ ->
               builtin_term @@
               Dolmen_type.Base.term_app_cst
                 (module Dl.Typer.T) env c) map)
@@ -239,7 +241,7 @@ module Const = struct
         let name = "bv2nat" in
         Id.mk ~name ~builtin:(BV2Nat n)
           (DStd.Path.global name) Ty.(arrow [bitv n] int))
-  
+
   let int2bv =
     with_cache (fun n ->
         let name = "int2bv" in

src/lib/frontend/d_cnf.mli

@@ -99,7 +99,8 @@ val pp_query :
 (** Registers the declarations in the cache. If there are more than one element
     in the list, it is assumed they are mutually recursive (but if it is not the
     case, it still work). *)
-val make_decls : D_loop.Typer_Pipe.decl list -> (Hstring.t * Ty.t list * Ty.t) list
+val make_decls :
+  D_loop.Typer_Pipe.decl list -> (Hstring.t * Ty.t list * Ty.t) list
 
 val builtins :
   Dolmen_loop.State.t ->