diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index e3a43ded39da4c886cfcb5493acabfc0b6bc44e5..b942a4063c86c2af263aa91d2ff07392230704d1 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -230,41 +230,56 @@ let solveGame () =
   in
 
   let root_idx1 = coreGetIdxOr1 (graphGetRoot ()) in
-  let game1 = (root_idx1, CU.compose Tcsbasedata.Enumerators.of_list nodeSucessors1, nodeData, fun _ -> None) in
   let root_idx2 = coreGetIdxOr (Some PG_Map.sat_node) (graphGetRoot ()) in
-  let game2 = (root_idx2, CU.compose Tcsbasedata.Enumerators.of_list nodeSucessors2, nodeData, fun _ -> None) in
-  (* Basics.verbosity := 3; *)
+  
+  (* Generate data as required by PG.pg_init *)
+  let game1 = PG.pg_create (PG_Map.size ()) in
+  let game2 = PG.pg_create (PG_Map.size ()) in
+  
+  let rec populate game succ node =
+    if PG.pg_get_owner game node <> PG.plr_undef then () else begin
+        let (prio, player) = nodeData node in
+        let children = succ node in
+        PG.pg_set_owner game node player;
+        PG.pg_set_priority game node prio;
+        List.iter (fun child -> begin
+                       populate game succ child;
+                       PG.pg_add_edge game node child
+                     end) children
+    end
+  in
+  populate game1 nodeSucessors1 root_idx1;
+  populate game2 nodeSucessors2 root_idx2;
 
   let seenmap = Hashtbl.create 10 in
   let rec printGame game node =
     if Hashtbl.mem seenmap node then () else
       begin
         Hashtbl.add seenmap node ();
-        let (_, suc, _, _) = game in
-        let children = Tcsbasedata.Enumerators.to_list (suc node) in
+        let children = PG.ns_nodes (PG.pg_get_successors game node) in
         let formatList l = "[" ^ String.concat "; " (List.map string_of_int l)  ^ "]" in
         Printf.printf "%d -> %s\n" node (formatList children);
         List.iter (printGame game) children
     end
   in
 
-  (* print_endline "GAME 1 ####################"; *)
-  (* printGame game1 root_idx1; *)
-  (* print_endline "GAME 2 ####################"; *)
-  (* Hashtbl.clear seenmap; *)
-  (* printGame game2 root_idx2; *)
-
-  let solution1 = Stratimprlocal2.partially_solve game1 in
-  let solution2 = Stratimprlocal2.partially_solve game2 in
+  (* print_endline "GAME 1 ####################";
+   * printGame game1 root_idx1;
+   * print_endline "GAME 2 ####################";
+   * Hashtbl.clear seenmap;
+   * printGame game2 root_idx2; *)
 
+  let (solution1, _) = Recursive.solve game1 in
+  let (solution2, _) = Recursive.solve game2 in
+  
   let nodeSetStatus node status = match PG_Map.find node with
     | PG_Map.State state -> stateSetStatus state status
     | PG_Map.Core core -> coreSetStatus core status
     | _ -> assert false
   in
   let applySolution node =
-    let (sol1_player,_) = solution1 node in
-    let (sol2_player,_) = solution2 node in
+    let sol1_player = solution1.(node) in
+    let sol2_player = solution2.(node) in
     if sol1_player = eloise then begin
         nodeSetStatus node Sat
       end 
diff --git a/src/lib/CoolGraph.ml b/src/lib/CoolGraph.ml
index c715f03bba4a1e33dbc64fdb23fa1d30806de4f1..0ad18f462e819bbaf7c725f64734ed45735bd3bc 100644
--- a/src/lib/CoolGraph.ml
+++ b/src/lib/CoolGraph.ml
@@ -102,6 +102,8 @@ module type S = sig
     val sat_node : Paritygame.node
     val unsat_node : Paritygame.node
 
+    val size : unit -> int
+
     val reset : unit -> unit
   end
 
@@ -363,6 +365,15 @@ let doSatPropagation () = match !prop_rate with
 (*        "Module type" and a specific implementation of the graph           *)
 (*****************************************************************************)
 
+(* Counter begins at 2 to have two reserved values 0 and 1
+   This is needed for special nodes in parity games *)
+let nodeCounter = ref 2
+let nextNodeIdx () : int =
+    let oldVal = !nodeCounter in
+    nodeCounter := oldVal + 1;
+    oldVal
+let nodeCounterReset () = nodeCounter := 2
+
 let graphStates = ref (Array.make 0 (GHt.create 0 : state GHt.t))
 let graphCores = ref (Array.make 0 (GHt.create 0 : core GHt.t))
 let graphCnstrs = ref (GHtS.create 0 : constrnt GHtS.t)
@@ -373,7 +384,8 @@ let graphInit () =
   graphStates := Array.init size (fun _ -> GHt.create 128);
   graphCores := Array.init size (fun _ -> GHt.create 128);
   graphCnstrs := GHtS.create 128;
-  graphRoot := None
+  graphRoot := None;
+  nodeCounterReset ()
 
 let graphIterStates fkt =
   Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphStates
@@ -461,6 +473,8 @@ module ParityGameMapping = struct
   let sat_node = 0
   let unsat_node = 1
 
+  let size () = Hashtbl.length node_table
+
   let reset () =
     Hashtbl.reset node_table;
     Hashtbl.add node_table sat_node Sat;
@@ -471,14 +485,6 @@ end
 (*      "Module type" and a specific implementation of state nodes           *)
 (*****************************************************************************)
 
-(* Counter begins at 2 to have two reserved values 0 and 1
-   This is needed for special nodes in parity games *)
-let nodeCounter = ref 2
-let nextNodeIdx () : int =
-    let oldVal = !nodeCounter in
-    nodeCounter := oldVal + 1;
-    oldVal
-
 let stateMake sort bs focus exp =
   let res = { sortS = sort; bsS = bs; focusS = focus; statusS = Expandable;
               parentsS = []; childrenS = []; constraintsS = cssEmpty;
diff --git a/src/lib/CoolGraph.mli b/src/lib/CoolGraph.mli
index aae81f2599039c49d2e220d23d0d55f810e0030d..984f578d6ba5c4248b862d4383f3e11b99235433 100644
--- a/src/lib/CoolGraph.mli
+++ b/src/lib/CoolGraph.mli
@@ -97,6 +97,9 @@ module type S = sig
     val sat_node : Paritygame.node
     val unsat_node : Paritygame.node
 
+    (** Return the number of nodes in the game *)
+    val size : unit -> int
+
     val reset : unit -> unit
   end