diff --git a/src/plugins/eva/partitioning/partition.ml b/src/plugins/eva/partitioning/partition.ml
index b1c1c6f7e2444d0c53b2ea3cd6f2f3b7e1c0d8b3..4c8675e975e8049a309f7dc4666cd1e72042f7f3 100644
--- a/src/plugins/eva/partitioning/partition.ml
+++ b/src/plugins/eva/partitioning/partition.ml
@@ -470,20 +470,24 @@ struct
       let states = function _ -> Abstract.Dom.top in
       Abstract_domain.{ states; result = None }
     in
-    let source = fst (predicate.Cil_types.pred_loc) in
-    let aux positive =
-      let+ state' =
-        Abstract.Dom.reduce_by_predicate env state predicate positive in
-      let x = Abstract.Dom.evaluate_predicate env state' predicate in
-      if x == Unknown
-      then
-        Self.warning ~source ~once:true
-          "failing to learn perfectly from split predicate";
-      if Abstract.Dom.equal state' state then raise Operation_failed;
-      let value = if positive then Integer.one else Integer.zero in
-      value, state'
-    in
-    Bottom.list_values [ aux true; aux false ]
+    match Abstract.Dom.evaluate_predicate env state predicate with
+    | True -> [ Integer.one, state ]
+    | False -> [ Integer.zero, state ]
+    | Unknown ->
+      let source = fst (predicate.Cil_types.pred_loc) in
+      let aux positive =
+        let+ state' =
+          Abstract.Dom.reduce_by_predicate env state predicate positive in
+        let x = Abstract.Dom.evaluate_predicate env state' predicate in
+        if x == Unknown
+        then
+          Self.warning ~source ~once:true
+            "failing to learn perfectly from split predicate";
+        if Abstract.Dom.equal state' state then raise Operation_failed;
+        let value = if positive then Integer.one else Integer.zero in
+        value, state'
+      in
+      Bottom.list_values [ aux true; aux false ]
 
   (* --- Applying partitioning actions onto flows --------------------------- *)
 
diff --git a/tests/value/oracle/partitioning-annots.0.res.oracle b/tests/value/oracle/partitioning-annots.0.res.oracle
index a9944c463d097f25c3d87b231526dd26e7f0ce46..ef583a47f12fc77c9189539ef61777c459342e78 100644
--- a/tests/value/oracle/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle/partitioning-annots.0.res.oracle
@@ -6,13 +6,13 @@
   nondet ∈ [--..--]
   k ∈ {0}
 [eva] computing for function test_slevel <- main.
-  Called from partitioning-annots.c:205.
-[eva] partitioning-annots.c:170: starting to merge loop iterations
-[eva] partitioning-annots.c:175: starting to merge loop iterations
+  Called from partitioning-annots.c:223.
+[eva] partitioning-annots.c:188: starting to merge loop iterations
+[eva] partitioning-annots.c:193: starting to merge loop iterations
 [eva] Recording results for test_slevel
 [eva] Done for function test_slevel
 [eva] computing for function test_unroll <- main.
-  Called from partitioning-annots.c:206.
+  Called from partitioning-annots.c:224.
 [eva:loop-unroll:partial] partitioning-annots.c:26: loop not completely unrolled
 [eva] partitioning-annots.c:26: starting to merge loop iterations
 [eva:loop-unroll:partial] partitioning-annots.c:34: loop not completely unrolled
@@ -25,7 +25,7 @@
 [eva] Recording results for test_unroll
 [eva] Done for function test_unroll
 [eva] computing for function test_split <- main.
-  Called from partitioning-annots.c:207.
+  Called from partitioning-annots.c:225.
 [eva] computing for function Frama_C_interval <- test_split <- main.
   Called from partitioning-annots.c:73.
 [eva] using specification for function Frama_C_interval
@@ -65,7 +65,7 @@
 [eva] Recording results for test_split
 [eva] Done for function test_split
 [eva] computing for function test_dynamic_split <- main.
-  Called from partitioning-annots.c:208.
+  Called from partitioning-annots.c:226.
 [eva] partitioning-annots.c:95: Warning: 
   this partitioning parameter cannot be evaluated safely on all states
 [eva] computing for function Frama_C_interval <- test_dynamic_split <- main.
@@ -89,6 +89,11 @@
 [eva] partitioning-annots.c:109: Frama_C_show_each_no_split: {0}, {0; 1; 2}
 [eva] Recording results for test_dynamic_split
 [eva] Done for function test_dynamic_split
+[eva] computing for function test_dynamic_split_predicate <- main.
+  Called from partitioning-annots.c:227.
+[eva] partitioning-annots.c:124: starting to merge loop iterations
+[eva] Recording results for test_dynamic_split_predicate
+[eva] Done for function test_dynamic_split_predicate
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -96,6 +101,10 @@
   Frama_C_entropy_source ∈ [--..--]
   a ∈ {0}
   b ∈ {0; 1; 2}
+[eva:final-states] Values at end of function test_dynamic_split_predicate:
+  x ∈ [0..44]
+  y ∈ [0..44]
+  c ∈ [--..--]
 [eva:final-states] Values at end of function test_slevel:
   a[0..9] ∈ {42}
   b[0..9] ∈ {42} or UNINITIALIZED
@@ -140,6 +149,8 @@
 [from] Computing for function Frama_C_interval <-test_dynamic_split
 [from] Done for function Frama_C_interval
 [from] Done for function test_dynamic_split
+[from] Computing for function test_dynamic_split_predicate
+[from] Done for function test_dynamic_split_predicate
 [from] Computing for function test_slevel
 [from] Done for function test_slevel
 [from] Computing for function test_split
@@ -155,6 +166,8 @@
   \result FROM Frama_C_entropy_source; min; max
 [from] Function test_dynamic_split:
   Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
+[from] Function test_dynamic_split_predicate:
+  NO EFFECTS
 [from] Function test_slevel:
   NO EFFECTS
 [from] Function test_split:
@@ -170,6 +183,10 @@
     Frama_C_entropy_source; a; b
 [inout] Inputs for function test_dynamic_split:
     Frama_C_entropy_source; nondet
+[inout] Out (internal) for function test_dynamic_split_predicate:
+    x; y; c; i
+[inout] Inputs for function test_dynamic_split_predicate:
+    nondet
 [inout] Out (internal) for function test_slevel:
     a[0..9]; b[0..9]; c[0..9]; d[0..9]; e[0..3]; i; i_0; i_1; i_2; i_3
 [inout] Inputs for function test_slevel:
diff --git a/tests/value/oracle/partitioning-annots.2.res.oracle b/tests/value/oracle/partitioning-annots.2.res.oracle
index b3602de56abbdca1033f0546dfe23e0d7304d74d..0a9a2fa297acc6eb4166b581852b99aa9f02c16f 100644
--- a/tests/value/oracle/partitioning-annots.2.res.oracle
+++ b/tests/value/oracle/partitioning-annots.2.res.oracle
@@ -6,41 +6,41 @@
   nondet ∈ [--..--]
   k ∈ {0}
 [eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from partitioning-annots.c:127.
+  Called from partitioning-annots.c:145.
 [eva] using specification for function Frama_C_interval
-[eva] partitioning-annots.c:127: 
+[eva] partitioning-annots.c:145: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from partitioning-annots.c:127.
+  Called from partitioning-annots.c:145.
 [eva] Done for function Frama_C_interval
-[eva] partitioning-annots.c:125: starting to merge loop iterations
+[eva] partitioning-annots.c:143: starting to merge loop iterations
 [eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from partitioning-annots.c:127.
+  Called from partitioning-annots.c:145.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from partitioning-annots.c:127.
+  Called from partitioning-annots.c:145.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from partitioning-annots.c:127.
+  Called from partitioning-annots.c:145.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from partitioning-annots.c:127.
+  Called from partitioning-annots.c:145.
 [eva] Done for function Frama_C_interval
-[eva:alarm] partitioning-annots.c:134: Warning: 
+[eva:alarm] partitioning-annots.c:152: Warning: 
   accessing uninitialized left-value. assert \initialized(&A[i]);
-[eva] partitioning-annots.c:139: Frama_C_show_each: {9}, {42}
-[eva] partitioning-annots.c:139: Frama_C_show_each: {8}, {42}
-[eva] partitioning-annots.c:139: Frama_C_show_each: {7}, {42}
-[eva] partitioning-annots.c:139: Frama_C_show_each: {6}, {42}
-[eva] partitioning-annots.c:139: Frama_C_show_each: {5}, {42}
-[eva] partitioning-annots.c:139: Frama_C_show_each: {4}, {42}
-[eva] partitioning-annots.c:139: Frama_C_show_each: {3}, {42}
-[eva] partitioning-annots.c:139: Frama_C_show_each: {2}, {42}
-[eva] partitioning-annots.c:139: Frama_C_show_each: {1}, {42}
-[eva] partitioning-annots.c:139: Frama_C_show_each: {0}, {42}
-[eva] partitioning-annots.c:140: assertion got status valid.
-[eva] partitioning-annots.c:143: Frama_C_show_each: {{ "Value 42 not found" }}
+[eva] partitioning-annots.c:157: Frama_C_show_each: {9}, {42}
+[eva] partitioning-annots.c:157: Frama_C_show_each: {8}, {42}
+[eva] partitioning-annots.c:157: Frama_C_show_each: {7}, {42}
+[eva] partitioning-annots.c:157: Frama_C_show_each: {6}, {42}
+[eva] partitioning-annots.c:157: Frama_C_show_each: {5}, {42}
+[eva] partitioning-annots.c:157: Frama_C_show_each: {4}, {42}
+[eva] partitioning-annots.c:157: Frama_C_show_each: {3}, {42}
+[eva] partitioning-annots.c:157: Frama_C_show_each: {2}, {42}
+[eva] partitioning-annots.c:157: Frama_C_show_each: {1}, {42}
+[eva] partitioning-annots.c:157: Frama_C_show_each: {0}, {42}
+[eva] partitioning-annots.c:158: assertion got status valid.
+[eva] partitioning-annots.c:161: Frama_C_show_each: {{ "Value 42 not found" }}
 [eva] Recording results for test_loop_split
 [eva] done for function test_loop_split
 [eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/partitioning-annots.3.res.oracle b/tests/value/oracle/partitioning-annots.3.res.oracle
index 48c5467e10e77085418645ceecaac33ba29fbd22..3fe49f8ff9266240c18aac21e67f32978e3992ca 100644
--- a/tests/value/oracle/partitioning-annots.3.res.oracle
+++ b/tests/value/oracle/partitioning-annots.3.res.oracle
@@ -6,13 +6,13 @@
   nondet ∈ [--..--]
   k ∈ {0}
 [eva] computing for function Frama_C_interval <- test_history.
-  Called from partitioning-annots.c:149.
+  Called from partitioning-annots.c:167.
 [eva] using specification for function Frama_C_interval
-[eva] partitioning-annots.c:149: 
+[eva] partitioning-annots.c:167: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] partitioning-annots.c:155: Frama_C_show_each: {0; 1}, {0; 1}
-[eva:alarm] partitioning-annots.c:158: Warning: 
+[eva] partitioning-annots.c:173: Frama_C_show_each: {0; 1}, {0; 1}
+[eva:alarm] partitioning-annots.c:176: Warning: 
   division by zero. assert j ≢ 0;
 [eva] Recording results for test_history
 [eva] done for function test_history
diff --git a/tests/value/oracle/partitioning-annots.4.res.oracle b/tests/value/oracle/partitioning-annots.4.res.oracle
index e0cd089be19d8497075019a68f420282e5ad95be..793324f2603cfd3fb554a92a29803c88ae31e867 100644
--- a/tests/value/oracle/partitioning-annots.4.res.oracle
+++ b/tests/value/oracle/partitioning-annots.4.res.oracle
@@ -6,13 +6,13 @@
   nondet ∈ [--..--]
   k ∈ {0}
 [eva] computing for function Frama_C_interval <- test_history.
-  Called from partitioning-annots.c:149.
+  Called from partitioning-annots.c:167.
 [eva] using specification for function Frama_C_interval
-[eva] partitioning-annots.c:149: 
+[eva] partitioning-annots.c:167: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] partitioning-annots.c:155: Frama_C_show_each: {0}, {0}
-[eva] partitioning-annots.c:155: Frama_C_show_each: {1}, {1}
+[eva] partitioning-annots.c:173: Frama_C_show_each: {0}, {0}
+[eva] partitioning-annots.c:173: Frama_C_show_each: {1}, {1}
 [eva] Recording results for test_history
 [eva] done for function test_history
 [eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle_apron/partitioning-annots.0.res.oracle b/tests/value/oracle_apron/partitioning-annots.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..94ed9ffca14931983ca8b0fcfd773dae01006fe7
--- /dev/null
+++ b/tests/value/oracle_apron/partitioning-annots.0.res.oracle
@@ -0,0 +1,6 @@
+105,106c105,106
+<   x ∈ [0..44]
+<   y ∈ [0..44]
+---
+>   x ∈ [31..44]
+>   y ∈ [31..44]
diff --git a/tests/value/oracle_apron/partitioning-annots.3.res.oracle b/tests/value/oracle_apron/partitioning-annots.3.res.oracle
index 33f66bd14fdd12275197377d63238791cc99f746..d04cebfc945498812ebf2de1f658c5458442d6d8 100644
--- a/tests/value/oracle_apron/partitioning-annots.3.res.oracle
+++ b/tests/value/oracle_apron/partitioning-annots.3.res.oracle
@@ -1,3 +1,3 @@
 15,16d14
-< [eva:alarm] partitioning-annots.c:158: Warning: 
+< [eva:alarm] partitioning-annots.c:176: Warning: 
 <   division by zero. assert j ≢ 0;
diff --git a/tests/value/oracle_multidim/partitioning-annots.2.res.oracle b/tests/value/oracle_multidim/partitioning-annots.2.res.oracle
index 51ebdf81d7b32f872c0aca78180648d357798c8d..aa0560a3189650ecd3273f1f2c75d759628f57d6 100644
--- a/tests/value/oracle_multidim/partitioning-annots.2.res.oracle
+++ b/tests/value/oracle_multidim/partitioning-annots.2.res.oracle
@@ -1,3 +1,3 @@
 30,31d29
-< [eva:alarm] partitioning-annots.c:134: Warning: 
+< [eva:alarm] partitioning-annots.c:152: Warning: 
 <   accessing uninitialized left-value. assert \initialized(&A[i]);
diff --git a/tests/value/oracle_octagon/partitioning-annots.0.res.oracle b/tests/value/oracle_octagon/partitioning-annots.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..cd64a1b908f4fcd56dac921a50c0bec490216e7e
--- /dev/null
+++ b/tests/value/oracle_octagon/partitioning-annots.0.res.oracle
@@ -0,0 +1,6 @@
+105,106c105,106
+<   x ∈ [0..44]
+<   y ∈ [0..44]
+---
+>   x ∈ {31; 32; 44}
+>   y ∈ {31; 32; 44}
diff --git a/tests/value/partitioning-annots.c b/tests/value/partitioning-annots.c
index a0a6b0161c0fe51695fbf948f723a10cda7e372e..d3ab58aaa5069ea02e5298ffff4abd6874bae81b 100644
--- a/tests/value/partitioning-annots.c
+++ b/tests/value/partitioning-annots.c
@@ -1,5 +1,5 @@
 /* run.config*
-   
+
    STDOPT: #"-eva-default-loop-unroll 10"
    STDOPT: +"-main test_split -eva-partition-value k"
    STDOPT: #"-main test_loop_split -eva-partition-history 1"
@@ -109,6 +109,24 @@ void test_dynamic_split()
   Frama_C_show_each_no_split(a, b);
 }
 
+void test_dynamic_split_predicate()
+{
+  int x, y;
+  //@ dynamic_split \initialized(&x);
+  int c = nondet;
+  if (c != 1) {
+    x = 42;
+  }
+  y = 2;
+  if (c != 1)
+    x += y; // No alarm on x initialization with the dynamic partitioning.
+  else {
+    for (int i = 0; i < 32; i++)
+      x = i;
+  }
+  y = x; // No alarm on x initialization with the dynamic partitioning.
+}
+
 void test_loop_split()
 {
   int A[N];
@@ -165,7 +183,7 @@ void test_slevel()
   for (int i = 0; i < N; i++) {
     a[i] = 42;
   }
-  
+
   //@slevel default;
   for (int i = 0; i < N; i++) {
     b[i] = 42;
@@ -188,7 +206,7 @@ void test_slevel()
     //@slevel merge;
     ; // Otherwise previous annotation is ignored
   }
-  
+
   //@slevel 0;
   ;
   //@slevel full;
@@ -206,5 +224,5 @@ void main(void)
   test_unroll();
   test_split();
   test_dynamic_split();
+  test_dynamic_split_predicate();
 }
-