Clear environment.

src/plugins/e-acsl/interval.ml

@@ -60,6 +60,7 @@ module Env = struct
   let tbl: Ival.t Logic_var.Hashtbl.t = Logic_var.Hashtbl.create 7
   let clear () = Logic_var.Hashtbl.clear tbl
   let add = Logic_var.Hashtbl.add tbl
+  let remove = Logic_var.Hashtbl.remove tbl
   let find = Logic_var.Hashtbl.find tbl
 end
 
@@ -193,9 +194,12 @@ let rec infer t =
 
   | Tlet (li,t) ->
     let li_t = Misc.term_of_li li in
+    let li_v = li.l_var_info in
     let i = infer li_t in
-    Env.add li.l_var_info i;
-    infer t
+    Env.add li_v i;
+    let i = infer t in
+    Env.remove li_v;
+    i
   | TConst (LStr _ | LWStr _ | LReal _)
   | TBinOp (PlusPI,_,_)
   | TBinOp (IndexPI,_,_)

src/plugins/e-acsl/interval.mli

@@ -65,6 +65,7 @@ val interv_of_typ: Cil_types.typ -> Ival.t
 module Env: sig
   val clear: unit -> unit
   val add: Cil_types.logic_var -> Ival.t -> unit
+  val remove: Cil_types.logic_var -> unit
 end
 
 (* ************************************************************************** *)

src/plugins/e-acsl/translate.ml

@@ -501,6 +501,7 @@ and context_insensitive_term_to_exp kf env t =
   | Tlet(li, t) ->
     let env = env_of_li li kf env loc in
     let e, env = term_to_exp kf env t in
+    Interval.Env.remove li.l_var_info;
     e, env, false, ""
 
 (* Convert an ACSL term into a corresponding C expression (if any) in the given
@@ -735,7 +736,9 @@ and named_predicate_content_to_exp ?name kf env p =
     conditional_to_exp loc None e1 res2 res3
   | Plet(li, p) ->
     let env = env_of_li li kf env loc in
-    named_predicate_to_exp kf env p
+    let e, env = named_predicate_to_exp kf env p in
+    Interval.Env.remove li.l_var_info;
+    e, env
   | Pforall _ | Pexists _ -> Quantif.quantif_to_exp kf env p
   | Pat(p, BuiltinLabel Here) ->
     named_predicate_to_exp kf env p