WIP: does not compile yet because we need to propagate the meta variable.

11 files changed, 226 insertions, 223 deletions

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 2563bd9d..6cdae078 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -5,6 +5,7 @@ open LlbcAst
 open LlbcAstUtils
 open ValuesUtils
 open Identifiers
+open Errors
 module L = Logging
 
 (** The [Id] module for dummy variables.
@@ -285,7 +286,7 @@ let lookup_const_generic_var (ctx : eval_ctx) (vid : ConstGenericVarId.id) :
   ConstGenericVarId.nth ctx.const_generic_vars vid
 
 (** Lookup a variable in the current frame *)
-let env_lookup_var (env : env) (vid : VarId.id) : var_binder * typed_value =
+let env_lookup_var (meta : Meta.meta) (env : env) (vid : VarId.id) : var_binder * typed_value =
   (* We take care to stop at the end of current frame: different variables
      in different frames can have the same id!
   *)
@@ -296,12 +297,12 @@ let env_lookup_var (env : env) (vid : VarId.id) : var_binder * typed_value =
     | EBinding (BVar var, v) :: env' ->
         if var.index = vid then (var, v) else lookup env'
     | (EBinding (BDummy _, _) | EAbs _) :: env' -> lookup env'
-    | EFrame :: _ -> raise (Failure "End of frame")
+    | EFrame :: _ -> craise meta "End of frame"
   in
   lookup env
 
-let ctx_lookup_var_binder (ctx : eval_ctx) (vid : VarId.id) : var_binder =
-  fst (env_lookup_var ctx.env vid)
+let ctx_lookup_var_binder (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) : var_binder =
+  fst (env_lookup_var meta ctx.env vid)
 
 let ctx_lookup_type_decl (ctx : eval_ctx) (tid : TypeDeclId.id) : type_decl =
   TypeDeclId.Map.find tid ctx.type_ctx.type_decls
@@ -320,12 +321,12 @@ let ctx_lookup_trait_impl (ctx : eval_ctx) (id : TraitImplId.id) : trait_impl =
   TraitImplId.Map.find id ctx.trait_impls_ctx.trait_impls
 
 (** Retrieve a variable's value in the current frame *)
-let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
-  snd (env_lookup_var env vid)
+let env_lookup_var_value (meta : Meta.meta) (env : env) (vid : VarId.id) : typed_value =
+  snd (env_lookup_var meta env vid)
 
 (** Retrieve a variable's value in an evaluation context *)
-let ctx_lookup_var_value (ctx : eval_ctx) (vid : VarId.id) : typed_value =
-  env_lookup_var_value ctx.env vid
+let ctx_lookup_var_value (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) : typed_value =
+  env_lookup_var_value meta ctx.env vid
 
 (** Retrieve a const generic value in an evaluation context *)
 let ctx_lookup_const_generic_value (ctx : eval_ctx) (vid : ConstGenericVarId.id)
@@ -337,18 +338,18 @@ let ctx_lookup_const_generic_value (ctx : eval_ctx) (vid : ConstGenericVarId.id)
     This is a helper function: it can break invariants and doesn't perform
     any check.
 *)
-let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env =
+let env_update_var_value (meta : Meta.meta) (env : env) (vid : VarId.id) (nv : typed_value) : env =
   (* We take care to stop at the end of current frame: different variables
      in different frames can have the same id!
   *)
   let rec update env =
     match env with
-    | [] -> raise (Failure "Unexpected")
+    | [] -> craise meta "Unexpected"
     | EBinding ((BVar b as var), v) :: env' ->
         if b.index = vid then EBinding (var, nv) :: env'
         else EBinding (var, v) :: update env'
     | ((EBinding (BDummy _, _) | EAbs _) as ee) :: env' -> ee :: update env'
-    | EFrame :: _ -> raise (Failure "End of frame")
+    | EFrame :: _ -> craise meta "End of frame"
   in
   update env
 
@@ -360,17 +361,17 @@ let var_to_binder (var : var) : var_binder =
     This is a helper function: it can break invariants and doesn't perform
     any check.
 *)
-let ctx_update_var_value (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) :
+let ctx_update_var_value (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) :
     eval_ctx =
-  { ctx with env = env_update_var_value ctx.env vid nv }
+  { ctx with env = env_update_var_value meta ctx.env vid nv }
 
 (** Push a variable in the context's environment.
 
     Checks that the pushed variable and its value have the same type (this
     is important).
 *)
-let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
-  assert (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty);
+let ctx_push_var (meta : Meta.meta) (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
+  cassert (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty) meta "Pushed variables and their values do not have the same type TODO: Error message";
   let bv = var_to_binder var in
   { ctx with env = EBinding (BVar bv, v) :: ctx.env }
 
@@ -379,7 +380,7 @@ let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
     Checks that the pushed variables and their values have the same type (this
     is important).
 *)
-let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
+let ctx_push_vars (meta : Meta.meta) (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
     =
   log#ldebug
     (lazy
@@ -390,11 +391,11 @@ let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
                (* We can unfortunately not use Print because it depends on Contexts... *)
                show_var var ^ " -> " ^ show_typed_value value)
              vars)));
-  assert (
+  cassert (
     List.for_all
       (fun (var, (value : typed_value)) ->
         TypesUtils.ty_is_ety var.var_ty && var.var_ty = value.ty)
-      vars);
+      vars) meta "Pushed variables and their values do not have the same type TODO: Error message";
   let vars =
     List.map
       (fun (var, value) -> EBinding (BVar (var_to_binder var), value))
@@ -416,11 +417,11 @@ let ctx_push_fresh_dummy_vars (ctx : eval_ctx) (vl : typed_value list) :
   List.fold_left (fun ctx v -> ctx_push_fresh_dummy_var ctx v) ctx vl
 
 (** Remove a dummy variable from a context's environment. *)
-let ctx_remove_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) :
+let ctx_remove_dummy_var meta (ctx : eval_ctx) (vid : DummyVarId.id) :
     eval_ctx * typed_value =
   let rec remove_var (env : env) : env * typed_value =
     match env with
-    | [] -> raise (Failure "Could not lookup a dummy variable")
+    | [] -> craise meta "Could not lookup a dummy variable"
     | EBinding (BDummy vid', v) :: env when vid' = vid -> (env, v)
     | ee :: env ->
         let env, v = remove_var env in
@@ -430,10 +431,10 @@ let ctx_remove_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) :
   ({ ctx with env }, v)
 
 (** Lookup a dummy variable in a context's environment. *)
-let ctx_lookup_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) : typed_value =
+let ctx_lookup_dummy_var (meta : Meta.meta) (ctx : eval_ctx) (vid : DummyVarId.id) : typed_value =
   let rec lookup_var (env : env) : typed_value =
     match env with
-    | [] -> raise (Failure "Could not lookup a dummy variable")
+    | [] -> craise meta "Could not lookup a dummy variable"
     | EBinding (BDummy vid', v) :: _env when vid' = vid -> v
     | _ :: env -> lookup_var env
   in
@@ -449,13 +450,13 @@ let erase_regions (ty : ty) : ty =
   v#visit_ty () ty
 
 (** Push an uninitialized variable (which thus maps to {!constructor:Values.value.VBottom}) *)
-let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx =
-  ctx_push_var ctx var (mk_bottom (erase_regions var.var_ty))
+let ctx_push_uninitialized_var (meta : Meta.meta) (ctx : eval_ctx) (var : var) : eval_ctx =
+  ctx_push_var meta ctx var (mk_bottom (erase_regions var.var_ty))
 
 (** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.VBottom}) *)
-let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx =
+let ctx_push_uninitialized_vars (meta : Meta.meta) (ctx : eval_ctx) (vars : var list) : eval_ctx =
   let vars = List.map (fun v -> (v, mk_bottom (erase_regions v.var_ty))) vars in
-  ctx_push_vars ctx vars
+  ctx_push_vars meta ctx vars
 
 let env_find_abs (env : env) (pred : abs -> bool) : abs option =
   let rec lookup env =
@@ -474,10 +475,10 @@ let env_lookup_abs_opt (env : env) (abs_id : AbstractionId.id) : abs option =
     this abstraction (for instance, remove the abs id from all the parent sets
     of all the other abstractions).
  *)
-let env_remove_abs (env : env) (abs_id : AbstractionId.id) : env * abs option =
+let env_remove_abs (meta : Meta.meta) (env : env) (abs_id : AbstractionId.id) : env * abs option =
   let rec remove (env : env) : env * abs option =
     match env with
-    | [] -> raise (Failure "Unreachable")
+    | [] -> craise meta "Unreachable"
     | EFrame :: _ -> (env, None)
     | EBinding (bv, v) :: env ->
         let env, abs_opt = remove env in
