diff --git a/src/sat/solver.ml b/src/sat/solver.ml
index 5137508e..007b2c34 100644
--- a/src/sat/solver.ml
+++ b/src/sat/solver.ml
@@ -1621,6 +1621,7 @@ let pick_branch_lit ~full self : bool =
 (* do some amount of search, until the number of conflicts or clause learnt
    reaches the given parameters *)
 let search (self : t) ~on_progress ~(max_conflicts : int) : unit =
+  let@ () = Profile.with_ "sat.search" in
   Log.debugf 3 (fun k ->
       k "(@[sat.search@ :max-conflicts %d@ :max-learnt %d@])" max_conflicts
         !(self.max_clauses_learnt));
@@ -1645,6 +1646,7 @@ let search (self : t) ~on_progress ~(max_conflicts : int) : unit =
       assert (self.elt_head = AVec.size self.trail);
       assert (self.elt_head = self.th_head);
       if max_conflicts > 0 && !n_conflicts >= max_conflicts then (
+        Profile.instant "sat.restart";
         Log.debug 1 "(sat.restarting)";
         cancel_until self 0;
         Stat.incr self.n_restarts;
@@ -1682,6 +1684,7 @@ let[@inline] eval st lit = fst @@ eval_level st lit
 (* fixpoint of propagation and decisions until a model is found, or a
    conflict is reached *)
 let solve_ ~on_progress (self : t) : unit =
+  let@ () = Profile.with_ "sat.solve" in
   Log.debugf 5 (fun k ->
       k "(@[sat.solve :assms %d@])" (AVec.size self.assumptions));
   check_unsat_ self;
@@ -1724,6 +1727,8 @@ let solve_ ~on_progress (self : t) : unit =
           check_is_conflict_ self c;
           Clause.iter self.store c ~f:(fun a ->
               insert_var_order self (Atom.var a));
+
+          Profile.instant "sat.th-conflict";
           Log.debugf 5 (fun k ->
               k "(@[sat.theory-conflict-clause@ %a@])" (Clause.debug self.store)
                 c);
diff --git a/src/smt/solver_internal.ml b/src/smt/solver_internal.ml
index eff96801..bf5adae7 100644
--- a/src/smt/solver_internal.ml
+++ b/src/smt/solver_internal.ml
@@ -73,10 +73,6 @@ let[@inline] cc (self : t) = self.cc
 let[@inline] tst self = self.tst
 let[@inline] proof self = self.proof
 let stats self = self.stat
-
-let[@inline] has_delayed_actions self =
-  not (Queue.is_empty self.delayed_actions)
-
 let registry self = self.registry
 let simplifier self = self.simp
 let simplify_t self (t : Term.t) : _ option = Simplify.normalize self.simp t
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index 57f81096..44a6ac2b 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -170,9 +170,9 @@ let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false)
   in
 
   let res =
-    Profile.with_ "solve" (fun () ->
-        Solver.solve ~assumptions ?on_progress ?should_stop s
-        (* ?gc ?restarts ?time ?memory ?progress *))
+    let@ () = Profile.with_ "process.solve" in
+    Solver.solve ~assumptions ?on_progress ?should_stop s
+    (* ?gc ?restarts ?time ?memory ?progress *)
   in
   let t2 = Sys.time () in
   Printf.printf "\r";