diff --git a/src/plugins/e-acsl/mpz.ml b/src/plugins/e-acsl/mpz.ml
index 29cb7ad11a1d6f1ceee3ef76e7291b5955654162..6f1b0854831c1818872951e3223a569bc815e0bd 100644
--- a/src/plugins/e-acsl/mpz.ml
+++ b/src/plugins/e-acsl/mpz.ml
@@ -47,7 +47,9 @@ let get_set_suffix_and_arg e =
   else
     match Cil.unrollType ty with
     | TInt(IChar, _) -> 
-      (if Cil.theMachine.Cil.char_is_unsigned then "_ui" else "_si"), [ e ]
+      (if Cil.theMachine.Cil.theMachine.char_is_unsigned then "_ui" 
+       else "_si"), 
+      [ e ]
     | TInt((IBool | IUChar | IUInt | IUShort | IULong), _) ->
       "_ui", [ e ]
     | TInt((ISChar | IShort | IInt | ILong), _) -> "_si", [ e ]
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 02f7eab91640cbeaf08daaa5e5b671752ea5f2cb..00fd5d7a686e1c32d0b214a7e40b24f807137489 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -41,11 +41,18 @@ let init_mpz () =
 (* ********************************************************************** *)
 
 let get_rte_by_stmt =
-  Dynamic.get
-    ~plugin:"RteGen"
-    "stmt_annotations"
-    (Datatype.func2 Kernel_function.ty Stmt.ty 
-       (let module L = Datatype.List(Code_annotation) in L.ty))
+  try
+    Dynamic.get
+      ~plugin:"RteGen"
+      "stmt_annotations"
+      (Datatype.func2 Kernel_function.ty Stmt.ty 
+	 (let module L = Datatype.List(Code_annotation) in L.ty))
+  with Failure _ | Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ as exn
+    ->
+    Options.warning "@[@[cannot run RTE:@ %s.@]@ \
+Ignoring potential runtime errors in annotations." 
+      (Printexc.to_string exn);
+    fun _ _ -> []
 
 module Env: sig
   val default_varinfos: Varinfo.Set.t option -> Varinfo.Set.t
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index aa6a48ae26ed96157ad7da9439d4ddcc8892a8bc..195ec761fbc852f58b598938483a5bfe882a0728 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -632,11 +632,19 @@ let assumes_predicate bhv =
     bhv.b_assumes
 
 let get_rte =
-  Dynamic.get
-    ~plugin:"RteGen"
-    "exp_annotations"
-    (Datatype.func3 Kernel_function.ty Stmt.ty Exp.ty 
-       (let module L = Datatype.List(Code_annotation) in L.ty))
+  try
+    Dynamic.get
+      ~plugin:"RteGen"
+      "exp_annotations"
+      (Datatype.func3 Kernel_function.ty Stmt.ty Exp.ty 
+	 (let module L = Datatype.List(Code_annotation) in L.ty))
+  with Failure _ | Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ as exn
+    ->
+      Options.warning "@[@[cannot run RTE:@ %s.@]@ \
+Ignoring potential runtime errors in annotations." 
+	(Printexc.to_string exn);
+      fun _ _ _ -> []
+  
 
 let rec translate_named_predicate kf _kinstr ?(rte=true) env p =
   Typing.type_named_predicate ~must_clear:rte p;
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index cb45ff778359d53af271ebf2a3dc94487b33adc2..d2f2739c8a4c044aa6f2ba6ea243bdfb79930311 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -213,7 +213,7 @@ let size_of ty =
   try int_to_interv (Cil.sizeOf_int ty)
   with Cil.SizeOfError _ -> eacsl_typ_of_typ Cil.ulongLongType
 
-let align_of ty = int_to_interv (Cil.alignOf_int ty)
+let align_of ty = int_to_interv (Cil.bytesAlignOf ty)
 
 type offset_ty = Ty_no_offset | Ty_field of eacsl_typ | Ty_index of eacsl_typ
 
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 713538f476ee975ffaf840ce61cf22c957cc67c1..f13f4f84f429771c9ea9fc1773f5cd2d82e2f150 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -24,11 +24,14 @@ open Cil_types
 open Cil_datatype
 
 let get_rte_by_stmt =
-  Dynamic.get
-    ~plugin:"RteGen"
-    "stmt_annotations"
-    (Datatype.func2 Kernel_function.ty Stmt.ty 
-       (let module L = Datatype.List(Code_annotation) in L.ty))
+  try
+    Dynamic.get
+      ~plugin:"RteGen"
+      "stmt_annotations"
+      (Datatype.func2 Kernel_function.ty Stmt.ty 
+	 (let module L = Datatype.List(Code_annotation) in L.ty))
+  with _ ->
+    fun _ _ -> []
 
 (* move all labels of [stmt] onto [new_stmt] *)
 let move_labels env stmt new_stmt =