diff --git a/src/main/main.ml b/src/main/main.ml
index 9795fc2a..769ec595 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -198,7 +198,13 @@ let main_smt ~config () : _ result =
   if !check then
     (* might have to check conflicts *)
     Solver.add_theory solver Process.Check_cc.theory;
-  Sidekick_smtlib.parse tst !file >>= fun input ->
+
+  let parse_res =
+    let@ () = Profile.with_ "parse" ~args:[ "file", !file ] in
+    Sidekick_smtlib.parse tst !file
+  in
+
+  parse_res >>= fun input ->
   (* process statements *)
   let res =
     try
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index 6fd22930..8083fe3f 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -245,6 +245,7 @@ let known_logics =
 let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model
     ?(check = false) ?time ?memory ?progress (solver : Solver.t)
     (stmt : Statement.t) : unit or_error =
+  let@ () = Profile.with_ "smtlib.process-stmt" in
   Log.debugf 5 (fun k ->
       k "(@[smtlib.process-statement@ %a@])" Statement.pp stmt);
   let decl_sort c n : unit =