diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 286d38ebb200193d5d17ba87f68dae77a3723d28..b3d4452cdf81211dc1ecd1d278c5eb501db9e9f1 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -697,14 +697,10 @@ end
   let do_user_predicates () =
     let gannot a =
       match a with
-      | Dfun_or_pred (li,loc) ->
-        (match li.l_body with
-         | LBpred p ->
-           (match Logic_normalizer.get_pred p with
-            | PoT_pred p -> process_quantif ~loc p
-            | PoT_term _ -> ())
-         | _ -> ())
-
+      | Dfun_or_pred ({l_body = LBpred p},loc) ->
+        (match Logic_normalizer.get_pred p with
+         | PoT_pred p -> process_quantif ~loc p
+         | PoT_term _ -> ())
       | _ -> ()
     in
     Annotations.iter_global (fun _ a -> gannot a)
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 1bd660bab3fa20a03ddc1089c24aba73e75e7639..25f51fa0e06856e9ab56b15c1827dbc77f11c3f3 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -65,9 +65,10 @@ let handle_annotations env kf stmt =
            | Some (t, measure_opt) ->
              let env = Env.set_annotation_kind env Smart_stmt.Variant in
              let env = Env.push env in
-             let lenv = Env.Local_vars.get env in
-             Typing.type_term ~use_gmp_opt:true ~lenv t;
-             let ty = Typing.get_typ ~lenv t in
+             (* There cannot be bound logical variables since we cannot write
+                loops inside logic functions or predicates, hence lenv is []*)
+             Typing.type_term ~use_gmp_opt:true ~lenv:[] t;
+             let ty = Typing.get_typ ~lenv:[] t in
              if Gmp_types.is_t ty then Error.not_yet "loop variant using GMP";
              let e, _, env = !term_to_exp_ref ~adata:Assert.no_data kf env t in
              let vi_old, e_old, env =
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index a60a380c5f78a1a60597d0f6e6323aeabbd03d0b..f38b09429a3030ef331abb6d9f8db1f22cfc8c1e 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -1056,9 +1056,7 @@ and predicate_content_to_exp ~adata ?name kf env p =
   | Pvalid_function _ -> Env.not_yet env "\\valid_function"
   | Prel(rel, t1, t2) ->
     let ity =
-      Typing.get_integer_op_of_predicate
-        ~lenv
-        p
+      Typing.get_integer_op_of_predicate ~lenv p
     in
     comparison_to_exp ~adata ~loc kf env ity (relation_to_binop rel) t1 t2 None
   | Pand(p1, p2) ->