@@ -499,11 +500,11 @@ let env_remove_abs (env : env) (abs_id : AbstractionId.id) : env * abs option =
     we also substitute the abstraction id wherever it is used (i.e., in the
     parent sets of the other abstractions).
  *)
-let env_subst_abs (env : env) (abs_id : AbstractionId.id) (nabs : abs) :
+let env_subst_abs (meta : Meta.meta) (env : env) (abs_id : AbstractionId.id) (nabs : abs) :
     env * abs option =
   let rec update (env : env) : env * abs option =
     match env with
-    | [] -> raise (Failure "Unreachable")
+    | [] -> craise meta "Unreachable"
     | EFrame :: _ -> (* We're done *) (env, None)
     | EBinding (bv, v) :: env ->
         let env, opt_abs = update env in
@@ -535,22 +536,22 @@ let ctx_find_abs (ctx : eval_ctx) (p : abs -> bool) : abs option =
   env_find_abs ctx.env p
 
 (** See the comments for {!env_remove_abs} *)
-let ctx_remove_abs (ctx : eval_ctx) (abs_id : AbstractionId.id) :
+let ctx_remove_abs (meta : Meta.meta) (ctx : eval_ctx) (abs_id : AbstractionId.id) :
     eval_ctx * abs option =
-  let env, abs = env_remove_abs ctx.env abs_id in
+  let env, abs = env_remove_abs meta ctx.env abs_id in
   ({ ctx with env }, abs)
 
 (** See the comments for {!env_subst_abs} *)
-let ctx_subst_abs (ctx : eval_ctx) (abs_id : AbstractionId.id) (nabs : abs) :
+let ctx_subst_abs (meta : Meta.meta) (ctx : eval_ctx) (abs_id : AbstractionId.id) (nabs : abs) :
     eval_ctx * abs option =
-  let env, abs_opt = env_subst_abs ctx.env abs_id nabs in
+  let env, abs_opt = env_subst_abs meta ctx.env abs_id nabs in
   ({ ctx with env }, abs_opt)
 
-let ctx_set_abs_can_end (ctx : eval_ctx) (abs_id : AbstractionId.id)
+let ctx_set_abs_can_end (meta : Meta.meta) (ctx : eval_ctx) (abs_id : AbstractionId.id)
     (can_end : bool) : eval_ctx =
   let abs = ctx_lookup_abs ctx abs_id in
   let abs = { abs with can_end } in
-  fst (ctx_subst_abs ctx abs_id abs)
+  fst (ctx_subst_abs meta ctx abs_id abs)
 
 let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool =
   let decl_group = TypeDeclId.Map.find id ctx.type_ctx.type_decls_groups in
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index ccae4588..961a64a4 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -173,7 +173,7 @@ let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig)
     - the list of symbolic values introduced for the input values
     - the instantiated function signature
  *)
-let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
+let initialize_symbolic_context_for_fun (meta : Meta.meta) (ctx : decls_ctx) (fdef : fun_decl) :
     eval_ctx * symbolic_value list * inst_fun_sig =
   (* The abstractions are not initialized the same way as for function
    * calls: they contain *loan* projectors, because they "provide" us
@@ -232,12 +232,12 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
     Collections.List.split_at (List.tl body.locals) body.arg_count
   in
   (* Push the return variable (initialized with ⊥) *)
-  let ctx = ctx_push_uninitialized_var ctx ret_var in
+  let ctx = ctx_push_uninitialized_var meta ctx ret_var in
   (* Push the input variables (initialized with symbolic values) *)
   let input_values = List.map mk_typed_value_from_symbolic_value input_svs in
-  let ctx = ctx_push_vars ctx (List.combine input_vars input_values) in
+  let ctx = ctx_push_vars meta ctx (List.combine input_vars input_values) in
   (* Push the remaining local variables (initialized with ⊥) *)
-  let ctx = ctx_push_uninitialized_vars ctx local_vars in
+  let ctx = ctx_push_uninitialized_vars meta ctx local_vars in
   (* Return *)
   (ctx, input_svs, inst_sg)
 
@@ -468,7 +468,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
       for the synthesis)
     - the symbolic AST generated by the symbolic execution
  *)
-let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
+let evaluate_function_symbolic (meta : Meta.meta) (synthesize : bool) (ctx : decls_ctx)
     (fdef : fun_decl) : symbolic_value list * SA.expression option =
   (* Debug *)
   let name_to_string () =
@@ -479,7 +479,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
   log#ldebug (lazy ("evaluate_function_symbolic: " ^ name_to_string ()));
 
   (* Create the evaluation context *)
-  let ctx, input_svs, inst_sg = initialize_symbolic_context_for_fun ctx fdef in
+  let ctx, input_svs, inst_sg = initialize_symbolic_context_for_fun meta ctx fdef in
 
   let regions_hierarchy =
     FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
@@ -612,7 +612,7 @@ module Test = struct
   (** Test a unit function (taking no arguments) by evaluating it in an empty
       environment.
    *)
-  let test_unit_function (crate : crate) (decls_ctx : decls_ctx)
+  let test_unit_function (meta : Meta.meta)  (crate : crate) (decls_ctx : decls_ctx)
       (fid : FunDeclId.id) : unit =
     (* Retrieve the function declaration *)
     let fdef = FunDeclId.Map.find fid crate.fun_decls in
@@ -634,7 +634,7 @@ module Test = struct
     let ctx = initialize_eval_ctx decls_ctx [] [] [] in
 
     (* Insert the (uninitialized) local variables *)
