diff --git a/src/symbolic_choice.ml b/src/symbolic_choice.ml
index e799358..534a023 100644
--- a/src/symbolic_choice.ml
+++ b/src/symbolic_choice.ml
@@ -19,7 +19,10 @@ let check sym_bool thread (S (solver_module, solver)) =
   | _ ->
     let check = no :: pc in
     let module Solver = (val solver_module) in
+
     let r = Solver.check solver check in
+        Solver.pp_statistics Stdlib.Format.std_formatter solver;
+        Stdlib.Format.pp_print_flush Stdlib.Format.std_formatter ();
     not r
 
 let list_select b ({ Thread.pc; _ } as thread) (S (solver_module, s)) =
@@ -34,6 +37,9 @@ let list_select b ({ Thread.pc; _ } as thread) (S (solver_module, s)) =
     let with_not_v = Bool.not v :: pc in
     let sat_true = Solver.check s with_v in
     let sat_false = Solver.check s with_not_v in
+
+        Solver.pp_statistics Stdlib.Format.std_formatter s;
+        Stdlib.Format.pp_print_flush Stdlib.Format.std_formatter ();
     match (sat_true, sat_false) with
     | false, false -> []
     | true, false | false, true -> [ (sat_true, thread) ]
@@ -78,6 +84,8 @@ let list_select_i32 sym_int thread (S (solver_module, solver)) =
       if not (Solver.check solver (additionnal @ pc)) then []
       else begin
         let model = Solver.model ~symbols:[ symbol ] solver in
+        Solver.pp_statistics Stdlib.Format.std_formatter solver;
+        Stdlib.Format.pp_print_flush Stdlib.Format.std_formatter ();
         match model with
         | None -> assert false (* ? *)
         | Some model -> (