diff --git a/infer/lib/linter_rules/linters.al b/infer/lib/linter_rules/linters.al
index b01eecff6..9d4d0cbaa 100644
--- a/infer/lib/linter_rules/linters.al
+++ b/infer/lib/linter_rules/linters.al
@@ -202,21 +202,20 @@ DEFINE-CHECKER CXX_REFERENCE_CAPTURED_IN_OBJC_BLOCK = {
 
 	};
 
-//
-// ** Commented for the moment. We use the hardcoded version
-//
-//	DEFINE-CHECKER ctl_unavailable_api_in_supported_ios_sdk_error = {
-//		  SET report_when =
-//			     WHEN
-//					    WITH-TRANSITION PointerToDecl
-//                (decl_unavailable_in_supported_ios_sdk AND NOT within_responds_to_selector_block)
-//	         HOLDS-IN-NODE DeclRefExpr, ObjCMessageExpr;
-//
-//		  SET message =
-//		        "%decl_ref_or_selector_name% is available only starting \
-//		         from ios sdk %available_ios_sdk% but we support earlier versions from \
-//		         ios sdk %iphoneos_target_sdk_version%;
-//
-//		  SET suggestion = "This could cause a crash.";
-//
-//		};
+	// If the declaration has availability attributes, check that it's compatible with
+	// the iphoneos_target_sdk_version
+	DEFINE-CHECKER UNAVAILABLE_API_IN_SUPPORTED_IOS_SDK = {
+
+		SET report_when =
+		     WHEN HOLDS-NEXT WITH-TRANSITION PointerToDecl
+	 				 (decl_unavailable_in_supported_ios_sdk() AND
+	 				 NOT within_responds_to_selector_block())
+				 HOLDS-IN-NODE DeclRefExpr, ObjCMessageExpr;
+
+		  SET message =
+		        "%decl_ref_or_selector_name% is not available in the required iOS SDK version
+		         %iphoneos_target_sdk_version% (only available from version %available_ios_sdk%)";
+
+		  SET suggestion = "This could cause a crash.";
+			SET severity = "ERROR";
+		};
diff --git a/infer/src/clang/cFrontend_checkers.ml b/infer/src/clang/cFrontend_checkers.ml
index 53b44d0ce..1b4bfaf79 100644
--- a/infer/src/clang/cFrontend_checkers.ml
+++ b/infer/src/clang/cFrontend_checkers.ml
@@ -97,25 +97,3 @@ let cxx_ref_captured_in_block an =
   let var_desc vars var_named_decl_info =
     vars ^ "'" ^ var_named_decl_info.Clang_ast_t.ni_name ^ "'" in
   IList.fold_left var_desc "" capt_refs
-
-(** If the declaration has avilability attributes, check that it's compatible with
-    the iphoneos_target_sdk_version *)
-let ctl_unavailable_api_in_supported_ios_sdk_error lctx an =
-  let open CTL in
-  let condition =
-    InNode(["DeclRefExpr"; "ObjCMessageExpr"],
-           EX (Some PointerToDecl, (
-               And
-                 (Atomic ("decl_unavailable_in_supported_ios_sdk", []),
-                  Not (Atomic ("within_responds_to_selector_block", [])))))) in
-  let issue_desc =
-    { CIssue.name = "UNAVAILABLE_API_IN_SUPPORTED_IOS_SDK";
-      severity = Exceptions.Kerror;
-      mode = CIssue.On;
-      description =
-        "%decl_ref_or_selector_name% is not available in the required iOS SDK version \
-         %iphoneos_target_sdk_version% (only available from version %available_ios_sdk%)";
-      suggestion = Some "This could cause a crash.";
-      loc = location_from_an lctx an
-    } in
-  condition, Some issue_desc
diff --git a/infer/src/clang/cFrontend_checkers.mli b/infer/src/clang/cFrontend_checkers.mli
index 3b76610f2..d2247e148 100644
--- a/infer/src/clang/cFrontend_checkers.mli
+++ b/infer/src/clang/cFrontend_checkers.mli
@@ -9,9 +9,6 @@
 
 open! IStd
 
-val ctl_unavailable_api_in_supported_ios_sdk_error :
-  CLintersContext.context -> CTL.ast_node -> CTL.t * CIssue.issue_desc option
-
 val location_from_stmt :
   CLintersContext.context -> Clang_ast_t.stmt -> Location.t
 
diff --git a/infer/src/clang/cFrontend_errors.ml b/infer/src/clang/cFrontend_errors.ml
index da21f0707..0a7163c5d 100644
--- a/infer/src/clang/cFrontend_errors.ml
+++ b/infer/src/clang/cFrontend_errors.ml
@@ -30,8 +30,7 @@ let decl_checkers_list =
 (* List of checkers on stmts *that return 0 or 1 issue* *)
 let stmt_single_checkers_list =
   [ComponentKit.component_file_cyclomatic_complexity_info;
-   ComponentKit.component_initializer_with_side_effects_advice;
-   CFrontend_checkers.ctl_unavailable_api_in_supported_ios_sdk_error;]
+   ComponentKit.component_initializer_with_side_effects_advice;]
 
 let stmt_checkers_list = IList.map single_to_multi stmt_single_checkers_list
 
diff --git a/infer/src/clang/ctl_parser.mly b/infer/src/clang/ctl_parser.mly
index b9327d5af..d8a4216d7 100644
--- a/infer/src/clang/ctl_parser.mly
+++ b/infer/src/clang/ctl_parser.mly
@@ -108,6 +108,7 @@ transition_label:
                   | "Body" | "body" -> Some CTL.Body
                   | "InitExpr" | "initexpr" -> Some CTL.InitExpr
                   | "Cond" | "cond" -> Some CTL.Cond
+                  | "PointerToDecl" | "pointertodecl" -> Some CTL.PointerToDecl
                   | _  -> None }
   ;
 
@@ -115,8 +116,12 @@ formula_EF:
  | LEFT_PAREN formula RIGHT_PAREN EF { $2 }
 ;
 
+formula_with_paren:
+ | LEFT_PAREN formula RIGHT_PAREN { $2 }
+;
+
 formula:
-  | LEFT_PAREN formula RIGHT_PAREN { $2 }
+  | formula_with_paren { $1 }
   | formula_id { $1 }
   | atomic_formula { Logging.out "\tParsed atomic formula\n"; $1 }
   | formula EU formula { Logging.out "\tParsed EU\n"; CTL.EU (None, $1, $3) }
@@ -134,6 +139,8 @@ formula:
      { Logging.out "\tParsed ET\n"; CTL.ET ($2, $4, $5)}
   | ETX params WITH_TRANSITION transition_label formula_EF
         { Logging.out "\tParsed ETX\n"; CTL.ETX ($2, $4, $5)}
+  | EX WITH_TRANSITION transition_label formula_with_paren
+    { Logging.out "\tParsed EX\n"; CTL.EX ($3, $4)}
   | formula AND formula { Logging.out "\tParsed AND\n"; CTL.And ($1, $3) }
   | formula OR formula { Logging.out "\tParsed OR\n"; CTL.Or ($1, $3) }
   | formula IMPLIES formula { Logging.out "\tParsed IMPLIES\n"; CTL.Implies ($1, $3) }