diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index a8d229ccf89ac13c5e8d90d99f48bbd33e889f80..36d851ebe14d4db402f2ffb40c6334915cc21d77 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -667,6 +667,9 @@ let rec verifyMuAltFree formula =
 	 else
 	   ("ν", newfree)
   | VAR s -> ("none", [s])
+  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ ->
+	 raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point"))
+
 
 (** Process from outside in. For every variable bound keep the tuple
     (name, negations). For every negation crossed map a +1 over snd on
@@ -703,6 +706,8 @@ let rec verifyMuMonotone negations formula =
 	 let increment (s, n) = (s, n+1) in
 	 let newNeg = List.map increment negations in
 	 verifyMuMonotone newNeg a
+  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ ->
+	 raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point"))
 
 let rec verifyMuGuarded unguarded formula =
   let proc = verifyMuGuarded unguarded in
@@ -730,6 +735,8 @@ let rec verifyMuGuarded unguarded formula =
 	 let finder x = compare x s == 0 in
 	 if List.exists finder unguarded then
 	   raise (CoAlgException ("formula not guarded"))
+  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ ->
+	 raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
 
 let verifyFormula formula =
   verifyMuAltFree formula;