diff --git a/charon/src/bin/charon-driver/driver.rs b/charon/src/bin/charon-driver/driver.rs
index 08886865..63bd69f3 100644
--- a/charon/src/bin/charon-driver/driver.rs
+++ b/charon/src/bin/charon-driver/driver.rs
@@ -256,7 +256,7 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa
     }
 
     // Update the error count
-    internal.error_count = transform_ctx.errors.error_count;
+    internal.error_count = transform_ctx.errors.borrow().error_count;
 
     export::CrateData::new(&transform_ctx)
 }
diff --git a/charon/src/bin/charon-driver/translate/translate_constants.rs b/charon/src/bin/charon-driver/translate/translate_constants.rs
index c4602c2b..782f1955 100644
--- a/charon/src/bin/charon-driver/translate/translate_constants.rs
+++ b/charon/src/bin/charon-driver/translate/translate_constants.rs
@@ -86,7 +86,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 RawConstantExpr::Adt(vid, fields)
             }
             ConstantExprKind::Array { .. } => {
-                error_or_panic!(self, span, "array constants are not supported yet")
+                raise_error!(self, span, "array constants are not supported yet")
             }
             ConstantExprKind::Tuple { fields } => {
                 let fields: Vec<ConstantExpr> = fields
@@ -130,19 +130,19 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 RawConstantExpr::Ref(Box::new(be))
             }
             ConstantExprKind::Cast { .. } => {
-                error_or_panic!(
+                raise_error!(
                     self,
                     span,
-                    &format!("Unsupported constant: `ConstantExprKind::Cast {{..}}`",)
+                    "Unsupported constant: `ConstantExprKind::Cast {{..}}`",
                 )
             }
             ConstantExprKind::RawBorrow {
                 mutability: false, ..
             } => {
-                error_or_panic!(
+                raise_error!(
                     self,
                     span,
-                    &format!("Unsupported constant: `ConstantExprKind::RawBorrow {{mutability: false, ..}}`",)
+                    "Unsupported constant: `ConstantExprKind::RawBorrow {{mutability: false, ..}}`",
                 )
             }
             ConstantExprKind::RawBorrow {
@@ -173,7 +173,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             }
             ConstantExprKind::Todo(msg) => {
                 // Case not yet handled by hax
-                error_or_panic!(self, span, format!("Unsupported constant: {:?}", msg))
+                raise_error!(self, span, "Unsupported constant: {:?}", msg)
             }
         };
 
@@ -206,11 +206,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             | RawConstantExpr::Ref(_)
             | RawConstantExpr::MutPtr(_)
             | RawConstantExpr::FnPtr { .. } => {
-                error_or_panic!(
-                    self,
-                    span,
-                    format!("Unexpected constant generic: {:?}", value)
-                )
+                raise_error!(self, span, "Unexpected constant generic: {:?}", value)
             }
             RawConstantExpr::Var(v) => Ok(ConstGeneric::Var(v)),
         }
diff --git a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs
index 910e2579..301e14ae 100644
--- a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs
+++ b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs
@@ -6,6 +6,7 @@ use charon_lib::transform::TransformCtx;
 use hax_frontend_exporter as hax;
 use rustc_hir::def_id::DefId;
 use rustc_middle::ty::TyCtxt;
+use std::cell::RefCell;
 use std::path::PathBuf;
 
 impl<'tcx, 'ctx> TranslateCtx<'tcx> {
