diff --git a/prusti-viper/src/encoder/high/procedures/inference/state/fold_unfold_state.rs b/prusti-viper/src/encoder/high/procedures/inference/state/fold_unfold_state.rs
index c83a95d1252..4b01800316a 100644
--- a/prusti-viper/src/encoder/high/procedures/inference/state/fold_unfold_state.rs
+++ b/prusti-viper/src/encoder/high/procedures/inference/state/fold_unfold_state.rs
@@ -10,7 +10,7 @@ use vir_crate::{
 
 use super::PredicateState;
 
-#[derive(Clone)]
+#[derive(Clone, Debug)]
 pub(in super::super::super) struct FoldUnfoldState {
     /// If this state is a merge of multiple incoming states, then
     /// `incoming_labels` contains the list of basic blocks from where the
diff --git a/prusti-viper/src/encoder/high/procedures/interface.rs b/prusti-viper/src/encoder/high/procedures/interface.rs
index 1f040e8f478..cd2b37d2b4f 100644
--- a/prusti-viper/src/encoder/high/procedures/interface.rs
+++ b/prusti-viper/src/encoder/high/procedures/interface.rs
@@ -122,9 +122,7 @@ impl<'v, 'tcx: 'v> HighProcedureEncoderInterface<'tcx> for super::super::super::
     ) -> SpannedEncodingResult<Vec<vir_mid::ProcedureDecl>> {
         let mut procedures = Vec::new();
         for procedure_high in self.encode_procedure_core_proof_high(proc_def_id, check_mode)? {
-            debug!("procedure_high:\n{}", procedure_high);
             let procedure_typed = self.procedure_high_to_typed(procedure_high)?;
-            debug!("procedure_typed:\n{}", procedure_typed);
             let procedure =
                 super::inference::infer_shape_operations(self, proc_def_id, procedure_typed)?;
             procedures.push(procedure);
diff --git a/prusti-viper/src/encoder/mir/specifications/specs.rs b/prusti-viper/src/encoder/mir/specifications/specs.rs
index f845a5741bd..41d569ece21 100644
--- a/prusti-viper/src/encoder/mir/specifications/specs.rs
+++ b/prusti-viper/src/encoder/mir/specifications/specs.rs
@@ -102,27 +102,27 @@ impl<'tcx> Specifications<'tcx> {
         self.user_typed_specs.get_ghost_end(def_id)
     }
 
+    #[tracing::instrument(level = "trace", skip(self))]
     pub(super) fn get_specification_region_begin(
         &self,
         def_id: &DefId,
     ) -> Option<&SpecificationRegionBegin> {
-        trace!("Get begin specification region specs of {:?}", def_id);
         self.user_typed_specs.get_specification_region_begin(def_id)
     }
 
+    #[tracing::instrument(level = "trace", skip(self))]
     pub(super) fn get_specification_region_end(
         &self,
         def_id: &DefId,
     ) -> Option<&SpecificationRegionEnd> {
-        trace!("Get end specification region specs of {:?}", def_id);
         self.user_typed_specs.get_specification_region_end(def_id)
     }
 
+    #[tracing::instrument(level = "trace", skip(self))]
     pub(super) fn get_specification_expression(
         &self,
         def_id: &DefId,
     ) -> Option<&SpecificationExpression> {
-        trace!("Get specification expression specs of {:?}", def_id);
         self.user_typed_specs.get_specification_expression(def_id)
     }