diff --git a/.gitattributes b/.gitattributes
index 44fee360..9f7be242 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -1,6 +1,4 @@
-*.catala* linguist-language=Markdown
 *.ml linguist-language=OCaml
-*.fst linguist-language=Fstar
 *.mld linguist-documentation
 *.md linguist-documentation
 *.hints linguist-generated
diff --git a/.nix/cmdliner.nix b/.nix/cmdliner.nix
deleted file mode 100644
index 7745db14..00000000
--- a/.nix/cmdliner.nix
+++ /dev/null
@@ -1,38 +0,0 @@
-{ lib, stdenv, fetchurl, ocaml, findlib, ocamlbuild, topkg, result }:
-
-let
-  pname = "cmdliner";
-in
-
-assert lib.versionAtLeast ocaml.version "4.01.0";
-
-let param =
-  {
-    version = "1.1.0";
-    hash = "sha256-irWd4HTlJSYuz3HMgi1de2GVL2qus0QjeCe1WdsSs8Q=";
-  }
-; in
-
-stdenv.mkDerivation rec {
-  name = "ocaml${ocaml.version}-${pname}-${version}";
-  inherit (param) version;
-
-  src = fetchurl {
-    url = "https://erratique.ch/software/${pname}/releases/${pname}-${version}.tbz";
-    inherit (param) hash;
-  };
-
-  nativeBuildInputs = [ ocaml ocamlbuild findlib ];
-  buildInputs = [ topkg ];
-  propagatedBuildInputs = [ result ];
-
-  inherit (topkg) buildPhase installPhase;
-
-  meta = with lib; {
-    homepage = "https://erratique.ch/software/cmdliner";
-    description = "An OCaml module for the declarative definition of command line interfaces";
-    license = licenses.bsd3;
-    platforms = ocaml.meta.platforms or [];
-    maintainers = [ ];
-  };
-}
\ No newline at end of file
diff --git a/build_system/clerk.ml b/build_system/clerk.ml
index f36fcc0e..2746622d 100644
--- a/build_system/clerk.ml
+++ b/build_system/clerk.ml
@@ -81,8 +81,8 @@ let info =
       `P "Please file bug reports at https://github.com/CatalaLang/catala/issues";
     ]
   in
-  let exits = Cmd.Exit.defaults @ [ Cmd.Exit.info ~doc:"on error." 1 ] in
-  Cmd.info "clerk" ~version ~doc ~exits ~man
+  let exits = Term.default_exits @ [ Term.exit_info ~doc:"on error." 1 ] in
+  Term.info "clerk" ~version ~doc ~exits ~man
 
 (**{1 Testing}*)
 
@@ -330,5 +330,7 @@ let driver (file_or_folder : string) (command : string) (catala_exe : string opt
       1
 
 let _ =
-  let return_code = Cmdliner.Cmd.eval' (Cmdliner.Cmd.v info (clerk_t driver)) in
-  exit return_code
+  let return_code = Cmdliner.Term.eval (clerk_t driver, info) in
+  match return_code with
+  | `Ok 0 -> Cmdliner.Term.exit (`Ok 0)
+  | _ -> Cmdliner.Term.exit (`Error `Term)
diff --git a/catala.opam b/catala.opam
index 6c3019ad..3a82d6f4 100644
--- a/catala.opam
+++ b/catala.opam
@@ -21,7 +21,7 @@ depends: [
   "menhirLib" {>= "20200211"}
   "unionFind" {>= "20200320"}
   "bindlib" {>= "5.0.1"}
-  "cmdliner" {>= "1.1.0"}
+  "cmdliner" {= "1.0.4"}
   "re" {>= "1.9.0"}
   "zarith" {>= "1.12"}
   "zarith_stubs_js" {>= "v0.14.1"}
diff --git a/compiler/driver.ml b/compiler/driver.ml
index 7e712200..c61f41a8 100644
--- a/compiler/driver.ml
+++ b/compiler/driver.ml
@@ -359,7 +359,7 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
       -1
 
 let main () =
-  let return_code =
-    Cmdliner.Cmd.eval' (Cmdliner.Cmd.v Cli.info (Cli.catala_t (fun f -> driver (FileName f))))
-  in
-  exit return_code
+  let return_code = Cmdliner.Term.eval (Cli.catala_t (fun f -> driver (FileName f)), Cli.info) in
+  match return_code with
+  | `Ok 0 -> Cmdliner.Term.exit (`Ok 0)
+  | _ -> Cmdliner.Term.exit (`Error `Term)
diff --git a/compiler/utils/cli.ml b/compiler/utils/cli.ml
index 0b14cb00..29e456ed 100644
--- a/compiler/utils/cli.ml
+++ b/compiler/utils/cli.ml
@@ -195,8 +195,8 @@ let info =
       `P "Please file bug reports at https://github.com/CatalaLang/catala/issues";
     ]
   in
-  let exits = Cmd.Exit.defaults @ [ Cmd.Exit.info ~doc:"on error." 1 ] in
-  Cmd.info "catala" ~version ~doc ~exits ~man
+  let exits = Term.default_exits @ [ Term.exit_info ~doc:"on error." 1 ] in
+  Term.info "catala" ~version ~doc ~exits ~man
 
 (**{1 Terminal formatting}*)
 
diff --git a/compiler/utils/cli.mli b/compiler/utils/cli.mli
index cee4c1f6..e020d851 100644
--- a/compiler/utils/cli.mli
+++ b/compiler/utils/cli.mli
@@ -95,7 +95,7 @@ val catala_t :
 
 val version : string
 
-val info : Cmdliner.Cmd.info
+val info : Cmdliner.Term.info
 
 (**{1 Terminal formatting}*)
 
diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml
index 173b1706..ffeeb738 100644
--- a/compiler/verification/conditions.ml
+++ b/compiler/verification/conditions.ml
@@ -88,7 +88,8 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : expr Pos.marked) :
                (Print.format_expr ~debug:true ctx.decl)
                e)
             (Pos.get_position e))
