diff --git a/tests/value/logic.c b/tests/value/logic.c
index 8806b1930519098b26629b39b460e9e53098c516..b91a17f6003d68520e79c5f642ca7ccbb7406542 100644
--- a/tests/value/logic.c
+++ b/tests/value/logic.c
@@ -134,7 +134,7 @@ void eq_tsets () {
   //@ assert s1 == s2; // True at link-time
   //@ assert t != u; // false
 
-  //@ assert \union(0) == \union(0.0); 
+  //@ assert \union(0) == \union(0.0);
   //@ assert \union(1.0) == \union(1);
   //@ assert \union(1, 1.0) == \union(1.0, 1);
 
@@ -503,6 +503,41 @@ void set_comprehension_assigns () {
   multi_memset(p, 1, 2, 10);
 }
 
+/* Tests the evaluation of \let bindings in ACSL predicates. */
+void plet () {
+  int x = Frama_C_interval(0, 120);
+  int y = Frama_C_interval(0, 10);
+  int z = Frama_C_interval(10, 30);
+  if (v) {
+    //@ assert unknown: \let l = 25; x < l;
+    Frama_C_show_each_0_24(x);
+  }
+  if (v) {
+    //@ assert true: \let l = 250; x < l;
+    Frama_C_show_each_0_120(x);
+  }
+  if (v) {
+    //@ assert false: \let l = 0; x < l;
+    Frama_C_show_each_bottom(x);
+  }
+
+  /* Tests multiple \let bindings. */
+  //@ assert true: \let l = y + z; \let l2 = 100; l < l2;
+  //@ assert unknown: \let l = y + z; \let l2 = x; l < l2;
+
+  /* Tests the kind of assertions generated by the instantiate plugin. */
+  unsigned int t[12];
+  /*@ assert valid: \let __fc_len=12; \valid(t + (0 .. __fc_len-1)); */
+  /*@ assert unknown: \let __fc_len=z; \valid(t + (0 .. __fc_len-1)); */
+  if (v) {
+    /*@ assert invalid: \let __fc_len=12; \valid(t + (0 .. __fc_len)); */
+    Frama_C_show_each_bottom(t);
+  }
+
+  /* Unsupported \let bindings. */
+  /*@ assert unsupported: \let id = (\lambda integer y; y); id(42) == 42; */
+}
+
 void main () {
   eq_tsets();
   eq_char();
@@ -521,4 +556,5 @@ void main () {
   float_abs();
   set_comprehension();
   set_comprehension_assigns();
+  plet();
 }
diff --git a/tests/value/oracle/logic.res.oracle b/tests/value/oracle/logic.res.oracle
index 30722c6f9202a123856a2607a254fc4cd1c34f78..f88f05e9117129bb86b043b56223a54f5c3c6475 100644
--- a/tests/value/oracle/logic.res.oracle
+++ b/tests/value/oracle/logic.res.oracle
@@ -14,7 +14,7 @@
   arr_ptr[0..2] ∈ {0}
   arr_ptr_arr[0..5] ∈ {0}
 [eva] computing for function eq_tsets <- main.
-  Called from logic.c:507.
+  Called from logic.c:542.
 [eva] logic.c:103: 
   cannot evaluate ACSL term, unsupported ACSL construct: == operation on non-supported type set<_#8>
 [eva:alarm] logic.c:103: Warning: assertion got status unknown.
@@ -56,20 +56,20 @@
 [eva] Recording results for eq_tsets
 [eva] Done for function eq_tsets
 [eva] computing for function eq_char <- main.
-  Called from logic.c:508.
+  Called from logic.c:543.
 [eva] logic.c:149: Frama_C_show_each: {-126}
 [eva] logic.c:150: assertion got status valid.
 [eva] logic.c:151: assertion got status valid.
 [eva] Recording results for eq_char
 [eva] Done for function eq_char
 [eva] computing for function casts <- main.
-  Called from logic.c:509.
+  Called from logic.c:544.
 [eva] logic.c:155: assertion got status valid.
 [eva] logic.c:156: assertion got status valid.
 [eva] Recording results for casts
 [eva] Done for function casts
 [eva] computing for function empty_tset <- main.
-  Called from logic.c:510.
+  Called from logic.c:545.
 [eva] computing for function f_empty_tset <- empty_tset <- main.
   Called from logic.c:166.
 [eva] using specification for function f_empty_tset
@@ -80,7 +80,7 @@
 [eva] Recording results for empty_tset
 [eva] Done for function empty_tset
 [eva] computing for function reduce_by_equal <- main.
-  Called from logic.c:511.
+  Called from logic.c:546.
 [eva:alarm] logic.c:172: Warning: accessing out of bounds index. assert 0 ≤ v;
 [eva:alarm] logic.c:172: Warning: accessing out of bounds index. assert v < 10;
 [eva:alarm] logic.c:173: Warning: assertion got status unknown.
@@ -88,7 +88,7 @@
 [eva] Recording results for reduce_by_equal
 [eva] Done for function reduce_by_equal
 [eva] computing for function alarms <- main.
-  Called from logic.c:512.
+  Called from logic.c:547.
 [eva:alarm] logic.c:182: Warning: assertion 'ASSUME' got status unknown.
 [eva:alarm] logic.c:184: Warning: assertion 'UNK' got status unknown.
 [eva] logic.c:185: Frama_C_show_each: {-1; 1}
@@ -112,7 +112,7 @@
 [eva] Recording results for alarms
 [eva] Done for function alarms
 [eva] computing for function cond_in_lval <- main.
-  Called from logic.c:513.
+  Called from logic.c:548.
 [eva] computing for function select_like <- cond_in_lval <- main.
   Called from logic.c:228.
 [eva] using specification for function select_like
@@ -140,7 +140,7 @@
 [eva] Recording results for cond_in_lval
 [eva] Done for function cond_in_lval
 [eva] computing for function pred <- main.
-  Called from logic.c:514.
+  Called from logic.c:549.
 [eva] logic.c:90: assertion got status valid.
 [eva] logic.c:91: assertion got status valid.
 [eva] logic.c:31: cannot evaluate ACSL term, \at() on a C label is unsupported
@@ -185,7 +185,7 @@
 [eva] Recording results for pred
 [eva] Done for function pred
 [eva] computing for function float_sign <- main.
-  Called from logic.c:515.
+  Called from logic.c:550.
 [eva] logic.c:251: assertion got status valid.
 [eva] logic.c:252: assertion got status valid.
 [eva] logic.c:253: assertion got status valid.
@@ -194,7 +194,7 @@
 [eva] Recording results for float_sign
 [eva] Done for function float_sign
 [eva] computing for function min_max <- main.
-  Called from logic.c:516.
+  Called from logic.c:551.
 [eva] computing for function Frama_C_interval <- min_max <- main.
   Called from logic.c:274.
 [eva] using specification for function Frama_C_interval
@@ -219,7 +219,7 @@
 [eva] Recording results for min_max
 [eva] Done for function min_max
 [eva] computing for function assign_tsets <- main.
-  Called from logic.c:517.
+  Called from logic.c:552.
 [eva] computing for function assign_tsets_aux <- assign_tsets <- main.
   Called from logic.c:269.
 [eva] using specification for function assign_tsets_aux
@@ -227,7 +227,7 @@
 [eva] Recording results for assign_tsets
 [eva] Done for function assign_tsets
 [eva] computing for function check_and_assert <- main.
-  Called from logic.c:518.
+  Called from logic.c:553.
 [eva:alarm] logic.c:295: Warning: assertion got status unknown.
 [eva] logic.c:296: Frama_C_show_each_42: {42}
 [eva] logic.c:297: check got status valid.
@@ -241,7 +241,7 @@
 [eva] Recording results for check_and_assert
 [eva] Done for function check_and_assert
 [eva] computing for function min_max_quantifier <- main.
-  Called from logic.c:519.
+  Called from logic.c:554.
 [eva] logic.c:321: check 'valid' got status valid.
 [eva] logic.c:322: check 'valid' got status valid.
 [eva] logic.c:323: check 'valid' got status valid.
@@ -303,7 +303,7 @@
 [eva] Recording results for min_max_quantifier
 [eva] Done for function min_max_quantifier
 [eva] computing for function int_abs <- main.
-  Called from logic.c:520.
+  Called from logic.c:555.
 [eva] computing for function abs <- int_abs <- main.
   Called from logic.c:365.
 [eva] using specification for function abs
@@ -425,7 +425,7 @@
 [eva] Recording results for int_abs
 [eva] Done for function int_abs
 [eva] computing for function float_abs <- main.
-  Called from logic.c:521.
+  Called from logic.c:556.
 [eva] computing for function fabs <- float_abs <- main.
   Called from logic.c:421.
 [eva] using specification for function fabs
@@ -484,7 +484,7 @@
 [eva] Recording results for float_abs
 [eva] Done for function float_abs
 [eva] computing for function set_comprehension <- main.
-  Called from logic.c:522.
+  Called from logic.c:557.
 [eva:alarm] logic.c:444: Warning: assertion got status unknown.
 [eva] logic.c:445: Frama_C_show_each_10_100: [10..100]
 [eva:alarm] logic.c:448: Warning: assertion got status unknown.
@@ -520,15 +520,55 @@
 [eva] Recording results for set_comprehension
 [eva] Done for function set_comprehension
 [eva] computing for function set_comprehension_assigns <- main.
-  Called from logic.c:523.
+  Called from logic.c:558.
 [eva] computing for function multi_memset <- set_comprehension_assigns <- main.
   Called from logic.c:503.
 [eva] using specification for function multi_memset
 [eva] Done for function multi_memset
 [eva] Recording results for set_comprehension_assigns
 [eva] Done for function set_comprehension_assigns
+[eva] computing for function plet <- main.
+  Called from logic.c:559.
+[eva] computing for function Frama_C_interval <- plet <- main.
+  Called from logic.c:508.
+[eva] logic.c:508: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- plet <- main.
+  Called from logic.c:509.
+[eva] logic.c:509: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- plet <- main.
+  Called from logic.c:510.
+[eva] logic.c:510: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:alarm] logic.c:512: Warning: assertion 'unknown' got status unknown.
+[eva] logic.c:513: Frama_C_show_each_0_24: [0..24]
+[eva] logic.c:516: assertion 'true' got status valid.
+[eva] logic.c:517: Frama_C_show_each_0_120: [0..120]
+[eva:alarm] logic.c:520: Warning: 
+  assertion 'false' got status invalid (stopping propagation).
+[eva] logic.c:525: assertion 'true' got status valid.
+[eva:alarm] logic.c:526: Warning: assertion 'unknown' got status unknown.
+[eva] logic.c:530: assertion 'valid' got status valid.
+[eva:alarm] logic.c:531: Warning: assertion 'unknown' got status unknown.
+[eva:alarm] logic.c:533: Warning: 
+  assertion 'invalid' got status invalid (stopping propagation).
+[eva] logic.c:538: 
+  cannot evaluate ACSL term, unsupported ACSL construct: \let binding
+[eva:alarm] logic.c:538: Warning: assertion 'unsupported' got status unknown.
+[eva] Recording results for plet
+[eva] Done for function plet
 [eva] Recording results for main
 [eva] Done for function main
+[eva] logic.c:530: 
+  Cannot evaluate range bound __fc_len - 1
+  (unsupported logic var __fc_len). Approximating
+[eva] logic.c:533: 
+  Cannot evaluate range bound __fc_len
+  (unsupported logic var __fc_len). Approximating
 [scope:rm_asserts] removing 5 assertion(s)
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function alarms:
@@ -661,6 +701,11 @@
      [61] ∈ {3}
      [62] ∈ {2}
      [63] ∈ {1}
+[eva:final-states] Values at end of function plet:
+  Frama_C_entropy_source ∈ [--..--]
+  x_0 ∈ [0..120]
+  y ∈ [0..10]
+  z ∈ [10..30]
 [eva:final-states] Values at end of function reduce_by_equal:
   a[0..8] ∈ {1}
    [9] ∈ [--..--]
@@ -762,6 +807,8 @@
 [from] Done for function min_max
 [from] Computing for function min_max_quantifier
 [from] Done for function min_max_quantifier
+[from] Computing for function plet
+[from] Done for function plet
 [from] Computing for function reduce_by_equal
 [from] Done for function reduce_by_equal
 [from] Computing for function cond_in_lval
@@ -830,6 +877,8 @@
 [from] Function multi_memset:
   buf1[0..9] FROM \nothing (and SELF)
   buf2[0..7] FROM \nothing (and SELF)
+[from] Function plet:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
 [from] Function reduce_by_equal:
   NO EFFECTS
 [from] Function select_like:
@@ -914,6 +963,10 @@
     Frama_C_entropy_source; i; j; t_0[0..63]
 [inout] Inputs for function min_max_quantifier:
     Frama_C_entropy_source
+[inout] Out (internal) for function plet:
+    Frama_C_entropy_source; x_0; y; z
+[inout] Inputs for function plet:
+    Frama_C_entropy_source; v
 [inout] Out (internal) for function reduce_by_equal:
     a[0..9]
 [inout] Inputs for function reduce_by_equal: