From bd9d13279ad65773158741f26ce5b134e6d4813e Mon Sep 17 00:00:00 2001
From: martin-neuhaeusser <martin.neuhaeusser@siemens.com>
Date: Wed, 6 Apr 2016 12:39:19 +0200
Subject: [PATCH] Pretty printing

---
 src/api/ml/z3.ml  | 14 +++++++-------
 src/api/ml/z3.mli | 12 ++++++------
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 60d83dd86..3a797e5d8 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -679,13 +679,13 @@ struct
       | _ ->
         let nopatterns_arr = Array.of_list nopatterns in
         Z3native.mk_quantifier_ex ctx universal
-        (match weight with | None -> 1 | Some x -> x)
-        (match quantifier_id with | None -> Z3native.mk_null_symbol ctx | Some x -> x)
-        (match skolem_id with | None -> Z3native.mk_null_symbol ctx | Some x -> x)
-        (Array.length patterns_arr) patterns_arr
-        (Array.length nopatterns_arr) nopatterns_arr
-        (Array.length sorts_arr) sorts_arr
-        names_arr body
+          (match weight with | None -> 1 | Some x -> x)
+          (match quantifier_id with | None -> Z3native.mk_null_symbol ctx | Some x -> x)
+          (match skolem_id with | None -> Z3native.mk_null_symbol ctx | Some x -> x)
+          (Array.length patterns_arr) patterns_arr
+          (Array.length nopatterns_arr) nopatterns_arr
+          (Array.length sorts_arr) sorts_arr
+          names_arr body
 
   let _internal_mk_quantifier_const ~universal ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id =
     let patterns_arr = Array.of_list patterns in
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 02d6a8b2a..9104b3080 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -285,7 +285,7 @@ sig
   sig
     (** Parameters of func_decls *)
     type parameter =
-                P_Int of int
+        P_Int of int
       | P_Dbl of float
       | P_Sym of Symbol.symbol
       | P_Srt of Sort.sort
@@ -3232,21 +3232,21 @@ sig
   val add : optimize -> Expr.expr list -> unit
 
   (** Asssert a soft constraint.
-     Supply integer weight and string that identifies a group
+      Supply integer weight and string that identifies a group
       of soft constraints.
-   *)
+  *)
   val add_soft : optimize -> Expr.expr -> string -> Symbol.symbol -> handle
 
   (** Add maximization objective.
-   *)
+  *)
   val maximize : optimize -> Expr.expr -> handle
 
   (** Add minimization objective.
-   *)
+  *)
   val minimize : optimize -> Expr.expr -> handle
 
   (** Checks whether the assertions in the context are satisfiable and solves objectives.
-   *)
+  *)
   val check : optimize -> Solver.status
 
   (** Retrieve model from satisfiable context *)