diff --git a/src/interpretation.ml b/src/interpretation.ml
index 4d5af8bad9c4fa51374ba4900e9a3b8ae71b1a5c..7e0bddfc54774e270951d169e97df4bbee55f67a 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -373,6 +373,9 @@ let interpret_task ~cwd env task =
   in
   let g, f = (Task.task_goal task, Task.task_goal_fmla task) in
   let f = CRE.normalize ~limit:Int.max_value engine Term.Mvs.empty f in
+  Logs.debug ~src:Logging.src_interpret_goal (fun m ->
+    m "Interpreted formula for goal '%a':@.%a@.%a" Pretty.print_pr g
+      Pretty.print_term f print_caisar_op_of_ls caisar_env);
   let _, task = Task.task_separate_goal task in
   let task = declare_language_lsymbols caisar_env task in
   let task = Task.(add_prop_decl task Pgoal g f) in
diff --git a/src/logging.ml b/src/logging.ml
index f15df62bc1de0e489d51a0b76536c93762f5895f..049a3d73c25fc6294bc48229be5148714f920110 100644
--- a/src/logging.ml
+++ b/src/logging.ml
@@ -26,10 +26,20 @@ let src_prover_spec =
   Logs.Src.create "ProverSpec" ~doc:"Prover-tailored specification"
 
 let src_prover_call = Logs.Src.create "ProverCall" ~doc:"Prover call"
+
+let src_interpret_goal =
+  Logs.Src.create "InterpretGoal" ~doc:"Goal interpretation"
+
 let src_stack_trace = Logs.Src.create "StackTrace" ~doc:"Print stack trace"
 
 let all_srcs () =
-  [ src_autodetect; src_prover_spec; src_prover_call; src_stack_trace ]
+  [
+    src_autodetect;
+    src_prover_spec;
+    src_prover_call;
+    src_interpret_goal;
+    src_stack_trace;
+  ]
 
 let is_debug_level src =
   match Logs.Src.level src with Some Debug -> true | _ -> false
diff --git a/src/logging.mli b/src/logging.mli
index 48e43c3b9e5caf1c36004dd8d25f6c58dea3d5e6..315bbc7251b96f6e0d95c1ddff9f30b951da6733 100644
--- a/src/logging.mli
+++ b/src/logging.mli
@@ -25,6 +25,7 @@
 val src_autodetect : Logs.src
 val src_prover_spec : Logs.src
 val src_prover_call : Logs.src
+val src_interpret_goal : Logs.src
 val src_stack_trace : Logs.src
 
 val all_srcs : unit -> Logs.src list