diff --git a/creusot-contracts-proc/src/invariant.rs b/creusot-contracts-proc/src/invariant.rs
index b6298f5773..e01775c410 100644
--- a/creusot-contracts-proc/src/invariant.rs
+++ b/creusot-contracts-proc/src/invariant.rs
@@ -1,125 +1,148 @@
 use crate::pretyping;
 use proc_macro2::{Span, TokenStream};
-use quote::{quote_spanned, ToTokens};
+use quote::{quote, quote_spanned, ToTokens};
 use syn::{
-    parse_quote_spanned, spanned::Spanned, AttrStyle, Attribute, Error, Expr, ExprForLoop,
-    ExprLoop, ExprWhile, Ident, Meta, Result,
+    parse_quote_spanned, spanned::Spanned, token::Brace, AttrStyle, Attribute, Block, Error, Expr,
+    ExprForLoop, ExprLoop, ExprWhile, Ident, ItemFn, Meta, Result, Stmt, Token,
 };
 
+#[derive(Debug)]
+enum Tag {
+    Invariant,
+    Variant,
+}
+
 #[derive(Debug)]
 struct Invariant {
+    tag: Tag,
     span: Span,
-    invariant: pearlite_syn::Term,
+    term: pearlite_syn::Term,
     expl: String,
 }
 
 impl ToTokens for Invariant {
     fn to_tokens(&self, tokens: &mut TokenStream) {
         let span = self.span;
+        let term = pretyping::encode_term(&self.term).unwrap_or_else(|e| e.into_tokens());
         let expl = &self.expl;
-        let inv_body = pretyping::encode_term(&self.invariant).unwrap_or_else(|e| e.into_tokens());
-
-        tokens.extend(quote_spanned! {span=>
-            #[allow(unused_must_use)]
-            let _ = {
-                #[creusot::no_translate]
-                #[creusot::spec]
-                #[creusot::spec::invariant = #expl]
-                ||{ #inv_body }
-            };
-        })
+        match self.tag {
+            Tag::Invariant => tokens.extend(quote_spanned! {span=>
+                #[allow(unused_must_use)]
+                let _ = {
+                    #[creusot::no_translate]
+                    #[creusot::spec]
+                    #[creusot::spec::invariant = #expl]
+                    ||{ #term } };
+            }),
+            Tag::Variant => tokens.extend(quote_spanned! {span=>
+                #[allow(unused_must_use)]
+                let _ =
+                    #[creusot::no_translate]
+                    #[creusot::spec]
+                    #[creusot::spec::variant::loop_]
+                    ||{ ::creusot_contracts::__stubs::variant_check(#term) };
+            }),
+        }
     }
 }
 
-enum LoopKind {
-    For(ExprForLoop),
-    While(ExprWhile),
-    Loop(ExprLoop),
+pub fn desugar_invariant(invariant0: TokenStream, expr: TokenStream) -> Result<TokenStream> {
+    desugar(Tag::Invariant, invariant0, expr)
 }
 
-pub struct Loop {
-    span: Span,
-    invariants: Vec<Invariant>,
-    kind: LoopKind,
-}
-
-fn filter_invariants(attrs: &mut Vec<Attribute>) -> Vec<Attribute> {
-    attrs
-        .extract_if(|attr| attr.path().get_ident().map(|i| i == "invariant").unwrap_or(false))
-        .collect()
+fn desugar(tag: Tag, invariant0: TokenStream, expr: TokenStream) -> Result<TokenStream> {
+    let expr: Expr = syn::parse2(expr)?;
+    let invariants = |attrs| filter_invariants(tag, invariant0, attrs);
+    match expr {
+        Expr::ForLoop(mut expr) => Ok(desugar_for(invariants(&mut expr.attrs)?, expr)),
+        Expr::While(mut expr) => Ok(desugar_while(invariants(&mut expr.attrs)?, expr)),
+        Expr::Loop(mut expr) => Ok(desugar_loop(invariants(&mut expr.attrs)?, expr)),
+        _ => {
+            return Err(Error::new_spanned(
+                expr,
+                "invariants must be attached to either a `for`, `loop` or `while`",
+            ))
+        }
+    }
 }
 
 // Set the expl before pushing the invariant into the vector
 fn parse_push_invariant(
     invariants: &mut Vec<Invariant>,
-    invariant: TokenStream,
+    tag: Tag,
+    term: TokenStream,
     numbering: bool,
 ) -> Result<()> {
-    let span = invariant.span();
-    let invariant = syn::parse2(invariant)?;
+    let span = term.span();
+    let term = syn::parse2(term)?;
     let expl = if numbering {
         format! {"expl:loop invariant #{}", invariants.len()}
     } else {
         "expl:loop invariant".to_string()
     };
-    invariants.push(Invariant { span, invariant, expl });
+    invariants.push(Invariant { tag, span, term, expl });
     Ok(())
 }
 
-pub fn parse(invariant: TokenStream, loopb: TokenStream) -> Result<Loop> {
-    let body: Expr = syn::parse2(loopb)?;
-    let span = body.span();
-    let (attrs, lkind) = match body {
-        Expr::ForLoop(mut floop) => (filter_invariants(&mut floop.attrs), LoopKind::For(floop)),
-        Expr::While(mut wloop) => (filter_invariants(&mut wloop.attrs), LoopKind::While(wloop)),
-        Expr::Loop(mut lloop) => (filter_invariants(&mut lloop.attrs), LoopKind::Loop(lloop)),
-        _ => {
-            return Err(Error::new_spanned(
-                body,
-                "invariants must be attached to either a `for`, `loop` or `while`",
-            ))
-        }
-    };
-
+fn filter_invariants(
+    tag: Tag,
+    invariant: TokenStream,
+    attrs: &mut Vec<Attribute>,
+) -> Result<Vec<Invariant>> {
     let mut invariants = Vec::new();
-    parse_push_invariant(&mut invariants, invariant, attrs.len() > 0)?;
+    parse_push_invariant(&mut invariants, tag, invariant, attrs.len() > 0)?;
 
+    let attrs = attrs.extract_if(|attr| {
+        attr.path().get_ident().map(|i| i == "invariant" || i == "variant").unwrap_or(false)
+    });
     for attr in attrs {
+        let i = if attr.path().get_ident().map(|i| i == "invariant").unwrap_or(false) {
+            Tag::Invariant
+        } else {
+            Tag::Variant
+        };
         if let Meta::List(l) = attr.meta {
-            parse_push_invariant(&mut invariants, l.tokens, true)?;
+            parse_push_invariant(&mut invariants, i, l.tokens, true)?;
         } else {
             return Err(Error::new_spanned(attr, "expected #[invariant(...)]"));
         }
     }
-
-    Ok(Loop { invariants, span, kind: lkind })
+    Ok(invariants)
 }
 
-pub fn lower(loop_: Loop) -> TokenStream {
-    let invariants = loop_.invariants;
-    match loop_.kind {
-        LoopKind::For(floop) => desugar_for(invariants, floop),
-        LoopKind::While(l) => {
-            let mut tokens = TokenStream::new();
-            for i in invariants {
-                i.to_tokens(&mut tokens);
-            }
-            let sp = loop_.span;
-            quote_spanned! {sp=>{
-                #tokens
-                #l
-            }}
-        }
-        LoopKind::Loop(l) => {
-            let sp = loop_.span;
-            quote_spanned! {sp=> {
-                #(#invariants)*
-                #l
-            }}
+fn while_to_loop(w: ExprWhile) -> ExprLoop {
+    let sp = w.span();
+    let body = w.body;
+    let body = match *w.cond {
+        Expr::Let(expr_let) => {
+            quote_spanned! {sp=> #[allow(irrefutable_let_patterns)] if #expr_let #body else { break; } }
         }
+        cond => quote_spanned! {sp=> if #cond #body else { break; } },
+    };
+    let body =
+        Block { brace_token: Brace(sp), stmts: vec![Stmt::Expr(Expr::Verbatim(body), None)] };
+    ExprLoop {
+        attrs: w.attrs,
+        label: w.label,
+        loop_token: Token![loop](w.while_token.span),
+        body: body,
     }
 }
 
+fn desugar_while(invariants: Vec<Invariant>, w: ExprWhile) -> TokenStream {
+    desugar_loop(invariants, while_to_loop(w))
+}
+
+fn desugar_loop(invariants: Vec<Invariant>, mut l: ExprLoop) -> TokenStream {
+    let span = l.loop_token.span;
+    l.body.stmts.insert(0, Stmt::Expr(Expr::Verbatim(quote! { #(#invariants)* }), None));
+    quote_spanned! {span=> {
+      #[allow(unused_must_use)]
+      let _ = { #[creusot::no_translate] #[creusot::before_loop] || {} };
+      #l
+    }}
+}
+
 // Lowers for loops to `loop` and inserts the structural invariant that we get 'for free'
 fn desugar_for(mut invariants: Vec<Invariant>, f: ExprForLoop) -> TokenStream {
     let lbl = f.label;
@@ -135,8 +158,9 @@ fn desugar_for(mut invariants: Vec<Invariant>, f: ExprForLoop) -> TokenStream {
 
     invariants.insert(0,
         Invariant {
+            tag: Tag::Invariant,
             span: for_span,
-            invariant: parse_quote_spanned! {for_span=> ::creusot_contracts::std::iter::Iterator::produces(#iter_old.inner(), #produced.inner(), #it) },
+            term: parse_quote_spanned! {for_span=> ::creusot_contracts::std::iter::Iterator::produces(#iter_old.inner(), #produced.inner(), #it) },
             expl: "expl:for invariant".to_string(),
         },
     );
@@ -144,16 +168,18 @@ fn desugar_for(mut invariants: Vec<Invariant>, f: ExprForLoop) -> TokenStream {
     invariants.insert(
         0,
         Invariant {
+            tag: Tag::Invariant,
             span: for_span,
-            invariant: parse_quote_spanned! {for_span=> ::creusot_contracts::invariant::inv(#it) },
+            term: parse_quote_spanned! {for_span=> ::creusot_contracts::invariant::inv(#it) },
             expl: "expl:for invariant".to_string(),
         },
     );
 
     invariants.insert(0,
         Invariant {
+            tag: Tag::Invariant,
             span: for_span,
-            invariant: parse_quote_spanned! {for_span=> ::creusot_contracts::invariant::inv(*#produced) },
+            term: parse_quote_spanned! {for_span=> ::creusot_contracts::invariant::inv(*#produced) },
             expl: "expl:for invariant".to_string(),
         },
     );
@@ -172,11 +198,12 @@ fn desugar_for(mut invariants: Vec<Invariant>, f: ExprForLoop) -> TokenStream {
         let mut #it = ::std::iter::IntoIterator::into_iter(#iter);
         let #iter_old = snapshot! { #it };
         let mut #produced = snapshot! { ::creusot_contracts::logic::Seq::EMPTY };
-        #(#invariants)*
+        let _ = { #[creusot::before_loop] || {} };
         #(#outer)*
         #lbl
         loop {
             #(#inner)*
+            #(#invariants)*
             match ::std::iter::Iterator::next(&mut #it) {
                 Some(#elem) => {
                     #[allow(unused_assignments)]
@@ -189,3 +216,42 @@ fn desugar_for(mut invariants: Vec<Invariant>, f: ExprForLoop) -> TokenStream {
         }
     } }
 }
+
+pub(crate) fn desugar_variant(attr: TokenStream, tokens: TokenStream) -> Result<TokenStream> {
+    match syn::parse2(tokens.clone()) {
+        Ok(f) => desugar_variant_fn(attr, f),
+        _ => desugar(Tag::Variant, attr, tokens),
+    }
+}
+
+fn variant_to_tokens(span: Span, p: &pearlite_syn::Term) -> (String, TokenStream) {
+    let var_name = crate::generate_unique_ident("variant");
+    let var_body = pretyping::encode_term(p).unwrap_or_else(|e| {
+        return e.into_tokens();
+    });
+    let name_tag = format!("{}", var_name);
+
+    let variant_tokens = quote_spanned! {span=>
+        #[allow(unused_must_use)]
+        let _ =
+            #[creusot::no_translate]
+            #[creusot::item=#name_tag]
+            #[creusot::spec::variant]
+            #[creusot::spec]
+            ||{ ::creusot_contracts::__stubs::variant_check(#var_body) }
+        ;
+    };
+    (name_tag, variant_tokens)
+}
+
+fn desugar_variant_fn(attr: TokenStream, mut f: ItemFn) -> Result<TokenStream> {
+    let span = attr.span();
+    let p = syn::parse2(attr)?;
+    let (name_tag, variant_tokens) = variant_to_tokens(span, &p);
+
+    f.block.stmts.insert(0, Stmt::Item(syn::Item::Verbatim(variant_tokens)));
+    Ok(quote! {
+        #[creusot::clause::variant=#name_tag]
+        #f
+    })
+}
diff --git a/creusot-contracts-proc/src/lib.rs b/creusot-contracts-proc/src/lib.rs
index a5a1a36d8b..c165cc70ce 100644
--- a/creusot-contracts-proc/src/lib.rs
+++ b/creusot-contracts-proc/src/lib.rs
@@ -8,7 +8,7 @@ use proc_macro2::{Span, TokenStream};
 use quote::{quote, quote_spanned, ToTokens, TokenStreamExt};
 use std::iter;
 use syn::{
-    parse::{discouraged::Speculative, Parse, Result},
+    parse::{Parse, Result},
     spanned::Spanned,
     *,
 };
@@ -43,7 +43,7 @@ impl<'a> FilterAttrs<'a> for &'a [Attribute] {
     }
 }
 
-fn generate_unique_ident(prefix: &str) -> Ident {
+pub(crate) fn generate_unique_ident(prefix: &str) -> Ident {
     let uuid = uuid::Uuid::new_v4();
     let ident = format!("{}_{}", prefix, uuid).replace('-', "_");
 
@@ -311,72 +311,11 @@ pub fn ensures(attr: TS1, tokens: TS1) -> TS1 {
     }
 }
 
-enum VariantAnnotation {
-    Fn(ItemFn),
-    WhileLoop(ExprWhile),
-}
-
-impl syn::parse::Parse for VariantAnnotation {
-    fn parse(input: parse::ParseStream) -> Result<Self> {
-        let fork = input.fork();
-        if let Ok(f) = fork.parse() {
-            input.advance_to(&fork);
-            Ok(VariantAnnotation::Fn(f))
-        } else if let Ok(w) = input.parse() {
-            Ok(VariantAnnotation::WhileLoop(w))
-        } else {
-            Err(Error::new(Span::call_site(), "TEST?"))
-        }
-    }
-}
-
 #[proc_macro_attribute]
 pub fn variant(attr: TS1, tokens: TS1) -> TS1 {
-    match variant_inner(attr, tokens) {
-        Ok(r) => r,
-        Err(err) => return TS1::from(err.to_compile_error()),
-    }
-}
-
-fn variant_inner(attr: TS1, tokens: TS1) -> Result<TS1> {
-    let p: pearlite_syn::Term = parse(attr)?;
-
-    let tgt: VariantAnnotation = parse(tokens)?;
-
-    let var_name = generate_unique_ident("variant");
-
-    let var_body = pretyping::encode_term(&p).unwrap_or_else(|e| {
-        return e.into_tokens();
-    });
-    let name_tag = format!("{}", quote! { #var_name });
-
-    let variant_attr = match tgt {
-        VariantAnnotation::Fn(_) => quote! { #[creusot::spec::variant] },
-        VariantAnnotation::WhileLoop(_) => quote! { #[creusot::spec::variant::loop_] },
-    };
-    let variant_tokens = quote! {
-        #[allow(unused_must_use)]
-        let _ =
-            #[creusot::no_translate]
-            #[creusot::item=#name_tag]
-            #variant_attr
-            #[creusot::spec]
-            ||{ ::creusot_contracts::__stubs::variant_check(#var_body) }
-        ;
-    };
-
-    match tgt {
-        VariantAnnotation::Fn(mut f) => {
-            f.block.stmts.insert(0, Stmt::Item(Item::Verbatim(variant_tokens)));
-            Ok(TS1::from(quote! {
-              #[creusot::clause::variant=#name_tag]
-              #f
-            }))
-        }
-        VariantAnnotation::WhileLoop(w) => Ok(TS1::from(quote! {
-          { #variant_tokens; #w }
-        })),
-    }
+    invariant::desugar_variant(attr.into(), tokens.into())
+        .unwrap_or_else(|e| e.to_compile_error())
+        .into()
 }
 
 struct Assertion(Vec<TermStmt>);
@@ -755,12 +694,10 @@ pub fn maintains(attr: TS1, body: TS1) -> TS1 {
 }
 
 #[proc_macro_attribute]
-pub fn invariant(invariant: TS1, loopb: TS1) -> TS1 {
-    let loop_ = match invariant::parse(invariant.into(), loopb.into()) {
-        Ok(l) => l,
-        Err(e) => return e.to_compile_error().into(),
-    };
-    invariant::lower(loop_).into()
+pub fn invariant(invariant: TS1, tokens: TS1) -> TS1 {
+    invariant::desugar_invariant(invariant.into(), tokens.into())
+        .unwrap_or_else(|e| e.to_compile_error())
+        .into()
 }
 
 #[proc_macro_attribute]
diff --git a/creusot/src/backend/program.rs b/creusot/src/backend/program.rs
index 543caa9a5a..05848092b1 100644
--- a/creusot/src/backend/program.rs
+++ b/creusot/src/backend/program.rs
@@ -949,7 +949,7 @@ impl<'tcx> Statement<'tcx> {
                 istmts.extend([IntermediateStmt::Assume(exp)]);
             }
             Statement::Assertion { cond, msg } => istmts.push(IntermediateStmt::Assert(Exp::Attr(
-                Attribute::Attr(format!("expl:{msg}")),
+                Attribute::Attr(msg),
                 Box::new(lower_pure(lower.ctx, lower.names, &cond)),
             ))),
             Statement::AssertTyInv { pl } => {
diff --git a/creusot/src/contracts_items/attributes.rs b/creusot/src/contracts_items/attributes.rs
index 5e8fd68648..b4a9bd8f22 100644
--- a/creusot/src/contracts_items/attributes.rs
+++ b/creusot/src/contracts_items/attributes.rs
@@ -42,6 +42,7 @@ attribute_functions! {
     [creusot::spec::invariant]               => is_invariant
     [creusot::spec::variant]                 => is_variant
     [creusot::spec::variant::loop_]          => is_loop_variant
+    [creusot::before_loop]                   => is_before_loop
     [creusot::spec::assert]                  => is_assertion
     [creusot::spec::snapshot]                => is_snapshot_closure
     [creusot::ghost]                         => is_ghost_closure
diff --git a/creusot/src/ctx.rs b/creusot/src/ctx.rs
index b0720aa81c..1f0199bf4c 100644
--- a/creusot/src/ctx.rs
+++ b/creusot/src/ctx.rs
@@ -327,6 +327,10 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
         self.tcx.dcx().struct_span_err(span, msg.to_string())
     }
 
+    pub(crate) fn warn(&self, span: Span, msg: impl Into<String>) {
+        self.tcx.dcx().span_warn(span, msg.into())
+    }
+
     queryish!(laws, &[DefId], laws_inner);
 
     // TODO Make private
diff --git a/creusot/src/gather_spec_closures.rs b/creusot/src/gather_spec_closures.rs
index a946ed15fa..a6f009e6b2 100644
--- a/creusot/src/gather_spec_closures.rs
+++ b/creusot/src/gather_spec_closures.rs
@@ -1,10 +1,11 @@
 use crate::{
-    contracts_items::{get_invariant_expl, is_assertion, is_loop_variant, is_snapshot_closure},
+    contracts_items::{
+        get_invariant_expl, is_assertion, is_before_loop, is_loop_variant, is_snapshot_closure,
+    },
     ctx::TranslationCtx,
     pearlite::Term,
 };
 use indexmap::{IndexMap, IndexSet};
-use rustc_data_structures::graph::Successors;
 use rustc_hir::def_id::DefId;
 use rustc_middle::{
     mir::{visit::Visitor, AggregateKind, BasicBlock, Body, Location, Operand, Rvalue},
@@ -83,22 +84,80 @@ impl<'tcx> Visitor<'tcx> for Closures<'tcx> {
     }
 }
 
-struct Invariants<'tcx> {
-    tcx: TyCtxt<'tcx>,
-    invariants: IndexMap<Location, (DefId, LoopSpecKind)>,
+pub(crate) struct Invariants<'tcx> {
+    pub(crate) loop_headers: IndexMap<BasicBlock, Vec<(LoopSpecKind, Term<'tcx>)>>,
+    /// Invariants for which we couldn't find a loop header are translated as assertions.
+    pub(crate) assertions: IndexMap<DefId, (Term<'tcx>, String)>,
 }
 
-impl<'tcx> Visitor<'tcx> for Invariants<'tcx> {
+struct InvariantsVisitor<'a, 'tcx> {
+    ctx: &'a mut TranslationCtx<'tcx>,
+    body: &'a Body<'tcx>,
+    before_loop: IndexSet<BasicBlock>,
+    invariants: Invariants<'tcx>,
+}
+
+impl<'a, 'tcx> InvariantsVisitor<'a, 'tcx> {
+    // Search backwards for the loop header: it should have more than one predecessor.
+    fn find_loop_header(&self, loc: Location) -> Option<BasicBlock> {
+        let mut block = loc.block;
+        if self.before_loop.contains(&block) {
+            // Reached "before_loop" marker in the same block.
+            // This assumes that statements are visited in order, so that if a block
+            // contains both invariants and a "before_block" marker, the marker is not
+            // in the `before_loop` set when we visit invariants before it.
+            return None;
+        }
+        loop {
+            let preds = &self.body.basic_blocks.predecessors()[block];
+            if preds.len() > 1 {
+                return Some(block);
+            }
+            let Some(pred) = preds.get(0) else {
+                // Reached the top of the function. Impossible.
+                panic!("The impossible happened: Missing 'before_loop' marker.");
+            };
+            if self.before_loop.contains(pred) {
+                // Reached "before_loop" marker.
+                return None;
+            }
+            block = *pred;
+        }
+    }
+}
+
+impl<'a, 'tcx> Visitor<'tcx> for InvariantsVisitor<'a, 'tcx> {
     fn visit_rvalue(&mut self, rvalue: &Rvalue<'tcx>, loc: Location) {
         if let Rvalue::Aggregate(box AggregateKind::Closure(id, _), _) = rvalue {
-            let kind = if let Some(expl) = get_invariant_expl(self.tcx, *id) {
+            let kind = if let Some(expl) = get_invariant_expl(self.ctx.tcx, *id) {
                 LoopSpecKind::Invariant(expl)
-            } else if is_loop_variant(self.tcx, *id) {
+            } else if is_loop_variant(self.ctx.tcx, *id) {
                 LoopSpecKind::Variant
             } else {
+                if is_before_loop(self.ctx.tcx, *id) {
+                    self.before_loop.insert(loc.block);
+                }
                 return;
             };
-            self.invariants.insert(loc, (*id, kind));
+            let term = self.ctx.term(*id).unwrap().clone();
+            match self.find_loop_header(loc) {
+                None if let LoopSpecKind::Invariant(expl) = kind => {
+                    self.ctx.warn(
+                        self.ctx.def_span(id),
+                        "This loop does not loop. This invariant could just be an assertion.",
+                    );
+                    let assertions = &mut self.invariants.assertions;
+                    assertions.insert(*id, (term, expl));
+                }
+                None => self.ctx.warn(
+                    self.ctx.def_span(id),
+                    "This loop does not loop. This variant will be ignored.",
+                ),
+                Some(target) => {
+                    let loop_headers = &mut self.invariants.loop_headers;
+                    loop_headers.entry(target).or_insert_with(Vec::new).push((kind, term))
+                }
+            }
         }
         self.super_rvalue(rvalue, loc);
     }
@@ -108,41 +167,13 @@ impl<'tcx> Visitor<'tcx> for Invariants<'tcx> {
 pub(crate) fn corrected_invariant_names_and_locations<'tcx>(
     ctx: &mut TranslationCtx<'tcx>,
     body: &Body<'tcx>,
-) -> IndexMap<BasicBlock, Vec<(LoopSpecKind, Term<'tcx>)>> {
-    let mut results = IndexMap::new();
-
-    let mut invs_gather = Invariants { tcx: ctx.tcx, invariants: IndexMap::new() };
+) -> Invariants<'tcx> {
+    let mut invs_gather = InvariantsVisitor {
+        ctx,
+        body,
+        before_loop: IndexSet::new(),
+        invariants: Invariants { loop_headers: IndexMap::new(), assertions: IndexMap::new() },
+    };
     invs_gather.visit_body(body);
-
-    for (loc, (clos, kind)) in invs_gather.invariants.into_iter() {
-        let mut target: BasicBlock = loc.block;
-
-        loop {
-            let mut succs = body.basic_blocks.successors(target);
-
-            target = succs.next().unwrap();
-
-            // Check if `taget_block` is a loop header by testing if it dominates
-            // one of its predecessors.
-            if let Some(preds) = body.basic_blocks.predecessors().get(target) {
-                let is_loop_header = preds
-                    .iter()
-                    .any(|pred| body.basic_blocks.dominators().dominates(target, *pred));
-
-                if is_loop_header {
-                    break;
-                }
-            };
-
-            // If we've hit a switch then stop trying to push the invariants down.
-            if body[target].terminator().kind.as_switch().is_some() {
-                panic!("Could not find loop header")
-            }
-        }
-
-        let term = ctx.term(clos).unwrap().clone();
-        results.entry(target).or_insert_with(Vec::new).push((kind, term));
-    }
-
-    results
+    invs_gather.invariants
 }
diff --git a/creusot/src/translation/function.rs b/creusot/src/translation/function.rs
index 0e666056b7..b3601fa6dd 100644
--- a/creusot/src/translation/function.rs
+++ b/creusot/src/translation/function.rs
@@ -81,7 +81,8 @@ struct BodyTranslator<'a, 'tcx> {
     fresh_id: usize,
 
     invariants: IndexMap<BasicBlock, Vec<(LoopSpecKind, Term<'tcx>)>>,
-
+    /// Invariants to translate as assertions.
+    invariant_assertions: IndexMap<DefId, (Term<'tcx>, String)>,
     /// Map of the `proof_assert!` blocks to their translated version.
     assertions: IndexMap<DefId, Term<'tcx>>,
     /// Map of the `snapshot!` blocks to their translated version.
@@ -167,7 +168,8 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
             past_blocks: Default::default(),
             ctx,
             fresh_id: body.basic_blocks.len(),
-            invariants,
+            invariants: invariants.loop_headers,
+            invariant_assertions: invariants.assertions,
             assertions,
             snapshots,
             is_ghost_closure: is_ghost_closure(tcx, body_id.def_id()),
diff --git a/creusot/src/translation/function/statement.rs b/creusot/src/translation/function/statement.rs
index 9ba586290b..86724a0664 100644
--- a/creusot/src/translation/function/statement.rs
+++ b/creusot/src/translation/function/statement.rs
@@ -1,7 +1,9 @@
 use super::BodyTranslator;
 use crate::{
     analysis::NotFinalPlaces,
-    contracts_items::{is_assertion, is_invariant, is_snapshot_closure, is_spec, is_variant},
+    contracts_items::{
+        is_assertion, is_before_loop, is_invariant, is_snapshot_closure, is_spec, is_variant,
+    },
     extended_location::ExtendedLocation,
     fmir::Operand,
     translation::{
@@ -143,8 +145,26 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
                         RValue::Constructor(variant, subst, fields)
                     }
                     Closure(def_id, subst) => {
-                        if is_invariant(self.tcx(), *def_id) || is_variant(self.tcx(), *def_id) {
+                        if is_variant(self.tcx(), *def_id) || is_before_loop(self.tcx(), *def_id) {
                             return;
+                        } else if is_invariant(self.tcx(), *def_id) {
+                            match self.invariant_assertions.remove(def_id) {
+                                None => return,
+                                Some((mut assertion, expl)) => {
+                                    assertion.subst(&inv_subst(
+                                        self.tcx(),
+                                        &self.body,
+                                        &self.locals,
+                                        si,
+                                    ));
+                                    self.check_frozen_in_logic(&assertion, loc);
+                                    self.emit_statement(fmir::Statement::Assertion {
+                                        cond: assertion,
+                                        msg: expl,
+                                    });
+                                    return;
+                                }
+                            }
                         } else if is_assertion(self.tcx(), *def_id) {
                             let mut assertion = self
                                 .assertions
@@ -154,7 +174,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
                             self.check_frozen_in_logic(&assertion, loc);
                             self.emit_statement(fmir::Statement::Assertion {
                                 cond: assertion,
-                                msg: "assertion".to_owned(),
+                                msg: "expl:assertion".to_owned(),
                             });
                             return;
                         } else if is_spec(self.tcx(), *def_id) {
diff --git a/creusot/src/translation/function/terminator.rs b/creusot/src/translation/function/terminator.rs
index 2370d60afc..c479a50a95 100644
--- a/creusot/src/translation/function/terminator.rs
+++ b/creusot/src/translation/function/terminator.rs
@@ -410,11 +410,11 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
 
     fn get_explanation(&mut self, msg: &mir::AssertKind<Operand<'tcx>>) -> String {
         match msg {
-            AssertKind::BoundsCheck { len: _, index: _ } => format!("index in bounds"),
-            AssertKind::Overflow(op, _a, _b) => format!("{op:?} overflow"),
-            AssertKind::OverflowNeg(_op) => format!("negation overflow"),
-            AssertKind::DivisionByZero(_) => format!("division by zero"),
-            AssertKind::RemainderByZero(_) => format!("remainder by zero"),
+            AssertKind::BoundsCheck { len: _, index: _ } => format!("expl:index in bounds"),
+            AssertKind::Overflow(op, _a, _b) => format!("expl:{op:?} overflow"),
+            AssertKind::OverflowNeg(_op) => format!("expl:negation overflow"),
+            AssertKind::DivisionByZero(_) => format!("expl:division by zero"),
+            AssertKind::RemainderByZero(_) => format!("expl:remainder by zero"),
             _ => unreachable!("Resume assertions"),
         }
     }