diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml
index a8eb69896..1d8e57718 100644
--- a/compiler/verification/z3backend.real.ml
+++ b/compiler/verification/z3backend.real.ml
@@ -758,6 +758,14 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
           args (ctx, [])
       in
       ctx, Expr.mk_app ctx.ctx_z3 fd z3_args
+    | EAbs { binder; _ } ->
+      let vars, _ = Bindlib.unmbind binder in
+      if Array.length vars != 1 || List.length args != 1 then
+        failwith "[Z3 encoding] EAbs not supported beyond let_in"
+      else
+        let arg = List.hd args in
+        let expr = Bindlib.msubst binder [| Marked.unmark arg |] in
+        translate_expr ctx expr
     | _ ->
       failwith
         "[Z3 encoding] EApp node: Catala function calls should only include \
diff --git a/tests/test_proof/bad/let_in_condition-empty.catala_en b/tests/test_proof/bad/let_in_condition-empty.catala_en
new file mode 100644
index 000000000..bf2150665
--- /dev/null
+++ b/tests/test_proof/bad/let_in_condition-empty.catala_en
@@ -0,0 +1,23 @@
+## Test
+
+```catala
+declaration scope A:
+  context x content boolean
+
+scope A:
+  definition x under condition
+    let y equals false in
+    y 
+  consequence equals true
+```
+
+```catala-test-inline
+$ catala Proof --disable_counterexamples
+[ERROR] [A.x] This variable might return an empty error:
+┌─⯈ tests/test_proof/bad/let_in_condition-empty.catala_en:5.10-11:
+└─┐
+5 │   context x content boolean
+  │           ‾
+  └─ Test
+Counterexample generation is disabled so none was generated.
+```
diff --git a/tests/test_proof/good/let_in_condition.catala_en b/tests/test_proof/good/let_in_condition.catala_en
new file mode 100644
index 000000000..c3a702ec2
--- /dev/null
+++ b/tests/test_proof/good/let_in_condition.catala_en
@@ -0,0 +1,17 @@
+## Test
+
+```catala
+declaration scope A:
+  context x content boolean
+
+scope A:
+  definition x under condition
+    let y equals true in
+    y 
+  consequence equals true
+```
+
+```catala-test-inline
+$ catala Proof --disable_counterexamples
+[RESULT] No errors found during the proof mode run.
+```