@@ -97,19 +98,22 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             | FullDefKind::TyParam { .. }
             | FullDefKind::Variant { .. } => {
                 let span = self.def_span(def_id);
-                self.span_err(
+                register_error!(
+                    self,
                     span,
-                    &format!(
-                        "Cannot register this item: `{def_id:?}` with kind `{:?}`",
-                        def.kind()
-                    ),
+                    "Cannot register this item: `{def_id:?}` with kind `{:?}`",
+                    def.kind()
                 );
             }
         }
     }
 
     pub(crate) fn translate_item(&mut self, item_src: TransItemSource, trans_id: AnyTransId) {
-        if self.errors.ignored_failed_decls.contains(&trans_id)
+        if self
+            .errors
+            .borrow()
+            .ignored_failed_decls
+            .contains(&trans_id)
             || self.translated.get_item(trans_id).is_some()
         {
             return;
@@ -119,12 +123,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             let span = ctx.def_span(rust_id);
             // Catch cycles
             let res = if ctx.translate_stack.contains(&trans_id) {
-                ctx.span_err(
+                register_error!(
+                    ctx,
                     span,
-                    &format!(
-                        "Cycle detected while translating {rust_id:?}! Stack: {:?}",
-                        &ctx.translate_stack
-                    ),
+                    "Cycle detected while translating {rust_id:?}! Stack: {:?}",
+                    &ctx.translate_stack
                 );
                 Err(())
             } else {
@@ -141,10 +144,10 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
                     Ok(Err(_)) => Err(()),
                     // Panic
                     Err(_) => {
-                        register_error_or_panic!(
+                        register_error!(
                             ctx,
                             span,
-                            format!("Thread panicked when extracting item `{rust_id:?}`.")
+                            "Thread panicked when extracting item `{rust_id:?}`."
                         );
                         Err(())
                     }
@@ -155,11 +158,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             };
 
             if res.is_err() {
-                ctx.span_err(
-                    span,
-                    &format!("Item `{rust_id:?}` caused errors; ignoring."),
-                );
-                ctx.errors.ignore_failed_decl(trans_id);
+                register_error!(ctx, span, "Item `{rust_id:?}` caused errors; ignoring.");
+                ctx.errors.borrow_mut().ignore_failed_decl(trans_id);
             }
         })
     }
@@ -215,9 +215,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         // Translate if not already translated.
         self.translate_item(item_source, id);
 
-        if self.errors.ignored_failed_decls.contains(&id) {
+        if self.errors.borrow().ignored_failed_decls.contains(&id) {
             let span = self.def_span(item_source.to_def_id());
-            error_or_panic!(self, span, format!("Failed to translate item {id:?}."))
+            raise_error!(self, span, "Failed to translate item {id:?}.")
         }
         Ok(self.translated.get_item(id).unwrap())
     }
@@ -255,7 +255,7 @@ pub fn translate<'tcx, 'ctx>(
         sysroot,
         hax_state,
         options: translate_options,
-        errors: error_ctx,
+        errors: RefCell::new(error_ctx),
         translated: TranslatedCrate {
             crate_name: requested_crate_name,
             options: options.clone(),
diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs
index 49c9ac6d..b7c55a9e 100644
--- a/charon/src/bin/charon-driver/translate/translate_ctx.rs
+++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs
@@ -14,17 +14,18 @@ use macros::VariantIndexArity;
 use rustc_hir::def_id::DefId;
 use rustc_middle::ty::TyCtxt;
 use std::borrow::Cow;
+use std::cell::RefCell;
 use std::cmp::Ord;
 use std::collections::HashMap;
 use std::collections::{BTreeMap, VecDeque};
-use std::fmt;
 use std::fmt::Debug;
 use std::path::{Component, PathBuf};
 use std::sync::Arc;
+use std::{fmt, mem};
 
 // Re-export to avoid having to fix imports.
 pub(crate) use charon_lib::errors::{
-    error_assert, error_or_panic, register_error_or_panic, DepSource, ErrorCtx,
+    error_assert, raise_error, register_error, DepSource, ErrorCtx,
 };
 
 /// TODO: maybe we should always target MIR Built, this would make things
@@ -55,8 +56,12 @@ impl TranslateOptions {
         let mut parse_pattern = |s: &str| match NamePattern::parse(s) {
             Ok(p) => Ok(p),
             Err(e) => {
-                let msg = format!("failed to parse pattern `{s}` ({e})");
-                error_or_panic!(error_ctx, &TranslatedCrate::default(), Span::dummy(), msg)
+                raise_error!(
+                    error_ctx,
+                    crate(&TranslatedCrate::default()),
+                    Span::dummy(),
+                    "failed to parse pattern `{s}` ({e})"
+                )
             }
         };
 
@@ -179,7 +184,7 @@ pub struct TranslateCtx<'tcx> {
     pub file_to_id: HashMap<FileName, FileId>,
 
     /// Context for tracking and reporting errors.
-    pub errors: ErrorCtx,
+    pub errors: RefCell<ErrorCtx>,
     /// The declarations we came accross and which we haven't translated yet. We keep them sorted
     /// to make the output order a bit more stable.
     pub items_to_translate: BTreeMap<TransItemSource, AnyTransId>,
@@ -366,23 +371,21 @@ where
     let unwind_safe_s = std::panic::AssertUnwindSafe(s);
     let unwind_safe_x = std::panic::AssertUnwindSafe(x);
     std::panic::catch_unwind(move || unwind_safe_x.sinto(*unwind_safe_s)).or_else(|_| {
-        error_or_panic!(
+        raise_error!(
             err,
-            krate,
+            crate(krate),
             span,
-            format!("Hax panicked when translating `{x:?}`.")
+            "Hax panicked when translating `{x:?}`."
         )
     })
 }
 
 impl<'tcx, 'ctx> TranslateCtx<'tcx> {
-    pub fn continue_on_failure(&self) -> bool {
-        self.errors.continue_on_failure()
-    }
-
     /// Span an error and register the error.
-    pub fn span_err(&mut self, span: Span, msg: &str) {
-        self.errors.span_err(&self.translated, span, msg)
+    pub fn span_err(&self, span: Span, msg: &str) -> Error {
+        self.errors
+            .borrow_mut()
+            .span_err(&self.translated, span, msg)
     }
 
     /// Register a file if it is a "real" file and was not already registered
@@ -471,10 +474,10 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             DefPathItem::Use => Some(PathElem::Ident("<use>".to_string(), disambiguator)),
             _ => {
                 let def_id = def.to_rust_def_id();
-                error_or_panic!(
+                raise_error!(
                     self,
                     span,
-                    format!("Unexpected DefPathItem for `{def_id:?}`: {path_elem:?}")
+                    "Unexpected DefPathItem for `{def_id:?}`: {path_elem:?}"
                 );
             }
         };
@@ -554,7 +557,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
     where
         T: Debug + SInto<S, U>,
     {
-        catch_sinto(s, &mut self.errors, &self.translated, span, x)
+        catch_sinto(s, &mut *self.errors.borrow_mut(), &self.translated, span, x)
     }
 
     pub fn hax_def(&mut self, def_id: impl Into<DefId>) -> Result<Arc<hax::FullDef>, Error> {
@@ -563,7 +566,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         // Hax takes care of caching the translation.
         catch_sinto(
             &self.hax_state,
-            &mut self.errors,
+            &mut *self.errors.borrow_mut(),
             &self.translated,
             span,
             &def_id,
@@ -585,7 +588,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             let rename = renames.next();
             if renames.next().is_some() {
                 let span = self.translate_span_from_hax(&def.span);
-                self.span_err(
+                register_error!(
+                    self,
                     span,
                     "There should be at most one `charon::rename(\"...\")` \
                     or `aeneas::rename(\"...\")` attribute per declaration",
@@ -795,7 +799,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
                     Ok(a) => Some(a),
                     Err(msg) => {
                         let span = self.translate_span_from_hax(&attr.span);
-                        self.span_err(span, &format!("Error parsing attribute: {msg}"));
+                        register_error!(self, span, "Error parsing attribute: {msg}");
                         None
                     }
                 }
@@ -884,6 +888,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             }
         };
         self.errors
+            .borrow_mut()
             .register_dep_source(src, item_id, id.to_def_id().is_local());
         item_id
     }
@@ -958,13 +963,14 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
     where
         F: FnOnce(&mut Self) -> T,
     {
-        let current_def_id = self.errors.def_id;
-        let current_def_id_is_local = self.errors.def_id_is_local;
-        self.errors.def_id = Some(item_id);
-        self.errors.def_id_is_local = def_id.is_local();
+        let mut errors = self.errors.borrow_mut();
+        let current_def_id = mem::replace(&mut errors.def_id, Some(item_id));
+        let current_def_id_is_local = mem::replace(&mut errors.def_id_is_local, def_id.is_local());
+        drop(errors); // important: release the refcell "lock"
         let ret = f(self);
-        self.errors.def_id = current_def_id;
-        self.errors.def_id_is_local = current_def_id_is_local;
+        let mut errors = self.errors.borrow_mut();
+        errors.def_id = current_def_id;
+        errors.def_id_is_local = current_def_id_is_local;
         ret
     }
 }
@@ -994,11 +1000,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         }
     }
 
-    pub fn continue_on_failure(&self) -> bool {
-        self.t_ctx.continue_on_failure()
-    }
-
-    pub fn span_err(&mut self, span: Span, msg: &str) {
+    pub fn span_err(&self, span: Span, msg: &str) -> Error {
         self.t_ctx.span_err(span, msg)
     }
 
@@ -1102,10 +1104,10 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         {
             Ok(self.bind_var(dbid, *rid))
         } else {
-            error_or_panic!(
+            raise_error!(
                 self,
                 span,
-                &format!("Unexpected error: could not find region '{dbid}_{var}")
+                "Unexpected error: could not find region '{dbid}_{var}"
             )
         }
     }
@@ -1122,11 +1124,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             }
         }
         let err = mk_err();
-        error_or_panic!(
-            self,
-            span,
-            &format!("Unexpected error: could not find {}", err)
-        )
+        raise_error!(self, span, "Unexpected error: could not find {}", err)
     }
 
     pub(crate) fn lookup_early_region(
@@ -1192,10 +1190,11 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             }
         }
         // Actually unreachable
-        error_or_panic!(
+        raise_error!(
             self,
             span,
-            &format!("Unexpected error: could not find clause variable {}", id)
+            "Unexpected error: could not find clause variable {}",
+            id
         )
     }
 
diff --git a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
index febc01d4..d79a594e 100644
--- a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
+++ b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
@@ -78,10 +78,10 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
             hax::BinOp::Shl => BinOp::Shl,
             hax::BinOp::Shr => BinOp::Shr,
             hax::BinOp::Cmp => {
-                error_or_panic!(self, span, "Unsupported binary operation: Cmp")
+                raise_error!(self, span, "Unsupported binary operation: Cmp")
             }
             hax::BinOp::Offset => {
-                error_or_panic!(self, span, "Unsupported binary operation: offset")
+                raise_error!(self, span, "Unsupported binary operation: offset")
             }
         })
     }
@@ -339,7 +339,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                                         ProjectionElem::Deref
                                     }
                                     _ => {
-                                        error_or_panic!(self, span, "Unexpected field projection");
+                                        raise_error!(self, span, "Unexpected field projection");
                                     }
                                 }
                             }
@@ -396,7 +396,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     }
                     hax::ProjectionElem::OpaqueCast => {
                         // Don't know what that is
-                        error_or_panic!(self, span, "Unexpected ProjectionElem::OpaqueCast");
+                        raise_error!(self, span, "Unexpected ProjectionElem::OpaqueCast");
                     }
                 };
 
@@ -460,7 +460,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 Ok(Rvalue::Ref(place, borrow_kind))
             }
             hax::Rvalue::ThreadLocalRef(_) => {
-                error_or_panic!(
+                raise_error!(
                     self,
                     span,
                     "charon does not support thread local references"
@@ -594,7 +594,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     hax::UnOp::Not => UnOp::Not,
                     hax::UnOp::Neg => UnOp::Neg,
                     hax::UnOp::PtrMetadata => {
-                        error_or_panic!(self, span, "Unsupported operation: PtrMetadata")
+                        raise_error!(self, span, "Unsupported operation: PtrMetadata")
                     }
                 };
                 Ok(Rvalue::UnaryOp(
@@ -607,13 +607,11 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 if let TyKind::Adt(TypeId::Adt(adt_id), _) = *place.ty().kind() {
                     Ok(Rvalue::Discriminant(place, adt_id))
                 } else {
-                    error_or_panic!(
+                    raise_error!(
                         self,
                         span,
-                        format!(
-                            "Unexpected scrutinee type for ReadDiscriminant: {}",
-                            place.ty().fmt_with_ctx(&self.into_fmt())
-                        )
+                        "Unexpected scrutinee type for ReadDiscriminant: {}",
+                        place.ty().fmt_with_ctx(&self.into_fmt())
                     )
                 }
             }
@@ -725,11 +723,11 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     }
                     hax::AggregateKind::RawPtr(..) => {
                         // TODO: replace with a call to `ptr::from_raw_parts`.
-                        error_or_panic!(self, span, "Wide raw pointers are not supported");
+                        raise_error!(self, span, "Wide raw pointers are not supported");
                     }
                     hax::AggregateKind::Coroutine(..)
                     | hax::AggregateKind::CoroutineClosure(..) => {
-                        error_or_panic!(self, span, "Coroutines are not supported");
+                        raise_error!(self, span, "Coroutines are not supported");
                     }
                 }
             }
@@ -949,7 +947,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 }))
             }
             StatementKind::Intrinsic(hax::NonDivergingIntrinsic::CopyNonOverlapping(..)) => {
-                error_or_panic!(self, span, "Unsupported statement kind: CopyNonOverlapping");
+                raise_error!(self, span, "Unsupported statement kind: CopyNonOverlapping");
             }
             // This is for the stacked borrows memory model.
             StatementKind::Retag(_, _) => None,