-  | EApp ((EOp (Unop (Log _)), _), [ ((ErrorOnEmpty (EDefault (_, _, _), _), _) as d) ]) ->
+  | ErrorOnEmpty (EApp ((EOp (Unop (Log _)), _), [ d ]), _)
+  | EApp ((EOp (Unop (Log _)), _), [ (ErrorOnEmpty d, _) ]) ->
       d (* input subscope variables and non-input scope variable *)
   | _ ->
       Errors.raise_spanned_error
diff --git a/compiler/verification/z3backend.ml b/compiler/verification/z3backend.ml
index 442f4f7e..c559bb31 100644
--- a/compiler/verification/z3backend.ml
+++ b/compiler/verification/z3backend.ml
@@ -41,8 +41,11 @@ type context = {
   (* A map from Catala temporary variables, generated when translating a match, to the corresponding
      enum accessor call as a Z3 expression *)
   ctx_z3structs : Sort.sort StructMap.t;
-      (* A map from Catala struct names to the corresponding Z3 sort, from which we can retrieve the
-         constructor and the accessors *)
+  (* A map from Catala struct names to the corresponding Z3 sort, from which we can retrieve the
+     constructor and the accessors *)
+  ctx_z3unit : Sort.sort * Expr.expr;
+      (* A pair containing the Z3 encodings of the unit type, encoded as a tuple of 0 elements, and
+         the unit value *)
 }
 (** The context contains all the required information to encode a VC represented as a Catala term to
     Z3. The fields [ctx_decl] and [ctx_var] are computed before starting the translation to Z3, and
@@ -108,9 +111,11 @@ let rec print_z3model_expr (ctx : context) (ty : typ Pos.marked) (e : Expr.expr)
     match ty with
     (* TODO: Print boolean according to current language *)
     | TBool -> Expr.to_string e
-    | TUnit -> failwith "[Z3 model]: Pretty-printing of unit literals not supported"
+    (* TUnit is only used for the absence of an enum constructor argument. Hence, when
+       pretty-printing, we print nothing to remain closer from Catala sources *)
+    | TUnit -> ""
     | TInt -> Expr.to_string e
-    | TRat -> failwith "[Z3 model]: Pretty-printing of rational literals not supported"
+    | TRat -> Arithmetic.Real.to_decimal_string e !Cli.max_prec_digits
     (* TODO: Print the right money symbol according to language *)
     | TMoney ->
         let z3_str = Expr.to_string e in
@@ -173,29 +178,42 @@ let print_model (ctx : context) (model : Model.model) : string =
     (Format.pp_print_list
        ~pp_sep:(fun fmt () -> Format.fprintf fmt "\n")
        (fun fmt d ->
-         match Model.get_const_interp model d with
-         (* TODO: Better handling of this case *)
-         | None -> failwith "[Z3 model]: A variable does not have an associated Z3 solution"
-         (* Prints "name : value\n" *)
-         | Some e ->
-             if FuncDecl.get_arity d = 0 then
-               (* Constant case *)
+         if FuncDecl.get_arity d = 0 then
+           (* Constant case *)
+           match Model.get_const_interp model d with
+           (* TODO: Better handling of this case *)
+           | None -> failwith "[Z3 model]: A variable does not have an associated Z3 solution"
+           (* Print "name : value\n" *)
+           | Some e ->
                let symbol_name = Symbol.to_string (FuncDecl.get_name d) in
                let v = StringMap.find symbol_name ctx.ctx_z3vars in
                Format.fprintf fmt "%s %s : %s"
                  (Cli.print_with_style [ ANSITerminal.blue ] "%s" "-->")
                  (Cli.print_with_style [ ANSITerminal.yellow ] "%s" (Bindlib.name_of v))
                  (print_z3model_expr ctx (VarMap.find v ctx.ctx_var) e)
-             else failwith "[Z3 model]: Printing of functions is not yet supported"))
+         else
+           (* Declaration d is a function *)
+           match Model.get_func_interp model d with
+           (* TODO: Better handling of this case *)
+           | None -> failwith "[Z3 model]: A variable does not have an associated Z3 solution"
+           (* Print "name : value\n" *)
+           | Some f ->
+               let symbol_name = Symbol.to_string (FuncDecl.get_name d) in
+               let v = StringMap.find symbol_name ctx.ctx_z3vars in
+               Format.fprintf fmt "%s %s : %s"
+                 (Cli.print_with_style [ ANSITerminal.blue ] "%s" "-->")
+                 (Cli.print_with_style [ ANSITerminal.yellow ] "%s" (Bindlib.name_of v))
+                 (* TODO: Model of a Z3 function should be pretty-printed *)
+                 (Model.FuncInterp.to_string f)))
     decls
 
 (** [translate_typ_lit] returns the Z3 sort corresponding to the Catala literal type [t] **)
 let translate_typ_lit (ctx : context) (t : typ_lit) : Sort.sort =
   match t with
   | TBool -> Boolean.mk_sort ctx.ctx_z3
