diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml
index 0ab123aa8..459e44efd 100644
--- a/infer/src/pulse/PulseExecutionDomain.ml
+++ b/infer/src/pulse/PulseExecutionDomain.ml
@@ -7,6 +7,7 @@
 
 open! IStd
 module F = Format
+module L = Logging
 module AbductiveDomain = PulseAbductiveDomain
 
 type t =
@@ -48,7 +49,8 @@ let map ~f exec_state =
 
 
 let of_posts pdesc posts =
-  List.filter_map posts ~f:(fun exec_state ->
+  List.filter_mapi posts ~f:(fun i exec_state ->
       let (AbortProgram astate | ContinueProgram astate | ExitProgram astate) = exec_state in
+      L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ;
       if PulseArithmetic.is_unsat_expensive astate then None
       else Some (map exec_state ~f:(AbductiveDomain.of_post pdesc)) )
diff --git a/infer/src/pulse/PulseSummary.ml b/infer/src/pulse/PulseSummary.ml
index ee933d5c2..bfd6032a6 100644
--- a/infer/src/pulse/PulseSummary.ml
+++ b/infer/src/pulse/PulseSummary.ml
@@ -11,11 +11,15 @@ open PulseDomainInterface
 
 type t = ExecutionDomain.t list
 
-let of_posts pdesc posts = ExecutionDomain.of_posts pdesc posts
-
 let pp fmt summary =
   F.open_vbox 0 ;
   F.fprintf fmt "%d pre/post(s)@;" (List.length summary) ;
   List.iteri summary ~f:(fun i pre_post ->
       F.fprintf fmt "#%d: @[%a@]@;" i ExecutionDomain.pp pre_post ) ;
   F.close_box ()
+
+
+let of_posts pdesc posts =
+  AnalysisCallbacks.html_debug_new_node_session (Procdesc.get_exit_node pdesc)
+    ~pp_name:(fun fmt -> F.pp_print_string fmt "pulse summary creation")
+    ~f:(fun () -> ExecutionDomain.of_posts pdesc posts)