diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 2245965b130230b944ba7bfd2cf54d5eb0a96166..0488e37ee5a2262012911677aea0eac88fb9daf7 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -440,15 +440,17 @@ let rec exportFormula_buffer sb f =
 	 Buffer.add_string sb "EG ";
 	 prio 4 f1
   | AU (f1, f2) ->
-	 Buffer.add_string sb "A ";
+	 Buffer.add_string sb "A (";
 	 prio 4 f1;
 	 Buffer.add_string sb " U ";
-	 prio 4 f2
+	 prio 4 f2;
+	 Buffer.add_string sb ")"
   | EU (f1, f2) ->
-	 Buffer.add_string sb "E ";
+	 Buffer.add_string sb "E (";
 	 prio 4 f1;
 	 Buffer.add_string sb " U ";
-	 prio 4 f2
+	 prio 4 f2;
+	 Buffer.add_string sb ")"
 
 (** Converts a formula into a string representation.
     Parentheses are ommited where possible
@@ -869,20 +871,18 @@ and parse_rest symtab ts =
 	  let f = parse_rest symtab ts in
 	  EG f
   | A.Kwd "A" ->
+	 assert (Stream.next ts = A.Kwd "(");
 	 let f1 = parse_rest symtab ts in
-	 let _ = match Stream.next ts with
-	   | A.Kwd "U" -> "U"
-	   | t -> A.printError mk_exn ~t ~ts "String \"U\" from CTL expected: "
-	 in
+	 assert (Stream.next ts = A.Kwd "U");
 	 let f2 = parse_rest symtab ts in
+	 assert (Stream.next ts = A.Kwd ")");
 	 AU (f1, f2)
   | A.Kwd "E" ->
+	 assert (Stream.next ts = A.Kwd "(");
 	 let f1 = parse_rest symtab ts in
-	 let _ = match Stream.next ts with
-	   | A.Kwd "U" -> "U"
-	   | t -> A.printError mk_exn ~t ~ts "String \"U\" from CTL expected: "
-	 in
+	 assert (Stream.next ts = A.Kwd "U");
 	 let f2 = parse_rest symtab ts in
+	 assert (Stream.next ts = A.Kwd ")");
 	 EU (f1, f2)
   | A.Kwd "AX" ->
 	 let f1 = parse_rest symtab ts in