@@ -1002,10 +1000,10 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             TerminatorKind::UnwindResume => {
                 // This is used to correctly unwind. We shouldn't get there: if
                 // we panic, the state gets stuck.
-                error_or_panic!(self, span, "Unexpected terminator: UnwindResume");
+                raise_error!(self, span, "Unexpected terminator: UnwindResume");
             }
             TerminatorKind::UnwindTerminate { .. } => {
-                error_or_panic!(self, span, "Unexpected terminator: UnwindTerminate")
+                raise_error!(self, span, "Unexpected terminator: UnwindTerminate")
             }
             TerminatorKind::Return => RawTerminator::Return,
             // A MIR `Unreachable` terminator indicates undefined behavior of the rust abstract
@@ -1080,16 +1078,12 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 RawTerminator::Goto { target }
             }
             TerminatorKind::InlineAsm { .. } => {
-                error_or_panic!(self, span, "Inline assembly is not supported");
+                raise_error!(self, span, "Inline assembly is not supported");
             }
             TerminatorKind::CoroutineDrop
             | TerminatorKind::TailCall { .. }
             | TerminatorKind::Yield { .. } => {
-                error_or_panic!(
-                    self,
-                    span,
-                    format!("Unsupported terminator: {:?}", terminator.kind)
-                );
+                raise_error!(self, span, "Unsupported terminator: {:?}", terminator.kind);
             }
         };
 
@@ -1287,7 +1281,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             // Translation error
             Ok(Err(e)) => Err(e),
             Err(_) => {
-                error_or_panic!(
+                raise_error!(
                     self,
                     item_meta.span,
                     "Thread panicked when extracting body."
@@ -1535,7 +1529,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
 
                 // Unpack the tupled arguments to match the body locals.
                 let TyKind::Adt(TypeId::Tuple, tuple_args) = tuple_arg.kind() else {
-                    error_or_panic!(self, span, "Closure argument is not a tuple")
+                    raise_error!(self, span, "Closure argument is not a tuple")
                 };
                 inputs.extend(tuple_args.types.iter().cloned());
 
diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs
index 874e7168..f8edcc62 100644
--- a/charon/src/bin/charon-driver/translate/translate_predicates.rs
+++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs
@@ -151,14 +151,10 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                         // directly? For now we just ignore it.
                     }
                     ClauseKind::WellFormed(_) => {
-                        error_or_panic!(
-                            self,
-                            span,
-                            format!("Well-formedness clauses are unsupported")
-                        )
+                        raise_error!(self, span, "Well-formedness clauses are unsupported")
                     }
                     ClauseKind::ConstEvaluatable(_) => {
-                        error_or_panic!(self, span, format!("Unsupported clause: {:?}", kind))
+                        raise_error!(self, span, "Unsupported clause: {:?}", kind)
                     }
                 }
             }
@@ -169,7 +165,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             | PredicateKind::DynCompatible(_)
             | PredicateKind::NormalizesTo(_)
             | PredicateKind::Subtype(_) => {
-                error_or_panic!(self, span, format!("Unsupported predicate: {:?}", pred))
+                raise_error!(self, span, "Unsupported predicate: {:?}", pred)
             }
         }
         Ok(())
@@ -197,16 +193,11 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         match self.translate_trait_impl_expr_aux(span, impl_expr, trait_decl_ref.clone()) {
             Ok(res) => Ok(res),
             Err(err) => {
-                if !self.t_ctx.continue_on_failure() {
-                    panic!("Error during trait resolution: {}", err.msg)
-                } else {
-                    let msg = format!("Error during trait resolution: {}", &err.msg);
-                    self.span_err(span, &msg);
-                    Ok(TraitRef {
-                        kind: TraitRefKind::Unknown(err.msg),
-                        trait_decl_ref,
-                    })
-                }
+                register_error!(self, span, "Error during trait resolution: {}", &err.msg);
+                Ok(TraitRef {
+                    kind: TraitRefKind::Unknown(err.msg),
+                    trait_decl_ref,
+                })
             }
         }
     }