-    let ctx = ctx_push_uninitialized_vars ctx body.locals in
+    let ctx = ctx_push_uninitialized_vars meta ctx body.locals in
 
     (* Create the continuation to check the function's result *)
     let config = mk_config ConcreteMode in
@@ -665,7 +665,7 @@ module Test = struct
     && def.signature.inputs = []
 
   (** Test all the unit functions in a list of function definitions *)
-  let test_unit_functions (crate : crate) : unit =
+  let test_unit_functions (meta : Meta.meta)  (crate : crate) : unit =
     let unit_funs =
       FunDeclId.Map.filter
         (fun _ -> fun_decl_is_transparent_unit)
@@ -673,7 +673,7 @@ module Test = struct
     in
     let decls_ctx = compute_contexts crate in
     let test_unit_fun _ (def : fun_decl) : unit =
-      test_unit_function crate decls_ctx def.def_id
+      test_unit_function meta crate decls_ctx def.def_id
     in
     FunDeclId.Map.iter test_unit_fun unit_funs
 end
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index ae251fbf..e37a67b7 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -1030,7 +1030,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
       (* Remove all the references to the id of the current abstraction, and remove
        * the abstraction itself.
        * **Rk.**: this is where we synthesize the updated symbolic AST *)
-      let cc = comp cc (end_abstraction_remove_from_context config abs_id) in
+      let cc = comp cc (end_abstraction_remove_from_context meta config abs_id) in
 
       (* Debugging *)
       let cc =
@@ -1273,10 +1273,10 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
       end_abstraction_borrows meta config chain abs_id cf ctx
 
 (** Remove an abstraction from the context, as well as all its references *)
-and end_abstraction_remove_from_context (_config : config)
+and end_abstraction_remove_from_context (meta : Meta.meta)  (_config : config)
     (abs_id : AbstractionId.id) : cm_fun =
  fun cf ctx ->
-  let ctx, abs = ctx_remove_abs ctx abs_id in
+  let ctx, abs = ctx_remove_abs meta ctx abs_id in
   let abs = Option.get abs in
   (* Apply the continuation *)
   let expr = cf ctx in
@@ -2502,8 +2502,8 @@ let merge_into_abstraction (meta : Meta.meta) (abs_kind : abs_kind) (can_end : b
 
   (* Update the environment: replace the abstraction 1 with the result of the merge,
      remove the abstraction 0 *)
-  let ctx = fst (ctx_subst_abs ctx abs_id1 nabs) in
-  let ctx = fst (ctx_remove_abs ctx abs_id0) in
+  let ctx = fst (ctx_subst_abs meta ctx abs_id1 nabs) in
+  let ctx = fst (ctx_remove_abs meta ctx abs_id0) in
 
   (* Merge all the regions from the abstraction into one (the first - i.e., the
      one with the smallest id). Note that we need to do this in the whole
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index e489ddc3..0a5a289e 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -13,6 +13,7 @@ open ValuesUtils
 open InterpreterUtils
 open InterpreterProjectors
 open Print.EvalCtx
+open Errors
 module S = SynthesizeSymbolic
 
 (** The local logger *)
@@ -47,7 +48,7 @@ type proj_kind = LoanProj | BorrowProj
     Note that 2. and 3. may have a little bit of duplicated code, but hopefully
     it would make things clearer.
 *)
-let apply_symbolic_expansion_to_target_avalues (config : config)
+let apply_symbolic_expansion_to_target_avalues (meta : Meta.meta) (config : config)
     (allow_reborrows : bool) (proj_kind : proj_kind)
     (original_sv : symbolic_value) (expansion : symbolic_expansion)
     (ctx : eval_ctx) : eval_ctx =
@@ -65,7 +66,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
       (** When visiting an abstraction, we remember the regions it owns to be
           able to properly reduce projectors when expanding symbolic values *)
       method! visit_abs current_abs abs =
-        assert (Option.is_none current_abs);
+        cassert (Option.is_none current_abs) meta "T";
         let current_abs = Some abs in
         super#visit_abs current_abs abs
 
@@ -77,7 +78,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
       method! visit_aproj current_abs aproj =
         (match aproj with
         | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
-            assert (not (same_symbolic_id sv original_sv))
+            cassert (not (same_symbolic_id sv original_sv)) meta "T"
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj current_abs aproj
 
@@ -97,7 +98,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
             (* Check if this is the symbolic value we are looking for *)
             if same_symbolic_id sv original_sv then (
               (* There mustn't be any given back values *)
-              assert (given_back = []);
+              cassert (given_back = []) meta "T";
               (* Apply the projector *)
               let projected_value =
                 apply_proj_loans_on_symbolic_expansion proj_regions
@@ -145,11 +146,11 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
 (** Auxiliary function.
     Apply a symbolic expansion to avalues in a context.
 *)
-let apply_symbolic_expansion_to_avalues (config : config)
+let apply_symbolic_expansion_to_avalues (meta : Meta.meta) (config : config)
     (allow_reborrows : bool) (original_sv : symbolic_value)
     (expansion : symbolic_expansion) (ctx : eval_ctx) : eval_ctx =
   let apply_expansion proj_kind ctx =
-    apply_symbolic_expansion_to_target_avalues config allow_reborrows proj_kind
+    apply_symbolic_expansion_to_target_avalues meta config allow_reborrows proj_kind
       original_sv expansion ctx
   in
   (* First target the loan projectors, then the borrow projectors *)
@@ -162,12 +163,12 @@ let apply_symbolic_expansion_to_avalues (config : config)
     Simply replace the symbolic values (*not avalues*) in the context with
     a given value. Will break invariants if not used properly.
 *)
-let replace_symbolic_values (at_most_once : bool) (original_sv : symbolic_value)
+let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool) (original_sv : symbolic_value)
     (nv : value) (ctx : eval_ctx) : eval_ctx =
   (* Count *)
   let replaced = ref false in
   let replace () =
-    if at_most_once then assert (not !replaced);
+    if at_most_once then cassert (not !replaced) meta "T";
     replaced := true;
     nv
   in
@@ -186,16 +187,16 @@ let replace_symbolic_values (at_most_once : bool) (original_sv : symbolic_value)
   (* Return *)
   ctx
 
-let apply_symbolic_expansion_non_borrow (config : config)
+let apply_symbolic_expansion_non_borrow (meta : Meta.meta) (config : config)
     (original_sv : symbolic_value) (expansion : symbolic_expansion)
     (ctx : eval_ctx) : eval_ctx =
   (* Apply the expansion to non-abstraction values *)
   let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in
   let at_most_once = false in
-  let ctx = replace_symbolic_values at_most_once original_sv nv.value ctx in
+  let ctx = replace_symbolic_values meta at_most_once original_sv nv.value ctx in
   (* Apply the expansion to abstraction values *)
   let allow_reborrows = false in
-  apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
+  apply_symbolic_expansion_to_avalues meta config allow_reborrows original_sv
     expansion ctx
 
 (** Compute the expansion of a non-assumed (i.e.: not [Box], etc.)
@@ -208,13 +209,13 @@ let apply_symbolic_expansion_non_borrow (config : config)
     [expand_enumerations] controls the expansion of enumerations: if false, it
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
-let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
+let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) (expand_enumerations : bool)
     (def_id : TypeDeclId.id) (generics : generic_args) (ctx : eval_ctx) :
     symbolic_expansion list =
   (* Lookup the definition and check if it is an enumeration with several
    * variants *)
   let def = ctx_lookup_type_decl ctx def_id in
-  assert (List.length generics.regions = List.length def.generics.regions);
+  cassert (List.length generics.regions = List.length def.generics.regions) meta "T";
   (* Retrieve, for every variant, the list of its instantiated field types *)
   let variants_fields_types =
     AssociatedTypes.type_decl_get_inst_norm_variants_fields_rtypes ctx def
@@ -222,7 +223,7 @@ let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
   in
   (* Check if there is strictly more than one variant *)
   if List.length variants_fields_types > 1 && not expand_enumerations then
-    raise (Failure "Not allowed to expand enumerations with several variants");
+    craise meta "Not allowed to expand enumerations with several variants";
   (* Initialize the expanded value for a given variant *)
   let initialize ((variant_id, field_types) : VariantId.id option * rty list) :
       symbolic_expansion =
@@ -260,21 +261,21 @@ let compute_expanded_symbolic_box_value (boxed_ty : rty) : symbolic_expansion =
     [expand_enumerations] controls the expansion of enumerations: if [false], it
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
-let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
+let compute_expanded_symbolic_adt_value (meta : Meta.meta) (expand_enumerations : bool)
     (adt_id : type_id) (generics : generic_args) (ctx : eval_ctx) :
     symbolic_expansion list =
   match (adt_id, generics.regions, generics.types) with
   | TAdtId def_id, _, _ ->
-      compute_expanded_symbolic_non_assumed_adt_value expand_enumerations def_id
+      compute_expanded_symbolic_non_assumed_adt_value meta expand_enumerations def_id
         generics ctx
   | TTuple, [], _ -> [ compute_expanded_symbolic_tuple_value generics.types ]
   | TAssumed TBox, [], [ boxed_ty ] ->
       [ compute_expanded_symbolic_box_value boxed_ty ]
   | _ ->
-      raise
-        (Failure "compute_expanded_symbolic_adt_value: unexpected combination")
+      craise
+        meta "compute_expanded_symbolic_adt_value: unexpected combination"
 
-let expand_symbolic_value_shared_borrow (config : config)
+let expand_symbolic_value_shared_borrow (meta : Meta.meta) (config : config)
     (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
     (ref_ty : rty) : cm_fun =
  fun cf ctx ->
@@ -307,7 +308,7 @@ let expand_symbolic_value_shared_borrow (config : config)
             Some [ AsbBorrow bid; shared_asb ]
           else (* Not in the set: ignore *)
             Some [ shared_asb ]
-      | _ -> raise (Failure "Unexpected")
+      | _ -> craise meta "Unexpected"
     else None
   in
   (* The fresh symbolic value for the shared value *)
@@ -324,7 +325,7 @@ let expand_symbolic_value_shared_borrow (config : config)
         else super#visit_VSymbolic env sv
 
       method! visit_EAbs proj_regions abs =
-        assert (Option.is_none proj_regions);
+        cassert (Option.is_none proj_regions) meta "T";
         let proj_regions = Some abs.regions in
         super#visit_EAbs proj_regions abs
 
@@ -349,7 +350,7 @@ let expand_symbolic_value_shared_borrow (config : config)
       method! visit_aproj proj_regions aproj =
         (match aproj with
         | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
-            assert (not (same_symbolic_id sv original_sv))
+            cassert (not (same_symbolic_id sv original_sv)) meta "T"
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj proj_regions aproj
 
@@ -375,27 +376,27 @@ let expand_symbolic_value_shared_borrow (config : config)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Finally, replace the projectors on loans *)
   let bids = !borrows in
-  assert (not (BorrowId.Set.is_empty bids));
+  cassert (not (BorrowId.Set.is_empty bids)) meta "T";
   let see = SeSharedRef (bids, shared_sv) in
   let allow_reborrows = true in
   let ctx =
-    apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see
+    apply_symbolic_expansion_to_avalues meta config allow_reborrows original_sv see
       ctx
   in
   (* Call the continuation *)
   let expr = cf ctx in
   (* Update the synthesized program *)
-  S.synthesize_symbolic_expansion_no_branching original_sv original_sv_place see
+  S.synthesize_symbolic_expansion_no_branching meta original_sv original_sv_place see
     expr
 
 (** TODO: simplify and merge with the other expansion function *)
-let expand_symbolic_value_borrow (config : config)
+let expand_symbolic_value_borrow (meta : Meta.meta) (config : config)
     (original_sv : symbolic_value) (original_sv_place : SA.mplace option)
     (region : region) (ref_ty : rty) (rkind : ref_kind) : cm_fun =
  fun cf ctx ->
-  assert (region <> RErased);
+  cassert (region <> RErased) meta "T";
   (* Check that we are allowed to expand the reference *)
-  assert (not (region_in_set region ctx.ended_regions));
+  cassert (not (region_in_set region ctx.ended_regions)) meta "T";
   (* Match on the reference kind *)
   match rkind with
   | RMut ->
@@ -408,20 +409,20 @@ let expand_symbolic_value_borrow (config : config)
        * check that we perform exactly one substitution) *)
       let nv = symbolic_expansion_non_shared_borrow_to_value original_sv see in
       let at_most_once = true in
-      let ctx = replace_symbolic_values at_most_once original_sv nv.value ctx in
+      let ctx = replace_symbolic_values meta at_most_once original_sv nv.value ctx in
       (* Expand the symbolic avalues *)
       let allow_reborrows = true in
       let ctx =
-        apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
+        apply_symbolic_expansion_to_avalues meta config allow_reborrows original_sv
           see ctx
       in
       (* Apply the continuation *)
       let expr = cf ctx in
       (* Update the synthesized program *)
-      S.synthesize_symbolic_expansion_no_branching original_sv original_sv_place
+      S.synthesize_symbolic_expansion_no_branching meta original_sv original_sv_place
         see expr
   | RShared ->
-      expand_symbolic_value_shared_borrow config original_sv original_sv_place
+      expand_symbolic_value_shared_borrow meta config original_sv original_sv_place
         ref_ty cf ctx
 
 (** A small helper.
@@ -440,12 +441,12 @@ let expand_symbolic_value_borrow (config : config)
     We need this continuation separately (i.e., we can't compose it with the
     continuations in [see_cf_l]) because we perform a join *before* calling it.
 *)
-let apply_branching_symbolic_expansions_non_borrow (config : config)
+let apply_branching_symbolic_expansions_non_borrow (meta : Meta.meta) (config : config)
     (sv : symbolic_value) (sv_place : SA.mplace option)
     (see_cf_l : (symbolic_expansion option * st_cm_fun) list)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
-  assert (see_cf_l <> []);
+  cassert (see_cf_l <> []) meta "T";
   (* Apply the symbolic expansion in the context and call the continuation *)
   let resl =
     List.map
@@ -456,7 +457,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : config)
         let ctx =
           match see_opt with
           | None -> ctx
-          | Some see -> apply_symbolic_expansion_non_borrow config sv see ctx
+          | Some see -> apply_symbolic_expansion_non_borrow meta config sv see ctx
         in
         (* Debug *)
         log#ldebug
@@ -475,15 +476,15 @@ let apply_branching_symbolic_expansions_non_borrow (config : config)
     match resl with
     | Some _ :: _ -> Some (List.map Option.get resl)
     | None :: _ ->
-        List.iter (fun res -> assert (res = None)) resl;
+        List.iter (fun res -> cassert (res = None) meta "T") resl;
         None
-    | _ -> raise (Failure "Unreachable")
+    | _ -> craise meta "Unreachable"
   in
   (* Synthesize and return *)
   let seel = List.map fst see_cf_l in
-  S.synthesize_symbolic_expansion sv sv_place seel subterms
+  S.synthesize_symbolic_expansion meta sv sv_place seel subterms
 
-let expand_symbolic_bool (config : config) (sv : symbolic_value)
+let expand_symbolic_bool (meta : Meta.meta) (config : config) (sv : symbolic_value)
     (sv_place : SA.mplace option) (cf_true : st_cm_fun) (cf_false : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
@@ -491,16 +492,16 @@ let expand_symbolic_bool (config : config) (sv : symbolic_value)
   let original_sv = sv in
   let original_sv_place = sv_place in
   let rty = original_sv.sv_ty in
-  assert (rty = TLiteral TBool);
+  cassert (rty = TLiteral TBool) meta "T";
   (* Expand the symbolic value to true or false and continue execution *)
   let see_true = SeLiteral (VBool true) in
   let see_false = SeLiteral (VBool false) in
   let seel = [ (Some see_true, cf_true); (Some see_false, cf_false) ] in
   (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *)
-  apply_branching_symbolic_expansions_non_borrow config original_sv
+  apply_branching_symbolic_expansions_non_borrow meta config original_sv
     original_sv_place seel cf_after_join ctx
 
-let expand_symbolic_value_no_branching (config : config) (sv : symbolic_value)
+let expand_symbolic_value_no_branching (meta : Meta.meta) (config : config) (sv : symbolic_value)
     (sv_place : SA.mplace option) : cm_fun =
  fun cf ctx ->
   (* Debug *)
@@ -522,29 +523,29 @@ let expand_symbolic_value_no_branching (config : config) (sv : symbolic_value)
         (* Compute the expanded value *)
         let allow_branching = false in
         let seel =
-          compute_expanded_symbolic_adt_value allow_branching adt_id generics
+          compute_expanded_symbolic_adt_value meta allow_branching adt_id generics
             ctx
         in
         (* There should be exacly one branch *)
         let see = Collections.List.to_cons_nil seel in
         (* Apply in the context *)
         let ctx =
-          apply_symbolic_expansion_non_borrow config original_sv see ctx
+          apply_symbolic_expansion_non_borrow meta config original_sv see ctx
         in
         (* Call the continuation *)
         let expr = cf ctx in
         (* Update the synthesized program *)
-        S.synthesize_symbolic_expansion_no_branching original_sv
+        S.synthesize_symbolic_expansion_no_branching meta original_sv
           original_sv_place see expr
     (* Borrows *)
     | TRef (region, ref_ty, rkind) ->
-        expand_symbolic_value_borrow config original_sv original_sv_place region
+        expand_symbolic_value_borrow meta config original_sv original_sv_place region
           ref_ty rkind cf ctx
     | _ ->
-        raise
-          (Failure
+        craise
+          meta
              ("expand_symbolic_value_no_branching: unexpected type: "
-            ^ show_rty rty))
+            ^ show_rty rty)
   in
   (* Debug *)
   let cc =
@@ -556,12 +557,12 @@ let expand_symbolic_value_no_branching (config : config) (sv : symbolic_value)
             ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
             ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
         (* Sanity check: the symbolic value has disappeared *)
-        assert (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)))
+        cassert (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta "T")
   in
   (* Continue *)
   cc cf ctx
 
