diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index 36ade122dc3459e0d29761256335671b85e3b411..caa37aa4bce1354fdd41bc79c6d12f0015e2054f 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -172,10 +172,6 @@ let main () =
   if Options.Run.get () then begin
     change_printer ();
     ignore (generate_code (Options.Project_name.get ()));
-  end else
-  if Options.Check.get () then begin
-    Gmp_types.init ();
-    ignore (check ())
   end
 
 let () = Db.Main.extend main
diff --git a/src/plugins/e-acsl/src/options.ml b/src/plugins/e-acsl/src/options.ml
index 0723d4300b24f00392046a26748031d30690059a..8c98ca1657933ca519eef73fa5697877efa50842 100644
--- a/src/plugins/e-acsl/src/options.ml
+++ b/src/plugins/e-acsl/src/options.ml
@@ -31,13 +31,6 @@ module P = Plugin.Register
 module PP = P (* [PP] required to avoid an ocamldoc error in OCaml 4.02 *)
 include PP
 
-module Check =
-  False
-    (struct
-      let option_name = "-e-acsl-check"
-      let help = "only type check E-ACSL annotated program"
-    end)
-
 module Run =
   False
     (struct
diff --git a/src/plugins/e-acsl/src/options.mli b/src/plugins/e-acsl/src/options.mli
index d42a088cb71655a3afe6aa1b2e824112d79cf25d..d5065c6a51dbbade2b491b5cf91fea75d17e7f23 100644
--- a/src/plugins/e-acsl/src/options.mli
+++ b/src/plugins/e-acsl/src/options.mli
@@ -22,7 +22,6 @@
 
 include Plugin.S (** implementation of Log.S for E-ACSL *)
 
-module Check: Parameter_sig.Bool
 module Run: Parameter_sig.Bool
 module Valid: Parameter_sig.Bool
 module Gmp_only: Parameter_sig.Bool
diff --git a/src/plugins/e-acsl/src/project_initializer/keep_status.ml b/src/plugins/e-acsl/src/project_initializer/keep_status.ml
index 93580c24d45643672906c9b4a7616977d5179420..aa933b5f1a417c43b94d5cb68d8a19fb5330adc8 100644
--- a/src/plugins/e-acsl/src/project_initializer/keep_status.ml
+++ b/src/plugins/e-acsl/src/project_initializer/keep_status.ml
@@ -86,8 +86,7 @@ let option_check = ref false
 
 let clear () =
   Datatype.String.Hashtbl.clear keep_status;
-  option_valid := Options.Valid.get ();
-  option_check := Options.Check.get ()
+  option_valid := Options.Valid.get ()
 
 let push kf kind ppt =
   (*  Options.feedback "PUSHING %a for %a"