diff --git a/src/smt/solver_internal.ml b/src/smt/solver_internal.ml
index 1efe553b..485a3a2b 100644
--- a/src/smt/solver_internal.ml
+++ b/src/smt/solver_internal.ml
@@ -314,17 +314,17 @@ let cc_resolve_expl self e : lit list * _ =
 
 (** {2 Interface with the SAT solver} *)
 
-let rec push_lvl_ = function
+let rec push_lvl_theories_ = function
   | Ths_nil -> ()
   | Ths_cons r ->
     r.push_level r.st;
-    push_lvl_ r.next
+    push_lvl_theories_ r.next
 
-let rec pop_lvls_ n = function
+let rec pop_lvls_theories_ n = function
   | Ths_nil -> ()
   | Ths_cons r ->
     r.pop_levels r.st n;
-    pop_lvls_ n r.next
+    pop_lvls_theories_ n r.next
 
 (** {2 Model construction and theory combination} *)
 
diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml
index 2b308703..17b34832 100644
--- a/src/th-data/Sidekick_th_data.ml
+++ b/src/th-data/Sidekick_th_data.ml
@@ -715,7 +715,6 @@ end = struct
     )
 
   let on_partial_check self solver acts trail =
-    Profile.with_ "data.partial-check" @@ fun () ->
     check_is_a self solver acts trail;
     ()