[interpretation] Log the resulting interpreted formula for debugging.

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

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

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