diff --git a/src/backend/dot.ml b/src/backend/dot.ml
index c9135a96..93981958 100644
--- a/src/backend/dot.ml
+++ b/src/backend/dot.ml
@@ -122,7 +122,7 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
     | S.Duplicate (p, l) ->
       print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Duplicate" "GREY"
         ((fun fmt () -> (Format.fprintf fmt "%s" (node_id n))) ::
-        List.map (ttify A.print_atom) l);
+         List.map (ttify A.print_atom) l);
       print_edge fmt (node_id n) (node_id (S.expand p))
     | S.Resolution (_, _, a) ->
       print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Resolution" "GREY"
diff --git a/src/core/formula_intf.ml b/src/core/formula_intf.ml
index 61e824dc..fe45e908 100644
--- a/src/core/formula_intf.ml
+++ b/src/core/formula_intf.ml
@@ -29,8 +29,8 @@ module type S = sig
   (** Equality over formulas. *)
 
   val hash : t -> int
-    (** Hashing function for formulas. Should be such that two formulas equal according
-        to {!val:Expr_intf.S.equal} have the same hash. *)
+  (** Hashing function for formulas. Should be such that two formulas equal according
+      to {!val:Expr_intf.S.equal} have the same hash. *)
 
   val print : Format.formatter -> t -> unit
   (** Printing function used among other thing for debugging.  *)
diff --git a/src/core/internal.ml b/src/core/internal.ml
index 916ba91a..d559fd88 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -80,7 +80,7 @@ module Make
        - this is repeated until a fixpoint is reached;
        - before a decision (and after the fixpoint),
          th_head = elt_head = length elt_queue
-      *)
+    *)
 
 
     mutable simpDB_props : int;
@@ -211,12 +211,12 @@ module Make
     let res = add_atom f in
     if St.mcsat then
       begin match res.var.v_assignable with
-      | Some _ -> ()
-      | None ->
-        let l = ref [] in
-        Plugin.iter_assignable (fun t -> l := add_term t :: !l) res.var.pa.lit;
-        res.var.v_assignable <- Some !l;
-    end;
+        | Some _ -> ()
+        | None ->
+          let l = ref [] in
+          Plugin.iter_assignable (fun t -> l := add_term t :: !l) res.var.pa.lit;
+          res.var.v_assignable <- Some !l;
+      end;
     res
 
   (* Variable and literal activity.
@@ -233,8 +233,8 @@ module Make
       Iheap.insert f_weight env.order v.vid;
       insert_subterms_order v
 
-    and insert_subterms_order v =
-      iter_sub (fun t -> insert_var_order (elt_of_lit t)) v
+  and insert_subterms_order v =
+    iter_sub (fun t -> insert_var_order (elt_of_lit t)) v
 
   (* Add new litterals/atoms on which to decide on, even if there is no
      clause that constrains it.
@@ -329,8 +329,8 @@ module Make
       ) clause.atoms;
     List.iter (fun a ->
         begin match a.var.seen with
-        | Both -> trivial := true
-        | _ -> ()
+          | Both -> trivial := true
+          | _ -> ()
         end;
         clear a.var) !res;
     if !trivial then
@@ -504,7 +504,7 @@ module Make
             let c' = make_clause (fresh_lname ()) l (History (cl :: history)) in
             Log.debugf debug "Simplified reason: @[<v>%a@,%a@]"
               (fun k -> k St.pp_clause cl St.pp_clause c');
-              Bcp c'
+            Bcp c'
           end
         | _ ->
           Log.debugf error "@[<v 2>Failed at reason simplification:@,%a@,%a@]"
@@ -759,9 +759,9 @@ module Make
   (* Get the correct vector to insert a clause in. *)
   let clause_vector c =
     match c.cpremise with
-      | Hyp -> env.clauses_hyps
-      | Local -> env.clauses_temp
-      | Lemma _ | History _ -> env.clauses_learnt
+    | Hyp -> env.clauses_hyps
+    | Local -> env.clauses_temp
+    | Lemma _ | History _ -> env.clauses_learnt
 
   (* Add a new clause, simplifying, propagating, and backtracking if
      the clause is false in the current trail *)
diff --git a/src/core/plugin_intf.ml b/src/core/plugin_intf.ml
index 60b546ac..c4dd3839 100644
--- a/src/core/plugin_intf.ml
+++ b/src/core/plugin_intf.ml
@@ -28,7 +28,7 @@ type 'term eval_res =
   | Valued of bool * ('term list) (** The given formula can be evaluated to the given bool.
                                       The list of terms to give is the list of terms that
                                       were effectively used for the evaluation.
-                                      *)
+                                  *)
 (** The type of evaluation results for a given formula.
     For instance, let's suppose we want to evaluate the formula [x * y = 0], the
     following result are correct:
@@ -36,15 +36,15 @@ type 'term eval_res =
     - [Valued (true, [x])] if [x] is assigned to [0]
     - [Valued (true, [y])] if [y] is assigned to [0]
     - [Valued (false, [x; y])] if [x] and [y] are assigned to 1 (or any non-zero number)
-  *)
+*)
 
 type ('formula, 'proof) res =
   | Sat