-  | TUnit -> failwith "[Z3 encoding] TUnit type not supported"
+  | TUnit -> fst ctx.ctx_z3unit
   | TInt -> Arithmetic.Integer.mk_sort ctx.ctx_z3
-  | TRat -> failwith "[Z3 encoding] TRat type not supported"
+  | TRat -> Arithmetic.Real.mk_sort ctx.ctx_z3
   | TMoney -> Arithmetic.Integer.mk_sort ctx.ctx_z3
   (* Dates are encoded as integers, corresponding to the number of days since Jan 1, 1900 *)
   | TDate -> Arithmetic.Integer.mk_sort ctx.ctx_z3
@@ -284,7 +302,7 @@ let translate_lit (ctx : context) (l : lit) : Expr.expr =
   | LBool b -> if b then Boolean.mk_true ctx.ctx_z3 else Boolean.mk_false ctx.ctx_z3
   | LEmptyError -> failwith "[Z3 encoding] LEmptyError literals not supported"
   | LInt n -> Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (Runtime.integer_to_int n)
-  | LRat _ -> failwith "[Z3 encoding] LRat literals not supported"
+  | LRat r -> Arithmetic.Real.mk_numeral_s ctx.ctx_z3 (string_of_float (Runtime.decimal_to_float r))
   | LMoney m ->
       let z3_m = Runtime.integer_to_int (Runtime.money_to_cents m) in
       Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 z3_m
@@ -311,6 +329,9 @@ let find_or_create_funcdecl (ctx : context) (v : Var.t) : context * FuncDecl.fun
           let ctx = add_funcdecl v fd ctx in
           let ctx = add_z3var name v ctx in
           (ctx, fd)
+      | TAny ->
+          failwith
+            "[Z3 Encoding] A function being applied has type TAny, the type was not fully inferred"
       | _ ->
           failwith
             "[Z3 Encoding] Ill-formed VC, a function application does not have a function type")
