From e0faf6ba72aa936ff7e5f068d5b13d5966b4f035 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 20 Aug 2022 00:21:45 -0400
Subject: [PATCH] feat: some spans in main/process

---
 src/main/main.ml      | 8 +++++++-
 src/smtlib/Process.ml | 1 +
 2 files changed, 8 insertions(+), 1 deletion(-)

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 =