-    (** The current set of assumptions is satisfiable. *)
+  (** The current set of assumptions is satisfiable. *)
   | Unsat of 'formula list * 'proof
-    (** The current set of assumptions is *NOT* satisfiable, and here is a
-        theory tautology (with its proof), for which every litteral is false
-        under the current assumptions. *)
+  (** The current set of assumptions is *NOT* satisfiable, and here is a
+      theory tautology (with its proof), for which every litteral is false
+      under the current assumptions. *)
 (** Type returned by the theory. Formulas in the unsat clause must come from the
     current set of assumptions, i.e must have been encountered in a slice. *)
 
diff --git a/src/core/res_intf.ml b/src/core/res_intf.ml
index 3ac445dd..72eb12fe 100644
--- a/src/core/res_intf.ml
+++ b/src/core/res_intf.ml
@@ -32,17 +32,17 @@ module type S = sig
   (** A proof can be expanded into a proof node, which show the first step of the proof. *)
   and step =
     | Hypothesis
-      (** The conclusion is a user-provided hypothesis *)
+    (** The conclusion is a user-provided hypothesis *)
     | Assumption
-      (** The conclusion has been locally assumed by the user *)
+    (** The conclusion has been locally assumed by the user *)
     | Lemma of lemma
     (** The conclusion is a tautology provided by the theory, with associated proof *)
     | Duplicate of proof * atom list
     (** The conclusion is obtained by eliminating multiple occurences of the atom in
         the conclusion of the provided proof. *)
     | Resolution of proof * proof * atom
-      (** The conclusion can be deduced by performing a resolution between the conclusions
-          of the two given proofs. The atom on which to perform the resolution is also given. *)
+    (** The conclusion can be deduced by performing a resolution between the conclusions
+        of the two given proofs. The atom on which to perform the resolution is also given. *)
   (** The type of reasoning steps allowed in a proof. *)
 
 
diff --git a/src/core/solver_types.ml b/src/core/solver_types.ml
index 6055b05a..1edbfbd3 100644
--- a/src/core/solver_types.ml
+++ b/src/core/solver_types.ml
@@ -196,8 +196,8 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
   let add_atom lit =
     let var, negated = make_boolean_var lit in
     match negated with
-      | Formula_intf.Negated -> var.na
-      | Formula_intf.Same_sign -> var.pa
+    | Formula_intf.Negated -> var.na
+    | Formula_intf.Same_sign -> var.pa
 
   let make_clause ?tag name ali premise =
     let atoms = Array.of_list ali in
diff --git a/src/core/theory_intf.ml b/src/core/theory_intf.ml
index 07fbc769..b465f4c9 100644
--- a/src/core/theory_intf.ml
+++ b/src/core/theory_intf.ml
@@ -25,11 +25,11 @@ Copyright 2016 Simon Cruanes
 
 type ('formula, 'proof) res = ('formula, 'proof) Plugin_intf.res =
   | Sat
-    (** The current set of assumptions is satisfiable. *)
+  (** The current set of assumptions is satisfiable. *)
   | Unsat of 'formula list * 'proof
