diff --git a/src/arith/lra/sidekick_arith_lra.ml b/src/arith/lra/sidekick_arith_lra.ml
index 2cfc6a6e..8d1d823f 100644
--- a/src/arith/lra/sidekick_arith_lra.ml
+++ b/src/arith/lra/sidekick_arith_lra.ml
@@ -368,7 +368,8 @@ module Make(A : ARG) : S with module A = A = struct
            end)
     end;
     Log.debug 5 "lra: call arith solver";
-    begin match SimpSolver.solve simplex with
+    let res = Profile.with1 "simplex.solve" SimpSolver.solve simplex in
+    begin match res with
       | SimpSolver.Solution _m ->
         Log.debug 5 "lra: solver returns SAT";
         Log.debugf 50
diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml
index 9ae61c09..47c421a5 100644
--- a/src/cc/Sidekick_cc.ml
+++ b/src/cc/Sidekick_cc.ml
@@ -373,6 +373,7 @@ module Make (A: CC_ARG)
     end
 
   let raise_conflict (cc:t) ~th (acts:actions) (e:lit list) : _ =
+    Profile.instant "cc.conflict";
     (* clear tasks queue *)
     Vec.clear cc.pending;
     Vec.clear cc.combine;
diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml
index 5c7ffc3e..5dc47f53 100644
--- a/src/msat-solver/Sidekick_msat_solver.ml
+++ b/src/msat-solver/Sidekick_msat_solver.ml
@@ -353,10 +353,12 @@ module Make(A : ARG)
 
     (* propagation from the bool solver *)
     let check_ ~final (self:t) (acts: msat_acts) =
+      let pb = if final then Profile.begin_ "solver.final-check" else Profile.null_probe in
       let iter = iter_atoms_ acts in
       Msat.Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter));
       self.on_progress();
-      assert_lits_ ~final self acts iter
+      assert_lits_ ~final self acts iter;
+      Profile.exit pb
 
     (* propagation from the bool solver *)
     let[@inline] partial_check (self:t) (acts:_ Msat.acts) : unit =
diff --git a/src/tef/Sidekick_tef.ml b/src/tef/Sidekick_tef.ml
index d7443323..5b7467b1 100644
--- a/src/tef/Sidekick_tef.ml
+++ b/src/tef/Sidekick_tef.ml
@@ -34,20 +34,32 @@ module Make()
     let now = Mtime_clock.now() in
     Mtime.Span.to_us (Mtime.span program_start now)
 
-  let emit_event ~name ~start ~end_ () : unit =
-    let dur = end_ -. start in
-    let ts = start in
-    let pid = Unix.getpid() in
-    let tid = Thread.id (Thread.self()) in
+  let emit_sep_ () =
     if !first_ then (
       first_ := false;
     ) else (
       output_string oc ",\n";
-    );
+    )
+
+  let emit_duration_event ~name ~start ~end_ () : unit =
+    let dur = end_ -. start in
+    let ts = start in
+    let pid = Unix.getpid() in
+    let tid = Thread.id (Thread.self()) in
+    emit_sep_();
     Printf.fprintf oc
       {json|{"pid": %d,"cat":"","tid": %d,"dur": %.2f,"ts": %.2f,"name":"%s","ph":"X"}|json}
       pid tid dur ts name;
-    flush oc
+    ()
+
+  let emit_instant_event ~name ~ts () : unit =
+    let pid = Unix.getpid() in
+    let tid = Thread.id (Thread.self()) in
+    emit_sep_();
+    Printf.fprintf oc
+      {json|{"pid": %d,"cat":"","tid": %d,"ts": %.2f,"name":"%s","ph":"I"}|json}
+      pid tid ts name;
+    ()
 
   let teardown () = teardown_ oc
 end
diff --git a/src/util/Profile.ml b/src/util/Profile.ml
index 3f0afc96..c0d6b6ca 100644
--- a/src/util/Profile.ml
+++ b/src/util/Profile.ml
@@ -2,13 +2,19 @@
 module type BACKEND = sig
   val get_ts : unit -> float
 
-  val emit_event :
+  val emit_duration_event :
     name : string ->
     start : float ->
     end_ : float ->
     unit ->
     unit
 
+  val emit_instant_event :
+    name : string ->
+    ts : float ->
+    unit ->
+    unit
+
   val teardown : unit -> unit
 end
 
@@ -21,6 +27,8 @@ type probe =
     start: float;
   }
 
+let null_probe = No_probe
+
 (* where to print events *)
 let out_ : backend option ref = ref None
 
@@ -32,10 +40,17 @@ let[@inline] begin_ name : probe =
   | None -> No_probe
   | Some b -> begin_with_ b name
 
+let[@inline] instant name =
+  match !out_ with
+  | None -> ()
+  | Some (module B) ->
+    let now = B.get_ts() in
+    B.emit_instant_event ~name ~ts:now ()
+
 (* slow path *)
 let exit_full_ (module B : BACKEND) name start =
   let now = B.get_ts() in
-  B.emit_event ~name ~start ~end_:now ()
+  B.emit_duration_event ~name ~start ~end_:now ()
 
 let exit_with_ b pb =
   match pb with
@@ -60,6 +75,19 @@ let[@inline] with_ name f =
       exit_with_ b pb;
       raise e
 
+let[@inline] with1 name f x =
+  match !out_ with
+  | None -> f x
+  | Some b ->
+    let pb = begin_with_ b name in
+    try
+      let res = f x in
+      exit_with_ b pb;
+      res
+    with e ->
+      exit_with_ b pb;
+      raise e
+
 module Control = struct
   let setup b =
     assert (!out_ = None);
diff --git a/src/util/Profile.mli b/src/util/Profile.mli
index d697a39a..ea3bb498 100644
--- a/src/util/Profile.mli
+++ b/src/util/Profile.mli
@@ -3,22 +3,34 @@
 
 type probe
 
+val null_probe : probe
+
+val instant : string -> unit
+
 val begin_ : string -> probe
 
 val exit : probe -> unit
 
 val with_ : string -> (unit -> 'a) -> 'a
 
+val with1 : string -> ('a -> 'b) -> 'a -> 'b
+
 module type BACKEND = sig
   val get_ts : unit -> float
 
-  val emit_event :
+  val emit_duration_event :
     name : string ->
     start : float ->
     end_ : float ->
     unit ->
     unit
 
+  val emit_instant_event :
+    name : string ->
+    ts : float ->
+    unit ->
+    unit
+
   val teardown : unit -> unit
 end