@@ -389,32 +410,32 @@ let rec translate_op (ctx : context) (op : operator) (args : expr Pos.marked lis
           | And -> (ctx, Boolean.mk_and ctx.ctx_z3 [ e1; e2 ])
           | Or -> (ctx, Boolean.mk_or ctx.ctx_z3 [ e1; e2 ])
           | Xor -> (ctx, Boolean.mk_xor ctx.ctx_z3 e1 e2)
-          | Add KInt -> (ctx, Arithmetic.mk_add ctx.ctx_z3 [ e1; e2 ])
+          | Add KInt | Add KRat | Add KMoney -> (ctx, Arithmetic.mk_add ctx.ctx_z3 [ e1; e2 ])
           | Add _ ->
               failwith "[Z3 encoding] application of non-integer binary operator Add not supported"
-          | Sub KInt -> (ctx, Arithmetic.mk_sub ctx.ctx_z3 [ e1; e2 ])
+          | Sub KInt | Sub KRat | Sub KMoney -> (ctx, Arithmetic.mk_sub ctx.ctx_z3 [ e1; e2 ])
           | Sub _ ->
               failwith "[Z3 encoding] application of non-integer binary operator Sub not supported"
-          | Mult KInt -> (ctx, Arithmetic.mk_mul ctx.ctx_z3 [ e1; e2 ])
+          | Mult KInt | Mult KRat | Mult KMoney -> (ctx, Arithmetic.mk_mul ctx.ctx_z3 [ e1; e2 ])
           | Mult _ ->
               failwith "[Z3 encoding] application of non-integer binary operator Mult not supported"
-          | Div KInt -> (ctx, Arithmetic.mk_div ctx.ctx_z3 e1 e2)
+          | Div KInt | Div KRat | Div KMoney -> (ctx, Arithmetic.mk_div ctx.ctx_z3 e1 e2)
           | Div _ ->
               failwith "[Z3 encoding] application of non-integer binary operator Div not supported"
-          | Lt KInt | Lt KMoney | Lt KDate -> (ctx, Arithmetic.mk_lt ctx.ctx_z3 e1 e2)
+          | Lt KInt | Lt KRat | Lt KMoney | Lt KDate -> (ctx, Arithmetic.mk_lt ctx.ctx_z3 e1 e2)
           | Lt _ ->
               failwith
                 "[Z3 encoding] application of non-integer or money binary operator Lt not supported"
-          | Lte KInt | Lte KMoney | Lte KDate -> (ctx, Arithmetic.mk_le ctx.ctx_z3 e1 e2)
+          | Lte KInt | Lte KRat | Lte KMoney | Lte KDate -> (ctx, Arithmetic.mk_le ctx.ctx_z3 e1 e2)
           | Lte _ ->
               failwith
                 "[Z3 encoding] application of non-integer or money binary operator Lte not \
                  supported"
-          | Gt KInt | Gt KMoney | Gt KDate -> (ctx, Arithmetic.mk_gt ctx.ctx_z3 e1 e2)
+          | Gt KInt | Gt KRat | Gt KMoney | Gt KDate -> (ctx, Arithmetic.mk_gt ctx.ctx_z3 e1 e2)
           | Gt _ ->
               failwith
                 "[Z3 encoding] application of non-integer or money binary operator Gt not supported"
-          | Gte KInt | Gte KMoney | Gte KDate -> (ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2)
+          | Gte KInt | Gte KRat | Gte KMoney | Gte KDate -> (ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2)
           | Gte _ ->
               failwith
                 "[Z3 encoding] application of non-integer or money binary operator Gte not \
@@ -557,6 +578,14 @@ and translate_expr (ctx : context) (vc : expr Pos.marked) : context * Expr.expr
           ] )
   | ErrorOnEmpty _ -> failwith "[Z3 encoding] ErrorOnEmpty unsupported"
 
+(** [create_z3unit] creates a Z3 sort and expression corresponding to the unit type and value
+    respectively. Concretely, we represent unit as a tuple with 0 elements **)
+let create_z3unit (ctx : Z3.context) : Z3.context * (Sort.sort * Expr.expr) =
+  let unit_sort = Tuple.mk_sort ctx (Symbol.mk_string ctx "unit") [] [] in
+  let mk_unit = Tuple.get_mk_decl unit_sort in
+  let unit_val = Expr.mk_app ctx mk_unit [] in
+  (ctx, (unit_sort, unit_val))
+
 module Backend = struct
   type backend_context = context
 
@@ -590,6 +619,7 @@ module Backend = struct
       (if !Cli.disable_counterexamples then [] else [ ("model", "true") ]) @ [ ("proof", "false") ]
     in
     let z3_ctx = mk_context cfg in
+    let z3_ctx, z3unit = create_z3unit z3_ctx in
     {
       ctx_z3 = z3_ctx;
       ctx_decl = decl_ctx;
@@ -599,6 +629,7 @@ module Backend = struct
       ctx_z3datatypes = EnumMap.empty;
       ctx_z3matchsubsts = VarMap.empty;
       ctx_z3structs = StructMap.empty;
+      ctx_z3unit = z3unit;
     }
 end
 
diff --git a/dune-project b/dune-project
index 7d26f1cf..a1fa7621 100644
--- a/dune-project
+++ b/dune-project
@@ -43,7 +43,7 @@
   (bindlib
    (>= 5.0.1))
   (cmdliner
-   (>= 1.1.0))
+   (= 1.0.4))
   (re
    (>= 1.9.0))
   (zarith
diff --git a/french_law/js/package-lock.json b/french_law/js/package-lock.json
index 66f81fe5..4358d772 100644
--- a/french_law/js/package-lock.json
+++ b/french_law/js/package-lock.json
@@ -1,8 +1,40 @@
 {
   "name": "french_law",
   "version": "0.5.0",
-  "lockfileVersion": 1,
+  "lockfileVersion": 2,
   "requires": true,
+  "packages": {
+    "": {
+      "name": "french_law",
+      "version": "0.5.0",
+      "license": "Apache-2.0",
+      "dependencies": {
+        "benchmark": "^2.1.4",
+        "lodash": "^4.17.21",
+        "platform": "^1.3.6"
+      },
+      "devDependencies": {}
+    },
+    "node_modules/benchmark": {
+      "version": "2.1.4",
+      "resolved": "https://registry.npmjs.org/benchmark/-/benchmark-2.1.4.tgz",
+      "integrity": "sha1-CfPeMckWQl1JjMLuVloOvzwqVik=",
+      "dependencies": {
+        "lodash": "^4.17.4",
+        "platform": "^1.3.3"
+      }
+    },
+    "node_modules/lodash": {
+      "version": "4.17.21",
+      "resolved": "https://registry.npmjs.org/lodash/-/lodash-4.17.21.tgz",
+      "integrity": "sha512-v2kDEe57lecTulaDIuNTPy3Ry4gLGJ6Z1O3vE1krgXZNrsQ+LFTGHVxVjcXPs17LhbZVGedAJv8XZ1tvj5FvSg=="
+    },
+    "node_modules/platform": {
+      "version": "1.3.6",
+      "resolved": "https://registry.npmjs.org/platform/-/platform-1.3.6.tgz",
+      "integrity": "sha512-fnWVljUchTro6RiCFvCXBbNhJc2NijN7oIQxbwsyL0buWJPG85v81ehlHI9fXrJsMNgTofEoWIQeClKpgxFLrg=="
+    }
+  },
   "dependencies": {
     "benchmark": {
       "version": "2.1.4",
diff --git a/release.nix b/release.nix
index a21f81e2..f1859d38 100644
--- a/release.nix
+++ b/release.nix
@@ -4,5 +4,4 @@ with pkgs;
 ocamlPackages.callPackage ./. {
   bindlib = ocamlPackages.callPackage ./.nix/bindlib.nix { };
   unionfind = ocamlPackages.callPackage ./.nix/unionfind.nix { };
-  cmdliner = ocamlPackages.callPackage ./.nix/cmdliner.nix { };
 }
diff --git a/shell.nix b/shell.nix
index 89656da8..9470086e 100644
--- a/shell.nix
+++ b/shell.nix
@@ -5,7 +5,6 @@ let
   pkg = ocamlPackages.callPackage ./. {
     bindlib = ocamlPackages.callPackage ./.nix/bindlib.nix { };
     unionfind = ocamlPackages.callPackage ./.nix/unionfind.nix { };
-    cmdliner = ocamlPackages.callPackage ./.nix/cmdliner.nix { };
   };
 in mkShell {
   inputsFrom = [ pkg ];
diff --git a/tests/test_proof/bad/enums_unit-empty.catala_en b/tests/test_proof/bad/enums_unit-empty.catala_en
new file mode 100644
index 00000000..2a1900e3
--- /dev/null
+++ b/tests/test_proof/bad/enums_unit-empty.catala_en
@@ -0,0 +1,20 @@
+## Article
+
+```catala
+declaration enumeration E:
+  -- Case1 content integer
+  -- Case2
+
+declaration scope A:
+  context x content E
+  context y content integer
+
+scope A:
+  definition x equals Case1 content 2
+  definition y under condition match x with pattern
+    -- Case1 of i : i > 0
+    -- Case2 : false consequence equals 2
+  definition y under condition match x with pattern
+    -- Case1 of i : false
+    -- Case2 : true consequence equals 2
+```
diff --git a/tests/test_proof/bad/enums_unit-overlap.catala_en b/tests/test_proof/bad/enums_unit-overlap.catala_en
new file mode 100644
index 00000000..66316065
--- /dev/null
+++ b/tests/test_proof/bad/enums_unit-overlap.catala_en
@@ -0,0 +1,20 @@
+## Article
+
+```catala
+declaration enumeration E:
+  -- Case1 content integer
+  -- Case2
+
+declaration scope A:
+  context x content E
+  context y content integer
+
+scope A:
+  definition x equals Case1 content 2
+  definition y under condition match x with pattern
+    -- Case1 of i : true
+    -- Case2 : true consequence equals 2
+  definition y under condition match x with pattern
+    -- Case1 of i : false
+    -- Case2 : true consequence equals 2
+```
diff --git a/tests/test_proof/bad/output/enums_unit-empty.catala_en.Proof b/tests/test_proof/bad/output/enums_unit-empty.catala_en.Proof
new file mode 100644
index 00000000..3ae0910e
--- /dev/null
+++ b/tests/test_proof/bad/output/enums_unit-empty.catala_en.Proof
@@ -0,0 +1,10 @@
+[ERROR] [A.y] This variable might return an empty error:
+  --> tests/test_proof/bad/enums_unit-empty.catala_en
+   | 
+10 |   context y content integer
+   |           ^
+   + Article
+Counterexample generation is disabled so none was generated.
+[RESULT] [A.y] No two exceptions to ever overlap for this variable
+[RESULT] [A.x] This variable never returns an empty error
+[RESULT] [A.x] No two exceptions to ever overlap for this variable
diff --git a/tests/test_proof/bad/output/enums_unit-overlap.catala_en.Proof b/tests/test_proof/bad/output/enums_unit-overlap.catala_en.Proof
new file mode 100644
index 00000000..f72a928d
--- /dev/null
+++ b/tests/test_proof/bad/output/enums_unit-overlap.catala_en.Proof
@@ -0,0 +1,10 @@
+[RESULT] [A.y] This variable never returns an empty error
+[ERROR] [A.y] At least two exceptions overlap for this variable:
+  --> tests/test_proof/bad/enums_unit-overlap.catala_en
+   | 
+10 |   context y content integer
+   |           ^
+   + Article
+Counterexample generation is disabled so none was generated.
+[RESULT] [A.x] This variable never returns an empty error
+[RESULT] [A.x] No two exceptions to ever overlap for this variable
diff --git a/tests/test_proof/bad/output/rationals-empty.catala_en.Proof b/tests/test_proof/bad/output/rationals-empty.catala_en.Proof
new file mode 100644
index 00000000..4062b129
--- /dev/null
+++ b/tests/test_proof/bad/output/rationals-empty.catala_en.Proof
@@ -0,0 +1,10 @@
+[ERROR] [A.y] This variable might return an empty error:
+ --> tests/test_proof/bad/rationals-empty.catala_en
+  | 
+6 |   context y content boolean
+  |           ^
+  + Test
+Counterexample generation is disabled so none was generated.
+[RESULT] [A.y] No two exceptions to ever overlap for this variable
+[RESULT] [A.x] This variable never returns an empty error
+[RESULT] [A.x] No two exceptions to ever overlap for this variable
diff --git a/tests/test_proof/bad/output/rationals-overlap.catala_en.Proof b/tests/test_proof/bad/output/rationals-overlap.catala_en.Proof
new file mode 100644
index 00000000..06c6b604
--- /dev/null
+++ b/tests/test_proof/bad/output/rationals-overlap.catala_en.Proof
@@ -0,0 +1,10 @@
+[RESULT] [A.y] This variable never returns an empty error
+[ERROR] [A.y] At least two exceptions overlap for this variable:
+ --> tests/test_proof/bad/rationals-overlap.catala_en
+  | 
+6 |   context y content boolean
+  |           ^
+  + Test
+Counterexample generation is disabled so none was generated.
+[RESULT] [A.x] This variable never returns an empty error
+[RESULT] [A.x] No two exceptions to ever overlap for this variable
diff --git a/tests/test_proof/bad/rationals-empty.catala_en b/tests/test_proof/bad/rationals-empty.catala_en
new file mode 100644
index 00000000..156738d3
--- /dev/null
+++ b/tests/test_proof/bad/rationals-empty.catala_en
@@ -0,0 +1,11 @@
+## Test
+
+```catala
+declaration scope A:
+  context x content decimal
+  context y content boolean
+
+scope A:
+  definition x equals 1.
+  definition y under condition x >. 1./.3. consequence equals true
+```
diff --git a/tests/test_proof/bad/rationals-overlap.catala_en b/tests/test_proof/bad/rationals-overlap.catala_en
new file mode 100644
index 00000000..305d9705
--- /dev/null
+++ b/tests/test_proof/bad/rationals-overlap.catala_en
@@ -0,0 +1,12 @@
+## Test
+
+```catala
+declaration scope A:
+  context x content decimal
+  context y content boolean
+
+scope A:
+  definition x equals 1.
+  definition y under condition x >=. 1./.3. consequence equals true
+  definition y under condition x <=. 1./.3. consequence equals false
+```
diff --git a/tests/test_proof/good/enums_unit.catala_en b/tests/test_proof/good/enums_unit.catala_en
new file mode 100644
index 00000000..a2cc866e
--- /dev/null
+++ b/tests/test_proof/good/enums_unit.catala_en
@@ -0,0 +1,20 @@
+## Article
+
+```catala
+declaration enumeration E:
+  -- Case1 content integer
+  -- Case2
+
+declaration scope A:
+  context x content E
+  context y content integer
+
+scope A:
+  definition x equals Case1 content 2
+  definition y under condition match x with pattern
+    -- Case1 of i : true
+    -- Case2 : false consequence equals 2
+  definition y under condition match x with pattern
+    -- Case1 of i : false
+    -- Case2 : true consequence equals 2
+```
diff --git a/tests/test_proof/good/output/enums_unit.catala_en.Proof b/tests/test_proof/good/output/enums_unit.catala_en.Proof
new file mode 100644
index 00000000..ebe1a223
--- /dev/null
+++ b/tests/test_proof/good/output/enums_unit.catala_en.Proof
@@ -0,0 +1,4 @@
+[RESULT] [A.y] This variable never returns an empty error
+[RESULT] [A.y] No two exceptions to ever overlap for this variable
+[RESULT] [A.x] This variable never returns an empty error
+[RESULT] [A.x] No two exceptions to ever overlap for this variable
diff --git a/tests/test_proof/good/output/rationals.catala_en.Proof b/tests/test_proof/good/output/rationals.catala_en.Proof
new file mode 100644
index 00000000..ebe1a223
--- /dev/null
+++ b/tests/test_proof/good/output/rationals.catala_en.Proof
@@ -0,0 +1,4 @@
+[RESULT] [A.y] This variable never returns an empty error
+[RESULT] [A.y] No two exceptions to ever overlap for this variable
+[RESULT] [A.x] This variable never returns an empty error
+[RESULT] [A.x] No two exceptions to ever overlap for this variable
diff --git a/tests/test_proof/good/rationals.catala_en b/tests/test_proof/good/rationals.catala_en
new file mode 100644
index 00000000..a38360c9
--- /dev/null
+++ b/tests/test_proof/good/rationals.catala_en
@@ -0,0 +1,12 @@
+## Test
+
+```catala
+declaration scope A:
+  context x content decimal
+  context y content boolean
+
+scope A:
+  definition x equals 1.
+  definition y under condition x >. 1./.3. consequence equals true
+  definition y under condition x <=. 1./.3. consequence equals false
+```