-    (** The current set of assumptions is *NOT* satisfiable, and here is a
-        theory tautology (with its proof), for which every litteral is false
-        under the current assumptions. *)
+  (** The current set of assumptions is *NOT* satisfiable, and here is a
+      theory tautology (with its proof), for which every litteral is false
+      under the current assumptions. *)
 (** Type returned by the theory. Formulas in the unsat clause must come from the
     current set of assumptions, i.e must have been encountered in a slice. *)
 
@@ -42,9 +42,9 @@ type ('form, 'proof) slice = {
   push : 'form list -> 'proof -> unit;  (** Allows to add to the solver a clause. *)
   propagate : 'form -> 'form list -> 'proof -> unit;
   (** [propagate lit causes proof] informs the solver to propagate [lit], with the reason
-    that the clause [causes => lit] is a theory tautology. It is faster than pushing
-    the associated clause but the clause will not be remembered by the sat solver,
-    i.e it will not be used by the solver to do boolean propagation. *)
+      that the clause [causes => lit] is a theory tautology. It is faster than pushing
+      the associated clause but the clause will not be remembered by the sat solver,
+      i.e it will not be used by the solver to do boolean propagation. *)
 }
 (** The type for a slice. Slices are some kind of view of the current
     propagation queue. They allow to look at the propagated literals,
diff --git a/src/smt/expr_smt.ml b/src/smt/expr_smt.ml
index 5fb8acfe..53beee62 100644
--- a/src/smt/expr_smt.ml
+++ b/src/smt/expr_smt.ml
@@ -66,10 +66,10 @@ let rec list_cmp ord l1 l2 =
   | [], _ -> -1
   | _, [] -> 1
   | x1::l1', x2::l2' ->
-      let c = ord x1 x2 in
-      if c = 0
-        then list_cmp ord l1' l2'
-        else c
+    let c = ord x1 x2 in
+    if c = 0
+    then list_cmp ord l1' l2'
+    else c
 
 (* Exceptions *)
 (* ************************************************************************ *)
diff --git a/src/solver/solver.ml b/src/solver/solver.ml
index 8dfe2409..eee3afba 100644
--- a/src/solver/solver.ml
+++ b/src/solver/solver.ml
@@ -50,12 +50,12 @@ module Plugin(E : Formula_intf.S)
       propagate f (Plugin_intf.Consequence (l, proof))
 
   let mk_slice s = {
-      Theory_intf.start = s.Plugin_intf.start;
-      length = s.Plugin_intf.length;
-      get = assume_get s.Plugin_intf.get;
-      push = s.Plugin_intf.push;
-      propagate = assume_propagate s.Plugin_intf.propagate;
-    }
+    Theory_intf.start = s.Plugin_intf.start;
+    length = s.Plugin_intf.length;
+    get = assume_get s.Plugin_intf.get;
+    push = s.Plugin_intf.push;
+    propagate = assume_propagate s.Plugin_intf.propagate;
+  }
 
   let assume s = Th.assume (mk_slice s)
 
diff --git a/src/util/log_real.ml b/src/util/log_real.ml
index 3c0e4878..8ab71503 100644
--- a/src/util/log_real.ml
+++ b/src/util/log_real.ml
@@ -18,7 +18,7 @@ let debugf l format k =
   if l <= !debug_level_
   then
     k (Format.kfprintf
-        (fun fmt -> Format.fprintf fmt "@]@.")
-        !debug_fmt_ format)
+         (fun fmt -> Format.fprintf fmt "@]@.")
+         !debug_fmt_ format)
 
 let debug l msg = debugf l "%s" (fun k->k msg)
diff --git a/src/util/vec.ml b/src/util/vec.ml
index b3b248f6..8a3c82b5 100644
--- a/src/util/vec.ml
+++ b/src/util/vec.ml
@@ -164,8 +164,8 @@ let print ?(sep=", ") pp out v =
   let first = ref true in
   iter
     (fun x ->
-      if !first then first := false else Format.fprintf out "%s@," sep;
-      pp out x)
+       if !first then first := false else Format.fprintf out "%s@," sep;
+       pp out x)
     v
 
 (*