diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index d5fa853278e19b22221722a1c0f9ea1304cb2c28..5fe9660ff361769705090186ba8aaec7dd5486e7 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -594,6 +594,27 @@ let build_automaton ~annotations kf =
   in
   G.iter_edges_e bind_labels g;
 
+  (* Recursively removes unreachable vertices, except those bound to a statement
+     in [table]. *)
+  let stmt_vertices =
+    let add _stmt (v1, v2) acc = Vertex.Set.(add v1 (add v2 acc)) in
+    StmtTable.fold add table Vertex.Set.empty
+  in
+  let is_unreachable vertex =
+    G.in_degree g vertex = 0
+    && not (Vertex.equal vertex entry_point)
+    && not (Vertex.Set.mem vertex stmt_vertices)
+  in
+  let rec remove_unreachable vertex =
+    let succs = G.succ g vertex in
+    G.remove_vertex g vertex;
+    List.iter remove_unreachable (List.filter is_unreachable succs)
+  in
+  let unreachables =
+    G.fold_vertex (fun v l -> if is_unreachable v then v :: l else l)  g []
+  in
+  List.iter remove_unreachable unreachables;
+
   (* Return the result *)
   {graph = g; entry_point; return_point; stmt_table = table}
 
diff --git a/tests/misc/oracle/interpreted_automata_dataflow_backward.dot b/tests/misc/oracle/interpreted_automata_dataflow_backward.dot
index 47e6019ac1093ecdc6ea36d337a1a351c2cb8f0d..90f737cafe26b8a2a85f1a103dadd5cf611984da 100644
--- a/tests/misc/oracle/interpreted_automata_dataflow_backward.dot
+++ b/tests/misc/oracle/interpreted_automata_dataflow_backward.dot
@@ -4,77 +4,73 @@ digraph G {
   cp1 [label=<x>, ];
   cp2 [label=< >, ];
   cp3 [label=<x>, ];
-  cp4 [label=< >, ];
+  cp4 [label=<x, y>, ];
   cp5 [label=<x, y>, ];
   cp6 [label=<x, y>, ];
-  cp7 [label=<x, y>, ];
-  cp8 [label=<x>, ];
-  cp9 [label=<x, a>, ];
-  cp10 [label=<x>, ];
-  cp11 [label=<x, a>, ];
-  cp12 [label=<x>, ];
+  cp7 [label=<x>, ];
+  cp8 [label=<x, a>, ];
+  cp9 [label=<x>, ];
+  cp10 [label=<x, a>, ];
+  cp11 [label=<x>, ];
+  cp12 [label=<x, a, i>, ];
   cp13 [label=<x, a, i>, ];
-  cp14 [label=<x, a, i>, ];
-  cp15 [label=<x, a, i>, shape=invtriangle, ];
+  cp14 [label=<x, a, i>, shape=invtriangle, ];
+  cp15 [label=<x, a, i>, ];
   cp16 [label=<x, a, i>, ];
   cp17 [label=<x, a, i>, ];
-  cp18 [label=<x, a, i>, ];
+  cp18 [label=<x>, ];
   cp19 [label=<x>, ];
-  cp20 [label=<x>, ];
+  cp20 [label=<x, a, i>, ];
   cp21 [label=<x, a, i>, ];
   cp22 [label=<x, a, i>, ];
   cp23 [label=<x, a, i>, ];
   cp24 [label=<x, a, i>, ];
-  cp25 [label=<x, a, i>, ];
-  cp26 [label=<x, a, i>, ];
+  cp25 [label=< >, ];
+  cp26 [label=< >, ];
   cp27 [label=< >, ];
   cp28 [label=< >, ];
   cp29 [label=< >, ];
   cp30 [label=< >, ];
-  cp31 [label=< >, ];
-  cp32 [label=< >, ];
+  cp31 [label=<x>, ];
+  cp32 [label=<x>, ];
   cp33 [label=<x>, ];
-  cp34 [label=<x>, ];
-  cp35 [label=<x>, ];
   
-  subgraph cluster_1 { cp26;cp25;cp24;cp23;cp22;cp18;cp17;cp16;cp15;cp14;
+  subgraph cluster_1 { cp24;cp23;cp22;cp21;cp20;cp17;cp16;cp15;cp14;cp13;
      };
   
   cp1 -> cp3 [label=<Enter y, z, w, a>, ];
-  cp3 -> cp5 [label=<int y = 3;>, ];
-  cp4 -> cp2 [label=<Exit y, z, w, a>, ];
-  cp5 -> cp6 [label=<y *= 2;>, ];
-  cp6 -> cp7 [label=<int z = y + 1;>, ];
-  cp7 -> cp8 [label=<int w = y + x;>, ];
-  cp8 -> cp9 [label=<int a = 1;>, ];
-  cp9 -> cp11 [label=<Enter i>, ];
-  cp10 -> cp28 [label=<x != 3>, ];
-  cp10 -> cp29 [label=<!(x != 3)>, ];
-  cp11 -> cp13 [label=<int i = 0;>, ];
-  cp12 -> cp10 [label=<Exit i>, ];
-  cp13 -> cp14 [label=< >, ];
-  cp14 -> cp15 [constraint=false, label=<Enter >, ];
-  cp15 -> cp18 [label=<i &lt; 10>, ];
-  cp15 -> cp19 [label=<!(i &lt; 10)>, ];
-  cp16 -> cp14 [label=<Exit >, ];
-  cp17 -> cp23 [label=<Enter b, c>, ];
-  cp18 -> cp17 [label=< >, ];
-  cp19 -> cp20 [label=<Enter >, ];
-  cp20 -> cp33 [label=< >, ];
-  cp21 -> cp17 [label=<Exit >, ];
-  cp22 -> cp16 [label=<i ++;>, ];
-  cp23 -> cp25 [label=<int b = 3;>, ];
-  cp24 -> cp22 [label=<Exit b, c>, ];
-  cp25 -> cp26 [label=<int c = i + 1;>, ];
-  cp26 -> cp24 [label=<a ++;>, ];
-  cp27 -> cp32 [label=<return>, ];
-  cp28 -> cp30 [label=<Enter >, ];
-  cp29 -> cp27 [label=< >, ];
-  cp30 -> cp31 [label=<x = 3;>, ];
-  cp31 -> cp27 [label=<Exit >, ];
-  cp32 -> cp2 [label=<Exit y, z, w, a>, ];
-  cp33 -> cp34 [label=<Exit i>, ];
-  cp34 -> cp35 [label=<Exit >, ];
-  cp35 -> cp10 [label=<Exit >, ];
+  cp3 -> cp4 [label=<int y = 3;>, ];
+  cp4 -> cp5 [label=<y *= 2;>, ];
+  cp5 -> cp6 [label=<int z = y + 1;>, ];
+  cp6 -> cp7 [label=<int w = y + x;>, ];
+  cp7 -> cp8 [label=<int a = 1;>, ];
+  cp8 -> cp10 [label=<Enter i>, ];
+  cp9 -> cp26 [label=<x != 3>, ];
+  cp9 -> cp27 [label=<!(x != 3)>, ];
+  cp10 -> cp12 [label=<int i = 0;>, ];
+  cp11 -> cp9 [label=<Exit i>, ];
+  cp12 -> cp13 [label=< >, ];
+  cp13 -> cp14 [constraint=false, label=<Enter >, ];
+  cp14 -> cp17 [label=<i &lt; 10>, ];
+  cp14 -> cp18 [label=<!(i &lt; 10)>, ];
+  cp15 -> cp13 [label=<Exit >, ];
+  cp16 -> cp21 [label=<Enter b, c>, ];
+  cp17 -> cp16 [label=< >, ];
+  cp18 -> cp19 [label=<Enter >, ];
+  cp19 -> cp31 [label=< >, ];
+  cp20 -> cp15 [label=<i ++;>, ];
+  cp21 -> cp23 [label=<int b = 3;>, ];
+  cp22 -> cp20 [label=<Exit b, c>, ];
+  cp23 -> cp24 [label=<int c = i + 1;>, ];
+  cp24 -> cp22 [label=<a ++;>, ];
+  cp25 -> cp30 [label=<return>, ];
+  cp26 -> cp28 [label=<Enter >, ];
+  cp27 -> cp25 [label=< >, ];
+  cp28 -> cp29 [label=<x = 3;>, ];
+  cp29 -> cp25 [label=<Exit >, ];
+  cp30 -> cp2 [label=<Exit y, z, w, a>, ];
+  cp31 -> cp32 [label=<Exit i>, ];
+  cp32 -> cp33 [label=<Exit >, ];
+  cp33 -> cp9 [label=<Exit >, ];
   
   }
\ No newline at end of file
diff --git a/tests/misc/oracle/interpreted_automata_dataflow_forward.dot b/tests/misc/oracle/interpreted_automata_dataflow_forward.dot
index 65c37595f4a46b8fde1a551920de17f3ecb8e92a..715c5beae70f84dfde5c5e293af5ab22b7f2c25f 100644
--- a/tests/misc/oracle/interpreted_automata_dataflow_forward.dot
+++ b/tests/misc/oracle/interpreted_automata_dataflow_forward.dot
@@ -4,77 +4,73 @@ digraph G {
   cp1 [label=< >, ];
   cp2 [label=<x: 3<br />y: 6<br />z: 7>, ];
   cp3 [label=< >, ];
-  cp4 [label=<⊥>, style="dashed", ];
-  cp5 [label=<y: 3>, ];
-  cp6 [label=<y: 6>, ];
+  cp4 [label=<y: 3>, ];
+  cp5 [label=<y: 6>, ];
+  cp6 [label=<y: 6<br />z: 7>, ];
   cp7 [label=<y: 6<br />z: 7>, ];
-  cp8 [label=<y: 6<br />z: 7>, ];
-  cp9 [label=<y: 6<br />z: 7<br />a: 1>, ];
-  cp10 [label=<y: 6<br />z: 7>, ];
-  cp11 [label=<y: 6<br />z: 7<br />a: 1>, ];
-  cp12 [label=<⊥>, style="dashed", ];
-  cp13 [label=<y: 6<br />z: 7<br />a: 1<br />i: 0>, ];
-  cp14 [label=<y: 6<br />z: 7>, shape=invtriangle, ];
-  cp15 [label=<y: 6<br />z: 7>, ];
-  cp16 [label=<y: 6<br />z: 7<br />b: 3>, ];
+  cp8 [label=<y: 6<br />z: 7<br />a: 1>, ];
+  cp9 [label=<y: 6<br />z: 7>, ];
+  cp10 [label=<y: 6<br />z: 7<br />a: 1>, ];
+  cp11 [label=<⊥>, style="dashed", ];
+  cp12 [label=<y: 6<br />z: 7<br />a: 1<br />i: 0>, ];
+  cp13 [label=<y: 6<br />z: 7>, shape=invtriangle, ];
+  cp14 [label=<y: 6<br />z: 7>, ];
+  cp15 [label=<y: 6<br />z: 7<br />b: 3>, ];
+  cp16 [label=<y: 6<br />z: 7>, ];
   cp17 [label=<y: 6<br />z: 7>, ];
   cp18 [label=<y: 6<br />z: 7>, ];
   cp19 [label=<y: 6<br />z: 7>, ];
-  cp20 [label=<y: 6<br />z: 7>, ];
-  cp21 [label=<⊥>, style="dashed", ];
+  cp20 [label=<y: 6<br />z: 7<br />b: 3>, ];
+  cp21 [label=<y: 6<br />z: 7>, ];
   cp22 [label=<y: 6<br />z: 7<br />b: 3>, ];
-  cp23 [label=<y: 6<br />z: 7>, ];
+  cp23 [label=<y: 6<br />z: 7<br />b: 3>, ];
   cp24 [label=<y: 6<br />z: 7<br />b: 3>, ];
-  cp25 [label=<y: 6<br />z: 7<br />b: 3>, ];
-  cp26 [label=<y: 6<br />z: 7<br />b: 3>, ];
+  cp25 [label=<x: 3<br />y: 6<br />z: 7>, ];
+  cp26 [label=<y: 6<br />z: 7>, ];
   cp27 [label=<x: 3<br />y: 6<br />z: 7>, ];
   cp28 [label=<y: 6<br />z: 7>, ];
   cp29 [label=<x: 3<br />y: 6<br />z: 7>, ];
-  cp30 [label=<y: 6<br />z: 7>, ];
-  cp31 [label=<x: 3<br />y: 6<br />z: 7>, ];
-  cp32 [label=<x: 3<br />y: 6<br />z: 7>, ];
+  cp30 [label=<x: 3<br />y: 6<br />z: 7>, ];
+  cp31 [label=<y: 6<br />z: 7>, ];
+  cp32 [label=<y: 6<br />z: 7>, ];
   cp33 [label=<y: 6<br />z: 7>, ];
-  cp34 [label=<y: 6<br />z: 7>, ];
-  cp35 [label=<y: 6<br />z: 7>, ];
   
-  subgraph cluster_1 { cp26;cp25;cp24;cp23;cp22;cp18;cp17;cp16;cp15;cp14;
+  subgraph cluster_1 { cp24;cp23;cp22;cp21;cp20;cp17;cp16;cp15;cp14;cp13;
      };
   
   cp1 -> cp3 [label=<Enter y, z, w, a>, ];
-  cp3 -> cp5 [label=<int y = 3;>, ];
-  cp4 -> cp2 [label=<Exit y, z, w, a>, style="dashed", ];
-  cp5 -> cp6 [label=<y *= 2;>, ];
-  cp6 -> cp7 [label=<int z = y + 1;>, ];
-  cp7 -> cp8 [label=<int w = y + x;>, ];
-  cp8 -> cp9 [label=<int a = 1;>, ];
-  cp9 -> cp11 [label=<Enter i>, ];
-  cp10 -> cp28 [label=<x != 3>, ];
-  cp10 -> cp29 [label=<!(x != 3)>, ];
-  cp11 -> cp13 [label=<int i = 0;>, ];
-  cp12 -> cp10 [label=<Exit i>, style="dashed", ];
-  cp13 -> cp14 [label=< >, ];
-  cp14 -> cp15 [label=<Enter >, ];
-  cp15 -> cp18 [label=<i &lt; 10>, ];
-  cp15 -> cp19 [label=<!(i &lt; 10)>, ];
-  cp16 -> cp14 [constraint=false, label=<Exit >, ];
-  cp17 -> cp23 [label=<Enter b, c>, ];
-  cp18 -> cp17 [label=< >, ];
-  cp19 -> cp20 [label=<Enter >, ];
-  cp20 -> cp33 [label=< >, ];
-  cp21 -> cp17 [label=<Exit >, style="dashed", ];
-  cp22 -> cp16 [label=<i ++;>, ];
-  cp23 -> cp25 [label=<int b = 3;>, ];
-  cp24 -> cp22 [label=<Exit b, c>, ];
-  cp25 -> cp26 [label=<int c = i + 1;>, ];
-  cp26 -> cp24 [label=<a ++;>, ];
-  cp27 -> cp32 [label=<return>, ];
-  cp28 -> cp30 [label=<Enter >, ];
-  cp29 -> cp27 [label=< >, ];
-  cp30 -> cp31 [label=<x = 3;>, ];
-  cp31 -> cp27 [label=<Exit >, ];
-  cp32 -> cp2 [label=<Exit y, z, w, a>, ];
-  cp33 -> cp34 [label=<Exit i>, ];
-  cp34 -> cp35 [label=<Exit >, ];
-  cp35 -> cp10 [label=<Exit >, ];
+  cp3 -> cp4 [label=<int y = 3;>, ];
+  cp4 -> cp5 [label=<y *= 2;>, ];
+  cp5 -> cp6 [label=<int z = y + 1;>, ];
+  cp6 -> cp7 [label=<int w = y + x;>, ];
+  cp7 -> cp8 [label=<int a = 1;>, ];
+  cp8 -> cp10 [label=<Enter i>, ];
+  cp9 -> cp26 [label=<x != 3>, ];
+  cp9 -> cp27 [label=<!(x != 3)>, ];
+  cp10 -> cp12 [label=<int i = 0;>, ];
+  cp11 -> cp9 [label=<Exit i>, style="dashed", ];
+  cp12 -> cp13 [label=< >, ];
+  cp13 -> cp14 [label=<Enter >, ];
+  cp14 -> cp17 [label=<i &lt; 10>, ];
+  cp14 -> cp18 [label=<!(i &lt; 10)>, ];
+  cp15 -> cp13 [constraint=false, label=<Exit >, ];
+  cp16 -> cp21 [label=<Enter b, c>, ];
+  cp17 -> cp16 [label=< >, ];
+  cp18 -> cp19 [label=<Enter >, ];
+  cp19 -> cp31 [label=< >, ];
+  cp20 -> cp15 [label=<i ++;>, ];
+  cp21 -> cp23 [label=<int b = 3;>, ];
+  cp22 -> cp20 [label=<Exit b, c>, ];
+  cp23 -> cp24 [label=<int c = i + 1;>, ];
+  cp24 -> cp22 [label=<a ++;>, ];
+  cp25 -> cp30 [label=<return>, ];
+  cp26 -> cp28 [label=<Enter >, ];
+  cp27 -> cp25 [label=< >, ];
+  cp28 -> cp29 [label=<x = 3;>, ];
+  cp29 -> cp25 [label=<Exit >, ];
+  cp30 -> cp2 [label=<Exit y, z, w, a>, ];
+  cp31 -> cp32 [label=<Exit i>, ];
+  cp32 -> cp33 [label=<Exit >, ];
+  cp33 -> cp9 [label=<Exit >, ];
   
   }
\ No newline at end of file
diff --git a/tests/value/oracle/partitioning-interproc.0.res.oracle b/tests/value/oracle/partitioning-interproc.0.res.oracle
index 76c88a345e072128c5c455ea5432d089b98654f0..4481fdb71c75b560b40d5f611f615da44aa446a3 100644
--- a/tests/value/oracle/partitioning-interproc.0.res.oracle
+++ b/tests/value/oracle/partitioning-interproc.0.res.oracle
@@ -12,9 +12,9 @@
 [eva] Done for function Frama_C_nondet
 [eva] Recording results for cassign
 [eva] Done for function cassign
-[eva:alarm] tests/value/partitioning-interproc.c:25: Warning: 
-  accessing uninitialized left-value. assert \initialized(&x);
 [eva] tests/value/partitioning-interproc.c:26: Frama_C_show_each: {1}
+[eva] tests/value/partitioning-interproc.c:30: 
+  Reusing old results for call to cassign
 [eva] computing for function cassign <- cassign_test.
   Called from tests/value/partitioning-interproc.c:30.
 [eva] computing for function Frama_C_nondet <- cassign <- cassign_test.
@@ -22,15 +22,6 @@
 [eva] Done for function Frama_C_nondet
 [eva] Recording results for cassign
 [eva] Done for function cassign
-[eva] computing for function cassign <- cassign_test.
-  Called from tests/value/partitioning-interproc.c:30.
-[eva] computing for function Frama_C_nondet <- cassign <- cassign_test.
-  Called from tests/value/partitioning-interproc.c:11.
-[eva] Done for function Frama_C_nondet
-[eva] Recording results for cassign
-[eva] Done for function cassign
-[eva:alarm] tests/value/partitioning-interproc.c:31: Warning: 
-  accessing uninitialized left-value. assert \initialized(&x);
 [eva] tests/value/partitioning-interproc.c:32: Frama_C_show_each: {1}
 [eva] Recording results for cassign_test
 [eva] done for function cassign_test
diff --git a/tests/value/oracle/partitioning-interproc.1.res.oracle b/tests/value/oracle/partitioning-interproc.1.res.oracle
index a2bde102b390521d164ac45c3f46efd0e6c0d98e..dfd3684a60556eb5eb3f3103610e38cf700f7c6a 100644
--- a/tests/value/oracle/partitioning-interproc.1.res.oracle
+++ b/tests/value/oracle/partitioning-interproc.1.res.oracle
@@ -14,7 +14,7 @@
 [eva:final-states] Values at end of function fabs:
   __retres ∈ [-0. .. 1.79769313486e+308]
 [eva:final-states] Values at end of function fabs_test:
-  x ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+  x ∈ [-1. .. 1.]
 [from] Computing for function fabs
 [from] Done for function fabs
 [from] Computing for function fabs_test