-let expand_symbolic_adt (config : config) (sv : symbolic_value)
+let expand_symbolic_adt (meta : Meta.meta) (config : config) (sv : symbolic_value)
     (sv_place : SA.mplace option) (cf_branches : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
  fun ctx ->
@@ -579,21 +580,21 @@ let expand_symbolic_adt (config : config) (sv : symbolic_value)
       let allow_branching = true in
       (* Compute the expanded value *)
       let seel =
-        compute_expanded_symbolic_adt_value allow_branching adt_id generics ctx
+        compute_expanded_symbolic_adt_value meta allow_branching adt_id generics ctx
       in
       (* Apply *)
       let seel = List.map (fun see -> (Some see, cf_branches)) seel in
-      apply_branching_symbolic_expansions_non_borrow config original_sv
+      apply_branching_symbolic_expansions_non_borrow meta config original_sv
         original_sv_place seel cf_after_join ctx
   | _ ->
-      raise (Failure ("expand_symbolic_adt: unexpected type: " ^ show_rty rty))
+      craise meta ("expand_symbolic_adt: unexpected type: " ^ show_rty rty)
 
-let expand_symbolic_int (config : config) (sv : symbolic_value)
+let expand_symbolic_int (meta : Meta.meta) (config : config) (sv : symbolic_value)
     (sv_place : SA.mplace option) (int_type : integer_type)
     (tgts : (scalar_value * st_cm_fun) list) (otherwise : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
   (* Sanity check *)
-  assert (sv.sv_ty = TLiteral (TInteger int_type));
+  cassert (sv.sv_ty = TLiteral (TInteger int_type)) meta "T";
   (* For all the branches of the switch, we expand the symbolic value
    * to the value given by the branch and execute the branch statement.
    * For the otherwise branch, we leave the symbolic value as it is
@@ -608,7 +609,7 @@ let expand_symbolic_int (config : config) (sv : symbolic_value)
   in
   let seel = List.append seel [ (None, otherwise) ] in
   (* Then expand and evaluate - this generates the proper symbolic AST *)
-  apply_branching_symbolic_expansions_non_borrow config sv sv_place seel
+  apply_branching_symbolic_expansions_non_borrow meta config sv sv_place seel
     cf_after_join
 
 (** Expand all the symbolic values which contain borrows.
@@ -619,7 +620,7 @@ let expand_symbolic_int (config : config) (sv : symbolic_value)
     an enumeration with strictly more than one variant, a slice, etc.) or if
     we need to expand a recursive type (because this leads to looping).
  *)
-let greedy_expand_symbolics_with_borrows (config : config) : cm_fun =
+let greedy_expand_symbolics_with_borrows (meta : Meta.meta) (config : config) : cm_fun =
  fun cf ctx ->
   (* The visitor object, to look for symbolic values in the concrete environment *)
   let obj =
@@ -660,33 +661,33 @@ let greedy_expand_symbolics_with_borrows (config : config) : cm_fun =
             (match def.kind with
             | Struct _ | Enum ([] | [ _ ]) -> ()
             | Enum (_ :: _) ->
-                raise
-                  (Failure
+                craise
+                  meta
                      ("Attempted to greedily expand a symbolic enumeration \
                        with > 1 variants (option \
                        [greedy_expand_symbolics_with_borrows] of [config]): "
-                     ^ name_to_string ctx def.name))
+                     ^ name_to_string ctx def.name)
             | Opaque ->
-                raise (Failure "Attempted to greedily expand an opaque type"));
+                craise meta "Attempted to greedily expand an opaque type");
             (* Also, we need to check if the definition is recursive *)
             if ctx_type_decl_is_rec ctx def_id then
