diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml
index 2f346fa35..9b9b9c192 100644
--- a/charon-ml/src/CharonVersion.ml
+++ b/charon-ml/src/CharonVersion.ml
@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.198"
+let supported_charon_version = "0.1.199"
diff --git a/charon-ml/src/PrintFmt.ml b/charon-ml/src/PrintFmt.ml
index ad51c9164..b0db01a9b 100644
--- a/charon-ml/src/PrintFmt.ml
+++ b/charon-ml/src/PrintFmt.ml
@@ -1376,6 +1376,9 @@ let pp_assertion (env : fmt_env) (fmt : Format.formatter) (a : assertion) : unit
         " (misaligned_pointer_dereference)"
     | Some NullPointerDereference -> " (null_pointer_dereference)"
     | Some (InvalidEnumConstruction _) -> " (invalid_enum_construction)"
+    | Some ResumedAfterReturn -> " (resumed_after_return)"
+    | Some ResumedAfterPanic -> " (resumed_after_panic)"
+    | Some ResumedAfterDrop -> " (resumed_after_drop)"
   in
   Format.fprintf fmt "assert(%s == %s)%s"
     (operand_to_string env a.cond)
diff --git a/charon-ml/src/generated/Generated_GAst.ml b/charon-ml/src/generated/Generated_GAst.ml
index 823c8dccb..82c6a493a 100644
--- a/charon-ml/src/generated/Generated_GAst.ml
+++ b/charon-ml/src/generated/Generated_GAst.ml
@@ -76,6 +76,9 @@ and builtin_assert_kind =
           - [found] *)
   | NullPointerDereference
   | InvalidEnumConstruction of operand
+  | ResumedAfterReturn
+  | ResumedAfterPanic
+  | ResumedAfterDrop
 
 and call = { func : fn_operand; args : operand list; dest : place }
 and copy_non_overlapping = { src : operand; dst : operand; count : operand }
diff --git a/charon-ml/src/generated/Generated_OfJson.ml b/charon-ml/src/generated/Generated_OfJson.ml
index a265d1347..e166ec8b2 100644
--- a/charon-ml/src/generated/Generated_OfJson.ml
+++ b/charon-ml/src/generated/Generated_OfJson.ml
@@ -265,6 +265,9 @@ and builtin_assert_kind_of_json (ctx : of_json_ctx) (js : json) :
           operand_of_json ctx invalid_enum_construction
         in
         Ok (InvalidEnumConstruction invalid_enum_construction)
+    | `String "ResumedAfterReturn" -> Ok ResumedAfterReturn
+    | `String "ResumedAfterPanic" -> Ok ResumedAfterPanic
+    | `String "ResumedAfterDrop" -> Ok ResumedAfterDrop
     | _ -> Error "")
 
 and builtin_fun_id_of_json (ctx : of_json_ctx) (js : json) :
diff --git a/charon-ml/src/generated/Generated_OfPostcard.ml b/charon-ml/src/generated/Generated_OfPostcard.ml
index 28af2042e..c277c29aa 100644
--- a/charon-ml/src/generated/Generated_OfPostcard.ml
+++ b/charon-ml/src/generated/Generated_OfPostcard.ml
@@ -243,6 +243,9 @@ and builtin_assert_kind_of_postcard (ctx : of_postcard_ctx)
      | 7 ->
          let* x_0 = operand_of_postcard ctx st in
          Ok (InvalidEnumConstruction x_0)
+     | 8 -> Ok ResumedAfterReturn
+     | 9 -> Ok ResumedAfterPanic
+     | 10 -> Ok ResumedAfterDrop
      | _ -> Error ("unknown enum variant tag: " ^ string_of_int __tag))
 
 and builtin_fun_id_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
diff --git a/charon/Cargo.lock b/charon/Cargo.lock
index 4dbd94a02..efeee5eb9 100644
--- a/charon/Cargo.lock
+++ b/charon/Cargo.lock
@@ -252,7 +252,7 @@ checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268"
 
 [[package]]
 name = "charon"
-version = "0.1.198"
+version = "0.1.199"
 dependencies = [
  "annotate-snippets",
  "anstream",
diff --git a/charon/Cargo.toml b/charon/Cargo.toml
index 363467cb7..c246d78cb 100644
--- a/charon/Cargo.toml
+++ b/charon/Cargo.toml
@@ -24,7 +24,7 @@ tracing = { version = "0.1", features = ["max_level_trace"] }
 
 [package]
 name = "charon"
-version = "0.1.198"
+version = "0.1.199"
 authors.workspace = true
 edition.workspace = true
 license.workspace = true
diff --git a/charon/src/ast/gast.rs b/charon/src/ast/gast.rs
index 3e0106f84..c54e7a4b1 100644
--- a/charon/src/ast/gast.rs
+++ b/charon/src/ast/gast.rs
@@ -494,6 +494,9 @@ pub enum BuiltinAssertKind {
     MisalignedPointerDereference { required: Operand, found: Operand },
     NullPointerDereference,
     InvalidEnumConstruction(Operand),
+    ResumedAfterReturn,
+    ResumedAfterPanic,
+    ResumedAfterDrop,
 }
 
 /// (U)LLBC is a language with side-effects: a statement may abort in a way that isn't tracked by
diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs
index 617732a8a..d4cd0fb5f 100644
--- a/charon/src/pretty/fmt_with_ctx.rs
+++ b/charon/src/pretty/fmt_with_ctx.rs
@@ -98,6 +98,9 @@ impl<C: AstFormatter> FmtWithCtx<C> for BuiltinAssertKind {
             BuiltinAssertKind::InvalidEnumConstruction(..) => {
                 write!(f, "invalid_enum_construction")
             }
+            BuiltinAssertKind::ResumedAfterReturn => write!(f, "resumed_after_return"),
+            BuiltinAssertKind::ResumedAfterDrop => write!(f, "resumed_after_drop"),
+            BuiltinAssertKind::ResumedAfterPanic => write!(f, "resumed_after_panic"),
         }
     }
 }