@@ -281,14 +272,12 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                             ..
                         } => {
                             if !generic_args.is_empty() {
-                                error_or_panic!(
+                                raise_error!(
                                     self,
                                     span,
-                                    format!(
-                                        "Found unsupported GAT `{}` when resolving trait `{}`",
-                                        item.name,
-                                        trait_decl_ref.fmt_with_ctx(&self.into_fmt())
-                                    )
+                                    "Found unsupported GAT `{}` when resolving trait `{}`",
+                                    item.name,
+                                    trait_decl_ref.fmt_with_ctx(&self.into_fmt())
                                 )
                             }
                             trait_id = TraitRefKind::ItemClause(
@@ -339,11 +328,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     trait_decl_ref,
                 };
                 if self.error_on_impl_expr_error {
-                    let error = format!("Error during trait resolution: {}", msg);
-                    self.span_err(span, &error);
-                    if !self.t_ctx.continue_on_failure() {
-                        panic!("{}", error)
-                    }
+                    register_error!(self, span, "Error during trait resolution: {}", msg);
                 }
                 trait_ref
             }
diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs
index 520c5c99..a9c399a4 100644
--- a/charon/src/bin/charon-driver/translate/translate_traits.rs
+++ b/charon/src/bin/charon-driver/translate/translate_traits.rs
@@ -52,11 +52,11 @@ impl BodyTransCtx<'_, '_> {
         let span = item_meta.span;
 
         if let hax::FullDefKind::TraitAlias { .. } = def.kind() {
-            error_or_panic!(self, span, &format!("Trait aliases are not supported"));
+            raise_error!(self, span, "Trait aliases are not supported");
         }
 
         let hax::FullDefKind::Trait { items, .. } = &def.kind else {
-            error_or_panic!(self, span, &format!("Unexpected definition: {def:?}"));
+            raise_error!(self, span, "Unexpected definition: {def:?}");
         };
         let items: Vec<(TraitItemName, &hax::AssocItem, Arc<hax::FullDef>)> = items
             .iter()
@@ -142,10 +142,10 @@ impl BodyTransCtx<'_, '_> {
                     consts.push((item_name.clone(), ty));
                 }
                 hax::FullDefKind::AssocTy { generics, .. } if !generics.params.is_empty() => {
-                    error_or_panic!(
+                    raise_error!(
                         self,
                         item_span,
-                        &format!("Generic associated types are not supported")
+                        "Generic associated types are not supported"
                     );
                 }
                 hax::FullDefKind::AssocTy { value, .. } => {
@@ -165,7 +165,7 @@ impl BodyTransCtx<'_, '_> {
 
         if item_meta.opacity.is_opaque() {
             let ctx = self.into_fmt();
-            self.t_ctx.errors.display_error(
+            self.t_ctx.errors.borrow_mut().display_error(
                 &self.t_ctx.translated,
                 item_meta.span,
                 Level::Warning,
@@ -173,7 +173,7 @@ impl BodyTransCtx<'_, '_> {
                     "Trait declarations cannot be \"opaque\"; the trait `{}` will be translated as normal.",
                     item_meta.name.fmt_with_ctx(&ctx)
                 ),
-            )
+            );
         }
         // In case of a trait implementation, some values may not have been
         // provided, in case the declaration provided default values. We
@@ -351,7 +351,7 @@ impl BodyTransCtx<'_, '_> {
 
         if item_meta.opacity.is_opaque() {
             let ctx = self.into_fmt();
-            self.t_ctx.errors.display_error(
+            self.t_ctx.errors.borrow_mut().display_error(
                 &self.t_ctx.translated,
                 item_meta.span,
                 Level::Warning,
@@ -359,7 +359,7 @@ impl BodyTransCtx<'_, '_> {
                     "Trait implementations cannot be \"opaque\"; the impl `{}` will be translated as normal.",
                     item_meta.name.fmt_with_ctx(&ctx)
                 ),
-            )
+            );
         }
 
         Ok(ast::TraitImpl {
diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs
index 34541ebb..f52d0d99 100644
--- a/charon/src/bin/charon-driver/translate/translate_types.rs
+++ b/charon/src/bin/charon-driver/translate/translate_types.rs
@@ -54,12 +54,14 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             }
             ReVar(..) | RePlaceholder(..) => {
                 // Shouldn't exist outside of type inference.
-                let err = format!("Should not exist outside of type inference: {region:?}");
-                error_or_panic!(self, span, err)
+                raise_error!(
+                    self,
+                    span,
+                    "Should not exist outside of type inference: {region:?}"
+                )
             }
             ReLateParam(..) | ReError(..) => {
-                let err = format!("Unexpected region kind: {region:?}");
-                error_or_panic!(self, span, err)
+                raise_error!(self, span, "Unexpected region kind: {region:?}")
             }
         }
     }
@@ -129,11 +131,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     return self.translate_ty(span, hidden_ty)
                 }
                 _ => {
-                    error_or_panic!(
-                        self,
-                        span,
-                        format!("Unsupported alias type: {:?}", alias.kind)
-                    )
+                    raise_error!(self, span, "Unsupported alias type: {:?}", alias.kind)
                 }
             },
 
@@ -260,7 +258,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             }
             hax::TyKind::Infer(_) => {
                 trace!("Infer");
-                error_or_panic!(self, span, "Unsupported type: infer type")
+                raise_error!(self, span, "Unsupported type: infer type")
             }
 
             hax::TyKind::Dynamic(_existential_preds, _region, _) => {
@@ -272,16 +270,16 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
 
             hax::TyKind::Coroutine(..) => {
                 trace!("Coroutine");
-                error_or_panic!(self, span, "Coroutine types are not supported yet")
+                raise_error!(self, span, "Coroutine types are not supported yet")
             }
 
             hax::TyKind::Bound(_, _) => {
                 trace!("Bound");
-                error_or_panic!(self, span, "Unexpected type kind: bound")
+                raise_error!(self, span, "Unexpected type kind: bound")
             }
             hax::TyKind::Placeholder(_) => {
                 trace!("PlaceHolder");
-                error_or_panic!(self, span, "Unsupported type: placeholder")
+                raise_error!(self, span, "Unsupported type: placeholder")
             }
             hax::TyKind::Arrow(box sig)
             | hax::TyKind::Closure(
@@ -305,11 +303,11 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             }
             hax::TyKind::Error => {
                 trace!("Error");
-                error_or_panic!(self, span, "Type checking error")
+                raise_error!(self, span, "Type checking error")
             }
             hax::TyKind::Todo(s) => {
                 trace!("Todo: {s}");
-                error_or_panic!(self, span, format!("Unsupported type: {:?}", s))
+                raise_error!(self, span, "Unsupported type: {:?}", s)
             }
         };
         let ty = kind.into_ty();
@@ -354,10 +352,10 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                         regions.push(Region::Erased);
                     }
                     hax::BoundVariableKind::Ty(_) => {
-                        error_or_panic!(self, span, "Unexpected locally bound type variable")
+                        raise_error!(self, span, "Unexpected locally bound type variable")
                     }
                     hax::BoundVariableKind::Const => {
-                        error_or_panic!(self, span, "Unexpected locally bound const generic")
+                        raise_error!(self, span, "Unexpected locally bound const generic")
                     }
                 }
             }