-              raise
-                (Failure
+              craise
+                meta
                    ("Attempted to greedily expand a recursive definition \
                      (option [greedy_expand_symbolics_with_borrows] of \
                      [config]): "
-                   ^ name_to_string ctx def.name))
-            else expand_symbolic_value_no_branching config sv None
+                   ^ name_to_string ctx def.name)
+            else expand_symbolic_value_no_branching meta config sv None
         | TAdt ((TTuple | TAssumed TBox), _) | TRef (_, _, _) ->
             (* Ok *)
-            expand_symbolic_value_no_branching config sv None
+            expand_symbolic_value_no_branching meta config sv None
         | TAdt (TAssumed (TArray | TSlice | TStr), _) ->
             (* We can't expand those *)
-            raise
-              (Failure
-                 "Attempted to greedily expand an ADT which can't be expanded ")
+            craise
+              meta
+                 "Attempted to greedily expand an ADT which can't be expanded "
         | TVar _ | TLiteral _ | TNever | TTraitType _ | TArrow _ | TRawPtr _ ->
-            raise (Failure "Unreachable")
+            craise meta "Unreachable"
       in
       (* Compose and continue *)
       comp cc expand cf ctx
@@ -694,9 +695,9 @@ let greedy_expand_symbolics_with_borrows (config : config) : cm_fun =
   (* Apply *)
   expand cf ctx
 
-let greedy_expand_symbolic_values (config : config) : cm_fun =
+let greedy_expand_symbolic_values (meta : Meta.meta) (config : config) : cm_fun =
  fun cf ctx ->
   if Config.greedy_expand_symbolics_with_borrows then (
     log#ldebug (lazy "greedy_expand_symbolic_values");
-    greedy_expand_symbolics_with_borrows config cf ctx)
+    greedy_expand_symbolics_with_borrows meta config cf ctx)
   else cf ctx
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index afbf4605..51be904f 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -23,7 +23,7 @@ let log = Logging.expressions_log
     Note that the place should have been prepared so that there are no remaining
     loans.
 *)
-let expand_primitively_copyable_at_place (config : config)
+let expand_primitively_copyable_at_place (meta : Meta.meta) (config : config)
     (access : access_kind) (p : place) : cm_fun =
  fun cf ctx ->
   (* Small helper *)
@@ -36,7 +36,7 @@ let expand_primitively_copyable_at_place (config : config)
     | None -> cf ctx
     | Some sv ->
         let cc =
-          expand_symbolic_value_no_branching config sv (Some (mk_mplace p ctx))
+          expand_symbolic_value_no_branching config sv (Some (mk_mplace meta p ctx))
         in
         comp cc expand cf ctx
   in
@@ -59,7 +59,7 @@ let read_place (access : access_kind) (p : place) (cf : typed_value -> m_fun) :
   (* Call the continuation *)
   cf v ctx
 
-let access_rplace_reorganize_and_read (config : config)
+let access_rplace_reorganize_and_read (meta : Meta.meta) (config : config)
     (expand_prim_copy : bool) (access : access_kind) (p : place)
     (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
@@ -71,7 +71,7 @@ let access_rplace_reorganize_and_read (config : config)
    * borrows) *)
   let cc =
     if expand_prim_copy then
-      comp cc (expand_primitively_copyable_at_place config access p)
+      comp cc (expand_primitively_copyable_at_place meta config access p)
     else cc
   in
   (* Read the place - note that this checks that the value doesn't contain bottoms *)
@@ -79,10 +79,10 @@ let access_rplace_reorganize_and_read (config : config)
   (* Compose *)
   comp cc read_place cf ctx
 
-let access_rplace_reorganize (config : config) (expand_prim_copy : bool)
+let access_rplace_reorganize (meta : Meta.meta) (config : config) (expand_prim_copy : bool)
     (access : access_kind) (p : place) : cm_fun =
  fun cf ctx ->
-  access_rplace_reorganize_and_read config expand_prim_copy access p
+  access_rplace_reorganize_and_read meta config expand_prim_copy access p
     (fun _v -> cf)
     ctx
 
@@ -224,7 +224,7 @@ let rec copy_value (allow_adt_copy : bool) (config : config) (ctx : eval_ctx)
     what we do in the formalization (because we don't enforce the same constraints
     as MIR in the formalization).
  *)
-let prepare_eval_operand_reorganize (config : config) (op : operand) : cm_fun =
+let prepare_eval_operand_reorganize (meta : Meta.meta) (config : config) (op : operand) : cm_fun =
  fun cf ctx ->
   let prepare : cm_fun =
    fun cf ctx ->
@@ -237,12 +237,12 @@ let prepare_eval_operand_reorganize (config : config) (op : operand) : cm_fun =
         let access = Read in
         (* Expand the symbolic values, if necessary *)
         let expand_prim_copy = true in
-        access_rplace_reorganize config expand_prim_copy access p cf ctx
+        access_rplace_reorganize meta config expand_prim_copy access p cf ctx
     | Move p ->
         (* Access the value *)
         let access = Move in
         let expand_prim_copy = false in
-        access_rplace_reorganize config expand_prim_copy access p cf ctx
+        access_rplace_reorganize meta config expand_prim_copy access p cf ctx
   in
   (* Apply *)
   prepare cf ctx
@@ -358,7 +358,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
       (* Compose and apply *)
       comp cc move cf ctx
 
-let eval_operand (config : config) (op : operand) (cf : typed_value -> m_fun) :
+let eval_operand (meta : Meta.meta)  (config : config) (op : operand) (cf : typed_value -> m_fun) :
     m_fun =
  fun ctx ->
   (* Debug *)
@@ -368,7 +368,7 @@ let eval_operand (config : config) (op : operand) (cf : typed_value -> m_fun) :
      ^ eval_ctx_to_string ctx ^ "\n"));
   (* We reorganize the context, then evaluate the operand *)
   comp
-    (prepare_eval_operand_reorganize config op)
+    (prepare_eval_operand_reorganize meta config op)
     (eval_operand_no_reorganize config op)
     cf ctx
 
@@ -376,16 +376,16 @@ let eval_operand (config : config) (op : operand) (cf : typed_value -> m_fun) :
 
     See [prepare_eval_operand_reorganize].
  *)
-let prepare_eval_operands_reorganize (config : config) (ops : operand list) :
+let prepare_eval_operands_reorganize (meta : Meta.meta) (config : config) (ops : operand list) :
     cm_fun =
-  fold_left_apply_continuation (prepare_eval_operand_reorganize config) ops
+  fold_left_apply_continuation (prepare_eval_operand_reorganize meta config) ops
 
 (** Evaluate several operands. *)
-let eval_operands (config : config) (ops : operand list)
+let eval_operands (meta : Meta.meta) (config : config) (ops : operand list)
     (cf : typed_value list -> m_fun) : m_fun =
  fun ctx ->
   (* Prepare the operands *)
-  let prepare = prepare_eval_operands_reorganize config ops in
+  let prepare = prepare_eval_operands_reorganize meta config ops in
   (* Evaluate the operands *)
   let eval =
     fold_left_list_apply_continuation (eval_operand_no_reorganize config) ops
@@ -393,9 +393,9 @@ let eval_operands (config : config) (ops : operand list)
   (* Compose and apply *)
   comp prepare eval cf ctx
 
-let eval_two_operands (config : config) (op1 : operand) (op2 : operand)
+let eval_two_operands (meta : Meta.meta) (config : config) (op1 : operand) (op2 : operand)
     (cf : typed_value * typed_value -> m_fun) : m_fun =
