diff --git a/coalgcompare.ml b/coalgcompare.ml
index b05055cd7f6a4b55e0cd089b1e03f3d45ef9dac5..b182e9205f5194c6b48f88aac0f4963489ce0675 100644
--- a/coalgcompare.ml
+++ b/coalgcompare.ml
@@ -112,6 +112,10 @@ let rec exportALCFormula f =
   | C.IMP (f1, f2) -> A.IMP (exportALCFormula f1, exportALCFormula f2)
   | C.EX (s, f1) -> A.EX (s, false, exportALCFormula f1)
   | C.AX (s, f1) -> A.AX (s, false, exportALCFormula f1)
+  | C.MIN (n, s, f1) -> A.MIN (n, s, false, exportALCFormula f1)
+  | C.MAX (n, s, f1) -> A.MAX (n, s, false, exportALCFormula f1)
+  | C.MORETHAN (n, s, f1) -> A.MIN (n+1, s, false, exportALCFormula f1)
+  | C.MAXEXCEPT (n, s, f1) -> A.MAX (n, s, false, exportALCFormula (C.NOT f1))
   | _ -> raise (C.CoAlgException "Formula is not expressible in ALC.")
 
 let exportALCQuery tbox (_, f) =
@@ -227,7 +231,7 @@ let doTestK (tboxsizes:int list) (szlist:int list) : testresults =
   runTests solvs formulas timeout
 
 let doTestGenericGML () : testresults =
-  let solvs = [(solvFact, "fact"); (solvCool "K", "cool")] in
+  let solvs = [(solvFact, "fact"); (solvCool "GML", "cool")] in
   let timeout = !ptimeout in (* 5 minutes *)
   let formulas = ref [] in
   let counter = ref 0 in