diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml
index f490b22f3349f4c251e599e8e4334e2d6d8e632e..c87a7b1e76d3f9e25e223179001ebbae2146bcdb 100644
--- a/src/coalg/coalg.ml
+++ b/src/coalg/coalg.ml
@@ -167,6 +167,13 @@ let choiceNNF () =
       done
     with End_of_file -> ()
 
+let choiceGraph () =
+  choiceSat ();
+  print_endline "digraph reasonerstate {";
+  CM.graphIterCores (fun core -> print_endline (CM.coreToDot core));
+  CM.graphIterStates (fun state -> print_endline (CM.stateToDot state));
+  print_endline "}"
+
 let choiceVerify () =
     try
       while true do
@@ -177,7 +184,7 @@ let choiceVerify () =
           incr counter;
           print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
           flush stdout;
-		  CoAlgFormula.verifyFormula f;
+          CoAlgFormula.verifyFormula f;
         else ()
       done
     with End_of_file -> ()
@@ -213,7 +220,6 @@ let _ =
     | "prov" -> choiceProvable ()
     | "print" -> choicePrint ()
     | "nnf" -> choiceNNF ()
-	| "verify" -> choiceVerify ()
+    | "verify" -> choiceVerify ()
+    | "graph" -> choiceGraph ()
     | _ -> printUsage ()
-
-