@@ -738,7 +736,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                         *ty,
                         param.name.clone(),
                     ),
-                    None => error_or_panic!(
+                    None => raise_error!(
                         self,
                         span,
                         "Constant parameters of non-literal type are not supported"
diff --git a/charon/src/errors.rs b/charon/src/errors.rs
index d9c49bd9..26f33b6a 100644
--- a/charon/src/errors.rs
+++ b/charon/src/errors.rs
@@ -10,56 +10,38 @@ use std::cmp::{Ord, PartialOrd};
 use std::collections::{HashMap, HashSet};
 
 #[macro_export]
-macro_rules! register_error_or_panic {
-    ($ctx:expr, $span: expr, $msg: expr) => {{
-        $ctx.span_err($span, &$msg);
-        if !$ctx.continue_on_failure() {
-            panic!("{}", $msg);
-        }
+macro_rules! register_error {
+    ($ctx:expr, crate($krate:expr), $span: expr, $($fmt:tt)*) => {{
+        let msg = format!($($fmt)*);
+        $ctx.span_err($krate, $span, &msg)
     }};
-    ($ctx:expr, $krate:expr, $span: expr, $msg: expr) => {{
-        $ctx.span_err($krate, $span, &$msg);
-        if !$ctx.continue_on_failure() {
-            panic!("{}", $msg);
-        }
+    ($ctx:expr, $span: expr, $($fmt:tt)*) => {{
+        let msg = format!($($fmt)*);
+        $ctx.span_err($span, &msg)
     }};
 }
-pub use register_error_or_panic;
+pub use register_error;
 
 /// Macro to either panic or return on error, depending on the CLI options
 #[macro_export]
-macro_rules! error_or_panic {
-    ($ctx:expr, $span:expr, $msg:expr) => {{
-        $crate::errors::register_error_or_panic!($ctx, $span, $msg);
-        let e = $crate::errors::Error {
-            span: $span,
-            msg: $msg.to_string(),
-        };
-        return Err(e);
-    }};
-    ($ctx:expr, $krate:expr, $span:expr, $msg:expr) => {{
-        $crate::errors::register_error_or_panic!($ctx, $krate, $span, $msg);
-        let e = $crate::errors::Error {
-            span: $span,
-            msg: $msg.to_string(),
-        };
-        return Err(e);
+macro_rules! raise_error {
+    ($($tokens:tt)*) => {{
+        return Err(register_error!($($tokens)*));
     }};
 }
-pub use error_or_panic;
+pub use raise_error;
 
 /// Custom assert to either panic or return an error
 #[macro_export]
 macro_rules! error_assert {
     ($ctx:expr, $span: expr, $b: expr) => {
         if !$b {
-            let msg = format!("assertion failure: {:?}", stringify!($b));
-            $crate::errors::error_or_panic!($ctx, $span, msg);
+            $crate::errors::raise_error!($ctx, $span, "assertion failure: {:?}", stringify!($b));
         }
     };
-    ($ctx:expr, $span: expr, $b: expr, $msg: expr) => {
+    ($ctx:expr, $span: expr, $b: expr, $($fmt:tt)*) => {
         if !$b {
-            $crate::errors::error_or_panic!($ctx, $span, $msg);
+            $crate::errors::raise_error!($ctx, $span, $($fmt)*);
         }
     };
 }
@@ -70,13 +52,17 @@ pub use error_assert;
 macro_rules! sanity_check {
     ($ctx:expr, $span: expr, $b: expr) => {
         if !$b {
-            let msg = format!("assertion failure: {:?}", stringify!($b));
-            $crate::errors::register_error_or_panic!($ctx, $span, msg);
+            $crate::errors::register_error!(
+                $ctx,
+                $span,
+                "assertion failure: {:?}",
+                stringify!($b)
+            );
         }
     };
-    ($ctx:expr, $span: expr, $b: expr, $msg: expr) => {
+    ($ctx:expr, $span: expr, $b: expr, $($fmt:tt)*) => {
         if !$b {
-            $crate::errors::register_error_or_panic!($ctx, $span, $msg);
+            $crate::errors::register_error!($ctx, $span, $($fmt)*);
         }
     };
 }
@@ -229,25 +215,31 @@ impl ErrorCtx {
     }
 
     /// Report an error without registering anything.
-    pub fn display_error(&self, krate: &TranslatedCrate, span: Span, level: Level, msg: String) {
-        // TODO: `Error` is redundantly constructed in two places
+    pub fn display_error(
+        &self,
+        krate: &TranslatedCrate,
+        span: Span,
+        level: Level,
+        msg: String,
+    ) -> Error {
         let error = Error { span, msg };
         anstream::eprintln!("{}\n", error.render(krate, level));
+        error
     }
 
     /// Report an error without registering anything.
-    pub fn span_err_no_register(&self, krate: &TranslatedCrate, span: Span, msg: &str) {
+    pub fn span_err_no_register(&self, krate: &TranslatedCrate, span: Span, msg: String) -> Error {
         let level = if self.error_on_warnings {
             Level::Error
         } else {
             Level::Warning
         };
-        self.display_error(krate, span, level, msg.to_string());
+        self.display_error(krate, span, level, msg)
     }
 
     /// Report and register an error.
-    pub fn span_err(&mut self, krate: &TranslatedCrate, span: Span, msg: &str) {
-        self.span_err_no_register(krate, span, msg);
+    pub fn span_err(&mut self, krate: &TranslatedCrate, span: Span, msg: &str) -> Error {
+        let err = self.span_err_no_register(krate, span, msg.to_string());
         self.error_count += 1;
         // If this item comes from an external crate, after the first error for that item we
         // display where in the local crate that item was reached from.
@@ -257,6 +249,10 @@ impl ErrorCtx {
         {
             self.report_external_dep_error(krate, id);
         }
+        if !self.continue_on_failure() {
+            panic!("{msg}");
+        }
+        err
     }
 
     pub fn ignore_failed_decl(&mut self, id: AnyTransId) {
diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs
index 13e0763a..8e814ee3 100644
--- a/charon/src/transform/check_generics.rs
+++ b/charon/src/transform/check_generics.rs
@@ -3,15 +3,14 @@ use derive_generic_visitor::*;
 use itertools::Itertools;
 use std::fmt::Display;
 
-use crate::{errors::ErrorCtx, llbc_ast::*, register_error_or_panic};
+use crate::{llbc_ast::*, register_error};
 
 use super::{ctx::TransformPass, TransformCtx};
 
 #[derive(Visitor)]
 struct CheckGenericsVisitor<'a> {
-    translated: &'a TranslatedCrate,
+    ctx: &'a TransformCtx,
     phase: &'static str,
-    error_ctx: &'a mut ErrorCtx,
     // Tracks an enclosing span to make errors useful.
     span: Span,
     /// Remember the names of the types visited up to here.
@@ -19,13 +18,14 @@ struct CheckGenericsVisitor<'a> {
 }
 
 impl CheckGenericsVisitor<'_> {
-    fn error(&mut self, message: impl Display) {
-        let message = format!(
+    fn error(&self, message: impl Display) {
+        register_error!(
+            self.ctx,
+            self.span,
             "Found inconsistent generics {}:\n{message}\nVisitor stack:\n  {}",
             self.phase,
             self.visit_stack.iter().rev().join("\n  ")
         );
-        register_error_or_panic!(self.error_ctx, self.translated, self.span, message);
     }
 }
 
@@ -54,13 +54,13 @@ impl VisitAst for CheckGenericsVisitor<'_> {
     fn enter_generic_args(&mut self, args: &GenericArgs) {
         let params = match &args.target {
             GenericsSource::Item(item_id) => {
-                let Some(item) = self.translated.get_item(*item_id) else {
+                let Some(item) = self.ctx.translated.get_item(*item_id) else {
                     return;
                 };
                 item.generic_params()
             }
             GenericsSource::Method(trait_id, method_name) => {
-                let Some(trait_decl) = self.translated.trait_decls.get(*trait_id) else {
+                let Some(trait_decl) = self.ctx.translated.trait_decls.get(*trait_id) else {
                     return;
                 };
                 let Some((_, bound_fn)) = trait_decl
@@ -84,7 +84,12 @@ impl VisitAst for CheckGenericsVisitor<'_> {
 
     // Special case that is not represented as a `GenericArgs`.
     fn enter_trait_impl(&mut self, timpl: &TraitImpl) {
-        let Some(tdecl) = self.translated.trait_decls.get(timpl.impl_trait.trait_id) else {
+        let Some(tdecl) = self
+            .ctx
+            .translated
+            .trait_decls
+            .get(timpl.impl_trait.trait_id)
+        else {
             return;
         };
         // See `lift_associated_item_clauses`
@@ -126,8 +131,7 @@ impl TransformPass for Check {
     fn transform_ctx(&self, ctx: &mut TransformCtx) {
         for item in ctx.translated.all_items() {
             let mut visitor = CheckGenericsVisitor {
-                translated: &ctx.translated,
-                error_ctx: &mut ctx.errors,
+                ctx,
                 phase: self.0,
                 span: item.item_meta().span,
                 visit_stack: Default::default(),
diff --git a/charon/src/transform/ctx.rs b/charon/src/transform/ctx.rs
index 1b586cad..8b4724eb 100644
--- a/charon/src/transform/ctx.rs
+++ b/charon/src/transform/ctx.rs
@@ -5,6 +5,7 @@ use crate::llbc_ast;
 use crate::name_matcher::NamePattern;
 use crate::pretty::FmtWithCtx;
 use crate::ullbc_ast;
+use std::cell::RefCell;
 use std::{fmt, mem};
 
 /// The options that control transformation.
@@ -33,7 +34,7 @@ pub struct TransformCtx {
     /// The translated data.
     pub translated: TranslatedCrate,
     /// Context for tracking and reporting errors.
-    pub errors: ErrorCtx,
+    pub errors: RefCell<ErrorCtx>,
 }
 
 /// A pass that modifies ullbc bodies.
@@ -154,16 +155,15 @@ pub trait TransformPass: Sync {
 }
 
 impl<'ctx> TransformCtx {
-    pub(crate) fn continue_on_failure(&self) -> bool {
-        self.errors.continue_on_failure()
-    }
     pub(crate) fn has_errors(&self) -> bool {
-        self.errors.has_errors()
+        self.errors.borrow().has_errors()
     }
 
     /// Span an error and register the error.
-    pub(crate) fn span_err(&mut self, span: Span, msg: &str) {
-        self.errors.span_err(&self.translated, span, msg)
+    pub(crate) fn span_err(&self, span: Span, msg: &str) -> Error {
+        self.errors
+            .borrow_mut()
+            .span_err(&self.translated, span, msg)
     }
 
     pub(crate) fn with_def_id<F, T>(
@@ -175,13 +175,14 @@ impl<'ctx> TransformCtx {
     where
         F: FnOnce(&mut Self) -> T,
     {
-        let current_def_id = self.errors.def_id;
-        let current_def_id_is_local = self.errors.def_id_is_local;
-        self.errors.def_id = Some(def_id.into());
-        self.errors.def_id_is_local = def_id_is_local;
+        let mut errors = self.errors.borrow_mut();
+        let current_def_id = mem::replace(&mut errors.def_id, Some(def_id.into()));
+        let current_def_id_is_local = mem::replace(&mut errors.def_id_is_local, def_id_is_local);
+        drop(errors); // important: release the refcell "lock"
         let ret = f(self);
-        self.errors.def_id = current_def_id;
-        self.errors.def_id_is_local = current_def_id_is_local;
+        let mut errors = self.errors.borrow_mut();
+        errors.def_id = current_def_id;
+        errors.def_id_is_local = current_def_id_is_local;
         ret
     }
 
diff --git a/charon/src/transform/reconstruct_boxes.rs b/charon/src/transform/reconstruct_boxes.rs
index dd510061..83878987 100644
--- a/charon/src/transform/reconstruct_boxes.rs
+++ b/charon/src/transform/reconstruct_boxes.rs
@@ -1,5 +1,5 @@
 //! # Micro-pass: reconstruct piecewise box allocations using `malloc` and `ShallowInitBox`.
-use crate::register_error_or_panic;
+use crate::register_error;
 use crate::transform::TransformCtx;
 use crate::ullbc_ast::*;
 
@@ -112,7 +112,7 @@ impl UllbcPass for Transform {
         // Make sure we got all the `ShallowInitBox`es.
         b.body.dyn_visit_in_body(|rvalue: &Rvalue| {
             if rvalue.is_shallow_init_box() {
-                register_error_or_panic!(
+                register_error!(
                     ctx,
                     b.span,
                     "Could not reconstruct `Box` initialization; \
diff --git a/charon/src/transform/remove_read_discriminant.rs b/charon/src/transform/remove_read_discriminant.rs
index f04a902b..4be04c66 100644
--- a/charon/src/transform/remove_read_discriminant.rs
+++ b/charon/src/transform/remove_read_discriminant.rs
@@ -3,7 +3,7 @@
 //! `drop(v)` where `v` has type `Never` (it can happen - this module does the
 //! filtering). Then, we filter the unused variables ([crate::remove_unused_locals]).
 
-use crate::errors::register_error_or_panic;
+use crate::errors::register_error;
 use crate::formatter::IntoFormatter;
 use crate::llbc_ast::*;
 use crate::pretty::FmtWithCtx;
@@ -41,13 +41,14 @@ impl Transform {
                         ..
                     }) => {
                         let name = ctx.translated.item_name(*adt_id).unwrap();
-                        let msg = format!(
+                        register_error!(
+                            ctx,
+                            block.span,
                             "reading the discriminant of an opaque enum. \
                             Add `--include {}` to the `charon` arguments \
                             to translate this enum.",
                             name.fmt_with_ctx(&ctx.into_fmt())
                         );
-                        register_error_or_panic!(ctx, block.span, msg);
                         None
                     }
                     Some(TypeDecl {
@@ -55,7 +56,7 @@ impl Transform {
                             TypeDeclKind::Struct(..) | TypeDeclKind::Union(..) | TypeDeclKind::Alias(..),
                         ..
                     }) => {
-                        register_error_or_panic!(
+                        register_error!(
                             ctx,
                             block.span,
                             "reading the discriminant of a non-enum type"
@@ -106,7 +107,7 @@ impl Transform {
                                             .filter_map(|discr| {
                                                 covered_discriminants.insert(discr);
                                                 discr_to_id.get(&discr).or_else(|| {
-                                                    register_error_or_panic!(
+                                                    register_error!(
                                                         ctx,
                                                         block.span,
                                                         "Found incorrect discriminant {discr} for enum {adt_id}"
diff --git a/charon/src/transform/skip_trait_refs_when_known.rs b/charon/src/transform/skip_trait_refs_when_known.rs
index ba70091b..f5cce3a8 100644
--- a/charon/src/transform/skip_trait_refs_when_known.rs
+++ b/charon/src/transform/skip_trait_refs_when_known.rs
@@ -1,4 +1,4 @@
-use crate::{register_error_or_panic, transform::TransformCtx, ullbc_ast::*};
+use crate::{register_error, transform::TransformCtx, ullbc_ast::*};
 
 use super::ctx::UllbcPass;
 
@@ -28,11 +28,13 @@ fn transform_call(ctx: &mut TransformCtx, span: Span, call: &mut Call) {
     let method_generics = &fn_ptr.generics;
 
     if !method_generics.matches(&bound_fn.params) {
-        let message = format!(
+        register_error!(
+            ctx,
+            span,
             "Mismatched method generics:\nparams:   {:?}\nsupplied: {:?}",
-            bound_fn.params, method_generics
+            bound_fn.params,
+            method_generics
         );
-        register_error_or_panic!(ctx.errors, &ctx.translated, span, message);
     }
 
     // Make the two levels of binding explicit: outer binder for the impl block, inner binder for