-  let eval_op = eval_operands config [ op1; op2 ] in
+  let eval_op = eval_operands meta config [ op1; op2 ] in
   let use_res cf res =
     match res with
     | [ v1; v2 ] -> cf (v1, v2)
@@ -403,10 +403,10 @@ let eval_two_operands (config : config) (op1 : operand) (op2 : operand)
   in
   comp eval_op use_res cf
 
-let eval_unary_op_concrete (config : config) (unop : unop) (op : operand)
+let eval_unary_op_concrete (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
     (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   (* Evaluate the operand *)
-  let eval_op = eval_operand config op in
+  let eval_op = eval_operand meta config op in
   (* Apply the unop *)
   let apply cf (v : typed_value) : m_fun =
     match (unop, v.value) with
@@ -451,11 +451,11 @@ let eval_unary_op_concrete (config : config) (unop : unop) (op : operand)
   in
   comp eval_op apply cf
 
-let eval_unary_op_symbolic (config : config) (unop : unop) (op : operand)
+let eval_unary_op_symbolic (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
     (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   (* Evaluate the operand *)
-  let eval_op = eval_operand config op in
+  let eval_op = eval_operand meta config op in
   (* Generate a fresh symbolic value to store the result *)
   let apply cf (v : typed_value) : m_fun =
    fun ctx ->
@@ -472,17 +472,17 @@ let eval_unary_op_symbolic (config : config) (unop : unop) (op : operand)
     let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in
     (* Synthesize the symbolic AST *)
     synthesize_unary_op ctx unop v
-      (mk_opt_place_from_op op ctx)
+      (mk_opt_place_from_op meta op ctx)
       res_sv None expr
   in
   (* Compose and apply *)
   comp eval_op apply cf ctx
 
-let eval_unary_op (config : config) (unop : unop) (op : operand)
+let eval_unary_op (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
     (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   match config.mode with
-  | ConcreteMode -> eval_unary_op_concrete config unop op cf
-  | SymbolicMode -> eval_unary_op_symbolic config unop op cf
+  | ConcreteMode -> eval_unary_op_concrete meta config unop op cf
+  | SymbolicMode -> eval_unary_op_symbolic meta config unop op cf
 
 (** Small helper for [eval_binary_op_concrete]: computes the result of applying
     the binop *after* the operands have been successfully evaluated
@@ -557,10 +557,10 @@ let eval_binary_op_concrete_compute (binop : binop) (v1 : typed_value)
         | Ne | Eq -> raise (Failure "Unreachable"))
     | _ -> raise (Failure "Invalid inputs for binop")
 
-let eval_binary_op_concrete (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op_concrete (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
     (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   (* Evaluate the operands *)
-  let eval_ops = eval_two_operands config op1 op2 in
+  let eval_ops = eval_two_operands meta config op1 op2 in
   (* Compute the result of the binop *)
   let compute cf (res : typed_value * typed_value) =
     let v1, v2 = res in
@@ -569,11 +569,11 @@ let eval_binary_op_concrete (config : config) (binop : binop) (op1 : operand)
   (* Compose and apply *)
   comp eval_ops compute cf
 
-let eval_binary_op_symbolic (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op_symbolic (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
     (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   (* Evaluate the operands *)
-  let eval_ops = eval_two_operands config op1 op2 in
+  let eval_ops = eval_two_operands meta config op1 op2 in
   (* Compute the result of applying the binop *)
   let compute cf ((v1, v2) : typed_value * typed_value) : m_fun =
    fun ctx ->
@@ -609,20 +609,20 @@ let eval_binary_op_symbolic (config : config) (binop : binop) (op1 : operand)
     let v = mk_typed_value_from_symbolic_value res_sv in
     let expr = cf (Ok v) ctx in
     (* Synthesize the symbolic AST *)
-    let p1 = mk_opt_place_from_op op1 ctx in
-    let p2 = mk_opt_place_from_op op2 ctx in
+    let p1 = mk_opt_place_from_op meta op1 ctx in
+    let p2 = mk_opt_place_from_op meta op2 ctx in
     synthesize_binary_op ctx binop v1 p1 v2 p2 res_sv None expr
   in
   (* Compose and apply *)
   comp eval_ops compute cf ctx
 
-let eval_binary_op (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
     (op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
   match config.mode with
-  | ConcreteMode -> eval_binary_op_concrete config binop op1 op2 cf
-  | SymbolicMode -> eval_binary_op_symbolic config binop op1 op2 cf
+  | ConcreteMode -> eval_binary_op_concrete meta config binop op1 op2 cf
+  | SymbolicMode -> eval_binary_op_symbolic meta config binop op1 op2 cf
 
-let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
+let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : borrow_kind)
     (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   match bkind with
@@ -643,7 +643,7 @@ let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
 
       let expand_prim_copy = false in
       let prepare =
-        access_rplace_reorganize_and_read config expand_prim_copy access p
+        access_rplace_reorganize_and_read meta config expand_prim_copy access p
       in
       (* Evaluate the borrowing operation *)
       let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun =
@@ -693,7 +693,7 @@ let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
       let access = Write in
       let expand_prim_copy = false in
       let prepare =
-        access_rplace_reorganize_and_read config expand_prim_copy access p
+        access_rplace_reorganize_and_read meta config expand_prim_copy access p
       in
       (* Evaluate the borrowing operation *)
       let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun =
@@ -714,10 +714,10 @@ let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
       (* Compose and apply *)
       comp prepare eval cf ctx
 
-let eval_rvalue_aggregate (config : config) (aggregate_kind : aggregate_kind)
+let eval_rvalue_aggregate (meta : Meta.meta) (config : config) (aggregate_kind : aggregate_kind)
     (ops : operand list) (cf : typed_value -> m_fun) : m_fun =
   (* Evaluate the operands *)
-  let eval_ops = eval_operands config ops in
+  let eval_ops = eval_operands meta config ops in
   (* Compute the value *)
   let compute (cf : typed_value -> m_fun) (values : typed_value list) : m_fun =
    fun ctx ->
@@ -781,7 +781,7 @@ let eval_rvalue_aggregate (config : config) (aggregate_kind : aggregate_kind)
   (* Compose and apply *)
   comp eval_ops compute cf
 
-let eval_rvalue_not_global (config : config) (rvalue : rvalue)
+let eval_rvalue_not_global (meta : Meta.meta) (config : config) (rvalue : rvalue)
     (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
   log#ldebug (lazy "eval_rvalue");
@@ -793,12 +793,12 @@ let eval_rvalue_not_global (config : config) (rvalue : rvalue)
   let comp_wrap f = comp f wrap_in_result cf in
   (* Delegate to the proper auxiliary function *)
   match rvalue with
-  | Use op -> comp_wrap (eval_operand config op) ctx
-  | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx
-  | UnaryOp (unop, op) -> eval_unary_op config unop op cf ctx
-  | BinaryOp (binop, op1, op2) -> eval_binary_op config binop op1 op2 cf ctx
+  | Use op -> comp_wrap (eval_operand meta config op) ctx
+  | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref meta config p bkind) ctx
+  | UnaryOp (unop, op) -> eval_unary_op meta config unop op cf ctx
+  | BinaryOp (binop, op1, op2) -> eval_binary_op meta config binop op1 op2 cf ctx
   | Aggregate (aggregate_kind, ops) ->
-      comp_wrap (eval_rvalue_aggregate config aggregate_kind ops) ctx
+      comp_wrap (eval_rvalue_aggregate meta config aggregate_kind ops) ctx
   | Discriminant _ ->
       raise
         (Failure
@@ -806,11 +806,11 @@ let eval_rvalue_not_global (config : config) (rvalue : rvalue)
             the AST")
   | Global _ -> raise (Failure "Unreachable")
 
-let eval_fake_read (config : config) (p : place) : cm_fun =
+let eval_fake_read (meta : Meta.meta) (config : config) (p : place) : cm_fun =
  fun cf ctx ->
   let expand_prim_copy = false in
   let cf_prepare cf =
-    access_rplace_reorganize_and_read config expand_prim_copy Read p cf
+    access_rplace_reorganize_and_read meta config expand_prim_copy Read p cf
   in
   let cf_continue cf v : m_fun =
    fun ctx ->
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index b07ba943..35582456 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -693,7 +693,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
                   AbstractionId.of_int (RegionGroupId.to_int rg_id)
                 in
                 (* By default, the [SynthInput] abs can't end *)
-                let ctx = ctx_set_abs_can_end ctx abs_id true in
+                let ctx = ctx_set_abs_can_end meta ctx abs_id true in
                 cassert (
                   let abs = ctx_lookup_abs ctx abs_id in
                   abs.kind = SynthInput rg_id) meta "TODO :  error message ";
@@ -764,7 +764,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
               in
               let abs = ctx_lookup_abs !fp !id0 in
               let abs = { abs with kind = abs_kind } in
-              let fp', _ = ctx_subst_abs !fp !id0 abs in
+              let fp', _ = ctx_subst_abs meta !fp !id0 abs in
               fp := fp';
               (* Merge all the abstractions into this one *)
               List.iter
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index e411db9b..cc1e3208 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -259,13 +259,13 @@ let access_place (meta : Meta.meta) (access : projection_access)
       (update : typed_value -> typed_value) (p : place) (ctx : eval_ctx) :
     (eval_ctx * typed_value) path_access_result =
   (* Lookup the variable's value *)
-  let value = ctx_lookup_var_value ctx p.var_id in
+  let value = ctx_lookup_var_value meta ctx p.var_id in
   (* Apply the projection *)
   match access_projection meta access ctx update p.projection value with
   | Error err -> Error err
   | Ok (ctx, res) ->
       (* Update the value *)
-      let ctx = ctx_update_var_value ctx p.var_id res.updated in
+      let ctx = ctx_update_var_value meta ctx p.var_id res.updated in
       (* Return *)
       Ok (ctx, res.read)
 
@@ -465,7 +465,7 @@ let rec update_ctx_along_read_place (meta : Meta.meta) (config : config) (access
             in
             let prefix = { p with projection = proj } in
             expand_symbolic_value_no_branching config sp
-              (Some (Synth.mk_mplace prefix ctx))
+              (Some (Synth.mk_mplace meta prefix ctx))
         | FailBottom (_, _, _) ->
             (* We can't expand {!Bottom} values while reading them *)
             craise meta "Found [Bottom] while reading a place"
@@ -490,7 +490,7 @@ let rec update_ctx_along_write_place (meta : Meta.meta) (config : config) (acces
         | FailSymbolic (_pe, sp) ->
             (* Expand the symbolic value *)
             expand_symbolic_value_no_branching config sp
-              (Some (Synth.mk_mplace p ctx))
+              (Some (Synth.mk_mplace meta p ctx))
         | FailBottom (remaining_pes, pe, ty) ->
             (* Expand the {!Bottom} value *)
             fun cf ctx ->
@@ -575,7 +575,7 @@ let drop_outer_loans_at_lplace (meta : Meta.meta) (config : config) (p : place)
   let rec drop : cm_fun =
    fun cf ctx ->
     (* Read the value *)
-    let v = ctx_lookup_dummy_var ctx dummy_id in
+    let v = ctx_lookup_dummy_var meta ctx dummy_id in
     (* Check if there are loans or borrows to end *)
     let with_borrows = false in
     match get_first_outer_loan_or_borrow_in_value with_borrows v with
@@ -599,7 +599,7 @@ let drop_outer_loans_at_lplace (meta : Meta.meta) (config : config) (p : place)
   let cc =
     comp cc (fun cf ctx ->
         (* Pop *)
-        let ctx, v = ctx_remove_dummy_var ctx dummy_id in
+        let ctx, v = ctx_remove_dummy_var meta ctx dummy_id in
         (* Reinsert *)
         let ctx = write_place meta access p v ctx in
         (* Sanity check *)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index bd6fab1a..8ccdcc93 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -58,33 +58,33 @@ let push_dummy_var (vid : DummyVarId.id) (v : typed_value) : cm_fun =
   cf ctx
 
 (** Remove a dummy variable from the environment *)
-let remove_dummy_var (vid : DummyVarId.id) (cf : typed_value -> m_fun) : m_fun =
+let remove_dummy_var (meta : Meta.meta) (vid : DummyVarId.id) (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
-  let ctx, v = ctx_remove_dummy_var ctx vid in
+  let ctx, v = ctx_remove_dummy_var meta ctx vid in
   cf v ctx
 
 (** Push an uninitialized variable to the environment *)
-let push_uninitialized_var (var : var) : cm_fun =
+let push_uninitialized_var (meta : Meta.meta) (var : var) : cm_fun =
  fun cf ctx ->
-  let ctx = ctx_push_uninitialized_var ctx var in
+  let ctx = ctx_push_uninitialized_var meta ctx var in
   cf ctx
 
 (** Push a list of uninitialized variables to the environment *)
-let push_uninitialized_vars (vars : var list) : cm_fun =
+let push_uninitialized_vars (meta : Meta.meta) (vars : var list) : cm_fun =
  fun cf ctx ->
-  let ctx = ctx_push_uninitialized_vars ctx vars in
+  let ctx = ctx_push_uninitialized_vars meta ctx vars in
   cf ctx
 
 (** Push a variable to the environment *)
-let push_var (var : var) (v : typed_value) : cm_fun =
+let push_var (meta : Meta.meta) (var : var) (v : typed_value) : cm_fun =
  fun cf ctx ->
-  let ctx = ctx_push_var ctx var v in
+  let ctx = ctx_push_var meta ctx var v in
   cf ctx
 
 (** Push a list of variables to the environment *)
-let push_vars (vars : (var * typed_value) list) : cm_fun =
+let push_vars (meta : Meta.meta) (vars : (var * typed_value) list) : cm_fun =
  fun cf ctx ->
-  let ctx = ctx_push_vars ctx vars in
+  let ctx = ctx_push_vars meta ctx vars in
   cf ctx
 
 (** Assign a value to a given place.
@@ -108,7 +108,7 @@ let assign_to_place (meta : Meta.meta) (config : config) (rv : typed_value) (p :
   (* Prepare the destination *)
   let cc = comp cc (prepare_lplace config p) in
   (* Retrieve the rvalue from the dummy variable *)
-  let cc = comp cc (fun cf _lv -> remove_dummy_var rvalue_vid cf) in
+  let cc = comp cc (fun cf _lv -> remove_dummy_var meta rvalue_vid cf) in
   (* Update the destination *)
   let move_dest cf (rv : typed_value) : m_fun =
    fun ctx ->
@@ -538,7 +538,7 @@ let eval_assumed_function_call_concrete (meta : Meta.meta) (config : config) (fi
             let ret_vid = VarId.zero in
             let ret_ty = get_assumed_function_return_type meta ctx fid generics in
             let ret_var = mk_var ret_vid (Some "@return") ret_ty in
-            let cc = comp cc (push_uninitialized_var ret_var) in
+            let cc = comp cc (push_uninitialized_var meta ret_var) in
 
             (* Create and push the input variables *)
             let input_vars =
@@ -546,7 +546,7 @@ let eval_assumed_function_call_concrete (meta : Meta.meta) (config : config) (fi
                 (fun id (v : typed_value) -> (mk_var id None v.ty, v))
                 args_vl
             in
-            let cc = comp cc (push_vars input_vars) in
+            let cc = comp cc (push_vars meta input_vars) in
 
             (* "Execute" the function body. As the functions are assumed, here we call
              * custom functions to perform the proper manipulations: we don't have
@@ -981,10 +981,10 @@ let rec eval_statement (meta : Meta.meta) (config : config) (st : statement) : s
                       let rp = rvalue_get_place rvalue in
                       let rp =
                         match rp with
-                        | Some rp -> Some (S.mk_mplace rp ctx)
+                        | Some rp -> Some (S.mk_mplace meta rp ctx)
                         | None -> None
                       in
-                      S.synthesize_assignment ctx (S.mk_mplace p ctx) rv rp expr
+                      S.synthesize_assignment ctx (S.mk_mplace meta p ctx) rv rp expr
                   )
             in
 
@@ -1094,7 +1094,7 @@ and eval_switch (meta : Meta.meta) (config : config) (switch : switch) : st_cm_f
               let cf_true : st_cm_fun = eval_statement meta config st1 in
               let cf_false : st_cm_fun = eval_statement meta config st2 in
               expand_symbolic_bool config sv
-                (S.mk_opt_place_from_op op ctx)
+                (S.mk_opt_place_from_op meta op ctx)
                 cf_true cf_false cf ctx
           | _ -> craise meta "Inconsistent state"
         in
@@ -1141,7 +1141,7 @@ and eval_switch (meta : Meta.meta) (config : config) (switch : switch) : st_cm_f
               let otherwise = eval_statement meta config otherwise in
               (* Expand and continue *)
               expand_symbolic_int config sv
-                (S.mk_opt_place_from_op op ctx)
+                (S.mk_opt_place_from_op meta op ctx)
                 int_ty stgts otherwise cf ctx
           | _ -> craise meta "Inconsistent state"
         in
@@ -1175,7 +1175,7 @@ and eval_switch (meta : Meta.meta) (config : config) (switch : switch) : st_cm_f
           | VSymbolic sv ->
               (* Expand the symbolic value - may lead to branching *)
               let cf_expand =
-                expand_symbolic_adt config sv (Some (S.mk_mplace p ctx))
+                expand_symbolic_adt config sv (Some (S.mk_mplace meta p ctx))
               in
               (* Re-evaluate the switch - the value is not symbolic anymore,
                  which means we will go to the other branch *)
@@ -1280,7 +1280,7 @@ and eval_transparent_function_call_concrete (meta : Meta.meta) (config : config)
         in
 
         let cc =
-          comp_transmit cc (push_var ret_var (mk_bottom ret_var.var_ty))
+          comp_transmit cc (push_var meta ret_var (mk_bottom ret_var.var_ty))
         in
 
         (* 2. Push the input values *)
@@ -1288,12 +1288,12 @@ and eval_transparent_function_call_concrete (meta : Meta.meta) (config : config)
           let inputs = List.combine input_locals args in
           (* Note that this function checks that the variables and their values
            * have the same type (this is important) *)
-          push_vars inputs cf
+          push_vars meta inputs cf
         in
         let cc = comp cc cf_push_inputs in
 
         (* 3. Push the remaining local variables (initialized as {!Bottom}) *)
-        let cc = comp cc (push_uninitialized_vars locals) in
+        let cc = comp cc (push_uninitialized_vars meta locals) in
 
         (* Execute the function body *)
         let cc = comp cc (eval_function_body meta config body_st) in
@@ -1366,8 +1366,8 @@ and eval_function_call_symbolic_from_inst_sig (meta : Meta.meta) (config : confi
   let ret_av regions =
     mk_aproj_loans_value_from_symbolic_value regions ret_spc
   in
-  let args_places = List.map (fun p -> S.mk_opt_place_from_op p ctx) args in
-  let dest_place = Some (S.mk_mplace dest ctx) in
+  let args_places = List.map (fun p -> S.mk_opt_place_from_op meta p ctx) args in
+  let dest_place = Some (S.mk_mplace meta dest ctx) in
 
   (* Evaluate the input operands *)
   let cc = eval_operands config args in
diff --git a/compiler/Main.ml b/compiler/Main.ml
index e4e4ce1f..bea7e4a8 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -271,7 +271,7 @@ let () =
       (* Some options for the execution *)
 
       (* Test the unit functions with the concrete interpreter *)
-      if !test_unit_functions then Test.test_unit_functions m;
+      if !test_unit_functions then Test.test_unit_functions meta m;
 
       (* Translate the functions *)
       Aeneas.Translate.translate_crate meta filename dest_dir m;
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index ad34c48e..787bfb4f 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -4,21 +4,22 @@ open Expressions
 open Values
 open LlbcAst
 open SymbolicAst
+open Errors
 
-let mk_mplace (p : place) (ctx : Contexts.eval_ctx) : mplace =
-  let bv = Contexts.ctx_lookup_var_binder ctx p.var_id in
+let mk_mplace (meta : Meta.meta) (p : place) (ctx : Contexts.eval_ctx) : mplace =
+  let bv = Contexts.ctx_lookup_var_binder meta ctx p.var_id in
   { bv; projection = p.projection }
 
-let mk_opt_mplace (p : place option) (ctx : Contexts.eval_ctx) : mplace option =
-  Option.map (fun p -> mk_mplace p ctx) p
+let mk_opt_mplace (meta : Meta.meta) (p : place option) (ctx : Contexts.eval_ctx) : mplace option =
+  Option.map (fun p -> mk_mplace meta p ctx) p
 
-let mk_opt_place_from_op (op : operand) (ctx : Contexts.eval_ctx) :
+let mk_opt_place_from_op (meta : Meta.meta) (op : operand) (ctx : Contexts.eval_ctx) :
     mplace option =
-  match op with Copy p | Move p -> Some (mk_mplace p ctx) | Constant _ -> None
+  match op with Copy p | Move p -> Some (mk_mplace meta p ctx) | Constant _ -> None
 
 let mk_emeta (m : emeta) (e : expression) : expression = Meta (m, e)
 
-let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
+let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) (place : mplace option)
     (seel : symbolic_expansion option list) (el : expression list option) :
     expression option =
   match el with
@@ -36,7 +37,7 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
              (Some (SeLiteral (VBool false)), false_exp);
             ] ->
                 ExpandBool (true_exp, false_exp)
-            | _ -> raise (Failure "Ill-formed boolean expansion"))
+            | _ -> craise meta "Ill-formed boolean expansion")
         | TLiteral (TInteger int_ty) ->
             (* Switch over an integer: split between the "regular" branches
                and the "otherwise" branch (which should be the last branch) *)
@@ -46,9 +47,9 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
             let get_scalar (see : symbolic_expansion option) : scalar_value =
               match see with
               | Some (SeLiteral (VScalar cv)) ->
-                  assert (cv.int_ty = int_ty);
+                  cassert (cv.int_ty = int_ty) meta "For all the regular branches, the symbolic value should have been expanded to a constant TODO: Error message";
                   cv
-              | _ -> raise (Failure "Unreachable")
+              | _ -> craise meta "Unreachable"
             in
             let branches =
               List.map (fun (see, exp) -> (get_scalar see, exp)) branches
@@ -56,7 +57,7 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
             (* For the otherwise branch, the symbolic value should have been left
              * unchanged *)
             let otherwise_see, otherwise = otherwise in
-            assert (otherwise_see = None);
+            cassert (otherwise_see = None) meta "For the otherwise branch, the symbolic value should have been left unchanged";
             (* Return *)
             ExpandInt (int_ty, branches, otherwise)
         | TAdt (_, _) ->
@@ -65,7 +66,7 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
                 VariantId.id option * symbolic_value list =
               match see with
               | Some (SeAdt (vid, fields)) -> (vid, fields)
-              | _ -> raise (Failure "Ill-formed branching ADT expansion")
+              | _ -> craise meta "Ill-formed branching ADT expansion"
             in
             let exp =
               List.map
@@ -79,18 +80,18 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
             (* Reference expansion: there should be one branch *)
             match ls with
             | [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
-            | _ -> raise (Failure "Ill-formed borrow expansion"))
+            | _ -> craise meta "Ill-formed borrow expansion")
         | TVar _ | TLiteral TChar | TNever | TTraitType _ | TArrow _ | TRawPtr _
           ->
-            raise (Failure "Ill-formed symbolic expansion")
+            craise meta "Ill-formed symbolic expansion"
       in
       Some (Expansion (place, sv, expansion))
 
-let synthesize_symbolic_expansion_no_branching (sv : symbolic_value)
+let synthesize_symbolic_expansion_no_branching (meta : Meta.meta) (sv : symbolic_value)
     (place : mplace option) (see : symbolic_expansion) (e : expression option) :
     expression option =
   let el = Option.map (fun e -> [ e ]) e in
-  synthesize_symbolic_expansion sv place [ Some see ] el
+  synthesize_symbolic_expansion meta sv place [ Some see ] el
 
 let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
     (sg : fun_sig option) (regions_hierarchy : region_var_groups)
@@ -188,7 +189,7 @@ let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list)
              loop_expr;
              meta;
            })
-  | _ -> raise (Failure "Unreachable")
+  | _ -> craise meta "Unreachable"
 
 let save_snapshot (ctx : Contexts.eval_ctx) (e : expression option) :
     expression option =
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 04aadafe..43d2fbb0 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -20,7 +20,7 @@ type symbolic_fun_translation = symbolic_value list * SA.expression
 (** Execute the symbolic interpreter on a function to generate a list of symbolic ASTs,
     for the forward function and the backward functions.
 *)
-let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
+let translate_function_to_symbolics (meta : Meta.meta) (trans_ctx : trans_ctx) (fdef : fun_decl) :
     symbolic_fun_translation option =
   (* Debug *)
   log#ldebug
@@ -32,7 +32,7 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
   | Some _ ->
       (* Evaluate *)
       let synthesize = true in
-      let inputs, symb = evaluate_function_symbolic synthesize trans_ctx fdef in
+      let inputs, symb = evaluate_function_symbolic meta synthesize trans_ctx fdef in
       Some (inputs, Option.get symb)
 
 (** Translate a function, by generating its forward and backward translations.
@@ -50,7 +50,7 @@ let translate_function_to_pure (meta : Meta.meta) (trans_ctx : trans_ctx)
     (lazy ("translate_function_to_pure: " ^ name_to_string trans_ctx fdef.name));
 
   (* Compute the symbolic ASTs, if the function is transparent *)
-  let symbolic_trans = translate_function_to_symbolics trans_ctx fdef in
+  let symbolic_trans = translate_function_to_symbolics meta trans_ctx fdef in
 
   (* Convert the symbolic ASTs to pure ASTs: *)