diff --git a/catala.opam b/catala.opam
index a98e01242..4917d14e6 100644
--- a/catala.opam
+++ b/catala.opam
@@ -31,7 +31,7 @@ depends: [
   "ocaml" {>= "4.13.0"}
   "ocamlfind" {!= "1.9.5"}
   "ocamlgraph" {>= "1.8.8"}
-  "ppx_yojson_conv" {>= "0.14.0"}
+  "ppx_yojson_conv" {= "v0.15.1"}
   "re" {>= "1.9.0"}
   "sedlex" {>= "2.4"}
   "uutf" {>= "1.0.3"}
diff --git a/compiler/driver.ml b/compiler/driver.ml
index e910d90fc..ccdc1e5f7 100644
--- a/compiler/driver.ml
+++ b/compiler/driver.ml
@@ -370,8 +370,7 @@ let driver source_file (options : Cli.options) : int =
                 | None -> None
                 | Some _ -> Some scope_uid)
             in
-
-            Verification.Solver.solve_vc prgm.decl_ctx vcs
+            Verification.Solver.solve_vcs prgm.decl_ctx vcs
           | `Interpret ->
             Message.emit_debug "Starting interpretation (dcalc)...";
             let results =
diff --git a/compiler/shared_ast/print.ml b/compiler/shared_ast/print.ml
index 08325fea4..734dbfa48 100644
--- a/compiler/shared_ast/print.ml
+++ b/compiler/shared_ast/print.ml
@@ -542,7 +542,10 @@ let rec expr_aux :
     pr colors fmt e;
     Format.pp_close_box fmt ()
   | EApp { f = EOp { op; _ }, _; args = [arg1] } ->
-    Format.fprintf fmt "@[<hv 2>%a@ %a@]" (operator ~debug) op (rhs exprc) arg1
+    (* FIXME: I'd like to have an imperative style printing of function calls
+       (ie f(a,b,c) rather than (f a b c)) for Mopsa export. How to concialiate
+       both? *)
+    Format.fprintf fmt "@[<hv 2>%a(%a)@]" (operator ~debug) op (rhs exprc) arg1
   | EApp { f; args } ->
     Format.fprintf fmt "@[<hv 2>%a@ %a@]" (lhs exprc) f
       (Format.pp_print_list
diff --git a/compiler/shared_ast/var.ml b/compiler/shared_ast/var.ml
index c1760b1a6..c21ed1437 100644
--- a/compiler/shared_ast/var.ml
+++ b/compiler/shared_ast/var.ml
@@ -76,6 +76,11 @@ module Set = struct
   let of_list l = of_list (List.map t l)
   let elements s = elements s |> List.map get
   let diff s1 s2 = diff s1 s2
+  let choose_opt s = Option.map get (choose_opt s)
+  let filter f s = filter (fun v -> f (get v)) s
+  let exists f s = exists (fun v -> f (get v)) s
+  let inter s1 s2 = inter s1 s2
+  let fold f s init = fold (fun v acc -> f (get v) acc) s init
 
   (* Add more as needed *)
 end
@@ -95,9 +100,14 @@ module Map = struct
   let find v m = find (t v) m
   let find_opt v m = find_opt (t v) m
   let bindings m = bindings m |> List.map (fun (v, x) -> get v, x)
+  let map f m = map f m
+  let mapi f m = mapi (fun v x -> f (get v) x) m
   let mem x m = mem (t x) m
   let union f m1 m2 = union (fun v x1 x2 -> f (get v) x1 x2) m1 m2
   let fold f m acc = fold (fun v x acc -> f (get v) x acc) m acc
+  let filter f m = filter (fun k v -> f (get k) v) m
+  let exists f m = exists (fun k v -> f (get k) v) m
+  let remove x s = remove (t x) s
 
   (* Add more as needed *)
 end
diff --git a/compiler/shared_ast/var.mli b/compiler/shared_ast/var.mli
index c03e64289..047ad31c5 100644
--- a/compiler/shared_ast/var.mli
+++ b/compiler/shared_ast/var.mli
@@ -49,6 +49,11 @@ module Set : sig
   val of_list : 'e var list -> 'e t
   val elements : 'e t -> 'e var list
   val diff : 'e t -> 'e t -> 'e t
+  val choose_opt : 'e t -> 'e var option
+  val filter : ('e var -> bool) -> 'e t -> 'e t
+  val exists : ('e var -> bool) -> 'e t -> bool
+  val inter : 'e t -> 'e t -> 'e t
+  val fold : ('e var -> 'x -> 'x) -> 'e t -> 'x -> 'x
 end
 
 (** Wrapper over [Map.S] but with a type variable for the AST type parameters.
@@ -59,14 +64,19 @@ module Map : sig
   val empty : ('e, 'x) t
   val singleton : 'e var -> 'x -> ('e, 'x) t
   val add : 'e var -> 'x -> ('e, 'x) t -> ('e, 'x) t
+  val remove : 'e var -> ('e, 'x) t -> ('e, 'x) t
   val update : 'e var -> ('x option -> 'x option) -> ('e, 'x) t -> ('e, 'x) t
   val find : 'e var -> ('e, 'x) t -> 'x
   val find_opt : 'e var -> ('e, 'x) t -> 'x option
   val bindings : ('e, 'x) t -> ('e var * 'x) list
   val mem : 'e var -> ('e, 'x) t -> bool
+  val map : ('x -> 'y) -> ('e, 'x) t -> ('e, 'y) t
+  val mapi : ('e var -> 'x -> 'y) -> ('e, 'x) t -> ('e, 'y) t
+  val filter : ('e var -> 'x -> bool) -> ('e, 'x) t -> ('e, 'x) t
 
   val union :
     ('e var -> 'x -> 'x -> 'x option) -> ('e, 'x) t -> ('e, 'x) t -> ('e, 'x) t
 
   val fold : ('e var -> 'x -> 'acc -> 'acc) -> ('e, 'x) t -> 'acc -> 'acc
+  val exists : ('e var -> 'x -> bool) -> ('e, 'x) t -> bool
 end
diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml
index 5687e44ad..750222159 100644
--- a/compiler/verification/conditions.ml
+++ b/compiler/verification/conditions.ml
@@ -26,11 +26,13 @@ open Ast
 type vc_return = typed expr
 (** The return type of VC generators is the VC expression *)
 
-type ctx = {
-  current_scope_name : ScopeName.t;
-  decl : decl_ctx;
-  input_vars : typed expr Var.t list;
-  scope_variables_typs : (typed expr, typ) Var.Map.t;
+type scope_conditions_ctx = {
+  scope_cond_decls : decl_ctx;
+  scope_cond_input_vars : typed expr Var.Set.t;
+  scope_cond_subscope_output_vars : typed expr Var.Set.t;
+  scope_cond_variables_typs : (typed expr, typ) Var.Map.t;
+  scope_cond_asserts : typed expr list;
+  scope_cond_possible_values : (typed expr, typed expr list) Var.Map.t;
 }
 
 let rec conjunction_exprs (exprs : typed expr list) (mark : typed mark) :
@@ -111,8 +113,9 @@ let half_product (l1 : 'a list) (l2 : 'b list) : ('a * 'b) list =
     variables, or [fun () -> e1] for subscope variables. But what we really want
     to analyze is only [e1], so we match this outermost structure explicitely
     and have a clean verification condition generator that only runs on [e1] *)
-let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr) :
-    typed expr =
+let match_and_ignore_outer_reentrant_default
+    (ctx : scope_conditions_ctx)
+    (e : typed expr) : typed expr =
   match Mark.remove e with
   | EErrorOnEmpty
       ( EDefault
@@ -122,7 +125,7 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr) :
             cons;
           },
         _ )
-    when List.exists (fun x' -> Var.eq x x') ctx.input_vars ->
+    when Var.Set.exists (fun x' -> Var.eq x x') ctx.scope_cond_input_vars ->
     (* scope variables*)
     cons
   | EAbs { binder; tys = [(TLit TUnit, _)] } ->
@@ -155,8 +158,9 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr) :
     [b] such that if [b] is true, then [e] will never return an empty error. It
     also returns a map of all the types of locally free variables inside the
     expression. *)
-let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) :
-    vc_return =
+let rec generate_vc_must_not_return_empty
+    (ctx : scope_conditions_ctx)
+    (e : typed expr) : vc_return =
   match Mark.remove e with
   | EAbs { binder; _ } ->
     (* Hot take: for a function never to return an empty error when called, it
@@ -247,8 +251,9 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) :
     expression [b] such that if [b] is true, then [e] will never return a
     conflict error. It also returns a map of all the types of locally free
     variables inside the expression. *)
-let rec generate_vc_must_not_return_conflict (ctx : ctx) (e : typed expr) :
-    vc_return =
+let rec generate_vc_must_not_return_conflict
+    (ctx : scope_conditions_ctx)
+    (e : typed expr) : vc_return =
   (* See the code of [generate_vc_must_not_return_empty] for a list of
      invariants on which this function relies on. *)
   match Mark.remove e with
@@ -289,34 +294,79 @@ let rec generate_vc_must_not_return_conflict (ctx : ctx) (e : typed expr) :
          e [])
       (Mark.get e)
 
+(** [slice_expression_for_date_computations ctx e] returns a list of
+    subexpressions of [e] whose top AST node is a computation on dates that can
+    raise [Dates_calc.AmbiguousComputation], that is [Dates_calc.add_dates]. The
+    list is ordered from the smallest subexpressions to the biggest. *)
+let rec slice_expression_for_date_computations
+    (ctx : scope_conditions_ctx)
+    (e : typed expr) : vc_return list =
+  (* let (Typed { ty = t; _ }) = Mark.get e in *)
+  match Mark.remove e with
+  | EApp
+      {
+        f =
+          ( EOp
+              {
+                op =
+                  ( Op.Lte_dat_dat | Op.Lt_dat_dat | Op.Gt_dat_dat
+                  | Op.Gte_dat_dat );
+                tys = _;
+              },
+            _ );
+        args;
+      } ->
+    let r =
+      List.flatten (List.map (slice_expression_for_date_computations ctx) args)
+    in
+    if r <> [] then [e] else []
+  | EApp
+      {
+        f =
+          EOp { op = Op.Add_dat_dur Dates_calc.Dates.AbortOnRound; tys = _ }, _;
+        args;
+      } ->
+    List.flatten (List.map (slice_expression_for_date_computations ctx) args)
+    @ [e]
+  | _ ->
+    Expr.shallow_fold
+      (fun e acc -> slice_expression_for_date_computations ctx e @ acc)
+      e []
+
+(* Expects a top [EDefault] node and below the tree of defaults. *)
+let rec generate_possible_values (ctx : scope_conditions_ctx) (e : typed expr) :
+    typed expr list =
+  match Mark.remove e with
+  | EDefault { excepts; just = _; cons = c } ->
+    generate_possible_values ctx c
+    @ List.flatten (List.map (generate_possible_values ctx) excepts)
+  | _ -> [e]
+
 (** {1 Interface}*)
 
-type verification_condition_kind = NoEmptyError | NoOverlappingExceptions
+type verification_condition_kind =
+  | NoEmptyError
+  | NoOverlappingExceptions
+  | DateComputation
 
 type verification_condition = {
   vc_guard : typed expr;
   (* should have type bool *)
   vc_kind : verification_condition_kind;
-  (* All assertions defined at the top-level of the scope corresponding to this
-     assertion *)
-  vc_asserts : typed expr;
-  vc_scope : ScopeName.t;
   vc_variable : typed expr Var.t Mark.pos;
 }
 
-let trivial_assert e = Mark.copy e (ELit (LBool true))
-
 let rec generate_verification_conditions_scope_body_expr
-    (ctx : ctx)
+    (ctx : scope_conditions_ctx)
     (scope_body_expr : 'm expr scope_body_expr) :
-    ctx * verification_condition list * typed expr list =
+    scope_conditions_ctx * verification_condition list =
   match scope_body_expr with
-  | Result _ -> ctx, [], []
+  | Result _ -> ctx, []
   | ScopeLet scope_let ->
     let scope_let_var, scope_let_next =
       Bindlib.unbind scope_let.scope_let_next
     in
-    let new_ctx, vc_list, assert_list =
+    let new_ctx, vc_list =
       match scope_let.scope_let_kind with
       | Assertion -> (
         let e =
@@ -325,7 +375,7 @@ let rec generate_verification_conditions_scope_body_expr
         match Mark.remove e with
         | EAssert e ->
           let e = match_and_ignore_outer_reentrant_default ctx e in
-          ctx, [], [e]
+          { ctx with scope_cond_asserts = e :: ctx.scope_cond_asserts }, []
         | _ ->
           Message.raise_spanned_error (Expr.pos e)
             "Internal error: this assertion does not have the structure \
@@ -333,7 +383,25 @@ let rec generate_verification_conditions_scope_body_expr
              %a"
             (Print.expr ()) e)
       | DestructuringInputStruct ->
-        { ctx with input_vars = scope_let_var :: ctx.input_vars }, [], []
+        ( {
+            ctx with
+            scope_cond_input_vars =
+              Var.Set.add scope_let_var ctx.scope_cond_input_vars;
+            scope_cond_variables_typs =
+              Var.Map.add scope_let_var scope_let.scope_let_typ
+                ctx.scope_cond_variables_typs;
+          },
+          [] )
+      | DestructuringSubScopeResults ->
+        ( {
+            ctx with
+            scope_cond_subscope_output_vars =
+              Var.Set.add scope_let_var ctx.scope_cond_subscope_output_vars;
+            scope_cond_variables_typs =
+              Var.Map.add scope_let_var scope_let.scope_let_typ
+                ctx.scope_cond_variables_typs;
+          },
+          [] )
       | ScopeVarDefinition | SubScopeVarDefinition ->
         (* For scope variables, we should check both that they never evaluate to
            emptyError nor conflictError. But for subscope variable definitions,
@@ -345,10 +413,14 @@ let rec generate_verification_conditions_scope_body_expr
         in
         let e = match_and_ignore_outer_reentrant_default ctx e in
         let vc_confl = generate_vc_must_not_return_conflict ctx e in
+        let possible_values : typed expr list =
+          generate_possible_values ctx e
+        in
         let vc_confl =
           if !Cli.optimize_flag then
             Expr.unbox
-              (Shared_ast.Optimizations.optimize_expr ctx.decl vc_confl)
+              (Shared_ast.Optimizations.optimize_expr ctx.scope_cond_decls
+                 vc_confl)
           else vc_confl
         in
         let vc_list =
@@ -358,8 +430,6 @@ let rec generate_verification_conditions_scope_body_expr
               vc_kind = NoOverlappingExceptions;
               (* Placeholder until we add all assertions in scope once
                * we finished traversing it *)
-              vc_asserts = trivial_assert e;
-              vc_scope = ctx.current_scope_name;
               vc_variable = scope_let_var, scope_let.scope_let_pos;
             };
           ]
@@ -371,42 +441,80 @@ let rec generate_verification_conditions_scope_body_expr
             let vc_empty =
               if !Cli.optimize_flag then
                 Expr.unbox
-                  (Shared_ast.Optimizations.optimize_expr ctx.decl vc_empty)
+                  (Shared_ast.Optimizations.optimize_expr ctx.scope_cond_decls
+                     vc_empty)
               else vc_empty
             in
             {
               vc_guard = Mark.copy e (Mark.remove vc_empty);
               vc_kind = NoEmptyError;
-              vc_asserts = trivial_assert e;
-              vc_scope = ctx.current_scope_name;
               vc_variable = scope_let_var, scope_let.scope_let_pos;
             }
             :: vc_list
           | _ -> vc_list
         in
-        ctx, vc_list, []
-      | _ -> ctx, [], []
+        let vc_list =
+          let subexprs_dates : vc_return list =
+            slice_expression_for_date_computations ctx e
+          in
+          let subexprs_dates =
+            List.map
+              (fun e ->
+                if !Cli.optimize_flag then
+                  Expr.unbox
+                    (Shared_ast.Optimizations.optimize_expr ctx.scope_cond_decls
+                       e)
+                else e)
+              subexprs_dates
+          in
+          vc_list
+          @ List.map
+              (fun subexpr_date ->
+                {
+                  vc_guard = subexpr_date;
+                  vc_kind = DateComputation;
+                  vc_variable = scope_let_var, scope_let.scope_let_pos;
+                })
+              subexprs_dates
+        in
+        ( {
+            ctx with
+            scope_cond_possible_values =
+              Var.Map.add scope_let_var possible_values
+                ctx.scope_cond_possible_values;
+          },
+          vc_list )
+      | CallingSubScope -> ctx, []
     in
-    let new_ctx, new_vcs, new_asserts =
+    let new_ctx, new_vcs =
       generate_verification_conditions_scope_body_expr
         {
           new_ctx with
-          scope_variables_typs =
+          scope_cond_variables_typs =
             Var.Map.add scope_let_var scope_let.scope_let_typ
-              new_ctx.scope_variables_typs;
+              new_ctx.scope_cond_variables_typs;
         }
         scope_let_next
     in
-    new_ctx, vc_list @ new_vcs, assert_list @ new_asserts
+    new_ctx, vc_list @ new_vcs
+
+type verification_conditions_scope = {
+  vc_scope_asserts : typed expr;
+  vc_scope_possible_variable_values :
+    (typed Dcalc.Ast.expr, typed Dcalc.Ast.expr list) Var.Map.t;
+  vc_scope_variables_defined_outside_of_scope : typed Dcalc.Ast.expr Var.Set.t;
+  vc_scope_list : verification_condition list;
+  vc_scope_variables_typs : (typed expr, typ) Var.Map.t;
+}
 
 let generate_verification_conditions_code_items
     (decl_ctx : decl_ctx)
     (code_items : 'm expr code_item_list)
-    (s : ScopeName.t option) : verification_condition list =
+    (s : ScopeName.t option) : verification_conditions_scope ScopeName.Map.t =
   Scope.fold_left
-    ~f:(fun vcs item _ ->
+    ~f:(fun (vcs : verification_conditions_scope ScopeName.Map.t) item _ ->
       match item with
-      | Topdef _ -> []
+      | Topdef _ -> vcs
       | ScopeDef (name, body) ->
         let is_selected_scope =
           match s with
@@ -414,52 +522,67 @@ let generate_verification_conditions_code_items
           | None -> true
           | _ -> false
         in
-        let new_vcs =
-          if is_selected_scope then
-            let _scope_input_var, scope_body_expr =
-              Bindlib.unbind body.scope_body_expr
-            in
-            let ctx =
-              {
-                current_scope_name = name;
-                decl = decl_ctx;
-                input_vars = [];
-                scope_variables_typs =
-                  Var.Map.empty
-                  (* We don't need to add the typ of the scope input var here
-                     because it will never appear in an expression for which we
-                     generate a verification conditions (the big struct is
-                     destructured with a series of let bindings just after. )*);
-              }
-            in
-            let _, vcs, asserts =
-              generate_verification_conditions_scope_body_expr ctx
-                scope_body_expr
-            in
-            let combined_assert =
-              conjunction_exprs asserts
-                (Typed
-                   { pos = Pos.no_pos; ty = Mark.add Pos.no_pos (TLit TBool) })
-            in
-            List.map (fun vc -> { vc with vc_asserts = combined_assert }) vcs
-          else []
-        in
-        new_vcs @ vcs)
-    ~init:[] code_items
+        if is_selected_scope then
+          let _scope_input_var, scope_body_expr =
+            Bindlib.unbind body.scope_body_expr
+          in
+          let init_ctx =
+            {
+              scope_cond_decls = decl_ctx;
+              scope_cond_asserts = [];
+              scope_cond_input_vars = Var.Set.empty;
+              scope_cond_possible_values = Var.Map.empty;
+              scope_cond_subscope_output_vars = Var.Set.empty;
+              scope_cond_variables_typs =
+                Var.Map.empty
+                (* We don't need to add the typ of the scope input var here
+                   because it will never appear in an expression for which we
+                   generate a verification conditions (the big struct is
+                   destructured with a series of let bindings just after. )*);
+            }
+          in
+          let ctx, scope_vcs =
+            generate_verification_conditions_scope_body_expr init_ctx
+              scope_body_expr
+          in
+          let combined_assert =
+            conjunction_exprs ctx.scope_cond_asserts
+              (Typed { pos = Pos.no_pos; ty = Mark.add Pos.no_pos (TLit TBool) })
+          in
+          ScopeName.Map.add name
+            {
+              vc_scope_asserts = combined_assert;
+              vc_scope_list = scope_vcs;
+              vc_scope_possible_variable_values = ctx.scope_cond_possible_values;
+              vc_scope_variables_defined_outside_of_scope =
+                Var.Set.union ctx.scope_cond_input_vars
+                  ctx.scope_cond_subscope_output_vars;
+              vc_scope_variables_typs = ctx.scope_cond_variables_typs;
+            }
+            vcs
+        else vcs)
+    ~init:ScopeName.Map.empty code_items
 
 let generate_verification_conditions (p : 'm program) (s : ScopeName.t option) :
-    verification_condition list =
-  let vcs =
+    verification_conditions_scope ScopeName.Map.t =
+  let vcs : verification_conditions_scope ScopeName.Map.t =
     generate_verification_conditions_code_items p.decl_ctx p.code_items s
   in
-  (* We sort this list by scope name and then variable name to ensure consistent
-     output for testing*)
-  List.sort
-    (fun vc1 vc2 ->
-      let to_str vc =
-        Format.asprintf "%s.%s"
-          (Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
-          (Bindlib.name_of (Mark.remove vc.vc_variable))
-      in
-      String.compare (to_str vc1) (to_str vc2))
+  ScopeName.Map.mapi
+    (fun scope_name scope_vc ->
+      {
+        scope_vc with
+        vc_scope_list =
+          (* We sort this list by scope name and then variable name to ensure
+             consistent output for testing*)
+          List.sort
+            (fun vc1 vc2 ->
+              let to_str vc =
+                Format.asprintf "%s.%s"
+                  (Format.asprintf "%a" ScopeName.format_t scope_name)
+                  (Bindlib.name_of (Mark.remove vc.vc_variable))
+              in
+              String.compare (to_str vc1) (to_str vc2))
+            scope_vc.vc_scope_list;
+      })
     vcs
diff --git a/compiler/verification/conditions.mli b/compiler/verification/conditions.mli
index d38095448..e994847db 100644
--- a/compiler/verification/conditions.mli
+++ b/compiler/verification/conditions.mli
@@ -23,24 +23,39 @@ open Shared_ast
 type verification_condition_kind =
   | NoEmptyError
       (** This verification condition checks whether a definition never returns
-          an empty error *)
+          an empty error. Has type [bool]. *)
   | NoOverlappingExceptions
       (** This verification condition checks whether a definition never returns
-          a conflict error *)
+          a conflict error. Has type [bool]. *)
+  | DateComputation
+      (** This verification condition is just a slice of the program (a
+          subexpression) that features computations on dates. *)
 
 type verification_condition = {
   vc_guard : typed Dcalc.Ast.expr;
       (** This expression should have type [bool]*)
   vc_kind : verification_condition_kind;
-  vc_asserts : typed Dcalc.Ast.expr;
-      (** A conjunction of all assertions in scope of this VC. * This expression
-          should have type [bool] *)
-  vc_scope : ScopeName.t;
   vc_variable : typed Dcalc.Ast.expr Var.t Mark.pos;
 }
 
+type verification_conditions_scope = {
+  vc_scope_asserts : typed Dcalc.Ast.expr;
+      (** A conjunction of all assertions in scope. This expression should have
+          type [bool] *)
+  vc_scope_possible_variable_values :
+    (typed Dcalc.Ast.expr, typed Dcalc.Ast.expr list) Var.Map.t;
+      (** For each variable, a list containing all the possible values that this
+          variable can have. This is a conservative analysis based on the
+          traversal of the default tree. *)
+  vc_scope_variables_defined_outside_of_scope : typed Dcalc.Ast.expr Var.Set.t;
+  vc_scope_list : verification_condition list;
+  vc_scope_variables_typs : (typed Dcalc.Ast.expr, typ) Var.Map.t;
+}
+
 val generate_verification_conditions :
-  typed Dcalc.Ast.program -> ScopeName.t option -> verification_condition list
+  typed Dcalc.Ast.program ->
+  ScopeName.t option ->
+  verification_conditions_scope ScopeName.Map.t
 (** [generate_verification_conditions p None] will generate the verification
     conditions for all the variables of all the scopes of the program [p], while
     [generate_verification_conditions p (Some s)] will focus only on the
diff --git a/compiler/verification/dune b/compiler/verification/dune
index 56e493680..60fbae4cb 100644
--- a/compiler/verification/dune
+++ b/compiler/verification/dune
@@ -2,6 +2,7 @@
  (name verification)
  (public_name catala.verification)
  (libraries
+  str
   bindlib
   catala_utils
   dcalc
@@ -11,7 +12,11 @@
    z3backend.ml
    from
    (z3 -> z3backend.real.ml)
-   (-> z3backend.dummy.ml))))
+   (-> z3backend.dummy.ml))
+  (select
+   mopsabackend.ml
+   from
+   (-> mopsabackend.real.ml))))
 
 (documentation
  (package catala)
diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml
index 69705e83f..4ea795217 100644
--- a/compiler/verification/io.ml
+++ b/compiler/verification/io.ml
@@ -27,7 +27,7 @@ module type Backend = sig
 
   type vc_encoding
 
-  val print_encoding : vc_encoding -> string
+  val print_encoding : backend_context -> vc_encoding -> string
 
   type model
   type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
@@ -37,27 +37,21 @@ module type Backend = sig
   val is_model_empty : model -> bool
 
   val translate_expr :
-    backend_context -> typed Dcalc.Ast.expr -> backend_context * vc_encoding
+    Conditions.verification_conditions_scope ->
+    backend_context ->
+    typed Dcalc.Ast.expr ->
+    backend_context * vc_encoding
 
   val encode_asserts :
-    backend_context -> typed Dcalc.Ast.expr -> backend_context
+    Conditions.verification_conditions_scope ->
+    backend_context ->
+    typed Dcalc.Ast.expr ->
+    backend_context
 end
 
 module type BackendIO = sig
-  val init_backend : unit -> unit
-
   type backend_context
-
-  val make_context : decl_ctx -> backend_context
-
   type vc_encoding
-
-  val translate_expr :
-    backend_context -> typed Dcalc.Ast.expr -> backend_context * vc_encoding
-
-  val encode_asserts :
-    backend_context -> typed Dcalc.Ast.expr -> backend_context
-
   type model
 
   type vc_encoding_result =
@@ -66,26 +60,22 @@ module type BackendIO = sig
 
   val print_negative_result :
     Conditions.verification_condition ->
+    ScopeName.t ->
     backend_context ->
     model option ->
     string
 
-  val encode_and_check_vc :
-    decl_ctx -> Conditions.verification_condition * vc_encoding_result -> bool
+  val check_vc :
+    decl_ctx ->
+    ScopeName.t ->
+    Conditions.verification_conditions_scope ->
+    Conditions.verification_condition * vc_encoding_result ->
+    bool
 end
 
 module MakeBackendIO (B : Backend) = struct
-  let init_backend = B.init_backend
-
   type backend_context = B.backend_context
-
-  let make_context = B.make_context
-
   type vc_encoding = B.vc_encoding
-
-  let translate_expr = B.translate_expr
-  let encode_asserts = B.encode_asserts
-
   type model = B.model
 
   type vc_encoding_result =
@@ -94,6 +84,7 @@ module MakeBackendIO (B : Backend) = struct
 
   let print_negative_result
       (vc : Conditions.verification_condition)
+      (scope : ScopeName.t)
       (ctx : B.backend_context)
       (model : B.model option) : string =
     let var_and_pos =
@@ -102,7 +93,7 @@ module MakeBackendIO (B : Backend) = struct
         Format.asprintf
           "@[<v>@{<yellow>[%a.%s]@} This variable might return an empty error:@,\
            %a@]"
-          ScopeName.format_t vc.vc_scope
+          ScopeName.format_t scope
           (Bindlib.name_of (Mark.remove vc.vc_variable))
           Pos.format_loc_text (Mark.get vc.vc_variable)
       | Conditions.NoOverlappingExceptions ->
@@ -110,9 +101,16 @@ module MakeBackendIO (B : Backend) = struct
           "@[<v>@{<yellow>[%a.%s]@} At least two exceptions overlap for this \
            variable:@,\
            %a@]"
-          ScopeName.format_t vc.vc_scope
+          ScopeName.format_t scope
           (Bindlib.name_of (Mark.remove vc.vc_variable))
           Pos.format_loc_text (Mark.get vc.vc_variable)
+      | DateComputation ->
+        Format.asprintf
+          "@[<v>@{<yellow>[%a.%s]@} This date computation might be ambiguous:@,\
+           %a@]"
+          ScopeName.format_t scope
+          (Bindlib.name_of (Mark.remove vc.vc_variable))
+          Pos.format_loc_text (Expr.pos vc.vc_guard)
     in
     let counterexample : string option =
       if !Cli.disable_counterexamples then
@@ -139,38 +137,62 @@ module MakeBackendIO (B : Backend) = struct
     | None -> ""
     | Some counterexample -> "\n" ^ counterexample
 
-  let encode_and_check_vc
+  let check_vc
       (_decl_ctx : decl_ctx)
+      (scope : ScopeName.t)
+      (vc_scope_ctx : Conditions.verification_conditions_scope)
       (vc : Conditions.verification_condition * vc_encoding_result) : bool =
     let vc, z3_vc = vc in
 
     Message.emit_debug "@[<v>For this variable:@,%a@,@]" Pos.format_loc_text
       (Expr.pos vc.Conditions.vc_guard);
-    Message.emit_debug
-      "@[<v>This verification condition was generated for @{<yellow>%s@}:@,\
-       %a@,\
-       with assertions:@,\
-       %a@]"
-      (match vc.vc_kind with
-      | Conditions.NoEmptyError ->
-        "the variable definition never to return an empty error"
-      | NoOverlappingExceptions -> "no two exceptions to ever overlap")
-      (Print.expr ()) vc.vc_guard (Print.expr ()) vc.vc_asserts;
+    if vc.vc_kind <> DateComputation then
+      Message.emit_debug
+        "@[<v>This verification condition was generated for @{<yellow>%s@}:@,\
+         %a@,\
+         with assertions:@,\
+         %a@,\
+         and possible values for variables:@,\
+         %a@]"
+        (match vc.vc_kind with
+        | Conditions.NoEmptyError ->
+          "the variable definition never to return an empty error"
+        | NoOverlappingExceptions -> "no two exceptions to ever overlap"
+        | DateComputation -> "this date computation cannot be ambiguous")
+        (Print.expr ()) vc.vc_guard (Print.expr ())
+        vc_scope_ctx.vc_scope_asserts
+        (fun fmt vars_possible_values ->
+          Format.pp_print_list
+            ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
+            (fun fmt (var, values) ->
+              Format.fprintf fmt "@[<hov 2>%a@ = @ %a@]" Print.var var
+                (Format.pp_print_list
+                   ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ")
+                   (Print.expr ()))
+                values)
+            fmt
+            (Var.Map.bindings vars_possible_values))
+        vc_scope_ctx.vc_scope_possible_variable_values;
 
     match z3_vc with
     | Success (encoding, backend_ctx) -> (
       Message.emit_debug "@[<v>The translation to Z3 is the following:@,%s@]"
-        (B.print_encoding encoding);
+        (B.print_encoding backend_ctx encoding);
       match B.solve_vc_encoding backend_ctx encoding with
       | ProvenTrue -> true
       | ProvenFalse model ->
-        Message.emit_warning "%s" (print_negative_result vc backend_ctx model);
+        Message.emit_warning "%s"
+          (print_negative_result vc scope backend_ctx model);
         false
-      | Unknown -> failwith "The solver failed at proving or disproving the VC")
+      | Unknown ->
+        (* FIXME: we probably want to have the choice of behavior between
+           failure and warning here *)
+        Message.emit_warning "The solver failed at proving or disproving the VC";
+        false)
     | Fail msg ->
       Message.emit_warning
         "@[<v>@{<yellow>[%a.%s]@} The translation to Z3 failed:@,%s@]"
-        ScopeName.format_t vc.vc_scope
+        ScopeName.format_t scope
         (Bindlib.name_of (Mark.remove vc.vc_variable))
         msg;
       false
diff --git a/compiler/verification/io.mli b/compiler/verification/io.mli
index 395733363..4b47b550a 100644
--- a/compiler/verification/io.mli
+++ b/compiler/verification/io.mli
@@ -28,7 +28,7 @@ module type Backend = sig
 
   type vc_encoding
 
-  val print_encoding : vc_encoding -> string
+  val print_encoding : backend_context -> vc_encoding -> string
 
   type model
   type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
@@ -38,27 +38,21 @@ module type Backend = sig
   val is_model_empty : model -> bool
 
   val translate_expr :
-    backend_context -> typed Dcalc.Ast.expr -> backend_context * vc_encoding
+    Conditions.verification_conditions_scope ->
+    backend_context ->
+    typed Dcalc.Ast.expr ->
+    backend_context * vc_encoding
 
   val encode_asserts :
-    backend_context -> typed Dcalc.Ast.expr -> backend_context
+    Conditions.verification_conditions_scope ->
+    backend_context ->
+    typed Dcalc.Ast.expr ->
+    backend_context
 end
 
 module type BackendIO = sig
-  val init_backend : unit -> unit
-
   type backend_context
-
-  val make_context : decl_ctx -> backend_context
-
   type vc_encoding
-
-  val translate_expr :
-    backend_context -> typed Dcalc.Ast.expr -> backend_context * vc_encoding
-
-  val encode_asserts :
-    backend_context -> typed Dcalc.Ast.expr -> backend_context
-
   type model
 
   type vc_encoding_result =
@@ -67,15 +61,19 @@ module type BackendIO = sig
 
   val print_negative_result :
     Conditions.verification_condition ->
+    ScopeName.t ->
     backend_context ->
     model option ->
     string
 
-  val encode_and_check_vc :
-    decl_ctx -> Conditions.verification_condition * vc_encoding_result -> bool
-  (** [encode_and_check_vc] spawns a new Z3 solver and tries to solve the
-      expression [vc]. Returns [true] if the vs was proven true and [false]
-      otherwise. **)
+  val check_vc :
+    decl_ctx ->
+    ScopeName.t ->
+    Conditions.verification_conditions_scope ->
+    Conditions.verification_condition * vc_encoding_result ->
+    bool
+  (** [check_vc] spawns a new Z3 solver and tries to solve the expression [vc].
+      Returns [true] if the vs was proven true and [false] otherwise. **)
 end
 
 module MakeBackendIO : functor (B : Backend) ->
diff --git a/compiler/verification/mopsabackend.dummy.ml b/compiler/verification/mopsabackend.dummy.ml
new file mode 100644
index 000000000..ad8ab72e8
--- /dev/null
+++ b/compiler/verification/mopsabackend.dummy.ml
@@ -0,0 +1,41 @@
+(* This file is part of the Catala compiler, a specification language for tax
+   and social benefits computation rules. Copyright (C) 2023 Inria, contributor:
+   Raphaël Monat <raphael.monat@inria.fr>
+
+   Licensed under the Apache License, Version 2.0 (the "License"); you may not
+   use this file except in compliance with the License. You may obtain a copy of
+   the License at
+
+   http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
+   WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
+   License for the specific language governing permissions and limitations under
+   the License. *)
+
+(** Replicating the interface, with no actual implementation for compiling
+    without the expected backend. All functions print an error message and exit *)
+
+let dummy () =
+  Catala_utils.Message.raise_error
+    "This instance of Catala is not linked with Mopsa."
+
+module Io = struct
+  let init_backend () = dummy ()
+
+  type backend_context = unit
+
+  let make_context _ = dummy ()
+
+  type vc_encoding = unit
+
+  let translate_expr _ _ = dummy ()
+  let encode_asserts _ _ = dummy ()
+
+  type model = unit
+  type vc_encoding_result = Success of model * model | Fail of string
+
+  let print_negative_result _ _ _ = dummy ()
+  let check_vc _ _ = dummy ()
+end
diff --git a/compiler/verification/mopsabackend.real.ml b/compiler/verification/mopsabackend.real.ml
new file mode 100644
index 000000000..b448be6db
--- /dev/null
+++ b/compiler/verification/mopsabackend.real.ml
@@ -0,0 +1,408 @@
+(* This file is part of the Catala compiler, a specification language for tax
+   and social benefits computation rules. Copyright (C) 2023 Inria,
+   contributors: Raphaël Monat <raphael.monat@inria.fr>, Denis Merigoux
+   <denis.merigoux@inria.fr>
+
+   Licensed under the Apache License, Version 2.0 (the "License"); you may not
+   use this file except in compliance with the License. You may obtain a copy of
+   the License at
+
+   http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
+   WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
+   License for the specific language governing permissions and limitations under
+   the License. *)
+
+open Catala_utils
+open Shared_ast
+
+let simplified_string_of_pos pos =
+  let basename =
+    Filename.basename (Pos.get_file pos) |> Filename.chop_extension
+  in
+  Format.asprintf "%s_%d-%d_%d-%d" basename (Pos.get_start_line pos)
+    (Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos)
+
+let rec vars_used_in_vc vc_scope_ctx (e : typed Dcalc.Ast.expr) :
+    (typed Dcalc.Ast.expr, typ) Var.Map.t =
+  let rec free_vars_with_types :
+      ('a, 't) gexpr -> (('a, 't) gexpr, typ) Var.Map.t =
+   fun e ->
+    match e with
+    | EVar v, _ -> Var.Map.singleton v (Expr.ty e)
+    | EAbs { binder; _ }, _ ->
+      let vs, body = Bindlib.unmbind binder in
+      Array.fold_right Var.Map.remove vs (free_vars_with_types body)
+    | e ->
+      Expr.shallow_fold
+        (fun e ->
+          Var.Map.union (fun _ _ -> assert false) (free_vars_with_types e))
+        e Var.Map.empty
+  in
+  let free_vars = free_vars_with_types e in
+  (* We search recursively in the possible definitions of each free variable. *)
+  let possible_values_of_free_vars =
+    Var.Map.filter
+      (fun v _ -> Var.Map.mem v free_vars)
+      vc_scope_ctx.Conditions.vc_scope_possible_variable_values
+  in
+  Var.Map.fold
+    (fun _ possible_values vars_used ->
+      List.fold_left
+        (fun vars_used possible_value ->
+          Var.Map.union
+            (fun _ _ -> assert false)
+            (vars_used_in_vc vc_scope_ctx possible_value)
+            vars_used)
+        vars_used possible_values)
+    possible_values_of_free_vars free_vars
+
+type mopsa_variable_declaration_value =
+  | Unknown of typ
+  | Known of typed Dcalc.Ast.expr
+
+type mopsa_program = {
+  initial_guard : typed Dcalc.Ast.expr;
+  main_guard : typed Dcalc.Ast.expr;
+  declared_variables :
+    ((dcalc, typed) gexpr Var.t * mopsa_variable_declaration_value) list;
+}
+
+type 'a mopsa_variable_declaration_boxed_value =
+  | BoxedUnknown of typ
+  | BoxedKnown of ('a, typed) marked
+
+module TypedValuesDcalcVarMap = struct
+  type 'x t =
+    (typed Dcalc.Ast.expr, 'x mopsa_variable_declaration_boxed_value) Var.Map.t
+
+  let map (f : 'a -> 'b) (m : 'a t) : 'b t =
+    Var.Map.map
+      (fun v ->
+        match v with
+        | BoxedUnknown ty -> BoxedUnknown ty
+        | BoxedKnown (e, te) -> BoxedKnown (f e, te))
+      m
+end
+
+module TypedValuesDcalcVarMapBoxLifting = Bindlib.Lift (TypedValuesDcalcVarMap)
+
+type mopsa_variable_declarations =
+  (typed Dcalc.Ast.expr, mopsa_variable_declaration_value) Var.Map.t
+
+module VarVertex = struct
+  include Var
+
+  type t = typed Dcalc.Ast.expr Var.t
+
+  let hash x = Bindlib.uid_of x
+  let equal x y = Bindlib.eq_vars x y
+end
+
+module VarDependencies =
+  Graph.Persistent.Digraph.ConcreteBidirectional (VarVertex)
+
+module VarDependenciesTraversal = Graph.Topological.Make (VarDependencies)
+
+let declaration_reverse_dependency_ordering (d : mopsa_variable_declarations) :
+    typed Dcalc.Ast.expr Var.t list =
+  let g = VarDependencies.empty in
+  let g =
+    Var.Map.fold
+      (fun (v : typed Dcalc.Ast.expr Var.t)
+           (e : mopsa_variable_declaration_value) g ->
+        let g = VarDependencies.add_vertex g v in
+        match e with
+        | Unknown _ -> g
+        | Known e ->
+          let used = Expr.free_vars e in
+          Var.Set.fold (fun used g -> VarDependencies.add_edge g used v) used g)
+      d g
+  in
+  List.rev (VarDependenciesTraversal.fold (fun v acc -> v :: acc) g [])
+
+(** To better split the load for MOPSA and improve debugging, we split the VC
+    into smaller parts by creating supplementary variables. *)
+let rec split_expression_into_atomic_parts (e : typed Dcalc.Ast.expr) :
+    ( typed Dcalc.Ast.expr,
+      (dcalc, typed) naked_gexpr Bindlib.box
+      mopsa_variable_declaration_boxed_value )
+    Var.Map.t
+    * (dcalc, typed) boxed_gexpr =
+  match Mark.remove e with
+  | EApp
+      {
+        f =
+          ( EOp
+              {
+                op =
+                  ( Op.Add_dat_dur Dates_calc.Dates.AbortOnRound
+                  | Op.FirstDayOfMonth );
+                tys = _;
+              },
+            _ ) as f;
+        args;
+      } ->
+    let acc, args =
+      List.fold_left_map
+        (fun acc arg ->
+          let toadd, arg = split_expression_into_atomic_parts arg in
+          (Var.Map.union (fun _ _ _ -> assert false)) acc toadd, arg)
+        Var.Map.empty args
+    in
+    let dummy_var =
+      let pos = Expr.pos e in
+      Var.make ("var_" ^ simplified_string_of_pos pos)
+    in
+    let new_e = Expr.eapp (Expr.box f) args (Mark.get e) in
+    ( Var.Map.add dummy_var (BoxedKnown new_e) acc,
+      Expr.evar dummy_var (Mark.get e) )
+  | _ ->
+    Expr.map_gather ~acc:Var.Map.empty
+      ~join:(Var.Map.union (fun _ _ _ -> assert false))
+      ~f:split_expression_into_atomic_parts e
+
+(** Sometimes VC contains struct accesses from larger values which are defined
+    elsewhere. Since MOPSA does not currently handle structs, etc., we prefer
+    replacing the struct access with its own variable coming with an unknown
+    value. *)
+let rec transform_field_accesses_into_variables
+    ~(is_vc_var : (dcalc, typed) naked_gexpr Bindlib.var -> bool)
+    (e : typed Dcalc.Ast.expr) :
+    (typed Dcalc.Ast.expr, typ) Var.Map.t * (dcalc, typed) boxed_gexpr =
+  match Mark.remove e with
+  | EStructAccess { e = EVar v, _; field; _ } when is_vc_var v ->
+    let var =
+      Var.make (Format.asprintf "%a__%a" Print.var v StructField.format_t field)
+    in
+    Var.Map.singleton var (Expr.ty e), Expr.evar var (Mark.get e)
+  | _ ->
+    Expr.map_gather ~acc:Var.Map.empty
+      ~join:(Var.Map.union (fun _ _ _ -> assert false))
+      ~f:(transform_field_accesses_into_variables ~is_vc_var)
+      e
+
+(* The goal of this part is to extract additions from expressions, and perform
+   them before as assignments. This will simplify the analysis and communication
+   with Mopsa. *)
+let translate_expr
+    (vc_scope_ctx : Conditions.verification_conditions_scope)
+    (original_vc_guard : typed Dcalc.Ast.expr) : mopsa_program =
+  let vars_used_in_vc = vars_used_in_vc vc_scope_ctx original_vc_guard in
+  let vars_used_in_vc_with_known_values =
+    Var.Map.filter
+      (fun v _ ->
+        Var.Map.mem v vc_scope_ctx.Conditions.vc_scope_possible_variable_values)
+      vars_used_in_vc
+  in
+  let vc_variables_declarations_unknown =
+    Var.Map.fold
+      (fun v ty declarations -> Var.Map.add v (Unknown ty) declarations)
+      (Var.Map.filter
+         (fun v _ -> not (Var.Map.mem v vars_used_in_vc_with_known_values))
+         vars_used_in_vc)
+      Var.Map.empty
+  in
+  let vc_variables_declarations_defined =
+    Var.Map.mapi
+      (fun var values ->
+        if List.length values <> 1 then
+          Message.emit_debug
+            "Only the first possible value was taken into account for %a"
+            Print.var_debug var;
+        (* FIXME: take into account multiple possible values *)
+        Known (List.hd values))
+      (Var.Map.filter
+         (fun v _ -> Var.Map.mem v vars_used_in_vc)
+         vc_scope_ctx.vc_scope_possible_variable_values)
+  in
+  let vc_variables_declarations : mopsa_variable_declarations =
+    Var.Map.union
+      (fun _ _ -> assert false)
+      vc_variables_declarations_unknown vc_variables_declarations_defined
+  in
+  let new_vars_for_struct_accesses, vc_guard =
+    transform_field_accesses_into_variables
+      ~is_vc_var:(fun v ->
+        Var.Map.exists
+          (fun v2 _ -> Var.compare v v2 = 0)
+          vc_variables_declarations)
+      original_vc_guard
+  in
+  let new_vars_for_struct_accesses : mopsa_variable_declarations =
+    Var.Map.map (fun ty -> Unknown ty) new_vars_for_struct_accesses
+  in
+  let vc_guard = Expr.unbox vc_guard in
+  let new_vars_for_atomic_splitting, (vc_guard, vc_guard_mark) =
+    split_expression_into_atomic_parts vc_guard
+  in
+  let new_vars_for_atomic_splitting, vc_guard =
+    (* This manipulation is done so that we only unbox once to keep all
+       variables in sync. *)
+    Bindlib.unbox
+      (Bindlib.box_apply2
+         (fun new_vars_for_atomic_splitting vc_guard ->
+           new_vars_for_atomic_splitting, (vc_guard, vc_guard_mark))
+         (TypedValuesDcalcVarMapBoxLifting.lift_box
+            new_vars_for_atomic_splitting)
+         vc_guard)
+  in
+  let new_vars_for_atomic_splitting : mopsa_variable_declarations =
+    Var.Map.map
+      (fun v ->
+        match v with BoxedUnknown ty -> Unknown ty | BoxedKnown e -> Known e)
+      new_vars_for_atomic_splitting
+  in
+  let vc_variables_declarations =
+    Var.Map.union
+      (fun _ _ -> assert false)
+      vc_variables_declarations
+      (Var.Map.union
+         (fun _ _ -> assert false)
+         new_vars_for_struct_accesses new_vars_for_atomic_splitting)
+  in
+  let declaration_reverse_dependency_ordering =
+    declaration_reverse_dependency_ordering vc_variables_declarations
+  in
+  {
+    initial_guard = original_vc_guard;
+    main_guard = vc_guard;
+    declared_variables =
+      (* Careful with the order! these definitions must be laid out in reverse
+         dependency order *)
+      List.map
+        (fun v -> v, Var.Map.find v vc_variables_declarations)
+        declaration_reverse_dependency_ordering;
+  }
+
+let print_encoding (prog : mopsa_program) =
+  let fmt = Format.str_formatter in
+  let () =
+    Format.fprintf fmt "%aassert(sync(%a));@."
+      (Format.pp_print_list
+         ~pp_sep:(fun _ () -> ())
+         (fun fmt (var, oexpr) ->
+           match oexpr with
+           | Unknown ty -> (
+             let make_random =
+               match Mark.remove ty with
+               | TLit TDate -> Some "date()"
+               | TLit TDuration -> Some "duration_ym()"
+               | TLit TBool -> Some "bool()"
+               | TLit TInt -> Some "int()"
+               | _ -> None
+             in
+             match make_random with
+             | Some make_random ->
+               Format.fprintf fmt "%a %a = make_random_%s;@." Print.typ_debug ty
+                 Print.var var make_random
+             | None ->
+               Message.emit_debug "Ignoring type declaration of var %a : %a"
+                 Print.var_debug var Print.typ_debug ty)
+           | Known expr ->
+             Format.fprintf fmt "%a %a = %a;@." Print.typ_debug (Expr.ty expr)
+               Print.var var
+               (Print.expr ~debug:false ())
+               expr))
+      prog.declared_variables
+      (Print.expr ~debug:false ())
+      prog.main_guard
+  in
+  let str = Format.flush_str_formatter () in
+  String.to_ascii str
+
+module Backend : Io.Backend = struct
+  type vc_encoding = mopsa_program
+
+  let init_backend () = ()
+
+  type backend_context = unit
+
+  let make_context _ = ()
+
+  let translate_expr
+      (scope_vcs : Conditions.verification_conditions_scope)
+      ()
+      (e : typed Dcalc.Ast.expr) : unit * mopsa_program =
+    (), translate_expr scope_vcs e
+
+  let print_encoding _ctx prog = print_encoding prog
+
+  type model = Yojson.Basic.t (* yeah, I'll have to fix that *)
+  type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
+
+  let solve_vc_encoding ctx mopsa_program =
+    let prog_name =
+      "proof_obligation_"
+      ^ simplified_string_of_pos (Expr.pos mopsa_program.main_guard)
+      ^ ".u"
+    in
+    let prog_channel = open_out prog_name in
+    Printf.fprintf prog_channel "%s" (print_encoding ctx mopsa_program);
+    close_out prog_channel;
+    Message.emit_debug "Generated new Mopsa program at %s" prog_name;
+    let process_mopsas_json j =
+      let open Yojson.Basic.Util in
+      if j |> member "success" |> to_bool then
+        let alarms = j |> member "checks" |> to_list in
+        (* FIXME: if list.hd fails the program is safe *)
+        let toparse = List.hd alarms |> member "messages" |> to_string in
+        let pos = Str.search_forward (Str.regexp_string "Hints: ") toparse 0 in
+        let sub_until_end s from = String.sub s from (String.length s - from) in
+        let new_json_to_parse =
+          sub_until_end toparse (pos + String.length "Hints: ")
+        in
+        Some (Yojson.Basic.from_string new_json_to_parse)
+      else
+        let () =
+          Message.emit_warning "Mopsa failed to analyze %s"
+            prog_name in
+        let () =
+          Message.emit_debug "Mopsa failed with message:\n%s"
+            (j |> member "exception" |> to_string)
+        in
+        None
+    in
+    (* I wanted to use mopsa as a library, but we have a small issue to fix
+       there first *)
+    let args =
+      [|
+        "mopsa-universal";
+        "-config=universal/ymd_poly_powerint_markerset.json";
+        (* "-debug=_"; *)
+        "-max-set-size=7";
+        "-numeric=polkagrid";
+        "-format=json";
+        "-silent";
+        "-output=tmp.json";
+        prog_name;
+      |]
+    in
+    (* I wanted to use mopsa as a library, but we have a small issue to fix
+       there first *)
+    (* let open Mopsa_analyzer.Framework.Runner in *)
+    (* let _ = *)
+    (*   try parse_options args analyze_files () *)
+    (*   with *)
+    (*   | Mopsa_utils.Exceptions.Panic (s, t) -> *)
+    (*     Message.emit_warning "Mopsa failed :(@.%s@%s" s t ; 0 *)
+    (*   | _ -> *)
+    (*     Message.emit_warning "Mopsa failed :("; 0 *)
+    (* in *)
+    let () = try Unix.unlink "tmp.json" with Unix.Unix_error _ -> () in
+    let _ =
+      Unix.system (Array.fold_left (fun acc s -> acc ^ " " ^ s) "" args)
+    in
+    match process_mopsas_json (Yojson.Basic.from_file "tmp.json") with
+    | Some hints -> ProvenFalse (Some hints)
+    | None -> Unknown
+
+  let print_model _ m : string = Yojson.Basic.pretty_to_string ~std:true m
+  let init_backend () = Message.emit_debug "Running Mopsa"
+  let is_model_empty _ = false
+  let encode_asserts _ _ _ = assert false
+end
+
+module Io = Io.MakeBackendIO (Backend)
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index d31791f78..b84ecd9c3 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -15,38 +15,61 @@
    the License. *)
 
 open Catala_utils
+open Shared_ast
 
 (** [solve_vc] is the main entry point of this module. It takes a list of
     expressions [vcs] corresponding to verification conditions that must be
     discharged by Z3, and attempts to solve them **)
-let solve_vc
+let solve_vcs
     (decl_ctx : Shared_ast.decl_ctx)
-    (vcs : Conditions.verification_condition list) : unit =
+    (vcs : Conditions.verification_conditions_scope ScopeName.Map.t) : unit =
   (* Right now we only use the Z3 backend but the functorial interface should
      make it easy to mix and match different proof backends. *)
-  Z3backend.Io.init_backend ();
-  let z3_vcs =
-    List.map
-      (fun vc ->
-        ( vc,
-          try
-            let ctx = Z3backend.Io.make_context decl_ctx in
-            let ctx =
-              Z3backend.Io.encode_asserts ctx vc.Conditions.vc_asserts
-            in
-            let ctx, z3_vc =
-              Z3backend.Io.translate_expr ctx vc.Conditions.vc_guard
-            in
-            Z3backend.Io.Success (z3_vc, ctx)
-          with Failure msg -> Fail msg ))
-      vcs
-  in
+  (* Z3backend.Backend.init_backend (); *)
+  Mopsabackend.Backend.init_backend ();
   let all_proven =
-    List.fold_left
-      (fun all_proven vc ->
-        if Z3backend.Io.encode_and_check_vc decl_ctx vc then all_proven
-        else false)
-      true z3_vcs
+    ScopeName.Map.fold
+      (fun scope_name (scope_vcs : Conditions.verification_conditions_scope)
+           all_proven ->
+        let dates_vcs =
+          List.filter
+            (fun vc ->
+              match vc.Conditions.vc_kind with
+              | Conditions.DateComputation -> true
+              | _ -> false)
+            scope_vcs.Conditions.vc_scope_list
+          |> List.map (fun vc ->
+                 let ctx, prog =
+                   Mopsabackend.Backend.translate_expr scope_vcs
+                     (Mopsabackend.Backend.make_context decl_ctx)
+                     vc.Conditions.vc_guard
+                 in
+                 vc, Mopsabackend.Io.Success (prog, ctx))
+        in
+        let all_proven =
+          List.fold_left
+            (fun all_proven vc ->
+              if Mopsabackend.Io.check_vc decl_ctx scope_name scope_vcs vc then
+                all_proven
+              else false)
+            all_proven dates_vcs
+        in
+        (* let z3_vcs = List.map (fun vc -> ( vc, try let ctx =
+           Z3backend.Io.make_context decl_ctx in let ctx =
+           Z3backend.Io.encode_asserts ctx scope_vcs.vc_scope_asserts in let
+           ctx, z3_vc = Z3backend.Io.translate_expr ctx vc.Conditions.vc_guard
+           in Z3backend.Io.Success (z3_vc, ctx) with Failure msg -> Fail msg ))
+           (List.filter (fun vc -> match vc.Conditions.vc_kind with |
+           Conditions.NoEmptyError | Conditions.NoOverlappingExceptions -> true
+           | Conditions.DateComputation -> false)
+           scope_vcs.Conditions.vc_scope_list) in let all_proven =
+           List.fold_left (fun all_proven vc -> if Z3backend.Io.check_vc
+           decl_ctx scope_name scope_vcs vc then all_proven else false)
+           all_proven z3_vcs in *)
+        all_proven)
+      vcs true
   in
   if all_proven then
-    Message.emit_result "No errors found during the proof mode run."
+    Message.emit_result "No potential errors found during the proof mode run."
+  else
+    Message.raise_error "Some potential errors were found during the proof run."
diff --git a/compiler/verification/solver.mli b/compiler/verification/solver.mli
index 5ea951cbc..6014a7047 100644
--- a/compiler/verification/solver.mli
+++ b/compiler/verification/solver.mli
@@ -16,5 +16,7 @@
 
 (** Solves verification conditions using various proof backends *)
 
-val solve_vc :
-  Shared_ast.decl_ctx -> Conditions.verification_condition list -> unit
+val solve_vcs :
+  Shared_ast.decl_ctx ->
+  Conditions.verification_conditions_scope Shared_ast.ScopeName.Map.t ->
+  unit
diff --git a/compiler/verification/z3backend.dummy.ml b/compiler/verification/z3backend.dummy.ml
index 7388fb75b..af084ffd2 100644
--- a/compiler/verification/z3backend.dummy.ml
+++ b/compiler/verification/z3backend.dummy.ml
@@ -21,7 +21,7 @@ let dummy () =
   Catala_utils.Message.raise_error
     "This instance of Catala was compiled without Z3 support."
 
-module Io = struct
+module Backend = struct
   let init_backend () = dummy ()
 
   type backend_context = unit
@@ -30,12 +30,25 @@ module Io = struct
 
   type vc_encoding = unit
 
-  let translate_expr _ _ = dummy ()
-  let encode_asserts _ _ = dummy ()
+  let print_encoding _ _ = dummy ()
+
+  type model = unit
+  type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
 
+  let solve_vc_encoding _ _ = dummy ()
+  let print_model _ _ = dummy ()
+  let is_model_empty _ = dummy () 
+
+  let translate_expr _ _ _ = dummy ()
+  let encode_asserts _ _ _ = dummy ()
+end
+
+module Io = struct
+  type backend_context = unit
+  type vc_encoding = unit
   type model = unit
   type vc_encoding_result = Success of model * model | Fail of string
 
   let print_negative_result _ _ _ = dummy ()
-  let encode_and_check_vc _ _ = dummy ()
+  let check_vc _ _ = dummy ()
 end
diff --git a/compiler/verification/z3backend.mli b/compiler/verification/z3backend.mli
index e43807b02..7b35b75bb 100644
--- a/compiler/verification/z3backend.mli
+++ b/compiler/verification/z3backend.mli
@@ -17,4 +17,5 @@
 
 (** Interfacing with the Z3 SMT solver *)
 
+module Backend : Io.Backend
 module Io : Io.BackendIO
diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml
index d21623bfa..871f627e2 100644
--- a/compiler/verification/z3backend.real.ml
+++ b/compiler/verification/z3backend.real.ml
@@ -793,7 +793,7 @@ module Backend = struct
   type backend_context = context
   type vc_encoding = Z3.Expr.expr
 
-  let print_encoding (vc : vc_encoding) : string = Expr.to_string vc
+  let print_encoding _ (vc : vc_encoding) : string = Expr.to_string vc
 
   type model = Z3.Model.model
   type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
@@ -817,11 +817,11 @@ module Backend = struct
 
   let is_model_empty (m : model) : bool = Z3.Model.get_decls m = []
 
-  let translate_expr (ctx : backend_context) (e : typed expr) =
+  let translate_expr _ (ctx : backend_context) (e : typed expr) =
     translate_expr ctx e
 
-  let encode_asserts (ctx : backend_context) (e : typed expr) =
-    let ctx, vc = translate_expr ctx e in
+  let encode_asserts scvs (ctx : backend_context) (e : typed expr) =
+    let ctx, vc = translate_expr scvs ctx e in
     add_z3constraint vc ctx
 
   let init_backend () =
diff --git a/examples/aides_logement/code_construction_reglementaire.catala_fr b/examples/aides_logement/code_construction_reglementaire.catala_fr
index 81f0286f4..7d8212013 100644
--- a/examples/aides_logement/code_construction_reglementaire.catala_fr
+++ b/examples/aides_logement/code_construction_reglementaire.catala_fr
@@ -2048,8 +2048,10 @@ champ d'application ÉligibilitéPrimeDeDéménagement:
       -- AprèsPremierJourMoisCivilTroisièmeMoisDeGrossesse: vrai
       -- DateDeNaissance de date_naissance:
         # VERIF: ambigü
-        date_courante <=
-          ((premier_jour_du_mois de (date_naissance + 2 an))) + (-1 jour))
+        #        date_courante <=
+        #  ((premier_jour_du_mois de (date_naissance + 2 an))) + (-1 jour))
+        date_courante < (premier_jour_du_mois de (date_naissance + 2 an))
+      )
     )
   conséquence rempli
 
diff --git a/tests/test_proof/bad/array_length-empty.catala_en b/tests/test_proof/bad/array_length-empty.catala_en
index 72066f257..5a0dd1043 100644
--- a/tests/test_proof/bad/array_length-empty.catala_en
+++ b/tests/test_proof/bad/array_length-empty.catala_en
@@ -19,4 +19,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/array_length-overlap.catala_en b/tests/test_proof/bad/array_length-overlap.catala_en
index 981b663ed..362f716ca 100644
--- a/tests/test_proof/bad/array_length-overlap.catala_en
+++ b/tests/test_proof/bad/array_length-overlap.catala_en
@@ -20,4 +20,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/assert-empty.catala_en b/tests/test_proof/bad/assert-empty.catala_en
index 870c662b0..b11bee855 100644
--- a/tests/test_proof/bad/assert-empty.catala_en
+++ b/tests/test_proof/bad/assert-empty.catala_en
@@ -31,4 +31,6 @@ $ catala Proof --disable_counterexamples
   │           ‾
 
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/dates_get_year-overlap.catala_en b/tests/test_proof/bad/dates_get_year-overlap.catala_en
index dca3c26ac..bf30d5fa6 100644
--- a/tests/test_proof/bad/dates_get_year-overlap.catala_en
+++ b/tests/test_proof/bad/dates_get_year-overlap.catala_en
@@ -22,4 +22,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/dates_simple-empty.catala_en b/tests/test_proof/bad/dates_simple-empty.catala_en
index 21c8ee2ed..7ae73aa8c 100644
--- a/tests/test_proof/bad/dates_simple-empty.catala_en
+++ b/tests/test_proof/bad/dates_simple-empty.catala_en
@@ -21,4 +21,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/dates_simple-overlap.catala_en b/tests/test_proof/bad/dates_simple-overlap.catala_en
index ad4952418..e68c193c0 100644
--- a/tests/test_proof/bad/dates_simple-overlap.catala_en
+++ b/tests/test_proof/bad/dates_simple-overlap.catala_en
@@ -22,4 +22,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/duration-empty.catala_en b/tests/test_proof/bad/duration-empty.catala_en
index ac710b8aa..88e5dcbef 100644
--- a/tests/test_proof/bad/duration-empty.catala_en
+++ b/tests/test_proof/bad/duration-empty.catala_en
@@ -19,4 +19,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/duration-overlap.catala_en b/tests/test_proof/bad/duration-overlap.catala_en
index e3bad00d6..ada9dff69 100644
--- a/tests/test_proof/bad/duration-overlap.catala_en
+++ b/tests/test_proof/bad/duration-overlap.catala_en
@@ -20,4 +20,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/enums-empty.catala_en b/tests/test_proof/bad/enums-empty.catala_en
index 81d1ca84a..5ed39b39a 100644
--- a/tests/test_proof/bad/enums-empty.catala_en
+++ b/tests/test_proof/bad/enums-empty.catala_en
@@ -37,4 +37,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/enums-nonbool-empty.catala_en b/tests/test_proof/bad/enums-nonbool-empty.catala_en
index 5e19edb3a..be42c044f 100644
--- a/tests/test_proof/bad/enums-nonbool-empty.catala_en
+++ b/tests/test_proof/bad/enums-nonbool-empty.catala_en
@@ -35,4 +35,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/enums-nonbool-overlap.catala_en b/tests/test_proof/bad/enums-nonbool-overlap.catala_en
index abf9f5610..820159750 100644
--- a/tests/test_proof/bad/enums-nonbool-overlap.catala_en
+++ b/tests/test_proof/bad/enums-nonbool-overlap.catala_en
@@ -35,4 +35,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/enums-overlap.catala_en b/tests/test_proof/bad/enums-overlap.catala_en
index 89e3ef2f9..f11a521e2 100644
--- a/tests/test_proof/bad/enums-overlap.catala_en
+++ b/tests/test_proof/bad/enums-overlap.catala_en
@@ -37,4 +37,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/enums_inj-empty.catala_en b/tests/test_proof/bad/enums_inj-empty.catala_en
index b6b2d602e..fce8d691c 100644
--- a/tests/test_proof/bad/enums_inj-empty.catala_en
+++ b/tests/test_proof/bad/enums_inj-empty.catala_en
@@ -30,4 +30,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Article
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/enums_inj-overlap.catala_en b/tests/test_proof/bad/enums_inj-overlap.catala_en
index 1f6bf5ae4..de3877804 100644
--- a/tests/test_proof/bad/enums_inj-overlap.catala_en
+++ b/tests/test_proof/bad/enums_inj-overlap.catala_en
@@ -25,4 +25,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Article
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/enums_unit-empty.catala_en b/tests/test_proof/bad/enums_unit-empty.catala_en
index 6a28690c0..a5af2ec56 100644
--- a/tests/test_proof/bad/enums_unit-empty.catala_en
+++ b/tests/test_proof/bad/enums_unit-empty.catala_en
@@ -28,4 +28,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Article
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/enums_unit-overlap.catala_en b/tests/test_proof/bad/enums_unit-overlap.catala_en
index 6e60e55b6..58c0ca6cc 100644
--- a/tests/test_proof/bad/enums_unit-overlap.catala_en
+++ b/tests/test_proof/bad/enums_unit-overlap.catala_en
@@ -28,4 +28,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Article
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/let_in_condition-empty.catala_en b/tests/test_proof/bad/let_in_condition-empty.catala_en
index 341e041eb..99b6057ee 100644
--- a/tests/test_proof/bad/let_in_condition-empty.catala_en
+++ b/tests/test_proof/bad/let_in_condition-empty.catala_en
@@ -20,4 +20,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/money-empty.catala_en b/tests/test_proof/bad/money-empty.catala_en
index 5de7fe034..e3b2e7669 100644
--- a/tests/test_proof/bad/money-empty.catala_en
+++ b/tests/test_proof/bad/money-empty.catala_en
@@ -23,4 +23,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/money-overlap.catala_en b/tests/test_proof/bad/money-overlap.catala_en
index aa60442be..2e41b0781 100644
--- a/tests/test_proof/bad/money-overlap.catala_en
+++ b/tests/test_proof/bad/money-overlap.catala_en
@@ -24,4 +24,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/no_vars-conflict.catala_en b/tests/test_proof/bad/no_vars-conflict.catala_en
index 178a790c8..e08f857f3 100644
--- a/tests/test_proof/bad/no_vars-conflict.catala_en
+++ b/tests/test_proof/bad/no_vars-conflict.catala_en
@@ -24,4 +24,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/no_vars-empty.catala_en b/tests/test_proof/bad/no_vars-empty.catala_en
index 6de8f1502..c6a640507 100644
--- a/tests/test_proof/bad/no_vars-empty.catala_en
+++ b/tests/test_proof/bad/no_vars-empty.catala_en
@@ -23,4 +23,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/rationals-empty.catala_en b/tests/test_proof/bad/rationals-empty.catala_en
index 528f013fa..ccaadfef3 100644
--- a/tests/test_proof/bad/rationals-empty.catala_en
+++ b/tests/test_proof/bad/rationals-empty.catala_en
@@ -19,4 +19,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/rationals-overlap.catala_en b/tests/test_proof/bad/rationals-overlap.catala_en
index 3f7a92ecb..df79de8f8 100644
--- a/tests/test_proof/bad/rationals-overlap.catala_en
+++ b/tests/test_proof/bad/rationals-overlap.catala_en
@@ -20,4 +20,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/sat_solving.catala_en b/tests/test_proof/bad/sat_solving.catala_en
index 7b5ce646b..17e078f50 100644
--- a/tests/test_proof/bad/sat_solving.catala_en
+++ b/tests/test_proof/bad/sat_solving.catala_en
@@ -47,4 +47,6 @@ $ catala Proof --disable_counterexamples
    │          ‾‾‾
    └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/structs-empty.catala_en b/tests/test_proof/bad/structs-empty.catala_en
index 4f2b1cc09..d64b0f5c7 100644
--- a/tests/test_proof/bad/structs-empty.catala_en
+++ b/tests/test_proof/bad/structs-empty.catala_en
@@ -28,4 +28,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/structs-overlap.catala_en b/tests/test_proof/bad/structs-overlap.catala_en
index 5bd9d0c48..587caa767 100644
--- a/tests/test_proof/bad/structs-overlap.catala_en
+++ b/tests/test_proof/bad/structs-overlap.catala_en
@@ -28,4 +28,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/good/array_length.catala_en b/tests/test_proof/good/array_length.catala_en
index 55c4cb8a2..5f52ae6e0 100644
--- a/tests/test_proof/good/array_length.catala_en
+++ b/tests/test_proof/good/array_length.catala_en
@@ -13,5 +13,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/assert.catala_en b/tests/test_proof/good/assert.catala_en
index 9da9d222d..25c18e635 100644
--- a/tests/test_proof/good/assert.catala_en
+++ b/tests/test_proof/good/assert.catala_en
@@ -24,5 +24,5 @@ scope Foo:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/dates_get_year.catala_en b/tests/test_proof/good/dates_get_year.catala_en
index 4c2c385c1..bf99dfbdc 100644
--- a/tests/test_proof/good/dates_get_year.catala_en
+++ b/tests/test_proof/good/dates_get_year.catala_en
@@ -15,5 +15,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/dates_simple.catala_en b/tests/test_proof/good/dates_simple.catala_en
index 11b893c49..ef36b4a1e 100644
--- a/tests/test_proof/good/dates_simple.catala_en
+++ b/tests/test_proof/good/dates_simple.catala_en
@@ -15,5 +15,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/direct_scope_call.catala_en b/tests/test_proof/good/direct_scope_call.catala_en
index d5bf66230..a6f785d29 100644
--- a/tests/test_proof/good/direct_scope_call.catala_en
+++ b/tests/test_proof/good/direct_scope_call.catala_en
@@ -16,5 +16,5 @@ scope Foo:
 
 ```catala-test-inline
 $ catala Proof -s Foo
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/direct_scope_call_with_context.catala_en b/tests/test_proof/good/direct_scope_call_with_context.catala_en
index 583012492..9c6be8530 100644
--- a/tests/test_proof/good/direct_scope_call_with_context.catala_en
+++ b/tests/test_proof/good/direct_scope_call_with_context.catala_en
@@ -17,5 +17,5 @@ scope Foo:
 
 ```catala-test-inline
 $ catala Proof -s Foo
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/duration.catala_en b/tests/test_proof/good/duration.catala_en
index 01a2e840c..e6a8adfc8 100644
--- a/tests/test_proof/good/duration.catala_en
+++ b/tests/test_proof/good/duration.catala_en
@@ -13,5 +13,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/enums-arith.catala_en b/tests/test_proof/good/enums-arith.catala_en
index 4fe972ee8..a476035d5 100644
--- a/tests/test_proof/good/enums-arith.catala_en
+++ b/tests/test_proof/good/enums-arith.catala_en
@@ -28,5 +28,5 @@ $ catala Proof --disable_counterexamples
 5 │    -- C content boolean
   │       ‾
   └─ Test
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/enums-nonbool.catala_en b/tests/test_proof/good/enums-nonbool.catala_en
index 227d7d4e9..43c18ea7e 100644
--- a/tests/test_proof/good/enums-nonbool.catala_en
+++ b/tests/test_proof/good/enums-nonbool.catala_en
@@ -28,5 +28,5 @@ $ catala Proof --disable_counterexamples
 5 │    -- C content boolean
   │       ‾
   └─ Test
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/enums.catala_en b/tests/test_proof/good/enums.catala_en
index dbd08291c..5df85a17c 100644
--- a/tests/test_proof/good/enums.catala_en
+++ b/tests/test_proof/good/enums.catala_en
@@ -27,5 +27,5 @@ $ catala Proof --disable_counterexamples
 5 │    -- C content boolean
   │       ‾
   └─ Test
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/enums_inj.catala_en b/tests/test_proof/good/enums_inj.catala_en
index 4e2c7b46a..c9043f879 100644
--- a/tests/test_proof/good/enums_inj.catala_en
+++ b/tests/test_proof/good/enums_inj.catala_en
@@ -17,5 +17,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/enums_unit.catala_en b/tests/test_proof/good/enums_unit.catala_en
index d74268a25..27c120263 100644
--- a/tests/test_proof/good/enums_unit.catala_en
+++ b/tests/test_proof/good/enums_unit.catala_en
@@ -21,5 +21,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/functions.catala_en b/tests/test_proof/good/functions.catala_en
index c4de65b47..c8d05a1dd 100644
--- a/tests/test_proof/good/functions.catala_en
+++ b/tests/test_proof/good/functions.catala_en
@@ -14,5 +14,5 @@ scope A:
 ```
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/let_in_condition.catala_en b/tests/test_proof/good/let_in_condition.catala_en
index a37062d66..390319dbb 100644
--- a/tests/test_proof/good/let_in_condition.catala_en
+++ b/tests/test_proof/good/let_in_condition.catala_en
@@ -13,5 +13,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/money.catala_en b/tests/test_proof/good/money.catala_en
index 039fb1dda..a17563c9b 100644
--- a/tests/test_proof/good/money.catala_en
+++ b/tests/test_proof/good/money.catala_en
@@ -15,5 +15,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/no_vars.catala_en b/tests/test_proof/good/no_vars.catala_en
index 93244be96..ef9f0d445 100644
--- a/tests/test_proof/good/no_vars.catala_en
+++ b/tests/test_proof/good/no_vars.catala_en
@@ -10,5 +10,5 @@ scope A:
 ```
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/rationals.catala_en b/tests/test_proof/good/rationals.catala_en
index 11c66a408..1a3efbbff 100644
--- a/tests/test_proof/good/rationals.catala_en
+++ b/tests/test_proof/good/rationals.catala_en
@@ -13,5 +13,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/simple_vars.catala_en b/tests/test_proof/good/simple_vars.catala_en
index 211082b1a..a32a57fef 100644
--- a/tests/test_proof/good/simple_vars.catala_en
+++ b/tests/test_proof/good/simple_vars.catala_en
@@ -16,5 +16,5 @@ scope A:
 ```
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/structs.catala_en b/tests/test_proof/good/structs.catala_en
index 30ae8e7de..a59226d7a 100644
--- a/tests/test_proof/good/structs.catala_en
+++ b/tests/test_proof/good/structs.catala_en
@@ -20,5 +20,5 @@ scope A:
 ```
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```