diff --git a/CHANGELOG.md b/CHANGELOG.md
index f979a0848..4ea5b873b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -32,6 +32,7 @@ Changes to hax-lib:
 
 Miscellaneous:
  - A lean tutorial has been added to the hax website (#1626)
+ - Diagnostics reporting were improved (#1692)
 
 ## 0.3.4
 
diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs
index fce2f79cd..b22624ff9 100644
--- a/cli/subcommands/src/cargo_hax.rs
+++ b/cli/subcommands/src/cargo_hax.rs
@@ -149,7 +149,12 @@ use hax_types::diagnostics::report::ReportCtx;
 
 #[extension_traits::extension(trait ExtHaxMessage)]
 impl HaxMessage {
-    fn report(self, message_format: MessageFormat, rctx: Option<&mut ReportCtx>) {
+    fn report(self, message_format: MessageFormat, mut rctx: Option<&mut ReportCtx>) {
+        if let (Some(r), HaxMessage::Diagnostic { diagnostic, .. }) = (rctx.as_mut(), &self)
+            && r.seen_already(diagnostic.clone())
+        {
+            return;
+        }
         match message_format {
             MessageFormat::Json => println!("{}", serde_json::to_string(&self).unwrap()),
             MessageFormat::Human => self.report_styled(rctx),
diff --git a/engine/lib/backend.ml b/engine/lib/backend.ml
index 9836708bf..bd6d3435e 100644
--- a/engine/lib/backend.ml
+++ b/engine/lib/backend.ml
@@ -55,7 +55,8 @@ module Make (InputLanguage : Features.T) (M : BackendMetadata) = struct
       let context = Diagnostics.Context.Backend M.backend in
       let kind = err.kind in
       let span = Span.to_thir err.span in
-      Diagnostics.SpanFreeError.raise ~span context kind
+      Diagnostics.SpanFreeError.raise ~span (Span.owner_hint err.span) context
+        kind
 
     let unimplemented ?issue_id ?details span =
       raise
diff --git a/engine/lib/deprecated_generic_printer/deprecated_generic_printer_base.ml b/engine/lib/deprecated_generic_printer/deprecated_generic_printer_base.ml
index 95da09674..d94a7adf8 100644
--- a/engine/lib/deprecated_generic_printer/deprecated_generic_printer_base.ml
+++ b/engine/lib/deprecated_generic_printer/deprecated_generic_printer_base.ml
@@ -130,7 +130,9 @@ module Make (F : Features.T) = struct
           let span = Span.to_thir current_span in
           let kind = Types.AssertionFailure { details } in
           let ctx = Diagnostics.Context.GenericPrinter print#printer_name in
-          Diagnostics.SpanFreeError.raise ~span ctx kind
+          Diagnostics.SpanFreeError.raise ~span
+            (Span.owner_hint current_span)
+            ctx kind
 
       method set_current_namespace ns = current_namespace <- ns
       method get_current_namespace () = current_namespace
diff --git a/engine/lib/diagnostics.ml b/engine/lib/diagnostics.ml
index e65beacba..4e555ead4 100644
--- a/engine/lib/diagnostics.ml
+++ b/engine/lib/diagnostics.ml
@@ -147,7 +147,9 @@ module SpanFreeError : sig
   exception Exn of t
 
   val payload : t -> Context.t * kind
-  val raise : ?span:T.span list -> Context.t -> kind -> 'a
+
+  val raise :
+    ?span:T.span list -> Types.def_id option -> Context.t -> kind -> 'a
 end = struct
   type t = Data of Context.t * kind [@@deriving show]
 
@@ -158,7 +160,8 @@ end = struct
   let raise_without_reporting (ctx : Context.t) (kind : kind) =
     raise (Exn (Data (ctx, kind)))
 
-  let raise ?(span = []) (ctx : Context.t) (kind : kind) =
-    report { span; kind; context = ctx; owner_id = None };
+  let raise ?(span = []) (owner_id : Types.def_id option) (ctx : Context.t)
+      (kind : kind) =
+    report { span; kind; context = ctx; owner_id };
     raise_without_reporting ctx kind
 end
diff --git a/engine/lib/feature_gate.ml b/engine/lib/feature_gate.ml
index 597f9511a..5af3e711d 100644
--- a/engine/lib/feature_gate.ml
+++ b/engine/lib/feature_gate.ml
@@ -43,14 +43,15 @@ struct
             =
           try f span x
           with S0.E err ->
-            let span = Span.to_thir span in
+            let thir_span = Span.to_thir span in
             let kind : Diagnostics.kind =
               ExplicitRejection { reason = S0.explain err feature_kind }
             in
             let context : Diagnostics.Context.t =
               Phase S0.metadata.current_phase
             in
-            Diagnostics.SpanFreeError.raise ~span context kind
+            Diagnostics.SpanFreeError.raise ~span:thir_span
+              (Span.owner_hint span) context kind
       end)
 
   include Subtype.Make (FA) (FB) (S)
diff --git a/engine/lib/generic_printer/generic_printer.ml b/engine/lib/generic_printer/generic_printer.ml
index 7221331fa..08d5b31f3 100644
--- a/engine/lib/generic_printer/generic_printer.ml
+++ b/engine/lib/generic_printer/generic_printer.ml
@@ -198,7 +198,9 @@ module Make (F : Features.T) = struct
           let span = Span.to_thir self#current_span in
           let kind = Types.AssertionFailure { details } in
           let ctx = Diagnostics.Context.GenericPrinter self#printer_name in
-          Diagnostics.SpanFreeError.raise ~span ctx kind
+          Diagnostics.SpanFreeError.raise ~span
+            (Span.owner_hint self#current_span)
+            ctx kind
       (** An assertion failed *)
 
       method unreachable : 'any. unit -> 'any =
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index 488af1546..c24c2dafd 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -20,7 +20,9 @@ open Diagnostics
 
 let assertion_failure (span : Thir.span list) (details : string) =
   let kind = T.AssertionFailure { details } in
-  Diagnostics.SpanFreeError.raise ~span ThirImport kind
+  Diagnostics.SpanFreeError.raise ~span
+    (Span.dummy () |> Span.owner_hint)
+    ThirImport kind
 
 let unimplemented ~issue_id (span : Thir.span list) (details : string) =
   let kind =
@@ -30,7 +32,9 @@ let unimplemented ~issue_id (span : Thir.span list) (details : string) =
         details = String.(if details = "" then None else Some details);
       }
   in
-  Diagnostics.SpanFreeError.raise ~span ThirImport kind
+  Diagnostics.SpanFreeError.raise ~span
+    (Span.dummy () |> Span.owner_hint)
+    ThirImport kind
 
 module Ast = struct
   include Ast
diff --git a/engine/lib/phase_utils.ml b/engine/lib/phase_utils.ml
index 987d85097..32ed2ec83 100644
--- a/engine/lib/phase_utils.ml
+++ b/engine/lib/phase_utils.ml
@@ -113,7 +113,8 @@ end) : ERROR = struct
 
   let raise err =
     let span = Span.to_thir err.span in
-    Diagnostics.SpanFreeError.raise ~span Ctx.ctx err.kind
+    Diagnostics.SpanFreeError.raise ~span (Span.owner_hint err.span) Ctx.ctx
+      err.kind
 
   let unimplemented ?issue_id ?details span =
     raise
diff --git a/engine/lib/span.ml b/engine/lib/span.ml
index 5bf6f86f9..2557c2728 100644
--- a/engine/lib/span.ml
+++ b/engine/lib/span.ml
@@ -150,7 +150,8 @@ let default = { id = 0; data = []; owner_hint = None }
 
 let owner_hint span =
   span.owner_hint
-  |> Option.bind ~f:(fun (OwnerId id) -> List.nth !owner_id_list id)
+  |> Option.map ~f:(fun (OwnerId id) ->
+         Option.value_exn (List.nth !owner_id_list id))
 
 let to_span2 span : Types.span2 =
   {
diff --git a/hax-types/src/diagnostics/mod.rs b/hax-types/src/diagnostics/mod.rs
index 401c38d99..cefb95d51 100644
--- a/hax-types/src/diagnostics/mod.rs
+++ b/hax-types/src/diagnostics/mod.rs
@@ -5,7 +5,7 @@ pub mod message;
 pub mod report;
 
 #[derive_group(Serializers)]
-#[derive(Debug, Clone, JsonSchema)]
+#[derive(Debug, Clone, JsonSchema, Eq, PartialEq, Hash)]
 pub struct Diagnostics {
     pub kind: Kind,
     pub span: Vec<hax_frontend_exporter::Span>,
@@ -15,7 +15,6 @@ pub struct Diagnostics {
 
 impl std::fmt::Display for Diagnostics {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
-        write!(f, "({}) ", self.context)?;
         match &self.kind {
             Kind::Unimplemented { issue_id, details } => write!(
                 f,
@@ -31,7 +30,7 @@ impl std::fmt::Display for Diagnostics {
             ),
             Kind::UnsupportedMacro { id } => write!(
                 f,
-                "The unexpanded macro {} it is not supported by this backend. Please verify the option you passed the {} (or {}) option.",
+                "The unexpanded macro {} is not supported by this backend.\nPlease verify the argument you passed to the {} (or {}) option.",
                 id.bold(),
                 "--inline-macro-call".bold(), "-i".bold()
             ),
@@ -49,10 +48,9 @@ impl std::fmt::Display for Diagnostics {
             ),
             Kind::ExpectedMutRef => write!(
                 f,
-                "At this position, Hax was expecting an expression of the shape `&mut _`. Hax forbids `f(x)` (where `f` expects a mutable reference as input) when `x` is not a {}{} or when it is a dereference expression.
+                "At this position, Hax was expecting an expression of the shape `&mut _`.\nHax forbids `f(x)` (where `f` expects a mutable reference as input) when `x` is not a {}{} or when it is a dereference expression.
 
-{}
-",
+{}",
                 "place expression".bold(),
                 "[1]".bright_black(),
                 "[1]: https://doc.rust-lang.org/reference/expressions.html#place-expressions-and-value-expressions"
@@ -62,15 +60,53 @@ impl std::fmt::Display for Diagnostics {
                 "The bindings {:?} cannot be mutated here: they don't belong to the closure scope, and this is not allowed.",
                 bindings
             ),
-            Kind::ArbitraryLHS => write!(f, "Assignation of an arbitrary left-hand side is not supported. `lhs = e` is fine only when `lhs` is a combination of local identifiers, field accessors and index accessors."),
+            Kind::ArbitraryLHS => write!(f, "Assignation of an arbitrary left-hand side is not supported.\n`lhs = e` is fine only when `lhs` is a combination of local identifiers, field accessors and index accessors."),
 
             Kind::AttributeRejected {reason} => write!(f, "Here, this attribute cannot be used: {reason}."),
 
-            Kind::NonTrivialAndMutFnInput => write!(f, "The support in hax of function with one or more inputs of type `&mut _` is limited. Onlu trivial patterns are allowed there: `fn f(x: &mut (T, U)) ...` is allowed while `f((x, y): &mut (T, U))` is rejected."),
+            Kind::NonTrivialAndMutFnInput => write!(f, "The support in hax of function with one or more inputs of type `&mut _` is limited.\nOnly trivial patterns are allowed there: `fn f(x: &mut (T, U)) ...` is allowed while `f((x, y): &mut (T, U))` is rejected."),
 
             Kind::FStarParseError { fstar_snippet, details: _ } => write!(f, "The following code snippet could not be parsed as valid F*:\n```\n{fstar_snippet}\n```"),
 
             _ => write!(f, "{:?}", self.kind),
+        }?;
+        write!(f, "\n\n")?;
+        if let Some(issue) = self.kind.issue_number() {
+            write!(
+                f,
+                "This is discussed in issue https://github.com/hacspec/hax/issues/{issue}.\nPlease upvote or comment this issue if you see this error message."
+            )?;
+        }
+        write!(
+            f,
+            "{}",
+            format!(
+                "\nNote: the error was labeled with context `{}`.\n",
+                self.context
+            )
+            .bright_black()
+        )?;
+        Ok(())
+    }
+}
+
+impl Kind {
+    fn issue_number(&self) -> Option<u32> {
+        match self {
+            Kind::UnsafeBlock => None,
+            Kind::Unimplemented { issue_id, .. } => issue_id.clone(),
+            Kind::AssertionFailure { .. } => None,
+            Kind::UnallowedMutRef => Some(420),
+            Kind::UnsupportedMacro { .. } => None,
+            Kind::ErrorParsingMacroInvocation { .. } => None,
+            Kind::ClosureMutatesParentBindings { .. } => Some(1060),
+            Kind::ArbitraryLHS => None,
+            Kind::ExplicitRejection { .. } => None,
+            Kind::UnsupportedTupleSize { .. } => None,
+            Kind::ExpectedMutRef => Some(420),
+            Kind::NonTrivialAndMutFnInput => Some(1405),
+            Kind::AttributeRejected { .. } => None,
+            Kind::FStarParseError { .. } => todo!(),
         }
     }
 }
diff --git a/hax-types/src/diagnostics/report.rs b/hax-types/src/diagnostics/report.rs
index e1cc96ef5..de28ade16 100644
--- a/hax-types/src/diagnostics/report.rs
+++ b/hax-types/src/diagnostics/report.rs
@@ -1,7 +1,7 @@
 use super::Diagnostics;
 use annotate_snippets::*;
 use miette::SourceOffset;
-use std::collections::HashMap;
+use std::collections::{HashMap, HashSet};
 use std::path::{Path, PathBuf};
 use std::rc::Rc;
 
@@ -9,6 +9,7 @@ use std::rc::Rc;
 #[derive(Clone, Debug, Default)]
 pub struct ReportCtx {
     files: HashMap<PathBuf, Rc<String>>,
+    seen: HashSet<Diagnostics>,
 }
 
 /// Translates a line and column position into an absolute offset
@@ -28,6 +29,11 @@ impl ReportCtx {
             })
             .clone()
     }
+
+    /// Check if `diagnostic` have been seen already, and mark `diagnostic` as seen.
+    pub fn seen_already(&mut self, diagnostic: Diagnostics) -> bool {
+        !self.seen.insert(diagnostic)
+    }
 }
 
 impl Diagnostics {
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst
index b4247da85..2e3c6b323 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst
@@ -3,7 +3,11 @@ module Coverage.Attr.Trait_impl_inherit
 open Core
 open FStar.Mul
 
-(* item error backend: (reject_TraitItemDefault) ExplicitRejection { reason: "a node of kind [Trait_item_default] have been found in the AST" }
+(* item error backend: ExplicitRejection { reason: "a node of kind [Trait_item_default] have been found in the AST" }
+
+
+Note: the error was labeled with context `reject_TraitItemDefault`.
+
 Last available AST for this item:
 
 #[<cfg>(any(feature = "json"))]#[feature(coverage_attribute)]#[<cfg>(any(feature = "json", feature = "lean", feature = "fstar", feature =
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Color.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Color.fst
index 1d7b7eb5c..acdae73af 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Color.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Color.fst
@@ -4,7 +4,7 @@ open Core
 open FStar.Mul
 
 let main (_: Prims.unit) : (Prims.unit & Prims.unit) =
-  Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+  Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
     "{\n for _i in (core::iter::traits::collect::f_into_iter(core::ops::range::Range {\n f_start: 0,\n f_end: 0,\n })) {\n Tuple0\n }\n }"
   ,
   ()
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.If_not.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.If_not.fst
index c7d0ce014..0a3ab1874 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.If_not.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.If_not.fst
@@ -58,11 +58,11 @@ let if_not (cond: bool) : Prims.unit =
 
 let main (_: Prims.unit) : (Prims.unit & Prims.unit) =
   let _:Prims.unit =
-    Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+    Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
       "{\n for _ in (core::iter::traits::collect::f_into_iter(core::ops::range::Range {\n f_start: 0,\n f_end: 8,\n })) {\n coverage::if_not::if_not(core::hint::black_box::<bool>(true))\n }\n }"
 
   in
-  Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+  Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
     "{\n for _ in (core::iter::traits::collect::f_into_iter(core::ops::range::Range {\n f_start: 0,\n f_end: 4,\n })) {\n coverage::if_not::if_not(core::hint::black_box::<bool>(false))\n }\n }"
   ,
   ()
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Inline.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Inline.fst
index 8dd3307cf..96f58ba53 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Inline.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Inline.fst
@@ -24,7 +24,7 @@ let display
       (xs: t_Slice v_T)
     : Prims.unit =
   let _:Prims.unit =
-    Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+    Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
       "{\n for x in (core::iter::traits::collect::f_into_iter(xs)) {\n {\n let args: [core::fmt::rt::t_Argument; 1] = {\n [core::fmt::rt::impl__new_display::<T>(x)]\n };\n {\n let _: tuple0 = {\n std::io::stdio::e_p..."
 
   in
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Inner_items.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Inner_items.fst
index 4df1e409e..8b00ef6bf 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Inner_items.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Inner_items.fst
@@ -35,7 +35,11 @@ type main__t_InStruct = { main__f_in_struct_field:u32 }
 
 let main__v_IN_CONST: u32 = mk_u32 1234
 
-(* item error backend: (reject_TraitItemDefault) ExplicitRejection { reason: "a node of kind [Trait_item_default] have been found in the AST" }
+(* item error backend: ExplicitRejection { reason: "a node of kind [Trait_item_default] have been found in the AST" }
+
+
+Note: the error was labeled with context `reject_TraitItemDefault`.
+
 Last available AST for this item:
 
 #[<cfg>(any(feature = "json", feature = "lean"))]#[allow(unused_assignments, unused_variables, dead_code)]#[feature(coverage_attribute)]#[allow(unused_attributes)]#[allow(dead_code)]#[allow(unreachable_code)]#[feature(register_tool)]#[register_tool(_hax)]trait main__t_InTrait<Self_>{#[_hax::json("\"TraitMethodNoPrePost\"")]fn main__f_trait_func_pre(_: Self,_: int) -> bool;
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Let_else_loop.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Let_else_loop.fst
index 822459fc4..73ad1814a 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Let_else_loop.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Let_else_loop.fst
@@ -7,7 +7,7 @@ let loopy (cond: bool) : Prims.unit =
   match cond <: bool with
   | true -> ()
   | _ ->
-    Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+    Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
       "{\n loop {\n Tuple0\n }\n }",
     ()
     <:
@@ -16,7 +16,7 @@ let loopy (cond: bool) : Prims.unit =
 let e_loop_either_way (cond: bool) : Prims.unit =
   match cond <: bool with
   | true ->
-    Rust_primitives.Hax.never_to_any ((Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+    Rust_primitives.Hax.never_to_any ((Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
             "{\n loop {\n Tuple0\n }\n }"
           <:
           Prims.unit),
@@ -24,7 +24,7 @@ let e_loop_either_way (cond: bool) : Prims.unit =
         <:
         (Prims.unit & Prims.unit))
   | _ ->
-    Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+    Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
       "{\n loop {\n Tuple0\n }\n }",
     ()
     <:
@@ -33,7 +33,7 @@ let e_loop_either_way (cond: bool) : Prims.unit =
 let e_if (cond: bool) : Prims.unit =
   if cond
   then
-    Rust_primitives.Hax.never_to_any ((Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+    Rust_primitives.Hax.never_to_any ((Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
             "{\n loop {\n Tuple0\n }\n }"
           <:
           Prims.unit),
@@ -41,7 +41,7 @@ let e_if (cond: bool) : Prims.unit =
         <:
         (Prims.unit & Prims.unit))
   else
-    Rust_primitives.Hax.never_to_any ((Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+    Rust_primitives.Hax.never_to_any ((Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
             "{\n loop {\n Tuple0\n }\n }"
           <:
           Prims.unit),
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Loop_break.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Loop_break.fst
index 703d3b0bf..29be26558 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Loop_break.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Loop_break.fst
@@ -4,7 +4,7 @@ open Core
 open FStar.Mul
 
 let main (_: Prims.unit) : (Prims.unit & Prims.unit) =
-  Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+  Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
     "{\n loop {\n (if core::hint::black_box::<bool>(true) {\n core::ops::control_flow::ControlFlow_Break(Tuple2(Tuple0, Tuple0()))\n } else {\n core::ops::control_flow::ControlFlow_Continue(Tuple0)\n })\n }\n }"
   ,
   ()
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Loop_break_value.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Loop_break_value.fst
index d4d459fb9..7537c8067 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Loop_break_value.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Loop_break_value.fst
@@ -5,7 +5,7 @@ open FStar.Mul
 
 let main (_: Prims.unit) : Prims.unit =
   let result:i32 =
-    Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+    Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
       "{\n loop {\n core::ops::control_flow::ControlFlow_Break(Tuple2(10, Tuple0()))\n }\n }",
     ()
     <:
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Loops_branches.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Loops_branches.fst
index be8b66179..0a9bdde0e 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Loops_branches.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Loops_branches.fst
@@ -25,7 +25,7 @@ let impl: Core.Fmt.t_Debug t_DebugTest =
         let _:Prims.unit =
           if false
           then
-            Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+            Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
               "{\n while true {\n Tuple0\n }\n }"
         in
         let tmp0, out:(Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error) =
@@ -56,7 +56,7 @@ let impl: Core.Fmt.t_Debug t_DebugTest =
                       let _:Prims.unit =
                         if false
                         then
-                          Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+                          Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
                             "{\n while true {\n Tuple0\n }\n }"
                       in
                       let tmp0, out:(Core.Fmt.t_Formatter &
@@ -142,7 +142,7 @@ let impl: Core.Fmt.t_Debug t_DebugTest =
                   let _:Prims.unit =
                     if false
                     then
-                      Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+                      Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
                         "{\n while true {\n Tuple0\n }\n }"
                   in
                   let tmp0, out:(Core.Fmt.t_Formatter &
@@ -248,7 +248,7 @@ let impl_1: Core.Fmt.t_Display t_DisplayTest =
                   let _:Prims.unit =
                     if false
                     then
-                      Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+                      Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
                         "{\n while true {\n Tuple0\n }\n }"
                   in
                   let tmp0, out:(Core.Fmt.t_Formatter &
@@ -307,7 +307,7 @@ let impl_1: Core.Fmt.t_Display t_DisplayTest =
         let _:Prims.unit =
           if false
           then
-            Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+            Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
               "{\n while true {\n Tuple0\n }\n }"
         in
         let tmp0, out:(Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error) =
@@ -345,7 +345,7 @@ let impl_1: Core.Fmt.t_Display t_DisplayTest =
                       let _:Prims.unit =
                         if false
                         then
-                          Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+                          Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
                             "{\n while true {\n Tuple0\n }\n }"
                       in
                       let tmp0, out:(Core.Fmt.t_Formatter &
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Mcdc.Condition_limit.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Mcdc.Condition_limit.fst
index 4f64c9faa..05f261d08 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Mcdc.Condition_limit.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Mcdc.Condition_limit.fst
@@ -4,7 +4,7 @@ open Core
 open FStar.Mul
 
 let accept_7_conditions (bool_arr: t_Array bool (mk_usize 7)) : Prims.unit =
-  Rust_primitives.Hax.failure "(AST import) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/804.\nPlease upvote or comment this issue if you see this error message.\nPat:Array"
+  Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/804.\nPlease upvote or comment this issue if you see this error message.\nPat:Array\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/804.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `AST import`.\n"
     ""
 
 let main (_: Prims.unit) : Prims.unit =
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Simple_loop.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Simple_loop.fst
index bd029574c..633be7115 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Simple_loop.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Simple_loop.fst
@@ -26,7 +26,7 @@ let main (_: Prims.unit) : (i32 & Prims.unit) =
       countdown
     else countdown
   in
-  Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/933.\nPlease upvote or comment this issue if you see this error message.\nUnhandled loop kind"
+  Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/933.\nPlease upvote or comment this issue if you see this error message.\nUnhandled loop kind\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/933.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
     "{\n (loop {\n |countdown| {\n (if rust_primitives::hax::machine_int::eq(countdown, 0) {\n core::ops::control_flow::ControlFlow_Break(Tuple2(Tuple0, countdown))\n } else {\n core::ops::control_flow::ControlF..."
   ,
   ()
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Simple_match.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Simple_match.fst
index 72f350aa5..4b0a4d2f7 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Simple_match.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Simple_match.fst
@@ -26,8 +26,8 @@ let main (_: Prims.unit) : (Prims.unit & Prims.unit) =
       countdown
     else countdown
   in
-  Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
-    "{\n for _ in (core::iter::traits::collect::f_into_iter(core::ops::range::Range {\n f_start: 0,\n f_end: 2,\n })) {\n rust_primitives::hax::failure(\n \"(AST import) something is not implemented yet.This is d..."
+  Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
+    "{\n for _ in (core::iter::traits::collect::f_into_iter(core::ops::range::Range {\n f_start: 0,\n f_end: 2,\n })) {\n rust_primitives::hax::failure(\n \"something is not implemented yet.This is discussed in i..."
   ,
   ()
   <:
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Tight_inf_loop.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Tight_inf_loop.fst
index 206095ec3..a340492b4 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.Tight_inf_loop.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Tight_inf_loop.fst
@@ -6,7 +6,7 @@ open FStar.Mul
 let main (_: Prims.unit) : Prims.unit =
   if false
   then
-    Rust_primitives.Hax.never_to_any ((Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+    Rust_primitives.Hax.never_to_any ((Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
             "{\n loop {\n Tuple0\n }\n }"
           <:
           Prims.unit),
diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.While_.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.While_.fst
index 8fbcd694b..663761076 100644
--- a/rustc-coverage-tests/snapshots/fstar/Coverage.While_.fst
+++ b/rustc-coverage-tests/snapshots/fstar/Coverage.While_.fst
@@ -5,7 +5,7 @@ open FStar.Mul
 
 let main (_: Prims.unit) : (Prims.unit & Prims.unit) =
   let num:i32 = mk_i32 9 in
-  Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+  Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
     "{\n while rust_primitives::hax::machine_int::ge(num, 10) {\n Tuple0\n }\n }",
   ()
   <: