diff --git a/lib/miniImp/Cfg.ml b/lib/miniImp/Cfg.ml
index a64066a..7e92de6 100644
--- a/lib/miniImp/Cfg.ml
+++ b/lib/miniImp/Cfg.ml
@@ -83,6 +83,7 @@ module Cfg = struct
     empty: bool;
     nodes: NodeSet.t;
     edges: (Node.t * (Node.t option)) NodeMap.t;
+    reverseedges: (Node.t list) NodeMap.t;
     initial: Node.t option;
     terminal: Node.t option;
     code: (simpleStatements list) NodeMap.t
@@ -92,6 +93,7 @@ module Cfg = struct
     { empty = true;
       nodes = NodeSet.empty;
       edges = NodeMap.empty;
+      reverseedges = NodeMap.empty;
       initial = None;
       terminal = None;
       code = NodeMap.empty }
@@ -114,6 +116,12 @@ module Cfg = struct
                 NodeMap.add entryNode (cfg1initial, Some cfg2initial) |>
                 NodeMap.add cfg1terminal (exitNode, None) |>
                 NodeMap.add cfg2terminal (exitNode, None);
+        reverseedges = NodeMap.union (fun _ -> failwith "Failed merging edges of cfg.")
+            cfg1.reverseedges cfg2.reverseedges |>
+                       NodeMap.add_to_list cfg1initial entryNode |>
+                       NodeMap.add_to_list cfg2initial entryNode |>
+                       NodeMap.add_to_list exitNode cfg1terminal |>
+                       NodeMap.add_to_list exitNode cfg2terminal;
         initial = Some entryNode;
         terminal = Some exitNode;
         code = NodeMap.union (fun _ -> failwith "Failed merging code of cfg.")
@@ -134,6 +142,9 @@ module Cfg = struct
         edges = NodeMap.union (fun _ -> failwith "Failed merging edges of cfg.")
                               cfg1.edges cfg2.edges |>
                 NodeMap.add cfg1terminal (cfg2initial, None);
+        reverseedges = NodeMap.union (fun _ -> failwith "Failed merging edges of cfg.")
+            cfg1.reverseedges cfg2.reverseedges |>
+                       NodeMap.add_to_list cfg2initial cfg1terminal;
         initial = Some cfg1initial;
         terminal = Some cfg2terminal;
         code = NodeMap.union (fun _ -> failwith "Failed merging code of cfg.")
@@ -146,6 +157,7 @@ module Cfg = struct
       { empty = false;
         nodes = NodeSet.singleton newnode;
         edges = NodeMap.empty;
+        reverseedges = NodeMap.empty;
         initial = Some newnode;
         terminal = Some newnode;
         code = NodeMap.singleton newnode [newcode]
@@ -170,6 +182,14 @@ module Cfg = struct
       ) (NodeMap.to_list c.edges);
     Printf.fprintf ppf "\n";
 
+    Printf.fprintf ppf "Nodes' back edges:\n";
+    List.iter (fun ((n, xs) : (Node.t * (Node.t list))) : unit ->
+        Printf.fprintf ppf "\t%d -> " n.id;
+        List.iter (fun (x: Node.t) -> Printf.fprintf ppf "%d, " x.id) xs;
+        Printf.fprintf ppf "\n"
+      ) (NodeMap.to_list c.reverseedges);
+    Printf.fprintf ppf "\n";
+
     Printf.fprintf ppf "Initial node's id: ";
     Printf.fprintf ppf "%d" ((Option.get c.initial).id);
     Printf.fprintf ppf "\n";
@@ -224,6 +244,11 @@ let rec convert_c (prevcfg: Cfg.t) (prg: Types.c_exp) : Cfg.t =
               NodeMap.add entrynode (guardnode, None) |>
               NodeMap.add guardnode (cfginitial, Some exitnode) |>
               NodeMap.add cfgterminal (guardnode, None);
+      reverseedges = cfg.reverseedges |>
+                     NodeMap.add_to_list guardnode entrynode |>
+                     NodeMap.add_to_list cfginitial guardnode |>
+                     NodeMap.add_to_list exitnode guardnode |>
+                     NodeMap.add_to_list guardnode cfgterminal;
       initial = Some entrynode;
       terminal = Some exitnode;
       code = NodeMap.add_to_list guardnode (SimpleGuard (convertedb)) cfg.code |>
@@ -250,6 +275,10 @@ let rec convert_c (prevcfg: Cfg.t) (prg: Types.c_exp) : Cfg.t =
       edges = bodyincrement.edges |>
               NodeMap.add guardnode (cfginitial, Some exitnode) |>
               NodeMap.add cfgterminal (guardnode, None);
+      reverseedges = bodyincrement.reverseedges |>
+                     NodeMap.add_to_list cfginitial guardnode |>
+                     NodeMap.add_to_list exitnode guardnode |>
+                     NodeMap.add_to_list guardnode cfgterminal;
       initial = Some guardnode;
       terminal = Some exitnode;
       code = NodeMap.add_to_list guardnode (SimpleGuard (convertedguard)) bodyincrement.code |>