diff --git a/examples/exception.ec b/examples/exception.ec
new file mode 100644
index 000000000..9ca2bd21e
--- /dev/null
+++ b/examples/exception.ec
@@ -0,0 +1,162 @@
+require import AllCore.
+
+exception assume.
+exception assert.
+
+op p1: int -> bool.
+op p2: int -> bool.
+
+module M' ={
+  proc truc (x:int) : int = {
+  raise (! p1 x \/ ! p2 x) assume;
+  if (!p1 x \/ !p2 x) { raise assert;}
+  return x;
+  }
+}.
+
+print M'.
+
+lemma assume_assert  (_x:int):
+hoare [M'.truc : _x = x ==> false | assume:p1 _x | assert: !(p1 _x /\ p2 _x)].
+    proof.
+      proc.
+      wp.
+      auto => &hr <- />. smt.
+     qed.
+
+lemma assert_assume (_x:int):
+hoare [M'.truc : _x = x ==> false | assume:p2 _x | assert: !(p2 _x /\ p1 _x) ].
+    proof.
+      proc.
+      wp.
+      auto => &hr <- />. smt.
+     qed.
+
+lemma assert_assume' ( _x:int)  :
+hoare [M'.truc : _x = x ==> false | assume: p1 _x /\ p2 _x | assert: !(p2 _x /\ p1 _x) ].
+    proof.
+      conseq (assume_assert _x) (assert_assume _x).
+      + auto.
+      + auto.
+    qed.
+
+exception e1.
+exception e2.
+exception e3.
+
+module M ={
+  proc f1 (x:int) : int = {
+    raise (x <> 3) e1;
+    x <- 5;
+    return x;
+  }
+
+ proc f2 (x:int) : int = {
+    if (x = 3)  {
+      x <- x;
+      x <@ f1(x);
+    } else {
+      x <@ f1(x);
+    }
+    return x;
+  }
+}.
+
+op pe: bool.
+op pe1: bool.
+op pe2: bool.
+op pe3: bool.
+op pe4: bool.
+op pd1: bool.
+op pd2: bool.
+op pd3: bool.
+
+axiom a1: pd2 => pd1.
+axiom a2: pe => pd1.
+axiom a3: pd2 => pe3.
+axiom a4: pd2 => pe4.
+axiom a5: pd1 => pd2.
+
+lemma l_f1 (_x: int):
+hoare [M.f1 : _x = x ==> (res <= 5) | e1:_x <= 3 | pd1].
+    proof.
+      proc.
+       conseq (: _ ==> x = 5 | e1: _x = 3 | e2: pe | pd2).
+      + move => &hr h x. smt.
+      + wp. auto.
+    qed.
+
+lemma l_f2 (_x: int):
+hoare [M.f2 : _x = x ==> res < 6 | e1: _x < 4 | e2:pe3 | e3: pe4 | pd2 ].
+    proof.
+      proc.
+      if.
+      + call (: _x = x ==> res = 5 | e1 : 3 = _x | e2: pd2 | pd2).
+       + proc.
+         wp. auto.
+      wp. auto. smt.
+      call (l_f1 _x).
+      auto. smt.
+  qed.
+
+module M1 ={
+    var i:int
+
+  proc f1 (x:int) : int = {
+    i <- 0;
+    raise e2;
+    return x;
+  }
+
+ proc f2 (x:int) : int = {
+      i <- 1;
+      x <@ f1(x);
+      return x;
+  }
+}.
+
+lemma test (_x: int):
+hoare [M1.f2 : true ==> true |e2: M1.i = 0].
+ proof.
+   proc.
+   call (: true ==> true | e2 : M1.i = 0).
+   + proc. wp. auto.
+   auto.
+qed.
+
+lemma test2 (_x: int):
+hoare [M1.f1 : true ==> true |e2: M1.i = 0].
+    proof.
+      proc.
+      conseq (: _ ==> _ |  e2: M1.i = 0).
+      auto.
+qed.
+
+module M2 ={
+
+  proc f1 (x:int) : int = {
+
+    return x;
+  }
+
+  proc f2 (x:int) : int = {
+    x <- x + 1;
+    x <@ f1(x);
+    return x;
+  }
+}.
+
+lemma test3 (_x: int):
+hoare [M2.f1 : _x = x ==> res = _x | e2 : _x = 0].
+proof.
+  proc.
+  auto.
+qed.
+
+lemma test4 (_x: int):
+hoare [M2.f2 : _x = x ==> res = _x + 1 | e2 : _x + 1= 0 ].
+ proof.
+   proc.
+   ecall(test3 x).
+   auto.
+qed.
diff --git a/src/ecAst.ml b/src/ecAst.ml
index aa9b6011a..0705e34e3 100644
--- a/src/ecAst.ml
+++ b/src/ecAst.ml
@@ -4,6 +4,7 @@ open EcSymbols
 open EcIdent
 open EcPath
 open EcUid
+open EcMaps
 
 module BI = EcBigInt
 
@@ -115,7 +116,7 @@ and instr_node =
   | Sif       of expr * stmt * stmt
   | Swhile    of expr * stmt
   | Smatch    of expr * ((EcIdent.t * ty) list * stmt) list
-  | Sassert   of expr
+  | Sraise    of EcPath.path
   | Sabstract of EcIdent.t
 
 and stmt = {
@@ -234,19 +235,21 @@ and equivS = {
   es_sr  : stmt;
   es_po  : form; }
 
+and post = (form * (EcPath.path, form) DMap.t * form option)
+
 and sHoareF = {
   hf_m  : memory;
   hf_pr : form;
   hf_f  : EcPath.xpath;
-  hf_po : form;
+  hf_po : post;
 }
 
 and sHoareS = {
   hs_m  : memenv;
   hs_pr : form;
   hs_s  : stmt;
-  hs_po : form; }
-
+  hs_po : post;
+}
 
 and eHoareF = {
   ehf_m   : memory;
@@ -462,19 +465,27 @@ let ts_inv_lower_right3 (fn: ss_inv -> ss_inv -> ss_inv -> form)
 
 (* ----------------------------------------------------------------- *)
 
+type hs_inv = {
+  hsi_m : memory;
+  hsi_inv : post;
+}
+
 type inv =
   | Inv_ss of ss_inv
   | Inv_ts of ts_inv
+  | Inv_hs of hs_inv
 
 let inv_of_inv (inv: inv) : form =
   match inv with
   | Inv_ss ss -> ss.inv
   | Inv_ts ts -> ts.inv
+  | _ -> failwith "expected single or two sided invarinat"
 
 let lift_ss_inv (f: ss_inv -> 'a) : inv -> 'a =
   let f inv = match inv with
   | Inv_ss ss -> f ss
-  | Inv_ts _ -> failwith "expected single sided invariant" in
+  | _ -> failwith "expected single sided invariant"
+  in
   f
 
 let lift_ss_inv2 (f: ss_inv -> ss_inv -> 'a) : inv -> inv -> 'a =
@@ -483,6 +494,13 @@ let lift_ss_inv2 (f: ss_inv -> ss_inv -> 'a) : inv -> inv -> 'a =
   | _ -> failwith "expected only single sided invariants" in
   f
 
+let lift_hs_ss_inv (f: ss_inv -> hs_inv -> 'a) : inv -> inv -> 'a =
+  let f inv1 inv2 = match inv1, inv2 with
+  | Inv_ss ss1, Inv_hs ss2 -> f ss1 ss2
+  | _ -> failwith "expected only single sided invariants" in
+  f
+
+
 let lift_ss_inv3 (f: ss_inv -> ss_inv -> ss_inv -> 'a) : inv -> inv -> inv -> 'a =
   let f inv1 inv2 inv3 = match inv1, inv2, inv3 with
   | Inv_ss ss1, Inv_ss ss2, Inv_ss ss3 -> f ss1 ss2 ss3
@@ -492,7 +510,7 @@ let lift_ss_inv3 (f: ss_inv -> ss_inv -> ss_inv -> 'a) : inv -> inv -> inv -> 'a
 let lift_ts_inv (f: ts_inv -> 'a) : inv -> 'a =
   let f inv = match inv with
   | Inv_ts ss -> f ss
-  | Inv_ss _ -> failwith "expected two sided invariant" in
+  |  _ -> failwith "expected two sided invariant" in
   f
 
 let lift_ts_inv2 (f: ts_inv -> ts_inv -> 'a) : inv -> inv -> 'a =
@@ -512,20 +530,22 @@ let map_inv (fn: form list -> form) (inv: inv list): inv =
   assert (List.length inv > 0);
   match List.hd inv with
   | Inv_ss ss' ->
-      Inv_ss (map_ss_inv fn (List.map (function 
+      Inv_ss (map_ss_inv fn (List.map (function
         Inv_ss ss -> assert (ss.m = ss'.m); ss
         | _ -> failwith "expected all invariants to have same kind") inv))
   | Inv_ts ts' ->
-      Inv_ts (map_ts_inv fn (List.map (function 
+      Inv_ts (map_ts_inv fn (List.map (function
         Inv_ts ts -> assert (ts.ml = ts'.ml && ts.mr = ts'.mr); ts
         | _ -> failwith "expected all invariants to have same kind") inv))
+  | _ ->  failwith  "Patch Inv_hs"
 
 let map_inv1 (fn: form -> form) (inv: inv): inv =
   match inv with
   | Inv_ss ss ->
       Inv_ss (map_ss_inv1 fn ss)
   | Inv_ts ts ->
-      Inv_ts (map_ts_inv1 fn ts)
+    Inv_ts (map_ts_inv1 fn ts)
+  | _ -> failwith  "Patch Inv_hs2"
 
 let map_inv2 (fn: form -> form -> form) (inv1: inv) (inv2: inv): inv =
   match inv1, inv2 with
@@ -546,6 +566,88 @@ let map_inv3 (fn: form -> form -> form -> form)
   | _ ->
       failwith "incompatible invariants for map_inv3"
 
+(* ----------------------------------------------------------------- *)
+let empty_poe f = (f, DMap.empty, None)
+
+let empty_hs f =
+  {hsi_m=f.m;hsi_inv = empty_poe f.inv}
+
+let is_empty_poe poe =
+  match poe with
+  | (_,m,None) when DMap.is_empty m-> true
+  | _ -> false
+
+let lift_f f = {hsi_m=f.m;hsi_inv=empty_poe f.inv}
+
+let lower_f f =
+  let (post, _,_) = f.hsi_inv in
+  {m=f.hsi_m;inv=post}
+
+let update_hs_ss f p =
+  assert (f.m == p.hsi_m);
+  let (_,m,d) = p.hsi_inv in
+  {hsi_m = f.m; hsi_inv=(f.inv,m,d)}
+
+let map_poe f (p,m,d) =
+  let p = f p in
+  let m = DMap.map f m in
+  let d = omap f d in
+  (p, m, d)
+
+let map_hs_inv1 f inv1 =  {inv1 with hsi_inv = map_poe f inv1.hsi_inv}
+
+let map2_poe f (p1,m1,d1) (p2,m2,d2) =
+  let p = f p1 p2 in
+  let aux _ a b =
+    match a, b with
+    | Some a, Some b -> Some (f a b)
+    | _ , _ -> failwith "missing entry in exception map"
+  in
+  let m = DMap.merge aux m1 m2 in
+  match d2, d1 with
+  | None, None -> (p, m, None)
+  | Some d2, Some d1 -> (p, m, Some (f d2 d1))
+  | _, _ -> failwith "missing default exception"
+
+let map_hs_inv2
+    (fn: form -> form -> form) (inv1: hs_inv) (inv2: hs_inv): hs_inv =
+  assert (inv1.hsi_m = inv2.hsi_m);
+  let inv' = map2_poe fn inv1.hsi_inv inv2.hsi_inv in
+  { hsi_m = inv1.hsi_m; hsi_inv = inv' }
+
+let exists_poe f (p,m,d) =
+  f p || DMap.exists (fun _ -> f) m || omap_dfl f false d
+
+let forall_poe f (p,m,d) =
+  f p && DMap.for_all (fun _ -> f) m && omap_dfl f true d
+
+let forall2_poe f (p1,m1,d1) (p2,m2,d2) =
+  let b1 = f p1 p2 in
+  let b2 = DMap.equal f m1 m2 in
+  b1 && b2 && oeq f d1 d2
+
+let poe_to_list (post,poe,d) =
+  let l =
+    DMap.fold
+      (fun p1 a -> p1 :: a)
+      poe
+      [post]
+  in
+  otolist d @ l
+
+let iter_poe f (p, m,d) =
+  f p;
+  DMap.iter (fun _ -> f) m;
+  oiter f d
+
+let iter2_poe f (p1,m1,d1) (p2,m2,d2) =
+  f p1 p2;
+  DMap.iter (fun e1 p1 -> f (DMap.find e1 m2) p1) m1;
+  match d2, d1 with
+  | None, None -> ()
+  | Some d2, Some d1 -> f d2 d1
+  | _, _ -> failwith "missing default exception"
+
 (* ----------------------------------------------------------------- *)
 (* Accessors for program logic                                       *)
 (* ----------------------------------------------------------------- *)
@@ -559,11 +661,11 @@ let ef_po ef = {ml=ef.ef_ml; mr=ef.ef_mr; inv=ef.ef_po}
 let es_pr es = {ml=fst es.es_ml; mr=fst es.es_mr; inv=es.es_pr}
 let es_po es = {ml=fst es.es_ml; mr=fst es.es_mr; inv=es.es_po}
 
-let hf_pr hf = {m=hf.hf_m; inv=hf.hf_pr}
-let hf_po hf = {m=hf.hf_m; inv=hf.hf_po}
+let hf_pr hf =  {m=hf.hf_m; inv=hf.hf_pr}
+let hf_po hf =  {hsi_m=hf.hf_m; hsi_inv=hf.hf_po}
 
 let hs_pr hs = {m=fst hs.hs_m; inv=hs.hs_pr}
-let hs_po hs = {m=fst hs.hs_m; inv=hs.hs_po}
+let hs_po hs = {hsi_m=fst hs.hs_m; hsi_inv=hs.hs_po}
 
 let ehf_pr ehf = {m=ehf.ehf_m; inv=ehf.ehf_pr}
 let ehf_po ehf = {m=ehf.ehf_m; inv=ehf.ehf_po}
@@ -916,15 +1018,27 @@ let b_hash (bs : bindings) =
     Why3.Hashcons.combine_list b1_hash 0 bs
 
 (*-------------------------------------------------------------------- *)
+
+let posts_equal (post1, eposts1, d1) (post2, eposts2, d2) =
+  let b = f_equal post1 post2 in
+  let b =  b && DMap.equal f_equal eposts1 eposts2 in
+  b &&
+  match d1, d2 with
+  | Some f1, Some f2 -> f_equal f1 f2
+  | None, None -> true
+  | _, _ -> false
+
+(*-------------------------------------------------------------------- *)
+
 let hf_equal hf1 hf2 =
      f_equal hf1.hf_pr hf2.hf_pr
-  && f_equal hf1.hf_po hf2.hf_po
+  && posts_equal hf1.hf_po hf2.hf_po
   && EcPath.x_equal hf1.hf_f hf2.hf_f
   && mem_equal hf1.hf_m hf2.hf_m
 
 let hs_equal hs1 hs2 =
      f_equal hs1.hs_pr hs2.hs_pr
-  && f_equal hs1.hs_po hs2.hs_po
+  && posts_equal hs1.hs_po hs2.hs_po
   && s_equal hs1.hs_s hs2.hs_s
   && me_equal hs1.hs_m hs2.hs_m
 
@@ -989,14 +1103,28 @@ let pr_equal pr1 pr2 =
   && f_equal          pr1.pr_args pr2.pr_args
   && mem_equal        pr1.pr_event.m pr2.pr_event.m
 
+(*-------------------------------------------------------------------- *)
+
+let post_hash e f = Why3.Hashcons.combine (EcPath.p_hash e) (f_hash f)
+
+let posts_hash (post, posts,d) =
+  let h = Why3.Hashcons.combine (f_hash post) (omap_dfl f_hash 0 d) in
+  DMap.foldi
+    (fun e f a -> Why3.Hashcons.combine a (post_hash e f))
+    posts h
+
 (* -------------------------------------------------------------------- *)
 let hf_hash hf =
   Why3.Hashcons.combine3
-    (f_hash hf.hf_pr) (f_hash hf.hf_po) (EcPath.x_hash hf.hf_f) (mem_hash hf.hf_m)
+  (f_hash hf.hf_pr)
+  (posts_hash hf.hf_po)
+  (EcPath.x_hash hf.hf_f)
+  (mem_hash hf.hf_m)
 
 let hs_hash hs =
   Why3.Hashcons.combine3
-    (f_hash hs.hs_pr) (f_hash hs.hs_po)
+    (f_hash hs.hs_pr)
+    (posts_hash hs.hs_po)
     (s_hash hs.hs_s)
     (me_hash hs.hs_m)
 
@@ -1344,6 +1472,13 @@ module Hsform = Why3.Hashcons.Make (struct
 
   let fv_mlr ml mr = Sid.add ml (Sid.singleton mr)
 
+  let posts_fv (post, posts, d) =
+    let fv = f_fv post in
+    let fv = d |> omap f_fv |> odfl fv in
+    DMap.fold
+      (fun f acc -> fv_union (f_fv f) acc)
+       posts fv
+
   let fv_node f =
     let union ex nodes =
       List.fold_left (fun s a -> fv_union s (ex a)) Mid.empty nodes
@@ -1371,11 +1506,11 @@ module Hsform = Why3.Hashcons.Make (struct
       fv_union (f_fv f1) fv2
 
     | FhoareF hf ->
-      let fv = fv_union (f_fv hf.hf_pr) (f_fv hf.hf_po) in
+      let fv = fv_union (f_fv hf.hf_pr) (posts_fv hf.hf_po) in
       EcPath.x_fv (Mid.remove hf.hf_m fv) hf.hf_f
 
     | FhoareS hs ->
-      let fv = fv_union (f_fv hs.hs_pr) (f_fv hs.hs_po) in
+      let fv = fv_union (f_fv hs.hs_pr) (posts_fv hs.hs_po) in
       fv_union (s_fv hs.hs_s) (Mid.remove (fst hs.hs_m) fv)
 
     | FeHoareF hf ->
@@ -1470,8 +1605,7 @@ module Hinstr = Why3.Hashcons.Make (struct
           in List.all2 forbs bs1 bs2 && s_equal s1 s2
         in e_equal e1 e2 && List.all2 forb b1 b2
 
-    | Sassert e1, Sassert e2 ->
-        (e_equal e1 e2)
+    | Sraise e1, Sraise e2 -> EcPath.p_equal e1 e2
 
     | Sabstract id1, Sabstract id2 -> EcIdent.id_equal id1 id2
 
@@ -1509,7 +1643,7 @@ module Hinstr = Why3.Hashcons.Make (struct
           in Why3.Hashcons.combine_list forbs (s_hash s) bds
         in Why3.Hashcons.combine_list forb (e_hash e) b
 
-    | Sassert e -> e_hash e
+    | Sraise e -> EcPath.p_hash e
 
     | Sabstract id -> EcIdent.id_hash id
 
@@ -1543,8 +1677,7 @@ module Hinstr = Why3.Hashcons.Make (struct
              (fun s b -> EcIdent.fv_union s (forb b))
              (e_fv e) b
 
-    | Sassert e    ->
-        e_fv e
+    | Sraise _ -> Mid.empty
 
     | Sabstract id ->
         EcIdent.fv_singleton id
diff --git a/src/ecAst.mli b/src/ecAst.mli
index 6da2cff79..90e9b1147 100644
--- a/src/ecAst.mli
+++ b/src/ecAst.mli
@@ -2,6 +2,7 @@
 open EcSymbols
 open EcIdent
 open EcPath
+open EcMaps
 
 module BI = EcBigInt
 
@@ -111,7 +112,7 @@ and instr_node =
   | Sif       of expr * stmt * stmt
   | Swhile    of expr * stmt
   | Smatch    of expr * ((EcIdent.t * ty) list * stmt) list
-  | Sassert   of expr
+  | Sraise    of EcPath.path
   | Sabstract of EcIdent.t
 
 and stmt = private {
@@ -239,13 +240,15 @@ and equivS = {
   [@alert priv_pl "Use the accessor function `es_po` instead of the field"]
 }
 
+and post = (form * (EcPath.path, form) DMap.t * form option)
+
 and sHoareF = {
   hf_m : memory;
   hf_pr : form;
   [@alert priv_pl "Use the accessor function `hf_pr` instead of the field"]
   hf_f  : EcPath.xpath;
-  hf_po : form;
-  [@alert priv_pl "Use the accessor function `hf_pr` instead of the field"]
+  hf_po : post;
+  [@alert priv_pl "Use the accessor function `hf_po` instead of the field"]
 }
 
 and sHoareS = {
@@ -253,7 +256,7 @@ and sHoareS = {
   hs_pr : form;
   [@alert priv_pl "Use the accessor function `hs_pr` instead of the field"]
   hs_s  : stmt;
-  hs_po : form;
+  hs_po : post;
   [@alert priv_pl "Use the accessor function `hs_po` instead of the field"]
 }
 
@@ -362,9 +365,33 @@ val ts_inv_lower_right3 : (ss_inv -> ss_inv -> ss_inv -> form) ->
 
 (* -------------------------------------------------------------------- *)
 
+type hs_inv = {
+  hsi_m : memory;
+  hsi_inv : post;
+}
+
+val empty_poe : form -> post
+val empty_hs : ss_inv -> hs_inv
+val is_empty_poe : post -> bool
+val lift_f : ss_inv -> hs_inv
+val lower_f : hs_inv -> ss_inv
+val update_hs_ss : ss_inv -> hs_inv -> hs_inv
+val map_poe : (form -> form) -> post -> post
+val map_hs_inv1 : (form -> form) -> hs_inv -> hs_inv
+val map_hs_inv2 : (form -> form -> form) -> hs_inv -> hs_inv -> hs_inv
+val exists_poe : (form -> bool) -> post -> bool
+val forall_poe : (form -> bool) -> post -> bool
+val forall2_poe : (form -> form -> bool) -> post -> post -> bool
+val poe_to_list : post -> form list
+val iter_poe : (form -> unit) -> post -> unit
+val iter2_poe : (form -> form -> unit) -> post -> post -> unit
+
+(* -------------------------------------------------------------------- *)
+
 type inv =
   | Inv_ss of ss_inv
   | Inv_ts of ts_inv
+  | Inv_hs of hs_inv
 
 val inv_of_inv : inv -> form
 
@@ -374,6 +401,8 @@ val lift_ss_inv3 : (ss_inv -> ss_inv -> ss_inv -> 'a) -> inv -> inv -> inv -> 'a
 val lift_ts_inv : (ts_inv -> 'a) -> inv -> 'a
 val lift_ts_inv2 : (ts_inv -> ts_inv -> 'a) -> inv -> inv -> 'a
 
+val lift_hs_ss_inv : (ss_inv -> hs_inv -> 'a) -> inv -> inv -> 'a
+
 val ss_inv_generalize_left : ss_inv -> memory -> ts_inv
 val ss_inv_generalize_right : ss_inv -> memory -> ts_inv
 
@@ -389,9 +418,9 @@ val ef_po : equivF -> ts_inv
 val es_pr : equivS -> ts_inv
 val es_po : equivS -> ts_inv
 val hf_pr : sHoareF -> ss_inv
-val hf_po : sHoareF -> ss_inv
+val hf_po : sHoareF -> hs_inv
 val hs_pr : sHoareS -> ss_inv
-val hs_po : sHoareS -> ss_inv
+val hs_po : sHoareS -> hs_inv
 val ehf_pr : eHoareF -> ss_inv
 val ehf_po : eHoareF -> ss_inv
 val ehs_pr : eHoareS -> ss_inv
diff --git a/src/ecCallbyValue.ml b/src/ecCallbyValue.ml
index f65c8f25e..b2a40dae4 100644
--- a/src/ecCallbyValue.ml
+++ b/src/ecCallbyValue.ml
@@ -482,20 +482,20 @@ and cbv (st : state) (s : subst) (f : form) (args : args) : form =
     assert (Args.isempty args);
     assert (not (Subst.has_mem s hf.hf_m));
     let hf_pr = norm st s (hf_pr hf).inv in
-    let hf_po = norm st s (hf_po hf).inv in
+    let hf_po = map_poe (norm st s) (hf_po hf).hsi_inv in
     let hf_f  = norm_xfun st s hf.hf_f in
     let (m,_) = norm_me s (abstract hf.hf_m) in
-    f_hoareF {m;inv=hf_pr} hf_f {m;inv=hf_po}
+    f_hoareF {m;inv=hf_pr} hf_f {hsi_m=m;hsi_inv=hf_po}
 
   | FhoareS hs ->
     assert (Args.isempty args);
     assert (not (Subst.has_mem s (fst hs.hs_m)));
     let hs_pr = norm st s (hs_pr hs).inv in
-    let hs_po = norm st s (hs_po hs).inv in
+    let hs_po = map_poe (norm st s) (hs_po hs).hsi_inv in
     let hs_s  = norm_stmt s hs.hs_s in
     let hs_m  = norm_me s hs.hs_m in
     let m = fst hs_m in
-    f_hoareS (snd hs_m) {m;inv=hs_pr} hs_s {m;inv=hs_po}
+    f_hoareS (snd hs_m) {m;inv=hs_pr} hs_s {hsi_m=m;hsi_inv=hs_po}
 
   | FeHoareF hf ->
     assert (Args.isempty args);
diff --git a/src/ecCommands.ml b/src/ecCommands.ml
index 9f647c52b..7f94ed212 100644
--- a/src/ecCommands.ml
+++ b/src/ecCommands.ml
@@ -454,6 +454,14 @@ and process_operator ?(src : string option) (scope : EcScope.scope) (pop : poper
   List.iter (fun s -> EcScope.notify scope `Info "added axiom: `%s'" s) axs;
   scope
 
+(* -------------------------------------------------------------------- *)
+and process_exception (scope :  EcScope.scope) (ed : pexception_decl located) =
+  let _, scope = EcScope.Except.add scope ed in
+  EcScope.check_state `InTop "exception" scope;
+  EcScope.notify scope `Info "added exception %s"
+    (unloc ed.pl_desc.pe_name);
+  scope
+
 (* -------------------------------------------------------------------- *)
 and process_procop ?(src : string option) (scope : EcScope.scope) (pop : pprocop located) =
   EcScope.check_state `InTop "operator" scope;
@@ -763,6 +771,7 @@ and process ?(src : string option) (ld : Loader.loader) (scope : EcScope.scope)
       | Gmodule      m    -> `Fct   (fun scope -> process_module     ?src scope m)
       | Ginterface   i    -> `Fct   (fun scope -> process_interface  ?src scope i)
       | Goperator    o    -> `Fct   (fun scope -> process_operator   ?src scope (mk_loc loc o))
+      | Gexception   e    -> `Fct   (fun scope -> process_exception  scope  (mk_loc loc e))
       | Gprocop      o    -> `Fct   (fun scope -> process_procop     ?src scope (mk_loc loc o))
       | Gpredicate   p    -> `Fct   (fun scope -> process_predicate  ?src scope (mk_loc loc p))
       | Gnotation    n    -> `Fct   (fun scope -> process_notation   scope  (mk_loc loc n))
diff --git a/src/ecCoreFol.ml b/src/ecCoreFol.ml
index 03dd1f64e..bbfc0d62d 100644
--- a/src/ecCoreFol.ml
+++ b/src/ecCoreFol.ml
@@ -270,13 +270,22 @@ let f_hoareS_r hs = mk_form (FhoareS hs) tbool
 let f_hoareF_r hf = mk_form (FhoareF hf) tbool
 
 let f_hoareS hs_mt hs_pr hs_s hs_po =
-  assert (hs_pr.m = hs_po.m);
-  f_hoareS_r { hs_m=(hs_pr.m, hs_mt); hs_pr=hs_pr.inv; hs_s; 
-    hs_po=hs_po.inv; } [@alert "-priv_pl"]
-
-let f_hoareF pr hf_f po =
-  assert (pr.m = po.m);
-  f_hoareF_r { hf_m=pr.m; hf_pr=pr.inv; hf_f; hf_po=po.inv; } [@alert "-priv_pl"]
+  assert (hs_pr.m = hs_po.hsi_m);
+  f_hoareS_r
+    { hs_m=(hs_pr.m, hs_mt);
+      hs_pr=hs_pr.inv;
+      hs_s;
+      hs_po=hs_po.hsi_inv;
+    } [@alert "-priv_pl"]
+
+let f_hoareF pr hf_f po  =
+  assert (pr.m = po.hsi_m);
+  f_hoareF_r
+    { hf_m=pr.m;
+      hf_pr=pr.inv;
+      hf_f;
+      hf_po=po.hsi_inv
+    } [@alert "-priv_pl"]
 
 (* -------------------------------------------------------------------- *)
 let f_eHoareS_r hs = mk_form (FeHoareS hs) tbool
@@ -475,13 +484,13 @@ let f_map gt g fp =
 
   | FhoareF hf ->
       let pr' = map_ss_inv1 g (hf_pr hf) in
-      let po' = map_ss_inv1 g (hf_po hf) in
-        f_hoareF pr' hf.hf_f po'
+      let po' = map_hs_inv1 g (hf_po hf) in
+      f_hoareF pr' hf.hf_f po'
 
   | FhoareS hs ->
       let pr' = map_ss_inv1 g (hs_pr hs) in
-      let po' = map_ss_inv1 g (hs_po hs) in
-        f_hoareS (snd hs.hs_m) pr' hs.hs_s po'
+      let po' = map_hs_inv1 g (hs_po hs) in
+      f_hoareS (snd hs.hs_m) pr' hs.hs_s po'
 
   | FeHoareF hf ->
       let pr' = map_ss_inv1 g (ehf_pr hf) in
@@ -542,8 +551,8 @@ let f_iter g f =
   | Ftuple   es           -> List.iter g es
   | Fproj    (e, _)       -> g e
 
-  | FhoareF  hf   -> g (hf_pr hf).inv; g (hf_po hf).inv
-  | FhoareS  hs   -> g (hs_pr hs).inv; g (hs_po hs).inv
+  | FhoareF  hf   -> g (hf_pr hf).inv; iter_poe g (hf_po hf).hsi_inv
+  | FhoareS  hs   -> g (hs_pr hs).inv; iter_poe g (hs_po hs).hsi_inv
   | FeHoareF  hf  -> g (ehf_pr hf).inv; g (ehf_po hf).inv
   | FeHoareS  hs  -> g (ehs_pr hs).inv; g (ehs_po hs).inv
   | FbdHoareF bhf -> g (bhf_pr bhf).inv; g (bhf_po bhf).inv; g (bhf_bd bhf).inv
@@ -571,8 +580,8 @@ let form_exists g f =
   | Ftuple   es           -> List.exists g es
   | Fproj    (e, _)       -> g e
 
-  | FhoareF   hf -> g (hf_pr hf).inv   || g (hf_po hf).inv
-  | FhoareS   hs -> g (hs_pr hs).inv   || g (hs_po hs).inv
+  | FhoareF   hf -> g (hf_pr hf).inv   || exists_poe g (hf_po hf).hsi_inv
+  | FhoareS   hs -> g (hs_pr hs).inv   || exists_poe g (hs_po hs).hsi_inv
   | FeHoareF  hf  -> g (ehf_pr hf).inv || g (ehf_po hf).inv
   | FeHoareS  hs  -> g (ehs_pr hs).inv || g (ehs_po hs).inv
   | FbdHoareF bhf -> g (bhf_pr bhf).inv || g (bhf_po bhf).inv
@@ -599,8 +608,8 @@ let form_forall g f =
   | Ftuple   es           -> List.for_all g es
   | Fproj    (e, _)       -> g e
 
-  | FhoareF  hf  -> g (hf_pr hf).inv  && g (hf_po hf).inv
-  | FhoareS  hs  -> g (hs_pr hs).inv  && g (hs_po hs).inv
+  | FhoareF  hf  -> g (hf_pr hf).inv  && forall_poe g (hf_po hf).hsi_inv
+  | FhoareS  hs  -> g (hs_pr hs).inv  && forall_poe g (hs_po hs).hsi_inv
   | FbdHoareF bhf -> g (bhf_pr bhf).inv && g (bhf_po bhf).inv
   | FbdHoareS bhs -> g (bhs_pr bhs).inv && g (bhs_po bhs).inv
   | FequivF   ef  -> g (ef_pr ef).inv   && g (ef_po ef).inv
diff --git a/src/ecCoreFol.mli b/src/ecCoreFol.mli
index 0977a33a5..90ea0dbc9 100644
--- a/src/ecCoreFol.mli
+++ b/src/ecCoreFol.mli
@@ -108,8 +108,8 @@ val f_lambda : bindings -> form -> form
 
 val f_forall_mems : (EcIdent.t * memtype) list -> form -> form
 
-val f_hoareF : ss_inv -> xpath -> ss_inv -> form
-val f_hoareS : memtype -> ss_inv -> stmt -> ss_inv -> form
+val f_hoareF : ss_inv -> xpath -> hs_inv -> form
+val f_hoareS : memtype -> ss_inv -> stmt -> hs_inv -> form
 
 val f_eHoareF : ss_inv -> xpath -> ss_inv -> form
 val f_eHoareS : memtype -> ss_inv -> EcCoreModules.stmt -> ss_inv -> form
diff --git a/src/ecCoreModules.ml b/src/ecCoreModules.ml
index 6f96118ab..784231708 100644
--- a/src/ecCoreModules.ml
+++ b/src/ecCoreModules.ml
@@ -93,7 +93,7 @@ let i_call     (lv, m, tys) = mk_instr (Scall (lv, m, tys))
 let i_if       (c, s1, s2)  = mk_instr (Sif (c, s1, s2))
 let i_while    (c, s)       = mk_instr (Swhile (c, s))
 let i_match    (e, b)       = mk_instr (Smatch (e, b))
-let i_assert   e            = mk_instr (Sassert e)
+let i_raise    e            = mk_instr (Sraise e)
 let i_abstract id           = mk_instr (Sabstract id)
 
 let s_seq      s1 s2        = stmt (s1.s_node @ s2.s_node)
@@ -105,7 +105,7 @@ let s_call     arg = stmt [i_call arg]
 let s_if       arg = stmt [i_if arg]
 let s_while    arg = stmt [i_while arg]
 let s_match    arg = stmt [i_match arg]
-let s_assert   arg = stmt [i_assert arg]
+let s_raise    arg = stmt [i_raise arg]
 let s_abstract arg = stmt [i_abstract arg]
 
 (* -------------------------------------------------------------------- *)
@@ -133,8 +133,8 @@ let get_match = function
   | { i_node = Smatch (e, b) } -> Some (e, b)
   | _ -> None
 
-let get_assert = function
-  | { i_node = Sassert e } -> Some e
+let get_raise = function
+  | { i_node = Sraise e } -> Some e
   | _ -> raise Not_found
 
 (* -------------------------------------------------------------------- *)
@@ -147,7 +147,7 @@ let destr_call   = _destr_of_get get_call
 let destr_if     = _destr_of_get get_if
 let destr_while  = _destr_of_get get_while
 let destr_match  = _destr_of_get get_match
-let destr_assert = _destr_of_get get_assert
+let destr_raise = _destr_of_get get_raise
 
 (* -------------------------------------------------------------------- *)
 let _is_of_get (get : instr -> 'a option) (i : instr) =
@@ -159,7 +159,7 @@ let is_call   = _is_of_get get_call
 let is_if     = _is_of_get get_if
 let is_while  = _is_of_get get_while
 let is_match  = _is_of_get get_match
-let is_assert = _is_of_get get_assert
+let is_raise  = _is_of_get get_raise
 
 (* -------------------------------------------------------------------- *)
 module Uninit = struct    (* FIXME: generalize this for use in ecPV *)
@@ -223,8 +223,8 @@ and i_get_uninit_read (w : Ssym.t) (i : instr) =
       let ws, rs = List.split wrs in
       (Ssym.union w (Ssym.big_inter ws), Ssym.big_union (r :: rs))
 
-  | Sassert e ->
-      (w, Ssym.diff (Uninit.e_pv e) w)
+  | Sraise _ ->
+      (w, Ssym.empty)
 
   | Sabstract (_ : EcIdent.t) ->
       (w, Ssym.empty)
diff --git a/src/ecCoreModules.mli b/src/ecCoreModules.mli
index 1b84c0df2..df8f7b345 100644
--- a/src/ecCoreModules.mli
+++ b/src/ecCoreModules.mli
@@ -42,7 +42,7 @@ val i_call     : lvalue option * xpath * expr list -> instr
 val i_if       : expr * stmt * stmt -> instr
 val i_while    : expr * stmt -> instr
 val i_match    : expr * ((EcIdent.t * ty) list * stmt) list -> instr
-val i_assert   : expr -> instr
+val i_raise    : EcPath.path  -> instr
 val i_abstract : EcIdent.t -> instr
 
 val s_asgn     : lvalue * expr -> stmt
@@ -51,7 +51,7 @@ val s_call     : lvalue option * xpath * expr list -> stmt
 val s_if       : expr * stmt * stmt -> stmt
 val s_while    : expr * stmt -> stmt
 val s_match    : expr * ((EcIdent.t * ty) list * stmt) list -> stmt
-val s_assert   : expr -> stmt
+val s_raise    : EcPath.path -> stmt
 val s_abstract : EcIdent.t -> stmt
 val s_seq      : stmt -> stmt -> stmt
 val s_empty    : stmt
@@ -66,7 +66,7 @@ val destr_call   : instr -> lvalue option * xpath * expr list
 val destr_if     : instr -> expr * stmt * stmt
 val destr_while  : instr -> expr * stmt
 val destr_match  : instr -> expr * ((EcIdent.t * ty) list * stmt) list
-val destr_assert : instr -> expr
+val destr_raise  : instr ->  EcPath.path
 
 val is_asgn   : instr -> bool
 val is_rnd    : instr -> bool
@@ -74,7 +74,7 @@ val is_call   : instr -> bool
 val is_if     : instr -> bool
 val is_while  : instr -> bool
 val is_match  : instr -> bool
-val is_assert : instr -> bool
+val is_raise  : instr -> bool
 
 (* -------------------------------------------------------------------- *)
 val get_uninit_read : stmt -> Sx.t
diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml
index d906a61e3..f668fb39a 100644
--- a/src/ecCorePrinting.ml
+++ b/src/ecCorePrinting.ml
@@ -83,17 +83,17 @@ module type PrinterAPI = sig
   val pp_vsubst : PPEnv.t -> vsubst pp
 
   (* ------------------------------------------------------------------ *)
-  val pp_typedecl    : PPEnv.t -> (path * tydecl                  ) pp
-  val pp_opdecl      : ?long:bool -> PPEnv.t -> (path * operator  ) pp
-  val pp_added_op    : PPEnv.t -> operator pp
-  val pp_axiom       : ?long:bool -> PPEnv.t -> (path * axiom     ) pp
-  val pp_theory      : PPEnv.t -> (path * ctheory                 ) pp
-  val pp_modtype1    : PPEnv.t -> (module_type                    ) pp
-  val pp_modtype     : PPEnv.t -> (module_type                    ) pp
-  val pp_modexp      : PPEnv.t -> (mpath * module_expr            ) pp
-  val pp_moditem     : PPEnv.t -> (mpath * module_item            ) pp
-  val pp_modsig      : ?long:bool -> PPEnv.t -> (path * module_sig) pp
-  val pp_modsig_smpl : PPEnv.t -> (path * module_smpl_sig         ) pp
+  val pp_typedecl     : PPEnv.t -> (path * tydecl                  ) pp
+  val pp_opdecl       : ?long:bool -> PPEnv.t -> (path * operator  ) pp
+  val pp_added_op     : PPEnv.t -> operator pp
+  val pp_axiom        : ?long:bool -> PPEnv.t -> (path * axiom     ) pp
+  val pp_theory       : PPEnv.t -> (path * ctheory                 ) pp
+  val pp_modtype1     : PPEnv.t -> (module_type                    ) pp
+  val pp_modtype      : PPEnv.t -> (module_type                    ) pp
+  val pp_modexp       : PPEnv.t -> (mpath * module_expr            ) pp
+  val pp_moditem      : PPEnv.t -> (mpath * module_item            ) pp
+  val pp_modsig       : ?long:bool -> PPEnv.t -> (path * module_sig) pp
+  val pp_modsig_smpl  : PPEnv.t -> (path * module_smpl_sig         ) pp
 
   (* ------------------------------------------------------------------ *)
   val pp_hoareS   : PPEnv.t -> ?prpo:prpo_display -> sHoareS  pp
diff --git a/src/ecCoreSubst.ml b/src/ecCoreSubst.ml
index c39a87a27..4646ef07a 100644
--- a/src/ecCoreSubst.ml
+++ b/src/ecCoreSubst.ml
@@ -332,8 +332,7 @@ let rec s_subst_top (s : f_subst) : stmt -> stmt =
 
       i_match (e_subst e, List.Smart.map forb b)
 
-    | Sassert e ->
-      i_assert (e_subst e)
+    | Sraise e -> i_raise e
 
     | Sabstract _ ->
       i
@@ -454,15 +453,15 @@ module Fsubst = struct
       let hf_f   = x_subst s hf.hf_f in
       let (s, m) = add_m_binding s hf.hf_m in
       let hf_pr  = f_subst ~tx s (hf_pr hf).inv in
-      let hf_po  = f_subst ~tx s (hf_po hf).inv in
-      f_hoareF {m;inv=hf_pr} hf_f {m;inv=hf_po}
+      let hf_po = map_poe (f_subst ~tx s) (hf_po hf).hsi_inv in
+      f_hoareF {m;inv=hf_pr} hf_f {hsi_m=m;hsi_inv=hf_po}
 
     | FhoareS hs ->
       let hs_s    = s_subst s hs.hs_s in
       let s, (m, mt) = add_me_binding s hs.hs_m in
       let hs_pr   = f_subst ~tx s (hs_pr hs).inv in
-      let hs_po   = f_subst ~tx s (hs_po hs).inv in
-      f_hoareS mt {m;inv=hs_pr} hs_s {m;inv=hs_po}
+      let hs_po = map_poe (f_subst ~tx s) (hs_po hs).hsi_inv in
+      f_hoareS mt {m;inv=hs_pr} hs_s {hsi_m=m;hsi_inv=hs_po}
 
     | FeHoareF hf ->
       let hf_f  = x_subst s hf.ehf_f in
diff --git a/src/ecDecl.ml b/src/ecDecl.ml
index 5636641ac..924fa74b9 100644
--- a/src/ecDecl.ml
+++ b/src/ecDecl.ml
@@ -152,6 +152,10 @@ type axiom = {
 let is_axiom  (x : axiom_kind) = match x with `Axiom _ -> true | _ -> false
 let is_lemma  (x : axiom_kind) = match x with `Lemma   -> true | _ -> false
 
+(* -------------------------------------------------------------------- *)
+
+type excep = {e_loca    : locality;}
+
 (* -------------------------------------------------------------------- *)
 let op_ty op = op.op_ty
 
@@ -217,6 +221,12 @@ let mk_op ?clinline ?unfold ~opaque tparams ty body lc =
   let kind = OB_oper body in
   gen_op ?clinline ?unfold ~opaque tparams ty kind lc
 
+let gen_excep lc = {
+  e_loca    = lc;
+}
+
+let mk_except lc = gen_excep lc
+
 let mk_abbrev ?(ponly = false) tparams xs (codom, body) lc =
   let kind = {
     ont_args  = xs;
diff --git a/src/ecDecl.mli b/src/ecDecl.mli
index 7864a0e0d..cb8e915f8 100644
--- a/src/ecDecl.mli
+++ b/src/ecDecl.mli
@@ -161,6 +161,11 @@ val axiomatized_op :
   -> locality
   -> axiom
 
+(* -------------------------------------------------------------------- *)
+type excep = { e_loca    : locality; }
+
+val mk_except : locality -> excep
+
 (* -------------------------------------------------------------------- *)
 type typeclass = {
   tc_prt : EcPath.path option;
diff --git a/src/ecEnv.ml b/src/ecEnv.ml
index a4a5c8a7c..dc4408d57 100644
--- a/src/ecEnv.ml
+++ b/src/ecEnv.ml
@@ -87,6 +87,7 @@ type mc = {
   mc_modsigs    : (ipath * top_module_sig) MMsym.t;
   mc_tydecls    : (ipath * EcDecl.tydecl) MMsym.t;
   mc_operators  : (ipath * EcDecl.operator) MMsym.t;
+  mc_except     : (ipath * EcDecl.excep) MMsym.t;
   mc_axioms     : (ipath * EcDecl.axiom) MMsym.t;
   mc_theories   : (ipath * ctheory) MMsym.t;
   mc_typeclasses: (ipath * typeclass) MMsym.t;
@@ -277,6 +278,7 @@ let empty_mc params = {
   mc_modsigs    = MMsym.empty;
   mc_tydecls    = MMsym.empty;
   mc_operators  = MMsym.empty;
+  mc_except     = MMsym.empty;
   mc_axioms     = MMsym.empty;
   mc_theories   = MMsym.empty;
   mc_variables  = MMsym.empty;
@@ -515,6 +517,7 @@ module MC = struct
   let _downpath_for_tydecl    = _downpath_for_th
   let _downpath_for_modsig    = _downpath_for_th
   let _downpath_for_operator  = _downpath_for_th
+  let _downpath_for_except    = _downpath_for_th
   let _downpath_for_axiom     = _downpath_for_th
   let _downpath_for_typeclass = _downpath_for_th
   let _downpath_for_rwbase    = _downpath_for_th
@@ -711,6 +714,20 @@ module MC = struct
   let import_axiom p ax env =
     import (_up_axiom true) (IPPath p) ax env
 
+  (* -------------------------------------------------------------------- *)
+  let lookup_except qnx env =
+    match lookup (fun mc -> mc.mc_except) qnx env with
+    | None -> lookup_error (`QSymbol qnx)
+    | Some (p, (args, obj)) -> (_downpath_for_except env p args, obj)
+
+  let _up_except candup mc x obj =
+    if not candup && MMsym.last x mc.mc_except <> None then
+      raise (DuplicatedBinding x);
+    { mc with mc_except = MMsym.add x obj mc.mc_except }
+
+  let import_except p e env =
+    import (_up_except true) (IPPath p) e env
+
   (* -------------------------------------------------------------------- *)
   let lookup_operator qnx env =
     match lookup (fun mc -> mc.mc_operators) qnx env with
@@ -1086,6 +1103,9 @@ module MC = struct
       | Th_operator (xop, op) ->
           (add2mc _up_operator xop op mc, None)
 
+      | Th_exception (xop, e) ->
+          (add2mc _up_except xop e mc, None)
+
       | Th_axiom (xax, ax) ->
           (add2mc _up_axiom xax ax mc, None)
 
@@ -1185,6 +1205,9 @@ module MC = struct
   and bind_axiom x ax env =
     bind _up_axiom x ax env
 
+  and bind_except x e env =
+    bind _up_except x e env
+
   and bind_operator x op env =
     bind _up_operator x op env
 
@@ -2780,6 +2803,39 @@ module Op = struct
     gen_all (fun mc -> mc.mc_operators) MC.lookup_operators ?check ?name env
 end
 
+(* -------------------------------------------------------------------- *)
+module Except = struct
+  type t = excep
+
+  let by_path_opt (p : EcPath.path) (env : env) =
+    omap
+      check_not_suspended
+      (MC.by_path (fun mc -> mc.mc_except) (IPPath p) env)
+
+  let by_path (p : EcPath.path) (env : env) =
+    match by_path_opt p env with
+    | None -> lookup_error (`Path p)
+    | Some obj -> obj
+
+  let add (p : EcPath.path) (env : env) =
+    let obj = by_path p env in
+      MC.import_except p obj env
+
+  let lookup qname (env : env) =
+   MC.lookup_except qname env
+
+  let lookup_opt name env =
+    try_lf (fun () -> lookup name env)
+
+  let lookup_path name env =
+    fst (lookup name env)
+
+  let bind ?(import = true) name e env =
+    let env = MC.bind_except name e env in
+    { env with env_item = mkitem ~import (Th_exception (name, e)) :: env.env_item }
+
+end
+
 (* -------------------------------------------------------------------- *)
 module Ax = struct
   type t = axiom
@@ -3086,6 +3142,9 @@ module Theory = struct
         | Th_operator (x, op) ->
             MC.import_operator (xpath x) op env
 
+        | Th_exception (x, e) ->
+            MC.import_except (xpath x) e env
+
         | Th_axiom (x, ax) ->
             MC.import_axiom (xpath x) ax env
 
diff --git a/src/ecEnv.mli b/src/ecEnv.mli
index 5a1d5bf60..adedf5c02 100644
--- a/src/ecEnv.mli
+++ b/src/ecEnv.mli
@@ -112,6 +112,8 @@ module Fun : sig
 
   val inv_memenv : memory -> memory -> env -> env
 
+  val inv_memenv1 : memory -> env -> env
+
   val equivF_memenv : memory -> memory -> xpath -> xpath -> env ->
     (memenv * memenv) * (memenv * memenv)
 
@@ -151,6 +153,17 @@ module Var : sig
   val bindall_pvglob : (EcSymbols.symbol * EcTypes.ty) list -> env -> env
 
 end
+(* -------------------------------------------------------------------- *)
+module Except : sig
+  type t = excep
+  val by_path     : path -> env -> t
+  val by_path_opt : path -> env -> t option
+  val add  : path -> env -> env
+  val lookup      : qsymbol -> env -> path * t
+  val lookup_opt  : qsymbol -> env -> (path * t) option
+  val lookup_path : qsymbol -> env -> path
+  val bind        : ?import:bool -> symbol -> t -> env -> env
+end
 
 (* -------------------------------------------------------------------- *)
 module Ax : sig
diff --git a/src/ecLexer.mll b/src/ecLexer.mll
index 19536eaae..6d55c8c92 100644
--- a/src/ecLexer.mll
+++ b/src/ecLexer.mll
@@ -53,7 +53,7 @@
     "match"       , MATCH      ;        (* KW: prog *)
     "for"         , FOR        ;        (* KW: prog *)
     "while"       , WHILE      ;        (* KW: prog *)
-    "assert"      , ASSERT     ;        (* KW: prog *)
+    "raise"       , RAISE     ;        (* KW: prog *)
     "return"      , RETURN     ;        (* KW: prog *)
     "res"         , RES        ;        (* KW: prog *)
     "equiv"       , EQUIV      ;        (* KW: prog *)
@@ -190,6 +190,7 @@
     "of"          , OF         ;        (* KW: global *)
     "const"       , CONST      ;        (* KW: global *)
     "op"          , OP         ;        (* KW: global *)
+    "exception"   , EXCEP      ;        (* KW: global *)
     "pred"        , PRED       ;        (* KW: global *)
     "inductive"   , INDUCTIVE  ;        (* KW: global *)
     "notation"    , NOTATION   ;        (* KW: global *)
diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml
index 97fe5f0b4..e0d1c207a 100644
--- a/src/ecLowPhlGoal.ml
+++ b/src/ecLowPhlGoal.ml
@@ -96,7 +96,7 @@ let pf_first_call   pe st = pf_first_gen  "call"   destr_call   pe st
 let pf_first_if     pe st = pf_first_gen  "if"     destr_if     pe st
 let pf_first_match  pe st = pf_first_gen  "match"  destr_match  pe st
 let pf_first_while  pe st = pf_first_gen  "while"  destr_while  pe st
-let pf_first_assert pe st = pf_first_gen  "assert" destr_assert pe st
+let pf_first_raise  pe st = pf_first_gen  "raise"  destr_raise  pe st
 
 (* -------------------------------------------------------------------- *)
 let pf_last_asgn   pe st = pf_last_gen  "asgn"   destr_asgn   pe st
@@ -105,7 +105,7 @@ let pf_last_call   pe st = pf_last_gen  "call"   destr_call   pe st
 let pf_last_if     pe st = pf_last_gen  "if"     destr_if     pe st
 let pf_last_match  pe st = pf_last_gen  "match"  destr_match  pe st
 let pf_last_while  pe st = pf_last_gen  "while"  destr_while  pe st
-let pf_last_assert pe st = pf_last_gen  "assert" destr_assert pe st
+let pf_last_raise  pe st = pf_last_gen  "raise"  destr_raise  pe st
 
 (* -------------------------------------------------------------------- *)
 let tc1_first_asgn   tc st = pf_first_asgn   !!tc st
@@ -114,7 +114,7 @@ let tc1_first_call   tc st = pf_first_call   !!tc st
 let tc1_first_if     tc st = pf_first_if     !!tc st
 let tc1_first_match  tc st = pf_first_match  !!tc st
 let tc1_first_while  tc st = pf_first_while  !!tc st
-let tc1_first_assert tc st = pf_first_assert !!tc st
+let tc1_first_raise  tc st = pf_first_raise  !!tc st
 
 (* -------------------------------------------------------------------- *)
 let tc1_last_asgn   tc st = pf_last_asgn   !!tc st
@@ -123,7 +123,7 @@ let tc1_last_call   tc st = pf_last_call   !!tc st
 let tc1_last_if     tc st = pf_last_if     !!tc st
 let tc1_last_match  tc st = pf_last_match  !!tc st
 let tc1_last_while  tc st = pf_last_while  !!tc st
-let tc1_last_assert tc st = pf_last_assert !!tc st
+let tc1_last_raise  tc st = pf_last_raise  !!tc st
 
 (* -------------------------------------------------------------------- *)
 (* TODO: use in change pos *)
@@ -139,7 +139,7 @@ let pf_pos_last_call   pe s = pf_pos_last_gen "call"   is_call   pe s
 let pf_pos_last_if     pe s = pf_pos_last_gen "if"     is_if     pe s
 let pf_pos_last_match  pe s = pf_pos_last_gen "match"  is_match  pe s
 let pf_pos_last_while  pe s = pf_pos_last_gen "while"  is_while  pe s
-let pf_pos_last_assert pe s = pf_pos_last_gen "assert" is_assert pe s
+let pf_pos_last_raise pe s = pf_pos_last_gen "raise"  is_raise pe s
 
 
 let tc1_pos_last_asgn   tc s = pf_pos_last_asgn   !!tc s
@@ -148,7 +148,7 @@ let tc1_pos_last_call   tc s = pf_pos_last_call   !!tc s
 let tc1_pos_last_if     tc s = pf_pos_last_if     !!tc s
 let tc1_pos_last_match  tc s = pf_pos_last_match  !!tc s
 let tc1_pos_last_while  tc s = pf_pos_last_while  !!tc s
-let tc1_pos_last_assert tc s = pf_pos_last_assert !!tc s
+let tc1_pos_last_raise  tc s = pf_pos_last_raise  !!tc s
 
 (* -------------------------------------------------------------------- *)
 let pf_as_hoareF   pe c = as_phl (`Hoare  `Pred) (fun () -> destr_hoareF   c) pe
@@ -258,8 +258,8 @@ let tc1_get_pre tc =
 (* -------------------------------------------------------------------- *)
 let get_post f =
   match f.f_node with
-  | FhoareF hf   -> Some (Inv_ss (hf_po hf))
-  | FhoareS hs   -> Some (Inv_ss (hs_po hs))
+  | FhoareF hf   -> Some (Inv_hs (hf_po hf))
+  | FhoareS hs   -> Some (Inv_hs (hs_po hs))
   | FeHoareF hf  -> Some (Inv_ss (ehf_po hf))
   | FeHoareS hs  -> Some (Inv_ss (ehs_po hs))
   | FbdHoareF hf -> Some (Inv_ss (bhf_po hf))
@@ -274,6 +274,7 @@ let tc1_get_post tc =
   | None   -> tc_error_noXhl ~kinds:hlkinds_Xhl !!tc
   | Some f -> f
 
+
 (* -------------------------------------------------------------------- *)
 let set_pre ~pre f =
   match f.f_node, pre with
@@ -684,9 +685,12 @@ let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc =
       match concl.f_node with
       | FhoareS hs ->
           let pr, po = hs_pr hs, hs_po hs in
+          let (po,_,_) = po.hsi_inv in
           let (me, stmt, cs) =
-            tx (pf, hyps) cpos (pr.inv, po.inv) (hs.hs_m, hs.hs_s) in
-          let concl = f_hoareS (snd me) (hs_pr hs) stmt (hs_po hs) in
+            tx (pf, hyps) cpos (pr.inv, po) (hs.hs_m, hs.hs_s) in
+          let concl =
+            f_hoareS (snd me) (hs_pr hs) stmt (hs_po hs)
+          in
           FApi.xmutate1 tc (tr None) (cs @ [concl])
 
       | FbdHoareS bhs when bdhoare ->
diff --git a/src/ecMaps.ml b/src/ecMaps.ml
index 61609a19d..318979c76 100644
--- a/src/ecMaps.ml
+++ b/src/ecMaps.ml
@@ -186,6 +186,6 @@ end = struct
         f prefix t.value;
       Map.iter (fun k v -> doit (k :: prefix) v) t.children
     in
-    
+
     doit [] t
 end
diff --git a/src/ecMatching.ml b/src/ecMatching.ml
index 7c8e6a2fb..6d872855d 100644
--- a/src/ecMatching.ml
+++ b/src/ecMatching.ml
@@ -695,8 +695,10 @@ let f_match_core opts hyps (ue, ev) f1 f2 =
               Fsubst.f_bind_mem subst hf1.hf_m hf2.hf_m in
           assert (not (Mid.mem hf1.hf_m mxs) && not (Mid.mem hf2.hf_m mxs));
           let mxs = Mid.add hf1.hf_m hf2.hf_m mxs in
+          let lf1 = poe_to_list (hf_po hf1).hsi_inv in
+          let lf2 = poe_to_list (hf_po hf2).hsi_inv in
           List.iter2 (doit env (subst, mxs))
-            [(hf_pr hf1).inv; (hf_po hf1).inv] [(hf_pr hf2).inv; (hf_po hf2).inv]
+            ((hf_pr hf1).inv :: lf1) ((hf_pr hf2).inv :: lf2)
       end
 
       | FbdHoareF hf1, FbdHoareF hf2 -> begin
@@ -1024,7 +1026,8 @@ module FPosition = struct
               doit pos (`WithSubCtxt [(ctxt, pr.pr_args); (subctxt, pr.pr_event.inv)])
 
           | FhoareF hs ->
-              doit pos (`WithCtxt (Sid.add hs.hf_m ctxt, [(hf_pr hs).inv; (hf_po hs).inv]))
+            let lf = poe_to_list (hf_po hs).hsi_inv in
+            doit pos (`WithCtxt (Sid.add hs.hf_m ctxt, (hf_pr hs).inv :: lf))
 
           (* TODO: A: From what I undertand, there is an error there:
              it should be  (subctxt, hs.bhf_bd) *)
@@ -1173,9 +1176,14 @@ module FPosition = struct
               f_pr pr.pr_mem pr.pr_fun args' {m;inv=event'}
 
           | FhoareF hf ->
-              let (hf_pr, hf_po) = as_seq2 (doit p [(hf_pr hf).inv; (hf_po hf).inv]) in
+              let hf_pr = as_seq1 (doit p [(hf_pr hf).inv]) in
+              let hf_po =
+                map_poe
+                  (fun f -> as_seq1 (doit p [f]))
+                  (hf_po hf).hsi_inv
+              in
               let m = hf.hf_m in
-              f_hoareF {m;inv=hf_pr} hf.hf_f {m;inv=hf_po}
+              f_hoareF {m;inv=hf_pr} hf.hf_f {hsi_m= m;hsi_inv=hf_po}
 
           | FeHoareF hf ->
               let (ehf_pr, ehf_po) =
diff --git a/src/ecPV.ml b/src/ecPV.ml
index 6d5c5bd5e..ff08186c3 100644
--- a/src/ecPV.ml
+++ b/src/ecPV.ml
@@ -129,7 +129,7 @@ module Mpv = struct
     | Sif    (c, s1, s2) -> i_if     (esubst c, ssubst s1, ssubst s2)
     | Swhile (e, stmt)   -> i_while  (esubst e, ssubst stmt)
     | Smatch (e, b)      -> i_match  (esubst e, List.Smart.map (snd_map ssubst) b)
-    | Sassert e          -> i_assert (esubst e)
+    | Sraise e           -> i_raise  e
     | Sabstract _        -> i
 
   and issubst env (s : esubst) (is : instr list) =
@@ -328,10 +328,12 @@ module PV = struct
           aux env fv e
 
       | FhoareF hf ->
-          in_mem_scope env fv [hf.hf_m] [(hf_pr hf).inv; (hf_po hf).inv]
+          let lf = poe_to_list (hf_po hf).hsi_inv in
+          in_mem_scope env fv [hf.hf_m] ((hf_pr hf).inv  :: lf)
 
       | FhoareS hs ->
-          in_mem_scope env fv [fst hs.hs_m] [(hs_pr hs).inv; (hs_po hs).inv]
+        let lf = poe_to_list (hs_po hs).hsi_inv in
+        in_mem_scope env fv [fst hs.hs_m] ((hs_pr hs).inv :: lf)
 
       | FeHoareF hf ->
           in_mem_scope env fv [hf.ehf_m] [(ehf_pr hf).inv; (ehf_po hf).inv]
@@ -412,7 +414,7 @@ module PV = struct
     { s_pv = Mnpv.set_diff fv1.s_pv fv2.s_pv;
       s_gl = Sm.diff fv1.s_gl fv2.s_gl }
 
-  let inter fv1 fv2 = 
+  let inter fv1 fv2 =
     { s_pv = Mnpv.inter (fun _ _ t2 -> Some t2) fv1.s_pv fv2.s_pv;
       s_gl = Sm.inter fv1.s_gl fv2.s_gl }
 
@@ -513,7 +515,7 @@ and i_write_r ?(except=Sx.empty) env w i =
   match i.i_node with
   | Sasgn  (lp, _) -> lp_write_r env w lp
   | Srnd   (lp, _) -> lp_write_r env w lp
-  | Sassert _      -> w
+  | Sraise _      -> w
 
   | Scall(lp,f,_) ->
     if Sx.mem f except then w else
@@ -571,7 +573,7 @@ and i_read_r env r i =
   match i.i_node with
   | Sasgn   (_lp, e) -> e_read_r env r e
   | Srnd    (_lp, e) -> e_read_r env r e
-  | Sassert e       -> e_read_r env r e
+  | Sraise  _        -> PV.empty
 
   | Scall (_lp, f, es) ->
       let r = List.fold_left (e_read_r env) r es in
@@ -1054,7 +1056,8 @@ and i_eqobs_in_refl env i eqo =
     let eqs = List.fold_left PV.union PV.empty eqs in
     add_eqs_refl env eqs e
 
-  | Sassert e -> add_eqs_refl env eqo e
+  | Sraise _ -> PV.empty
+
   | Sabstract _ -> assert false
 
 and eqobs_inF_refl env f' eqo =
diff --git a/src/ecParser.mly b/src/ecParser.mly
index 46205d02b..14127c7a7 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -384,7 +384,7 @@
 %token AMP
 %token APPLY
 %token AS
-%token ASSERT
+%token RAISE
 %token ASSUMPTION
 %token ASYNC
 %token AT
@@ -443,6 +443,7 @@
 %token EQUIV
 %token ETA
 %token EXACT
+%token EXCEP
 %token EXFALSO
 %token EXIST
 %token EXIT
@@ -1224,9 +1225,22 @@ hoare_bd_cmp :
 | EQ { EcAst.FHeq }
 | GE { EcAst.FHge }
 
+epost(P): x=qident COLON post=form_r(P)
+    { (x,post) }
+
+epostl(P):
+| PIPE f=form_r(P)              { [], Some f }
+| PIPE p=epost(P)               { [ p ], None }
+| PIPE p=epost(P) a=epostl(P)   { p :: fst a, snd a }
+
+hoare_epost(P):
+| empty            { ([],None) }
+| c=epostl(P)      { c }
+
 hoare_body(P):
   mp=loc(fident) m=brace(mident)? COLON pre=form_r(P) LONGARROW post=form_r(P)
-    { PFhoareF (m, pre, mp, post) }
+                                                 epost=hoare_epost(P)
+    { PFhoareF (m, pre, mp, post, epost) }
 
 ehoare_body(P):
   mp=loc(fident) m=brace(mident)? COLON pre=form_r(P) LONGARROW
@@ -1347,8 +1361,8 @@ base_instr:
 | f=loc(fident) LPAREN es=loc(plist0(expr, COMMA)) RPAREN
     { PScall (None, f, es) }
 
-| ASSERT LPAREN c=expr RPAREN
-    { PSassert c }
+| RAISE e=paren(expr)? x=qident
+     { PSraise (x, e) }
 
 instr:
 | bi=base_instr SEMICOLON
@@ -1861,6 +1875,13 @@ procop:
 | locality=locality PROC OP x=ident EQ f=loc(fident)
     { { ppo_name = x; ppo_target = f; ppo_locality = locality; } }
 
+(* -------------------------------------------------------------------- *)
+(* Exceptions                                                           *)
+excep:
+| locality=locality EXCEP x=ident
+   { { pe_name     = x;
+       pe_locality = locality; } }
+
 (* -------------------------------------------------------------------- *)
 (* Predicate definitions                                                *)
 predicate:
@@ -2510,17 +2531,35 @@ conseq:
 | UNDERSCORE LONGARROW f2=form    { None, Some f2 }
 | f1=form LONGARROW f2=form       { Some f1, Some f2 }
 
+epost_xt:
+| x=qident COLON f=form      { (x, f) }
+
+epostl_xt:
+| PIPE f=form                   { [], Some f }
+| PIPE p=epost_xt               { [ p ], None }
+| PIPE p=epost_xt a=epostl_xt   { p :: fst a, snd a }
+
+conseq_epost:
+| empty            { None }
+| c=epostl_xt      { Some c }
+
 conseq_xt:
-| c=conseq                                     { c, None }
-| c=conseq   COLON cmp=hoare_bd_cmp? bd=sform  { c, Some (CQI_bd (cmp, bd)) }
-| UNDERSCORE COLON cmp=hoare_bd_cmp? bd=sform  { (None, None), Some (CQI_bd (cmp, bd)) }
+| c=conseq d=conseq_epost
+    { (fst c, snd c, d), None }
+| c=conseq   COLON cmp=hoare_bd_cmp? bd=sform
+    { (fst c, snd c, None), Some (CQI_bd (cmp, bd)) }
+| UNDERSCORE COLON cmp=hoare_bd_cmp? bd=sform
+    { (None, None, None), Some (CQI_bd (cmp, bd)) }
 
+call_epost:
+| empty             { ([],None) }
+| c=epostl_xt       { c }
 
 call_info:
-| f1=form LONGARROW f2=form          { CI_spec (f1, f2) }
-| f=form                             { CI_inv  f }
-| bad=form COMMA p=form              { CI_upto (bad,p,None) }
-| bad=form COMMA p=form COMMA q=form { CI_upto (bad,p,Some q) }
+| f1=form LONGARROW f2=form poe=call_epost { CI_spec (f1, f2, poe) }
+| f=form                                   { CI_inv  (f) }
+| bad=form COMMA p=form                    { CI_upto (bad,p,None) }
+| bad=form COMMA p=form COMMA q=form       { CI_upto (bad,p,Some q) }
 
 tac_dir:
 | BACKS { Backs }
@@ -3847,6 +3886,7 @@ global_action:
 | typeclass        { Gtypeclass   $1 }
 | tycinstance      { Gtycinstance $1 }
 | operator         { Goperator    $1 }
+| excep            { Gexception   $1 }
 | procop           { Gprocop      $1 }
 | predicate        { Gpredicate   $1 }
 | notation         { Gnotation    $1 }
@@ -3938,6 +3978,11 @@ iplist1_r(X, S):
 %inline empty:
 | /**/ { () }
 
+(* -------------------------------------------------------------------- *)
+%inline splist(X, S):
+| /* empty */     { [] }
+| S xs=iplist1_r(X, S) { xs }
+
 (* -------------------------------------------------------------------- *)
 __rlist1(X, S):                         (* left-recursive *)
 | x=X { [x] }
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 0189383d6..2074b777a 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -160,7 +160,7 @@ and pinstr_r =
   | PSif     of pscond * pscond list * pstmt
   | PSwhile  of pscond
   | PSmatch  of pexpr * psmatch
-  | PSassert of pexpr
+  | PSraise  of pqsymbol * pexpr option
 
 and psmatch = [
   | `Full of (ppattern * pstmt) list
@@ -201,8 +201,7 @@ and pformula_r =
   | PFeqf     of pformula list
   | PFlsless  of pgamepath
   | PFscope   of pqsymbol * pformula
-
-  | PFhoareF   of psymbol option * pformula * pgamepath * pformula
+  | PFhoareF   of psymbol option * pformula * pgamepath * pformula * ((pqsymbol * pformula) list * pformula option)
   | PFehoareF  of psymbol option * pformula * pgamepath * pformula
   | PFequivF   of psymbol option * psymbol option * pformula * (pgamepath * pgamepath) * pformula
   | PFeagerF   of psymbol option * psymbol option * pformula * (pstmt * pgamepath * pgamepath * pstmt) * pformula
@@ -435,6 +434,11 @@ and pprocop = {
   ppo_locality : locality;
 }
 
+type pexception_decl = {
+    pe_name : psymbol;
+    pe_locality : locality;
+  }
+
 type ppred_def =
   | PPabstr of pty list
   | PPconcr of ptybindings * pformula
@@ -537,8 +541,10 @@ type pipattern =
 
 and pspattern = unit
 
+type excep_spec_preds = ((pqsymbol * pformula) list * pformula option)
+
 type call_info =
-  | CI_spec of (pformula * pformula)
+  | CI_spec of (pformula * pformula * excep_spec_preds)
   | CI_inv of pformula
   | CI_upto of (pformula * pformula * pformula option)
 
@@ -691,7 +697,9 @@ type deno_ppterm = (pformula option pair) gppterm
 type conseq_info =
   | CQI_bd of phoarecmp option * pformula
 
-type conseq_ppterm = ((pformula option pair) * (conseq_info) option) gppterm
+type conseq_contra = pformula option * pformula option * excep_spec_preds option
+
+type conseq_ppterm = (conseq_contra * (conseq_info) option) gppterm
 
 (* -------------------------------------------------------------------- *)
 type sim_info = {
@@ -1279,6 +1287,7 @@ type global_action =
   | Gmodule      of pmodule_def_or_decl
   | Ginterface   of pinterface
   | Goperator    of poperator
+  | Gexception   of pexception_decl
   | Gprocop      of pprocop
   | Gpredicate   of ppredicate
   | Gnotation    of pnotation
diff --git a/src/ecPath.ml b/src/ecPath.ml
index 0cb0edf4d..5130a498b 100644
--- a/src/ecPath.ml
+++ b/src/ecPath.ml
@@ -17,6 +17,7 @@ and path_node =
 (* -------------------------------------------------------------------- *)
 let p_equal   = ((==) : path -> path -> bool)
 let p_hash    = fun p -> p.p_tag
+let p_node    = fun p -> p.p_node
 let p_compare = fun p1 p2 -> p_hash p1 - p_hash p2
 
 module Hspath = Why3.Hashcons.Make (struct
@@ -59,6 +60,14 @@ let rec p_ntr_compare (p1 : path) (p2 : path) =
       | n -> n
     end
 
+let rec p_ntr_equal (p1 : path) (p2 : path) =
+  match p1.p_node, p2.p_node with
+  | Psymbol x1, Psymbol x2 ->
+    String.equal x1 x2
+  | Pqname (p1, x1), Pqname (p2, x2) ->
+    p_ntr_equal p1 p2 && String.equal x1 x2
+  | _, _ -> false
+
 (* -------------------------------------------------------------------- *)
 module Mp = Path.M
 module Hp = Path.H
diff --git a/src/ecPath.mli b/src/ecPath.mli
index ef2d2e8c0..1555e9d1a 100644
--- a/src/ecPath.mli
+++ b/src/ecPath.mli
@@ -22,6 +22,7 @@ val poappend : path -> path option -> path
 
 val p_equal       : path -> path -> bool
 val p_compare     : path -> path -> int
+val p_ntr_equal   : path -> path -> bool
 val p_ntr_compare : path -> path -> int
 val p_hash        : path -> int
 
diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml
index b37fbe228..9fa414df6 100644
--- a/src/ecPrinting.ml
+++ b/src/ecPrinting.ml
@@ -213,6 +213,13 @@ module PPEnv = struct
     in
       p_shorten ppe exists (P.toqsymbol p)
 
+  let ex_symb (ppe : t) p =
+    let exists sm =
+      try  EcPath.p_equal (EcEnv.Except.lookup_path sm ppe.ppe_env) p
+      with EcEnv.LookupFailure _ -> false
+    in
+      p_shorten ppe exists (P.toqsymbol p)
+
   let op_symb (ppe : t) p info =
     let specs = [1, EcPath.pqoname (EcPath.prefix EcCoreLib.CI_Bool.p_eq) "<>"] in
 
@@ -619,7 +626,7 @@ let pp_modtype1 (ppe : PPEnv.t) fmt mty =
   pp_msymbol fmt (PPEnv.modtype_symb ppe mty)
 
 (* -------------------------------------------------------------------- *)
-let pp_local (ppe : PPEnv.t) fmt x =
+let pp_local (_ppe : PPEnv.t) fmt x =
   Format.fprintf fmt "%s" (EcIdent.name x)
 
 (* -------------------------------------------------------------------- *)
@@ -1504,6 +1511,10 @@ let lower_left (ppe : PPEnv.t) (t_ty : form -> EcTypes.ty) (f : form) (opprec :
     | _ -> None in
   l_l f opprec
 
+let pp_excep ppe fmt e =
+  let q = PPEnv.ex_symb ppe e in
+  EcSymbols.pp_qsymbol fmt q
+
 (* -------------------------------------------------------------------- *)
 let rec pp_lvalue (ppe : PPEnv.t) fmt lv =
   match lv with
@@ -1545,9 +1556,8 @@ and pp_instr_for_form (ppe : PPEnv.t) fmt i =
         (pp_funname ppe) xp
         (pp_list ",@ " (pp_expr ppe)) args
 
-  | Sassert e ->
-      Format.fprintf fmt "assert %a;"
-        (pp_expr ppe) e
+  | Sraise e ->
+      Format.fprintf fmt "raise %a;" (pp_excep ppe) e
 
   | Swhile (e, _) ->
       Format.fprintf fmt "while (%a) {...}"
@@ -1810,6 +1820,17 @@ and try_pp_notations
     let f    = f_app f eargs f.f_ty in
     pp_form_core_r ppe outer fmt f; true
 
+and ppepoe ppepr fmt (l,d) =
+  let aux fmt (e, f) =
+    Format.fprintf fmt " %a: %a" pp_path e (pp_form ppepr) f
+  in
+  match l , d with
+  | [], None  -> Format.fprintf fmt ""
+  | [], Some f -> Format.fprintf fmt "| %a" (pp_form ppepr) f
+  | _, None -> Format.fprintf fmt "| %a" (pp_list "|" aux) l
+  | _, Some f ->
+    Format.fprintf fmt "| %a | %a" (pp_list "|" aux) l (pp_form ppepr) f
+
 and pp_form_core_r
   (ppe   : PPEnv.t)
   (outer : opprec * iassoc)
@@ -1941,21 +1962,28 @@ and pp_form_core_r
       let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
       let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
       let pm = debug_mode || hf.hf_m.id_symb <> "&hr" in
-      Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@]@]]"
+      let post,poe, d = (hf_po hf).hsi_inv in
+      let poe = DMap.foldi (fun e f c -> (e,f) :: c) poe [] in
+      let d = match d with None -> None | Some f  -> Some f in
+      Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@ %a]@]]"
         (pp_funname ppe) hf.hf_f
         (pp_pl_mem_binding pm ppe) hf.hf_m
         (pp_form ppepr) (hf_pr hf).inv
-        (pp_form ppepo) (hf_po hf).inv
+        (pp_form ppepo) (post)
+        (ppepoe ppepo) (poe, d)
 
   | FhoareS hs ->
       let ppe = PPEnv.push_mem ppe ~active:true hs.hs_m in
+      let post,poe, d = (hs_po hs).hsi_inv in
+      let poe = DMap.foldi (fun e f c -> (e,f) :: c) poe [] in
       let pm = debug_mode || (fst hs.hs_m).id_symb <> "&hr" in
-      Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@]@]]"
+      Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@ %a]@]]"
         (pp_stmt_for_form ppe) hs.hs_s
         (pp_pl_mem_binding pm ppe) (fst hs.hs_m)
         (pp_form ppe) (hs_pr hs).inv
-        (pp_form ppe) (hs_po hs).inv
-    
+        (pp_form ppe) post
+        (ppepoe ppe) (poe, d)
+
   | FeHoareF hf ->
       let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.ehf_m hf.ehf_f ppe.PPEnv.ppe_env in
       let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
@@ -2648,7 +2676,8 @@ let pp_axiom ?(long=false) (ppe : PPEnv.t) fmt (x, ax) =
 (* -------------------------------------------------------------------- *)
 type ppnode1 = [
   | `Asgn     of (EcModules.lvalue * EcTypes.expr)
-  | `Assert   of (EcTypes.expr)
+  | `Raise    of (EcPath.path)
+  | `ERaise   of (EcPath.path * EcTypes.expr)
   | `Call     of (EcModules.lvalue option * P.xpath * EcTypes.expr list)
   | `Rnd      of (EcModules.lvalue * EcTypes.expr)
   | `Abstract of EcIdent.t
@@ -2671,12 +2700,16 @@ let at (ppe : PPEnv.t) n i =
   | Sasgn (lv, e)    , 0 -> Some (`Asgn (lv, e)    , `P, [])
   | Srnd  (lv, e)    , 0 -> Some (`Rnd  (lv, e)    , `P, [])
   | Scall (lv, f, es), 0 -> Some (`Call (lv, f, es), `P, [])
-  | Sassert e        , 0 -> Some (`Assert e        , `P, [])
+  | Sraise e         , 0 -> Some (`Raise e         , `P, [])
   | Sabstract id     , 0 -> Some (`Abstract id     , `P, [])
 
   | Swhile (e, s), 0 -> Some (`While e, `P, s.s_node)
   | Swhile _     , 1 -> Some (`EBlk   , `B, [])
 
+  | Sif (e, {s_node=[{i_node=Sraise p}]}, {s_node= []}), 0 ->
+    Some (`ERaise (p,e), `P, [])
+  | Sif (_, {s_node=[{i_node=Sraise _}]}, {s_node= []}), 1 ->
+    None
   | Sif (e, s, _ ), 0 -> Some (`If e, `P, s.s_node)
   | Sif (_, _, s ), 1 -> begin
       match s.s_node with
@@ -2755,12 +2788,23 @@ let c_split ?width pp x =
     end;
     EcRegexp.split0 (`S "(?:\r?\n)+") (Buffer.contents buf)
 
+let is_op_not p = EcPath.p_equal EcCoreLib.CI_Bool.p_not p
+
+let add_not e =
+  match e.e_node with
+  | Eapp ({e_node= Eop (op, _)}, [e]) when is_op_not op -> e
+  | _ -> EcTypes.e_not e
+
 let pp_i_asgn (ppe : PPEnv.t) fmt (lv, e) =
   Format.fprintf fmt "%a <-@ %a"
     (pp_lvalue ppe) lv (pp_expr ppe) e
 
-let pp_i_assert (ppe : PPEnv.t) fmt e =
-  Format.fprintf fmt "assert (%a)" (pp_expr ppe) e
+let pp_i_raise (ppe : PPEnv.t) fmt (e:EcPath.path) =
+  Format.fprintf fmt "raise %a" (pp_excep ppe) e
+
+let pp_i_eraise (ppe : PPEnv.t) fmt (p,e) =
+  Format.fprintf fmt "raise (%a) %a"
+    (pp_expr ppe) (add_not e) (pp_excep ppe) p
 
 let pp_i_call (ppe : PPEnv.t) fmt (lv, xp, args) =
   match lv with
@@ -2807,7 +2851,8 @@ let pp_i_abstract (_ppe : PPEnv.t) fmt id =
 let c_ppnode1 ~width ppe (pp1 : ppnode1) =
   match pp1 with
   | `Asgn     x -> c_split ~width (pp_i_asgn     ppe) x
-  | `Assert   x -> c_split ~width (pp_i_assert   ppe) x
+  | `Raise    x -> c_split ~width (pp_i_raise    ppe) x
+  | `ERaise   x -> c_split ~width (pp_i_eraise   ppe) x
   | `Call     x -> c_split ~width (pp_i_call     ppe) x
   | `Rnd      x -> c_split ~width (pp_i_rnd      ppe) x
   | `Abstract x -> c_split ~width (pp_i_abstract ppe) x
@@ -2977,32 +3022,58 @@ let pp_post (ppe : PPEnv.t) ?prpo fmt post =
     (omap (fun x -> x.prpo_po) prpo |> odfl false)
     fmt post None
 
+(* -------------------------------------------------------------------- *)
+let pp_poe (ppe : PPEnv.t) ?prpo (fmt: Format.formatter) (poe,d) =
+  begin
+    match d with
+    | None -> ()
+    | Some d ->
+      pp_prpo ppe "_"
+        (omap (fun x -> x.prpo_po) prpo |> odfl false)
+        fmt d None
+  end;
+  List.iter (fun ((e:EcPath.path),f) ->
+      pp_prpo ppe (EcPath.basename e)
+        (omap (fun x -> x.prpo_po) prpo |> odfl false)
+        fmt f None
+    ) poe
+
 (* -------------------------------------------------------------------- *)
 let pp_hoareF (ppe : PPEnv.t) ?prpo fmt hf =
   let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.hf_m hf.hf_f ppe.PPEnv.ppe_env in
   let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
   let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
 
+  let post,poe, d = (hf_po hf).hsi_inv in
+  let poe = DMap.foldi (fun e f c -> (e,f) :: c) poe [] in
+
   Format.fprintf fmt "%a@\n%!" (pp_pre ppepr ?prpo) (hf_pr hf).inv;
   let pm = debug_mode || hf.hf_m.id_symb <> "&hr" in
   Format.fprintf fmt "    %a %a@\n%!" (pp_funname ppe) hf.hf_f (pp_pl_mem_binding pm ppe) hf.hf_m;
-  Format.fprintf fmt "@\n%a%!" (pp_post ppepo ?prpo) (hf_po hf).inv
+  Format.fprintf fmt "@\n%a%!" (pp_post ppepo ?prpo) post;
+  Format.fprintf fmt "@\n%a%!" (pp_poe ppepo ?prpo) (poe,d)
 
 (* -------------------------------------------------------------------- *)
 
 let pp_hoareS (ppe : PPEnv.t) ?prpo fmt hs =
   let ppef = PPEnv.push_mem ppe ~active:true hs.hs_m in
   let ppnode = collect2_s ppef hs.hs_s.s_node [] in
-  let ppnode = c_ppnode ~width:ppe.PPEnv.ppe_width ppef ppnode
-  in
-    Format.fprintf fmt "Context : %a: %a@\n%!" (pp_mem ppe) (fst hs.hs_m) 
-                                               (pp_memtype ppe) (snd hs.hs_m);
-    Format.fprintf fmt "@\n%!";
-    Format.fprintf fmt "%a%!" (pp_pre ppef ?prpo) (hs_pr hs).inv;
-    Format.fprintf fmt "@\n%!";
-    Format.fprintf fmt "%a" (pp_node `Left) ppnode;
-    Format.fprintf fmt "@\n%!";
-    Format.fprintf fmt "%a%!" (pp_post ppef ?prpo) (hs_po hs).inv
+
+  let post,poe, d = (hs_po hs).hsi_inv in
+  let poe = DMap.foldi (fun e f c -> (e,f) :: c) poe [] in
+
+  let ppnode = c_ppnode ~width:ppe.PPEnv.ppe_width ppef ppnode in
+
+  Format.fprintf fmt "Context : %a: %a@\n%!" (pp_mem ppe) (fst hs.hs_m)
+                                             (pp_memtype ppe) (snd hs.hs_m);
+  Format.fprintf fmt "@\n%!";
+  Format.fprintf fmt "%a%!" (pp_pre ppef ?prpo) (hs_pr hs).inv;
+  Format.fprintf fmt "@\n%!";
+  Format.fprintf fmt "%a" (pp_node `Left) ppnode;
+  Format.fprintf fmt "@\n%!";
+  Format.fprintf fmt "%a%!" (pp_post ppef ?prpo) post;
+  Format.fprintf fmt "@\n%!";
+  Format.fprintf fmt "%a%!" (pp_poe ppef ?prpo) (poe,d)
 
 (* -------------------------------------------------------------------- *)
 let pp_eHoareF (ppe : PPEnv.t) ?prpo fmt hf =
@@ -3022,7 +3093,7 @@ let pp_eHoareS (ppe : PPEnv.t) ?prpo fmt hs =
   let ppnode = collect2_s ppef hs.ehs_s.s_node [] in
   let ppnode = c_ppnode ~width:ppe.PPEnv.ppe_width ppef ppnode
   in
-    Format.fprintf fmt "Context : %a: %a@\n%!" (pp_mem ppe) (fst hs.ehs_m) 
+    Format.fprintf fmt "Context : %a: %a@\n%!" (pp_mem ppe) (fst hs.ehs_m)
                                                (pp_memtype ppe) (snd hs.ehs_m);
     Format.fprintf fmt "@\n%!";
     Format.fprintf fmt "%a%!" (pp_pre ppef ?prpo) (ehs_pr hs).inv;
@@ -3395,14 +3466,17 @@ let rec pp_instr_r (ppe : PPEnv.t) fmt i =
       (pp_funname ppe) xp
       (pp_list ",@ " (pp_expr ppe)) args
 
-  | Sassert e ->
-    Format.fprintf fmt "@[<hov 2>assert %a@];"
-      (pp_expr ppe) e
+  | Sraise e ->
+    Format.fprintf fmt "@[<hov 2>raise %a@];" (pp_excep ppe) e
 
   | Swhile (e, s) ->
     Format.fprintf fmt "@[<v>while (@[%a@])%a@]"
       (pp_expr ppe) e (pp_block ppe) s
 
+  | Sif (e, {s_node=[{i_node=Sraise p}]}, {s_node= []})->
+    Format.fprintf fmt "@[<v>raise (@[%a@]) %a@];"
+      (pp_expr ppe) (add_not e) (pp_excep ppe) p
+
   | Sif (e, s1, s2) ->
     let pp_else ppe fmt s =
       match s.s_node with
@@ -3441,7 +3515,7 @@ and pp_block ppe fmt s =
   | [] ->
     Format.fprintf fmt "{}"
 
-  | [ { i_node = (Sasgn _ | Srnd _ | Scall _ | Sassert _ | Sabstract _) } as i ] ->
+  | [ { i_node = (Sasgn _ | Srnd _ | Scall _ | Sraise _ | Sabstract _) } as i ] ->
     Format.fprintf fmt "@;<1 2>%a" (pp_instr ppe) i
 
   | _ ->
@@ -3558,6 +3632,9 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) =
   | EcTheory.Th_operator (id, op) ->
       pp_opdecl ppe fmt (EcPath.pqname p id, op)
 
+  | EcTheory.Th_exception (_id, _e) ->
+    Format.fprintf fmt "exception <FIXME>."
+
   | EcTheory.Th_axiom (id, ax) ->
       pp_axiom ppe fmt (EcPath.pqname p id, ax)
 
diff --git a/src/ecProcSem.ml b/src/ecProcSem.ml
index 26df3e622..2fb1af20f 100644
--- a/src/ecProcSem.ml
+++ b/src/ecProcSem.ml
@@ -191,7 +191,7 @@ let rec translate_i (env : senv) (cont : senv -> mode * expr) (i : instr) =
 
   | Swhile    _
   | Smatch    _
-  | Sassert   _
+  | Sraise   _
   | Sabstract _
   | Scall     _ ->
      raise SemNotSupported;
diff --git a/src/ecProofTyping.ml b/src/ecProofTyping.ml
index abc49d124..0ea3aee5b 100644
--- a/src/ecProofTyping.ml
+++ b/src/ecProofTyping.ml
@@ -7,6 +7,7 @@ open EcEnv
 open EcCoreGoal
 open EcAst
 open EcParsetree
+open EcMaps
 
 module Msym = EcSymbols.Msym
 
@@ -83,6 +84,21 @@ let pf_process_exp pe hyps mode oty e =
 let pf_process_pattern pe hyps fp =
   Exn.recast_pe pe hyps (fun () -> process_pattern hyps fp)
 
+let pf_process_poe tc hyps ty (epost,d)=
+  let env  = LDecl.toenv hyps in
+  let aux acc (e,f) =
+    let _,p = EcTyping.except_genpath env e in
+    match DMap.find p acc with
+    | exception Not_found ->
+      let f = pf_process_form !!tc hyps ty f in
+      DMap.add p f acc
+    | _ -> tc_error !!tc "duplicated exception"
+  in
+  let epost = List.fold aux DMap.empty epost in
+  match d with
+  | None -> (epost, None)
+  | Some d -> (epost, Some (pf_process_form !!tc hyps ty d))
+
 (* ------------------------------------------------------------------ *)
 let tc1_process_form_opt ?mv tc oty pf =
   Exn.recast_tc1 tc (fun hyps -> process_form_opt ?mv hyps pf oty)
@@ -164,7 +180,9 @@ let tc1_process_Xhl_form ?side tc ty pf =
 
   let mv =
     match concl.f_node with
-    | FhoareS   hs -> Some ((hs_pr hs).inv , (hs_po hs).inv )
+    | FhoareS   hs ->
+      let (po, _, _) = (hs_po hs).hsi_inv in
+      Some ((hs_pr hs).inv , po )
     | FeHoareS  hs -> Some ((ehs_pr hs).inv, (ehs_po hs).inv)
     | FbdHoareS hs -> Some ((bhs_pr hs).inv, (bhs_po hs).inv)
     | _            -> None
@@ -250,3 +268,24 @@ let destruct_exists ?(reduce = true) hyps fp : dexists option =
     | _ -> raise NoMatch
   in
     lazy_destruct ~reduce hyps doit fp
+
+(* -------------------------------------------------------------------- *)
+let merge2_poe_list f (poe1,d1) (poe2,d2) =
+  let get_default d =
+    match d with
+    | Some d -> d
+    | None ->  failwith "no default exception"
+  in
+  let aux _ a b =
+    match a,b with
+    | Some a, Some b -> Some (f b a)
+    | Some a, None -> Some (f (get_default d2) a)
+    | None, Some b -> Some (f b (get_default d1))
+    | None, None -> assert false
+  in
+  let epost = DMap.merge aux poe1 poe2 in
+  let poe = List.map snd ( DMap.bindings epost) in
+  match d2, d1 with
+  | None, _ -> poe
+  | Some d2, Some d1 -> f d2 d1 :: poe
+  | _, _ -> failwith "no default exception"
diff --git a/src/ecProofTyping.mli b/src/ecProofTyping.mli
index 359b57045..d32f72834 100644
--- a/src/ecProofTyping.mli
+++ b/src/ecProofTyping.mli
@@ -5,6 +5,7 @@ open EcDecl
 open EcEnv
 open EcCoreGoal
 open EcAst
+open EcMaps
 
 (* -------------------------------------------------------------------- *)
 type ptnenv = ty Mid.t * EcUnify.unienv
@@ -32,6 +33,7 @@ val pf_process_xreal    : proofenv -> ?mv:metavs -> LDecl.hyps -> pformula -> fo
 
 val pf_process_exp      : proofenv -> LDecl.hyps -> [`InProc|`InOp] -> ty option -> pexpr -> expr
 val pf_process_pattern  : proofenv -> LDecl.hyps -> pformula -> ptnenv * form
+val pf_process_poe      : tcenv1 -> LDecl.hyps -> ty -> excep_spec_preds -> (EcPath.path, form) DMap.t * form option
 
 (* Typing in the [proofenv] implies for the [tcenv].
  * Typing exceptions are recasted in the proof env. context *)
@@ -79,3 +81,11 @@ type dexists = [
 
 val destruct_product: ?reduce:bool -> EcEnv.LDecl.hyps -> form -> dproduct option
 val destruct_exists : ?reduce:bool -> EcEnv.LDecl.hyps -> form -> dexists  option
+
+(* -------------------------------------------------------------------- *)
+
+val merge2_poe_list :
+  (form -> form -> form) ->
+  (EcPath.path, form) DMap.t * form option ->
+  (EcPath.path, form) DMap.t * form option ->
+  form list
diff --git a/src/ecReduction.ml b/src/ecReduction.ml
index 976c52312..b0be1be37 100644
--- a/src/ecReduction.ml
+++ b/src/ecReduction.ml
@@ -243,8 +243,7 @@ end) = struct
         with E.NotConv -> false
       end
 
-    | Sassert a1, Sassert a2 ->
-        for_expr env alpha ~norm a1 a2
+    | Sraise e1, Sraise e2 -> EcPath.p_equal e1 e2
 
     | Sabstract id1, Sabstract id2 ->
         EcIdent.id_equal id1 id2
@@ -555,13 +554,13 @@ let is_alpha_eq ?(subst=Fsubst.f_subst_id) hyps f1 f2 =
       check_xp env subst hf1.hf_f hf2.hf_f;
       let subst = check_m_binding subst hf1.hf_m hf2.hf_m in
       aux env subst (hf_pr hf1).inv (hf_pr hf2).inv;
-      aux env subst (hf_po hf1).inv (hf_po hf2).inv
+      iter2_poe (aux env subst) (hf_po hf1).hsi_inv (hf_po hf2).hsi_inv
 
     | FhoareS hs1, FhoareS hs2 ->
       check_s env subst hs1.hs_s hs2.hs_s;
       let subst = check_me_binding env subst hs1.hs_m hs2.hs_m in
       aux env subst (hs_pr hs1).inv (hs_pr hs2).inv;
-      aux env subst (hs_po hs1).inv (hs_po hs2).inv
+      iter2_poe (aux env subst) (hs_po hs1).hsi_inv (hs_po hs2).hsi_inv
 
     | FeHoareF hf1, FeHoareF hf2 ->
       check_xp env subst hf1.ehf_f hf2.ehf_f;
@@ -1344,6 +1343,22 @@ let ztuple args1 args2 ty stk = zpush Ztuple [] args1 args2 ty stk
 let zproj i ty stk = zpush (Zproj i) [] [] [] ty stk
 let zhl f fs1 fs2 stk = zpush (Zhl f) [] fs1 fs2 f.f_ty stk
 
+let zpoe (_,epost,d) dpoe =
+  let d,dpoe =
+    match d,dpoe with
+    | None,_ -> None,dpoe
+    | _ ,h::q -> Some h, q
+    | _, _ -> assert false
+  in
+  let key = List.map fst (EcMaps.DMap.bindings epost) in
+  let poe = List.fold_left2
+    (fun m a b -> EcMaps.DMap.add a b m)
+    EcMaps.DMap.empty
+    key
+    dpoe
+  in
+  (poe,d)
+
 let zpop ri side f hd =
   let args =
     match side with
@@ -1360,12 +1375,14 @@ let zpop ri side f hd =
   | Zapp, f1::args     -> f_app f1 args hd.se_ty
   | Ztuple, args       -> f_tuple args
   | Zproj i, [f1]      -> f_proj f1 i hd.se_ty
-  | Zhl {f_node = FhoareF hf}, [pr;po] ->
+  | Zhl {f_node = FhoareF hf}, (pr :: po :: dpoe) ->
     let m = hf.hf_m in
-    f_hoareF {m;inv=pr} hf.hf_f {m;inv=po}
-  | Zhl {f_node = FhoareS hs}, [pr;po] ->
+    let poe,d = zpoe (hf_po hf).hsi_inv dpoe in
+    f_hoareF {m;inv=pr} hf.hf_f {hsi_m = m;hsi_inv=(po,poe,d)}
+  | Zhl {f_node = FhoareS hs}, (pr :: po :: dpoe) ->
     let m = fst hs.hs_m in
-    f_hoareS (snd hs.hs_m) {m;inv=pr} hs.hs_s {m;inv=po}
+    let poe,d = zpoe (hs_po hs).hsi_inv dpoe in
+    f_hoareS (snd hs.hs_m) {m;inv=pr} hs.hs_s {hsi_m=m;hsi_inv=(po,poe,d)}
   | Zhl {f_node = FeHoareF hf}, [pr;po] ->
     let m = hf.ehf_m in
     f_eHoareF {m;inv=pr} hf.ehf_f {m;inv=po}
@@ -1483,18 +1500,37 @@ let rec conv ri env f1 f2 stk =
         && EcMemory.mem_equal mem1 mem2 ->
       conv_next ri env f1 stk
 
-  | FhoareF hf1, FhoareF hf2 when EqTest_i.for_xp env hf1.hf_f hf2.hf_f ->
+  | FhoareF hf1, FhoareF hf2
+    when EqTest_i.for_xp env hf1.hf_f hf2.hf_f &&
+    forall2_poe (fun _ _ -> true) (hf_po hf1).hsi_inv (hf_po hf2).hsi_inv ->
     let pr2 = (ss_inv_rebind (hf_pr hf2) hf1.hf_m).inv in
-    let po2 = (ss_inv_rebind (hf_po hf2) hf1.hf_m).inv in
-    conv ri env (hf_pr hf1).inv pr2 (zhl f1 [(hf_po hf1).inv] [po2] stk)
+    let po2 = (hs_inv_rebind (hf_po hf2) hf1.hf_m).hsi_inv in
+    let aux (post,poe,d) =
+      let poe =
+        List.map snd (EcMaps.DMap.bindings poe)
+      in
+      match d with None -> post :: poe | Some d -> post :: d :: poe
+    in
+    let lf1 = aux (hf_po hf1).hsi_inv in
+    let lf2 = aux po2 in
+    let stk = (zhl f1 lf1 lf2 stk) in
+    conv ri env (hf_pr hf1).inv pr2 stk
 
-  | FhoareS hs1, FhoareS hs2
-      when EqTest_i.for_stmt env hs1.hs_s hs2.hs_s ->
+  | FhoareS hs1, FhoareS hs2 when EqTest_i.for_stmt env hs1.hs_s hs2.hs_s ->
     begin match check_me_binding env Fsubst.f_subst_id hs1.hs_m hs2.hs_m with
     | _subst ->
       let pr2 = (ss_inv_rebind (hs_pr hs2) (fst hs1.hs_m)).inv in
-      let po2 = (ss_inv_rebind (hs_po hs2) (fst hs1.hs_m)).inv in
-      conv ri env (hs_pr hs1).inv pr2 (zhl f1 [(hs_po hs1).inv] [po2] stk)
+      let po2 = (hs_inv_rebind (hs_po hs2) (fst hs1.hs_m)).hsi_inv in
+      let aux (post,poe,d) =
+        let poe =
+          List.map snd (EcMaps.DMap.bindings poe)
+        in
+        match d with None -> post :: poe | Some d -> post :: d :: poe
+      in
+      let lf1 = aux (hs_po hs1).hsi_inv in
+      let lf2 = aux po2 in
+      let stk = (zhl f1 lf1 lf2 stk) in
+      conv ri env (hs_pr hs1).inv pr2 stk
     | exception NotConv -> force_head ri env f1 f2 stk
     end
 
@@ -1825,6 +1861,11 @@ let ts_inv_alpha_eq hyps (inv1 : ts_inv) (inv2 : ts_inv) =
   let subst = Fsubst.f_bind_mem Fsubst.f_subst_id inv1.ml inv2.ml in
   let subst = Fsubst.f_bind_mem subst inv1.mr inv2.mr in
   is_alpha_eq ~subst hyps inv2.inv inv1.inv
+
+let hs_inv_alpha_eq hyps (inv1 : hs_inv) (inv2 : hs_inv) =
+  let subst = Fsubst.f_bind_mem Fsubst.f_subst_id inv1.hsi_m inv2.hsi_m in
+  forall2_poe (is_alpha_eq ~subst hyps) inv2.hsi_inv inv1.hsi_inv
+
 module EqTest = struct
   include EqTest_base
 
diff --git a/src/ecReduction.mli b/src/ecReduction.mli
index 27dea22f8..ceb057d24 100644
--- a/src/ecReduction.mli
+++ b/src/ecReduction.mli
@@ -118,3 +118,4 @@ val xconv : xconv -> LDecl.hyps -> form -> form -> bool
 
 val ss_inv_alpha_eq : LDecl.hyps -> ss_inv -> ss_inv -> bool
 val ts_inv_alpha_eq : LDecl.hyps -> ts_inv -> ts_inv -> bool
+val hs_inv_alpha_eq : LDecl.hyps -> hs_inv -> hs_inv -> bool
diff --git a/src/ecScope.ml b/src/ecScope.ml
index d8a4676f1..26c25d178 100644
--- a/src/ecScope.ml
+++ b/src/ecScope.ml
@@ -1501,6 +1501,7 @@ module Op = struct
     tyop, List.rev !axs, scope
 
 
+
   let add_opsem ?(src : string option) (scope : scope) (op : pprocop located) =
     let module Sem = EcProcSem in
 
@@ -1617,6 +1618,14 @@ module Op = struct
            let res   = f_pvar pv_res sig_.fs_ret m in
            let args  = f_pvar pv_arg sig_.fs_arg m in
 
+           let post =
+             f_eq
+               res.inv
+               (f_app
+                  (f_op oppath [] opdecl.op_ty)
+                  (List.map (fun (x, ty) -> f_local x ty) locs)
+                  sig_.fs_ret)
+           in
            f_forall
              (List.map (fun (x, ty) -> (x, GTty ty)) locs)
              (f_hoareF
@@ -1624,12 +1633,7 @@ module Op = struct
                    args.inv
                    (f_tuple (List.map (fun (x, ty) -> f_local x ty) locs)))}
                 f
-                {m;inv=(f_eq
-                   res.inv
-                   (f_app
-                      (f_op oppath [] opdecl.op_ty)
-                      (List.map (fun (x, ty) -> f_local x ty) locs)
-                      sig_.fs_ret))})
+                {hsi_m=m;hsi_inv= empty_poe post})
          in
 
          let prax = EcDecl.{
@@ -1649,6 +1653,25 @@ module Op = struct
     scope
 end
 
+(* -------------------------------------------------------------------- *)
+module Except = struct
+  module TT = EcTyping
+
+  let bind ?(import = true) (scope : scope) ((x, e) : _ * excep) =
+    assert (scope.sc_pr_uc = None);
+    let item = EcTheory.mkitem ~import (EcTheory.Th_exception (x, e)) in
+    { scope with sc_env = EcSection.add_item item scope.sc_env; }
+
+  let add (scope : scope) (pe : pexception_decl located) =
+    assert (scope.sc_pr_uc = None);
+    let pe = pe.pl_desc in
+    let lc = pe.pe_locality in
+    let e   = EcDecl.mk_except lc in
+    let scope = bind scope (unloc pe.pe_name, e) in
+    e, scope
+
+end
+
 (* -------------------------------------------------------------------- *)
 module Pred = struct
   module TT = EcTyping
diff --git a/src/ecScope.mli b/src/ecScope.mli
index d64007674..e84c7dfdf 100644
--- a/src/ecScope.mli
+++ b/src/ecScope.mli
@@ -114,6 +114,11 @@ module Op : sig
   val add_opsem : ?src:string -> scope -> pprocop located -> scope
 end
 
+(* -------------------------------------------------------------------- *)
+module Except : sig
+  val add : scope -> pexception_decl located -> EcDecl.excep * scope
+end
+
 (* -------------------------------------------------------------------- *)
 module Pred : sig
   val add : ?src:string -> scope -> ppredicate located -> EcDecl.operator * scope
diff --git a/src/ecSection.ml b/src/ecSection.ml
index 3534ea58e..df3b93b13 100644
--- a/src/ecSection.ml
+++ b/src/ecSection.ml
@@ -18,6 +18,7 @@ type cbarg = [
   | `Type       of path
   | `Op         of path
   | `Ax         of path
+  | `Ex         of path
   | `Module     of mpath
   | `ModuleType of path
   | `Typeclass  of path
@@ -39,6 +40,7 @@ let pp_cbarg env fmt (who : cbarg) =
   | `Type p -> Format.fprintf fmt "type %a" (EcPrinting.pp_tyname ppe) p
   | `Op   p -> Format.fprintf fmt "operator %a" (EcPrinting.pp_opname ppe) p
   | `Ax   p -> Format.fprintf fmt "lemma/axiom %a" (EcPrinting.pp_axname ppe) p
+  | `Ex   _p -> Format.fprintf fmt "TODO"
   | `Module mp ->
     let ppe =
       match mp.m_top with
@@ -157,8 +159,7 @@ let rec on_instr (cb : cb) (i : instr)=
       on_lv cb lv;
       on_expr cb e
 
-  | Sassert e ->
-      on_expr cb e
+  | Sraise _ -> ()
 
   | Scall (lv, f, args) ->
       lv |> oiter (on_lv cb);
@@ -220,12 +221,12 @@ let rec on_form (cb : cb) (f : EcFol.form) =
 
   and on_hf cb hf =
     on_form cb (hf_pr hf).inv;
-    on_form cb (hf_po hf).inv;
+    iter_poe (on_form cb) (hf_po hf).hsi_inv;
     on_xp cb hf.EcAst.hf_f
 
   and on_hs cb hs =
     on_form cb (hs_pr hs).inv;
-    on_form cb (hs_po hs).inv;
+    iter_poe (on_form cb) (hs_po hs).hsi_inv;
     on_stmt cb hs.EcAst.hs_s;
     on_memenv cb hs.EcAst.hs_m
 
@@ -507,6 +508,7 @@ let locality (env : EcEnv.env) (who : cbarg) =
   | `Type p -> (EcEnv.    Ty.by_path p env).tyd_loca
   | `Op   p -> (EcEnv.    Op.by_path p env).op_loca
   | `Ax   p -> (EcEnv.    Ax.by_path p env).ax_loca
+  | `Ex   _p -> assert false
   | `Typeclass  p -> ((EcEnv.TypeClass.by_path p env).tc_loca :> locality)
   | `Module mp    ->
     begin match EcEnv.Mod.by_mpath_opt mp env with
@@ -1043,6 +1045,7 @@ let rec set_lc_item lc_override item =
     match item.ti_item with
     | Th_type         (s,ty) -> Th_type      (s, { ty with tyd_loca = set_lc lc_override ty.tyd_loca })
     | Th_operator     (s,op) -> Th_operator  (s, { op with op_loca  = set_lc lc_override op.op_loca   })
+    | Th_exception     (s,e) -> Th_exception (s, { e  with e_loca   = set_lc lc_override e.e_loca   })
     | Th_axiom        (s,ax) -> Th_axiom     (s, { ax with ax_loca  = set_lc lc_override ax.ax_loca   })
     | Th_modtype      (s,ms) -> Th_modtype   (s, { ms with tms_loca = set_lc lc_override ms.tms_loca  })
     | Th_module          me  -> Th_module        { me with tme_loca = set_lc lc_override me.tme_loca  }
@@ -1102,6 +1105,7 @@ type can_depend = {
     d_ty    : locality list;
     d_op    : locality list;
     d_ax    : locality list;
+    d_ex    : locality list;
     d_sc    : locality list;
     d_mod   : locality list;
     d_modty : locality list;
@@ -1112,6 +1116,7 @@ let cd_glob =
   { d_ty    = [`Global];
     d_op    = [`Global];
     d_ax    = [`Global];
+    d_ex    = [`Global];
     d_sc    = [`Global];
     d_mod   = [`Global];
     d_modty = [`Global];
@@ -1122,6 +1127,7 @@ let can_depend (cd : can_depend) = function
   | `Type       _ -> cd.d_ty
   | `Op         _ -> cd.d_op
   | `Ax         _ -> cd.d_ax
+  | `Ex         _ -> cd.d_ex
   | `Sc         _ -> cd.d_sc
   | `Module     _ -> cd.d_mod
   | `ModuleType _ -> cd.d_modty
@@ -1154,6 +1160,7 @@ let check_tyd scenv prefix name tyd =
         d_ty    = [`Declare; `Global];
         d_op    = [`Global];
         d_ax    = [];
+        d_ex    = [];
         d_sc    = [];
         d_mod   = [`Global];
         d_modty = [];
@@ -1200,6 +1207,7 @@ let check_op scenv prefix name op =
         d_ty    = [`Declare; `Global];
         d_op    = [`Declare; `Global];
         d_ax    = [];
+        d_ex    = [];
         d_sc    = [];
         d_mod   = [`Declare; `Global];
         d_modty = [];
@@ -1212,6 +1220,7 @@ let check_op scenv prefix name op =
         d_ty    = [`Declare; `Global];
         d_op    = [`Declare; `Global];
         d_ax    = [];
+        d_ex    = [];
         d_sc    = [];
         d_mod   = [`Global];
         d_modty = [];
@@ -1231,6 +1240,7 @@ let check_ax (scenv : scenv) (prefix : path) (name : symbol) (ax : axiom) =
       d_ty    = [`Declare; `Global];
       d_op    = [`Declare; `Global];
       d_ax    = [];
+      d_ex    = [];
       d_sc    = [];
       d_mod   = [`Declare; `Global];
       d_modty = [`Global];
@@ -1283,6 +1293,7 @@ let check_module scenv prefix tme =
         { d_ty    = [`Global];
           d_op    = [`Global];
           d_ax    = [];
+          d_ex    = [];
           d_sc    = [];
           d_mod   = [`Global]; (* FIXME section: add local *)
           d_modty = [`Global];
@@ -1344,6 +1355,7 @@ let add_item_ ?(override_locality=None) (item : theory_item) (scenv:scenv) =
     | Th_type    (s,tyd)     -> EcEnv.Ty.bind ~import s tyd env
     | Th_operator (s,op)     -> EcEnv.Op.bind ~import s op env
     | Th_axiom   (s, ax)     -> EcEnv.Ax.bind ~import s ax env
+    | Th_exception (s,e)     -> EcEnv.Except.bind ~import s e env
     | Th_modtype (s, ms)     -> EcEnv.ModTy.bind ~import s ms env
     | Th_module       me     -> EcEnv.Mod.bind ~import me.tme_expr.me_name me env
     | Th_typeclass(s,tc)     -> EcEnv.TypeClass.bind ~import s tc env
@@ -1372,6 +1384,7 @@ let rec generalize_th_item (to_gen : to_gen) (prefix : path) (th_item : theory_i
     match th_item.ti_item with
     | Th_type tydecl     -> generalize_tydecl to_gen prefix tydecl
     | Th_operator opdecl -> generalize_opdecl to_gen prefix opdecl
+    | Th_exception _     -> assert false
     | Th_axiom  ax       -> generalize_axiom  to_gen prefix ax
     | Th_modtype ms      -> generalize_modtype to_gen ms
     | Th_module me       -> generalize_module  to_gen prefix me
@@ -1476,6 +1489,7 @@ let check_item scenv item =
   match item.ti_item with
   | Th_type     (s,tyd) -> check_tyd scenv prefix s tyd
   | Th_operator  (s,op) -> check_op  scenv prefix s op
+  | Th_exception _      -> ()
   | Th_axiom    (s, ax) -> check_ax  scenv prefix s ax
   | Th_modtype  (s, ms) -> check_modtype scenv prefix s ms
   | Th_module        me -> check_module  scenv prefix me
@@ -1521,6 +1535,7 @@ let add_decl_mod id mt scenv =
       d_ty    = [`Global];
       d_op    = [`Global];
       d_ax    = [];
+      d_ex    = [];
       d_sc    = [];
       d_mod   = [`Declare; `Global];
       d_modty = [`Global];
diff --git a/src/ecSubst.ml b/src/ecSubst.ml
index 45bdb2f74..7438ddff8 100644
--- a/src/ecSubst.ml
+++ b/src/ecSubst.ml
@@ -426,8 +426,7 @@ and subst_instr (s : subst) (i : instr) : instr =
 
      i_match (e, bs)
 
-  | Sassert e ->
-     i_assert (subst_expr s e)
+  | Sraise e -> i_raise e
 
   | Sabstract _ ->
      i
@@ -533,14 +532,14 @@ let rec subst_form (s : subst) (f : form) =
      let hf_f  = subst_xpath s hf.hf_f in
      let s = add_memory s hf.hf_m hf.hf_m in
      let hf_pr = map_ss_inv1 (subst_form s) (hf_pr hf) in
-     let hf_po = map_ss_inv1 (subst_form s) (hf_po hf) in
+     let hf_po = map_hs_inv1 (subst_form s) (hf_po hf) in
      f_hoareF hf_pr hf_f hf_po
 
   | FhoareS hs ->
      let hs_s = subst_stmt s hs.hs_s in
      let s, (_,mt) = subst_memtype s hs.hs_m in
      let hs_pr = map_ss_inv1 (subst_form s) (hs_pr hs) in
-     let hs_po = map_ss_inv1 (subst_form s) (hs_po hs) in
+     let hs_po = map_hs_inv1 (subst_form s) (hs_po hs) in
      f_hoareS mt hs_pr hs_s hs_po
 
   | FbdHoareF bhf ->
@@ -1024,6 +1023,9 @@ let rec subst_theory_item_r (s : subst) (item : theory_item_r) =
   | Th_operator (x, op) ->
       Th_operator (x, subst_op s op)
 
+  | Th_exception (e, es) ->
+      Th_exception (e, es)
+
   | Th_axiom (x, ax) ->
       Th_axiom (x, subst_ax s ax)
 
@@ -1092,10 +1094,16 @@ let subst_ts_inv (s : subst) (inv : ts_inv) =
   let s = add_memory s inv.mr inv.mr in
   { inv = subst_form s inv.inv; ml = inv.ml; mr = inv.mr; }
 
+let subst_hs_inv (s : subst) (inv : hs_inv) =
+  let s = add_memory s inv.hsi_m inv.hsi_m in
+  { hsi_inv = map_poe (subst_form s) inv.hsi_inv; hsi_m = inv.hsi_m }
+
+
 let subst_inv (s : subst) (inv : inv) =
   match inv with
   | Inv_ss inv -> Inv_ss (subst_ss_inv s inv)
   | Inv_ts inv -> Inv_ts (subst_ts_inv s inv)
+  | Inv_hs inv -> Inv_hs (subst_hs_inv s inv)
 
 (* -------------------------------------------------------------------- *)
 let init_tparams (params : (EcIdent.t * ty) list) : subst =
@@ -1181,4 +1189,12 @@ let ss_inv_forall_ml_ts_inv menvl inv =
 
 let ss_inv_forall_mr_ts_inv menvr inv =
   let inv' = f_forall_mems [menvr] (ts_inv_rebind_right inv (fst menvr)).inv in
-  { inv=inv'; m=inv.ml }
\ No newline at end of file
+  { inv=inv'; m=inv.ml }
+
+(* -------------------------------------------------------------------- *)
+let hs_inv_rebind ({hsi_inv;hsi_m}: hs_inv) (m': memory) : hs_inv =
+  if m' = hsi_m then
+    { hsi_inv; hsi_m }
+  else
+    let hsi_inv = map_poe (subst_form (add_memory empty hsi_m m')) hsi_inv in
+    { hsi_inv; hsi_m = m' }
diff --git a/src/ecSubst.mli b/src/ecSubst.mli
index 5ad3879db..673fb6996 100644
--- a/src/ecSubst.mli
+++ b/src/ecSubst.mli
@@ -96,3 +96,6 @@ val f_forall_mems_ts_inv : memenv -> memenv -> ts_inv -> form
 
 val ss_inv_forall_ml_ts_inv : memenv -> ts_inv -> ss_inv
 val ss_inv_forall_mr_ts_inv : memenv -> ts_inv -> ss_inv
+
+(* -------------------------------------------------------------------- *)
+val hs_inv_rebind : hs_inv -> memory -> hs_inv
diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml
index a2f24e593..10566682e 100644
--- a/src/ecThCloning.ml
+++ b/src/ecThCloning.ml
@@ -437,6 +437,8 @@ end = struct
          let ovrd = (ovrd, mode) in
          nt_ovrd oc (proofs, evc) (loced (xdth @ prefix, x)) ovrd
 
+      | Th_exception _ ->  (proofs, evc)
+
       | Th_axiom (x, _) ->
         let axd = loced (thd @ prefix, x) in
         let name = (loced (xdth @ prefix, x)) in
diff --git a/src/ecTheory.ml b/src/ecTheory.ml
index ffe226d06..4f5c4f798 100644
--- a/src/ecTheory.ml
+++ b/src/ecTheory.ml
@@ -21,6 +21,7 @@ and theory_item = {
 and theory_item_r =
   | Th_type      of (symbol * tydecl)
   | Th_operator  of (symbol * operator)
+  | Th_exception of (symbol * excep)
   | Th_axiom     of (symbol * axiom)
   | Th_modtype   of (symbol * top_module_sig)
   | Th_module    of top_module_expr
diff --git a/src/ecTheory.mli b/src/ecTheory.mli
index f246ee3f4..2b8551ed4 100644
--- a/src/ecTheory.mli
+++ b/src/ecTheory.mli
@@ -17,6 +17,7 @@ and theory_item = {
 and theory_item_r =
   | Th_type      of (symbol * tydecl)
   | Th_operator  of (symbol * operator)
+  | Th_exception of (symbol * excep)
   | Th_axiom     of (symbol * axiom)
   | Th_modtype   of (symbol * top_module_sig)
   | Th_module    of top_module_expr
diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml
index 0eff5cf66..fd726eb9d 100644
--- a/src/ecTheoryReplay.ml
+++ b/src/ecTheoryReplay.ml
@@ -108,7 +108,7 @@ end = struct
     if rlen <> nlen then
       raise (Incompatible (NotSameNumberOfTyParam (rlen, nlen)))
 
-  let for_params 
+  let for_params
     (hyps : hyps)
     (s    : EcSubst.subst)
     (p1   : (EcIdent.ident * ty) list)
@@ -785,6 +785,14 @@ and replay_ntd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oont) =
       (subst, ops, proofs, scope)
   end
 
+
+(* -------------------------------------------------------------------- *)
+and replay_excep
+  (ove : _ ovrenv) (subst, ops, proofs, scope) (import, name, excep)
+=
+  let scope = ove.ovre_hooks.hadd_item scope ~import (Th_exception (name, excep)) in
+  (subst, ops, proofs, scope)
+
 (* -------------------------------------------------------------------- *)
 and replay_axd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, ax) =
   let scenv = ove.ovre_hooks.henv scope in
@@ -1100,6 +1108,9 @@ and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) (hidden, item) =
   | Th_operator (x, ({ op_kind = OB_nott _} as oont)) ->
      replay_ntd ove (subst, ops, proofs, scope) (import, x, oont)
 
+  | Th_exception (x, e) ->
+    replay_excep ove (subst, ops, proofs, scope) (import, x, e)
+
   | Th_axiom (x, ax) ->
      replay_axd ove (subst, ops, proofs, scope) (import, x, ax)
 
diff --git a/src/ecTypes.ml b/src/ecTypes.ml
index 87efc57be..1abff28aa 100644
--- a/src/ecTypes.ml
+++ b/src/ecTypes.ml
@@ -387,6 +387,9 @@ let e_app x args ty =
 let e_app_op ?(tyargs=[]) op args ty =
   e_app (e_op op tyargs (toarrow (List.map e_ty args) ty)) args ty
 
+let e_not e =
+  e_app (e_op EcCoreLib.CI_Bool.p_not [] tbool) [e] tbool
+
 (* -------------------------------------------------------------------- *)
 module Reals : sig
   val of_lit : EcBigInt.zint -> expr
diff --git a/src/ecTypes.mli b/src/ecTypes.mli
index 34b7b4cbf..6ea1d38b7 100644
--- a/src/ecTypes.mli
+++ b/src/ecTypes.mli
@@ -173,6 +173,7 @@ val e_local    : EcIdent.t -> ty -> expr
 val e_var      : prog_var -> ty -> expr
 val e_op       : EcPath.path -> ty list -> ty -> expr
 val e_app      : expr -> expr list -> ty -> expr
+val e_not      : expr -> expr
 val e_let      : lpattern -> expr -> expr -> expr
 val e_tuple    : expr list -> expr
 val e_if       : expr -> expr -> expr -> expr
diff --git a/src/ecTyping.ml b/src/ecTyping.ml
index 75f594a10..0af93131a 100644
--- a/src/ecTyping.ml
+++ b/src/ecTyping.ml
@@ -139,6 +139,7 @@ type tyerror =
 | DuplicatedTyVar
 | DuplicatedLocal        of symbol
 | DuplicatedField        of symbol
+| DuplicatedException    of qsymbol
 | NonLinearPattern
 | LvNonLinear
 | NonUnitFunWithoutReturn
@@ -153,6 +154,7 @@ type tyerror =
 | UnknownModName         of qsymbol
 | UnknownTyModName       of qsymbol
 | UnknownFunName         of qsymbol
+| UnknownExceptionName   of qsymbol
 | UnknownModVar          of qsymbol
 | UnknownMemName         of symbol
 | InvalidFunAppl         of funapp_error
@@ -283,8 +285,7 @@ let (_i_inuse, s_inuse, se_inuse) =
       let map = List.fold_left (fun map -> s_inuse map |- snd) map bs in
         map
 
-    | Sassert e ->
-      se_inuse map e
+    | Sraise _ -> map
 
     | Sabstract _ ->
       assert false (* FIXME *)
@@ -1466,6 +1467,12 @@ let trans_gamepath (env : EcEnv.env) gp =
           tyerror gp.pl_loc env (UnknownFunName (modsymb, funsymb));
         EcPath.xpath mpath funsymb
 
+let except_genpath env name =
+  let symb = unloc name in
+  match EcEnv.Except.lookup_opt symb env with
+  | None -> tyerror name.pl_loc env (UnknownExceptionName symb)
+  | Some (p,_) -> symb, p
+
 (* -------------------------------------------------------------------- *)
 let trans_oracle (env : EcEnv.env) (m,f) =
   let msymbol = mk_loc (loc m) [m,None] in
@@ -2749,10 +2756,15 @@ and transinstr
       [ i_match (e, branches) ]
     end
 
-  | PSassert pe ->
+  | PSraise (name,pe) ->
+    let _,path = except_genpath env name in
+    match pe with
+    | None ->  [i_raise path]
+    | Some pe ->
       let e, ety = transexp env `InProc ue pe in
+      let e = e_not e in
       unify_or_fail env ue pe.pl_loc ~expct:tbool ety;
-      [ i_assert e ]
+      [i_if (e, stmt [i_raise path], stmt [])]
 
 (* -------------------------------------------------------------------- *)
 and trans_pv env { pl_desc = x; pl_loc = loc } =
@@ -3442,7 +3454,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt =
         unify_or_fail env ue event.pl_loc ~expct:tbool event'.inv.f_ty;
         f_pr memid fpath (f_tuple args) event'
 
-    | PFhoareF (m, pre, gp, post) ->
+    | PFhoareF (m, pre, gp, post, (eposts,dpost)) ->
         if mode <> `Form then
           tyerror f.pl_loc env (NotAnExpression `Logic);
         let fpath = trans_gamepath env gp in
@@ -3451,9 +3463,28 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt =
         let penv, qenv = EcEnv.Fun.hoareF m fpath env in
         let pre'  = transf penv pre in
         let post' = transf qenv post in
-          unify_or_fail penv ue pre.pl_loc  ~expct:tbool pre' .f_ty;
-          unify_or_fail qenv ue post.pl_loc ~expct:tbool post'.f_ty;
-          f_hoareF {m;inv=pre'} fpath {m;inv=post'}
+        let penv_e = EcEnv.Fun.inv_memenv1 m env in
+        let epost' =
+          List.fold
+            (fun m (e,f) ->
+               let s,p = except_genpath env e in
+               match DMap.find p m with
+               | exception Not_found -> DMap.add p (transf penv_e f) m
+               | _ -> tyerror f.pl_loc env (DuplicatedException s)
+            )
+            DMap.empty
+            eposts
+        in
+        let dpost' = omap (transf penv) dpost in
+
+        unify_or_fail penv ue pre.pl_loc  ~expct:tbool pre'.f_ty;
+        unify_or_fail qenv ue post.pl_loc ~expct:tbool post'.f_ty;
+
+        let aux f = unify_or_fail penv_e ue post.pl_loc ~expct:tbool f.f_ty in
+        DMap.iter (fun _ -> aux) epost';
+        oiter aux dpost';
+
+        f_hoareF {m;inv=pre'} fpath {hsi_m=m;hsi_inv=(post',epost',dpost')}
 
     | PFehoareF (m, pre, gp, post) ->
         if mode <> `Form then
diff --git a/src/ecTyping.mli b/src/ecTyping.mli
index bf2da3aa2..d74148435 100644
--- a/src/ecTyping.mli
+++ b/src/ecTyping.mli
@@ -131,6 +131,7 @@ type tyerror =
 | DuplicatedTyVar
 | DuplicatedLocal        of symbol
 | DuplicatedField        of symbol
+| DuplicatedException    of qsymbol
 | NonLinearPattern
 | LvNonLinear
 | NonUnitFunWithoutReturn
@@ -145,6 +146,7 @@ type tyerror =
 | UnknownModName         of qsymbol
 | UnknownTyModName       of qsymbol
 | UnknownFunName         of qsymbol
+| UnknownExceptionName   of qsymbol
 | UnknownModVar          of qsymbol
 | UnknownMemName         of symbol
 | InvalidFunAppl         of funapp_error
@@ -264,6 +266,7 @@ val transmod     : attop:bool -> env -> pmodule_def -> module_expr
 val trans_topmsymbol : env -> pmsymbol located -> mpath
 val trans_msymbol    : env -> pmsymbol located -> mpath * module_smpl_sig
 val trans_gamepath   : env -> pgamepath -> xpath
+val except_genpath   : env -> qsymbol located -> qsymbol * path
 val trans_oracle     : env -> psymbol * psymbol -> xpath
 val trans_restr_mem  : env -> pmod_restr_mem -> mod_restr
 
diff --git a/src/ecUnifyProc.ml b/src/ecUnifyProc.ml
index e7ef218a7..d723bb438 100644
--- a/src/ecUnifyProc.ml
+++ b/src/ecUnifyProc.ml
@@ -170,8 +170,7 @@ let rec unify_instrs env umap i1 i2 =
       unify_stmts env umap b1 b2
     ) umap bs1 bs2
 
-  | Sassert e1, Sassert e2 ->
-    unify_exprs env umap e1 e2
+  | Sraise e1, Sraise e2 when EcPath.p_equal e1 e2 -> umap
 
   | Sabstract x1, Sabstract x2 when EcIdent.id_equal x1 x2 -> umap
 
diff --git a/src/ecUserMessages.ml b/src/ecUserMessages.ml
index 9c947c1b6..45b5c003d 100644
--- a/src/ecUserMessages.ml
+++ b/src/ecUserMessages.ml
@@ -301,6 +301,9 @@ end = struct
     | DuplicatedField name ->
         msg "duplicated field name: `%s'" name
 
+    |DuplicatedException name ->
+        msg "duplicated exception: %a" pp_qsymbol name
+
     | NonLinearPattern ->
         msg "non-linear pattern matching"
 
@@ -423,7 +426,10 @@ end = struct
         msg "unknown type name: %a" pp_qsymbol name
 
     | UnknownFunName name ->
-        msg "unknown procedure: %a" pp_qsymbol name
+      msg "unknown procedure: %a" pp_qsymbol name
+
+    | UnknownExceptionName name ->
+      msg "unknown exception: %a" pp_qsymbol name
 
     | UnknownModVar x ->
         msg "unknown module-level variable: %a" pp_qsymbol x
diff --git a/src/phl/ecPhlApp.ml b/src/phl/ecPhlApp.ml
index 4ebf52413..937c8b7af 100644
--- a/src/phl/ecPhlApp.ml
+++ b/src/phl/ecPhlApp.ml
@@ -19,8 +19,9 @@ let t_hoare_app_r i phi tc =
   let hs = tc1_as_hoareS tc in
   let phi = ss_inv_rebind phi (fst hs.hs_m) in
   let s1, s2 = s_split env i hs.hs_s in
-  let a = f_hoareS (snd hs.hs_m) (hs_pr hs) (stmt s1) phi in
-  let b = f_hoareS (snd hs.hs_m) phi (stmt s2) (hs_po hs) in
+  let post = update_hs_ss phi (hs_po hs) in
+  let a = f_hoareS (snd hs.hs_m) (hs_pr hs) (stmt s1) post in
+  let b = f_hoareS (snd hs.hs_m) phi (stmt s2) (hs_po hs)  in
   FApi.xmutate1 tc `HlApp [a; b]
 
 let t_hoare_app = FApi.t_low2 "hoare-app" t_hoare_app_r
@@ -51,7 +52,8 @@ let t_bdhoare_app_r_low i (phi, pR, f1, f2, g1, g2) tc =
   let s1, s2 = stmt s1, stmt s2 in
   let nR = map_ss_inv1 f_not pR in
   let mt = snd bhs.bhs_m in
-  let cond_phi = f_hoareS mt (bhs_pr bhs) s1 phi in
+  let post = lift_f phi in
+  let cond_phi = f_hoareS mt (bhs_pr bhs) s1 post in
   let condf1 = f_bdHoareS mt (bhs_pr bhs) s1 pR bhs.bhs_cmp f1 in
   let condg1 = f_bdHoareS mt (bhs_pr bhs) s1 nR bhs.bhs_cmp g1 in
   let condf2 = f_bdHoareS mt (map_ss_inv2 f_and_simpl phi pR) s2 (bhs_po bhs) bhs.bhs_cmp f2 in
@@ -69,9 +71,12 @@ let t_bdhoare_app_r_low i (phi, pR, f1, f2, g1, g2) tc =
   let condnm =
     let eqs = map_ss_inv2 f_and (map_ss_inv1 ((EcUtils.flip f_eq) r1) f2)
                                 (map_ss_inv1 ((EcUtils.flip f_eq) r2) g2) in
+    let post = empty_hs eqs in
     f_forall
       [(ir1, GTty treal); (ir2, GTty treal)]
-      (f_hoareS (snd bhs.bhs_m) (map_ss_inv2 f_and (bhs_pr bhs) eqs) s1 eqs) in
+      (f_hoareS (snd bhs.bhs_m)
+         (map_ss_inv2 f_and (bhs_pr bhs) eqs) s1 post)
+  in
   let conds = [EcSubst.f_forall_mems_ss_inv bhs.bhs_m condbd; condnm] in
   let conds =
     if   f_equal g1.inv f_r0
@@ -95,7 +100,11 @@ let t_bdhoare_app_r_low i (phi, pR, f1, f2, g1, g2) tc =
 let t_bdhoare_app_r i info tc =
   let tactic tc =
     let hs  = tc1_as_hoareS tc in
-    let tt1 = EcPhlConseq.t_hoareS_conseq_nm (hs_pr hs) {m=(fst hs.hs_m);inv=f_true} in
+    let tt1 =
+      EcPhlConseq.t_hoareS_conseq_nm
+        (hs_pr hs)
+        {hsi_m=(fst hs.hs_m);hsi_inv=empty_poe f_true}
+    in
     let tt2 = EcPhlAuto.t_pl_trivial in
     FApi.t_seqs [tt1; tt2; t_fail] tc
   in
diff --git a/src/phl/ecPhlAuto.ml b/src/phl/ecPhlAuto.ml
index 0970d5646..7dfe142f1 100644
--- a/src/phl/ecPhlAuto.ml
+++ b/src/phl/ecPhlAuto.ml
@@ -14,12 +14,13 @@ let tc_noauto_error pf ?loc () =
 
 (* -------------------------------------------------------------------- *)
 let t_exfalso_r tc =
+  let pre = tc1_get_pre tc in
   let post = tc1_get_post tc in
 
   FApi.t_or
     EcPhlTAuto.t_core_exfalso
     (FApi.t_seqsub
-       (EcPhlConseq.t_conseq (map_inv1 (fun _ -> f_false) post) post)
+       (EcPhlConseq.t_conseq (map_inv1 (fun _ -> f_false) pre) post)
        [t_id; t_trivial; EcPhlTAuto.t_core_exfalso])
     tc
 
diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml
index 8231b9f27..df6d26f37 100644
--- a/src/phl/ecPhlCall.ml
+++ b/src/phl/ecPhlCall.ml
@@ -59,6 +59,7 @@ let wp2_call
   map_ts_inv2 f_anda_simpl (map_ts_inv1 (PVM.subst env spre) fpre) post
 
 (* -------------------------------------------------------------------- *)
+
 let t_hoare_call fpre fpost tc =
   let env = FApi.tc1_env tc in
   let hs = tc1_as_hoareS tc in
@@ -69,22 +70,33 @@ let t_hoare_call fpre fpost tc =
   let f_concl = f_hoareF fpre f fpost in
   (* substitute memories *)
   let fpre = (ss_inv_rebind fpre m) in
-  let fpost = (ss_inv_rebind fpost m) in
+  let fpost = hs_inv_rebind fpost m in
+  let (inv, fepost,fd) = fpost.hsi_inv in
+  let fpost = {m;inv} in
   (* The wp *)
+  let (post,epost,d) = (hs_po hs).hsi_inv in
   let pvres = pv_res in
   let vres = EcIdent.create "result" in
   let fres = {m;inv=f_local vres fsig.fs_ret} in
-  let post = wp_asgn_call env lp fres (hs_po hs) in
+  let post = wp_asgn_call env lp fres {m=(hs_po hs).hsi_m;inv=post} in
   let fpost = map_ss_inv2 (PVM.subst1 env pvres m) fres fpost in
   let modi = f_write env f in
-  let post = generalize_mod_ss_inv env modi (map_ss_inv2 f_imp_simpl fpost post) in
+
+  let post = map_ss_inv2 f_imp_simpl fpost post in
+  let post = generalize_mod_ss_inv env modi post in
   let post = map_ss_inv1 (f_forall_simpl [(vres, GTty fsig.fs_ret)]) post in
   let spre = subst_args_call env m (e_tuple args) PVM.empty in
   let post = map_ss_inv2 f_anda_simpl (map_ss_inv1 (PVM.subst env spre) fpre) post in
-  let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s post in
 
-  FApi.xmutate1 tc `HlCall [f_concl; concl]
+  let poe = EcProofTyping.merge2_poe_list f_imp_simpl (epost,d) (fepost,fd) in
+  let poe = List.map (fun inv -> {m;inv}) poe in
+  let penv_e = EcEnv.Fun.inv_memenv1 m env in
+  let poe = List.map (generalize_mod_ss_inv penv_e modi) poe in
 
+  let post = List.fold (map_ss_inv2 f_anda_simpl) post poe in
+  let post = {hsi_m=post.m;hsi_inv=(post.inv,epost,d)} in
+  let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s post in
+  FApi.xmutate1 tc `HlCall [f_concl; concl]
 
 (* -------------------------------------------------------------------- *)
 let ehoare_call_pre_post fpre fpost tc =
@@ -223,6 +235,7 @@ let t_bdhoare_call fpre fpost opt_bd tc =
     let _,mt = bhs.bhs_m in
     match bhs.bhs_cmp, opt_bd with
     | FHle, None ->
+        let post =empty_hs post in
         f_hoareS mt bhs_pr s post
     | FHeq, Some bd ->
         f_bdHoareS mt bhs_pr s post bhs.bhs_cmp (map_ss_inv2 f_real_div bhs_bd bd)
@@ -409,18 +422,11 @@ let mk_inv_spec (_pf : proofenv) env inv fl fr =
       let post = map_ts_inv2 f_and eq_res inv in
         f_equivF pre fl fr post
 
+
 let process_call side info tc =
-  let process_spec tc side pre post =
+  let process_spec_2 tc side pre post =
     let (hyps, concl) = FApi.tc1_flat tc in
       match concl.f_node, side with
-      | FhoareS hs, None ->
-          let (_,f,_) = fst (tc1_last_call tc hs.hs_s) in
-          let m = (EcIdent.create "&hr") in
-          let penv, qenv = LDecl.hoareF m f hyps in
-          let pre  = TTC.pf_process_form !!tc penv tbool pre  in
-          let post = TTC.pf_process_form !!tc qenv tbool post in
-          f_hoareF {m;inv=pre} f {m;inv=post}
-
       | FbdHoareS bhs, None ->
           let (_,f,_) = fst (tc1_last_call tc bhs.bhs_s) in
           let m = (EcIdent.create "&hr") in
@@ -462,20 +468,37 @@ let process_call side info tc =
 
       | _ -> tc_error !!tc "the conclusion is not a hoare or an equiv" in
 
-  let process_inv tc side inv =
+
+  let process_spec_1 tc side pre post poe =
+    let (hyps, concl) = FApi.tc1_flat tc in
+    match concl.f_node, side with
+    | FhoareS hs, None ->
+      let (_,f,_) = fst (tc1_last_call tc hs.hs_s) in
+      let m = (EcIdent.create "&hr") in
+      let penv, qenv = LDecl.hoareF m f hyps in
+      let pre  = TTC.pf_process_form !!tc penv tbool pre  in
+      let post = TTC.pf_process_form !!tc qenv tbool post in
+      let env_e = LDecl.inv_memenv1 m hyps in
+      let (poe,d) = TTC.pf_process_poe tc env_e tbool poe in
+      f_hoareF {m;inv=pre} f {hsi_m=m;hsi_inv=(post,poe,d)}
+
+    | _ -> tc_error !!tc "the conclusion is not a hoare" in
+
+  let process_inv_1 tc side inv =
     if not (is_none side) then
       tc_error !!tc "cannot specify side for call with invariants";
 
     let hyps, concl = FApi.tc1_flat tc in
     match concl.f_node with
     | FhoareS hs ->
-        let m = fst hs.hs_m in
-        let (_,f,_) = fst (tc1_last_call tc hs.hs_s) in
-        let me = EcMemory.abstract m in
-        let hyps = LDecl.push_active_ss me hyps in
-        let inv = TTC.pf_process_form !!tc hyps tbool inv in
-        let inv = {m; inv} in
-        (f_hoareF inv f inv, Inv_ss inv)
+      let m = fst hs.hs_m in
+      let (_,f,_) = fst (tc1_last_call tc hs.hs_s) in
+      let me = EcMemory.abstract m in
+      let hyps = LDecl.push_active_ss me hyps in
+      let inv = TTC.pf_process_form !!tc hyps tbool inv in
+      let inv = {m; inv} in
+      let post = lift_f inv in
+      (f_hoareF inv f post , Inv_ss inv)
 
     | FeHoareS hs ->
         let m = fst hs.ehs_m in
@@ -509,7 +532,7 @@ let process_call side info tc =
 
     | _ -> tc_error !!tc "the conclusion is not a hoare or an equiv" in
 
-  let process_upto tc side info =
+   let process_upto tc side info =
     if not (is_none side) then
       tc_error !!tc "cannot specify side for call with invariants";
     let env, _, concl = FApi.tc1_eflat tc in
@@ -541,13 +564,23 @@ let process_call side info tc =
 
   let process_cut tc info =
     match info with
-    | CI_spec (pre, post) ->
-      process_spec tc side pre post
+    | CI_spec (pre, post, poe) ->
+      begin
+        let _, concl = FApi.tc1_flat tc in
+        match concl.f_node with
+        | FhoareS _ ->
+          process_spec_1 tc side pre post poe
+        | _ ->
+           process_spec_2 tc side pre post
+      end
+
     | CI_inv inv ->
-      let f, inv = process_inv tc side inv in
-      subtactic := (fun tc ->
-        FApi.t_firsts t_trivial 2 (EcPhlFun.t_fun inv tc));
-      f
+      begin
+        let f, inv = process_inv_1 tc side inv in
+        subtactic := (fun tc ->
+            FApi.t_firsts t_trivial 2 (EcPhlFun.t_fun inv tc));
+        f
+      end
 
     | CI_upto info ->
       let bad, p, q, form = process_upto tc side info in
@@ -614,7 +647,7 @@ let process_call_concave (fc, info) tc =
 
   let process_cut tc info =
     match info with
-    | CI_spec (pre, post) ->
+    | CI_spec (pre, post, ([],None)) ->
       let ty,fmake = process_spec tc in
       let _, pre = TTC.tc1_process_Xhl_form tc ty pre in
       let _, post = TTC.tc1_process_Xhl_form tc ty post in
diff --git a/src/phl/ecPhlCall.mli b/src/phl/ecPhlCall.mli
index 79da81f63..1c87ae8f2 100644
--- a/src/phl/ecPhlCall.mli
+++ b/src/phl/ecPhlCall.mli
@@ -13,7 +13,7 @@ val wp2_call :
   -> ts_inv
   -> EcEnv.LDecl.hyps -> ts_inv
 
-val t_hoare_call   : ss_inv -> ss_inv -> backward
+val t_hoare_call   : ss_inv -> hs_inv -> backward
 val t_bdhoare_call : ss_inv -> ss_inv -> ss_inv option -> backward
 val t_equiv_call   : ts_inv -> ts_inv -> backward
 val t_equiv_call1  : side -> ss_inv -> ss_inv -> backward
diff --git a/src/phl/ecPhlCase.ml b/src/phl/ecPhlCase.ml
index 069c05035..7aa9ceca2 100644
--- a/src/phl/ecPhlCase.ml
+++ b/src/phl/ecPhlCase.ml
@@ -9,8 +9,16 @@ let t_hoare_case_r ?(simplify = true) f tc =
   let fand = if simplify then f_and_simpl else f_and in
   let hs = tc1_as_hoareS tc in
   let mt = snd hs.hs_m in
-  let concl1 = f_hoareS mt (map_ss_inv2 fand (hs_pr hs) f) hs.hs_s (hs_po hs) in
-  let concl2 = f_hoareS mt (map_ss_inv2 fand (hs_pr hs) (map_ss_inv1 f_not f)) hs.hs_s (hs_po hs) in
+  let concl1 =
+    f_hoareS mt (map_ss_inv2 fand (hs_pr hs) f) hs.hs_s (hs_po hs)
+  in
+  let concl2 =
+    f_hoareS
+      mt
+      (map_ss_inv2 fand (hs_pr hs) (map_ss_inv1 f_not f))
+      hs.hs_s
+      (hs_po hs)
+  in
   FApi.xmutate1 tc (`HlCase f) [concl1; concl2]
 
 (* --------------------------------------------------------------------- *)
@@ -73,6 +81,7 @@ let t_hl_case_r ?simplify f tc =
       ~tbh:err
       ~te:(t_equiv_case ?simplify f)
       tc
+  | _ -> tc_error !!tc "exception are not supported"
 
 (* -------------------------------------------------------------------- *)
 let t_hl_case ?simplify = FApi.t_low1 "hl-case" (t_hl_case_r ?simplify)
diff --git a/src/phl/ecPhlCond.ml b/src/phl/ecPhlCond.ml
index 86432d60e..69d5c4210 100644
--- a/src/phl/ecPhlCond.ml
+++ b/src/phl/ecPhlCond.ml
@@ -142,7 +142,9 @@ end = struct
         Inv_ts (ss_inv_generalize_left f ml)
       | Inv_ss _, _ ->
         Inv_ss f
-      | Inv_ts _, None -> tc_error !!tc "expecting a side" in
+      | Inv_ts _, None -> tc_error !!tc "expecting a side"
+      | Inv_hs _, _ -> assert false
+    in
 
     let onsub (i : int) (tc : tcenv1) =
       let cname, cargs = List.nth indt.tydt_ctors i in
diff --git a/src/phl/ecPhlConseq.ml b/src/phl/ecPhlConseq.ml
index d4631bfe6..a2604787b 100644
--- a/src/phl/ecPhlConseq.ml
+++ b/src/phl/ecPhlConseq.ml
@@ -58,27 +58,44 @@ let bd_goal tc fcmp fbd cmp bd =
   | Some fp -> fp
 
 (* -------------------------------------------------------------------- *)
+
 let t_hoareF_conseq pre post tc =
   let env = FApi.tc1_env tc in
   let hf  = tc1_as_hoareF tc in
   let pre = ss_inv_rebind pre hf.hf_m in
-  let post = ss_inv_rebind post hf.hf_m in
+  let post = hs_inv_rebind post hf.hf_m in
+  let (post, epost, d) = post.hsi_inv in
+  let (fpost, fepost,fd) = (hf_po hf).hsi_inv in
   let mpr,mpo = EcEnv.Fun.hoareF_memenv hf.hf_m hf.hf_f env in
-  let cond1, cond2 = conseq_cond_ss (hf_pr hf) (hf_po hf) pre post in
+  let m = hf.hf_m in
+  let cond1, cond2 =
+    conseq_cond_ss (hf_pr hf) {m;inv=fpost} pre {m;inv=post}
+  in
+  let cond2e = EcProofTyping.merge2_poe_list f_imp (fepost,fd) (epost,d) in
+  let cond2 = List.fold f_and cond2.inv cond2e in
   let concl1 = f_forall_mems_ss_inv mpr cond1 in
-  let concl2 = f_forall_mems_ss_inv mpo cond2 in
-  let concl3 = f_hoareF pre hf.hf_f post in
+  let concl2 = f_forall_mems_ss_inv mpo {m;inv=cond2} in
+  let concl3 = f_hoareF pre hf.hf_f {hsi_m=m;hsi_inv=(post, epost,d)} in
   FApi.xmutate1 tc `Conseq [concl1; concl2; concl3]
 
 (* -------------------------------------------------------------------- *)
 let t_hoareS_conseq pre post tc =
   let hs = tc1_as_hoareS tc in
   let pre = ss_inv_rebind pre (fst hs.hs_m) in
-  let post = ss_inv_rebind post (fst hs.hs_m) in
-  let cond1, cond2 = conseq_cond_ss (hs_pr hs) (hs_po hs) pre post in
+  let post = hs_inv_rebind post (fst hs.hs_m) in
+  let (post, epost, d) = post.hsi_inv in
+  let (fpost, fepost,fd) = (hs_po hs).hsi_inv in
+  let m = fst hs.hs_m in
+  let cond1, cond2 =
+    conseq_cond_ss (hs_pr hs) {m;inv=fpost} pre {m;inv=post}
+  in
+  let cond2e = EcProofTyping.merge2_poe_list f_imp (fepost,fd) (epost,d) in
+  let cond2 = List.fold f_and cond2.inv cond2e in
   let concl1 = f_forall_mems_ss_inv hs.hs_m cond1 in
-  let concl2 = f_forall_mems_ss_inv hs.hs_m cond2 in
-  let concl3 = f_hoareS (snd hs.hs_m) pre hs.hs_s post in
+  let concl2 = f_forall_mems_ss_inv hs.hs_m {m=fst hs.hs_m;inv=cond2} in
+  let concl3 =
+    f_hoareS (snd hs.hs_m) pre hs.hs_s {hsi_m=m;hsi_inv=(post, epost,d)}
+  in
   FApi.xmutate1 tc `HlConseq [concl1; concl2; concl3]
 
 (* -------------------------------------------------------------------- *)
@@ -205,8 +222,20 @@ let t_equivS_conseq pre post tc =
 (* -------------------------------------------------------------------- *)
 let t_conseq pre post tc =
   match (FApi.tc1_goal tc).f_node, pre, post with
-  | FhoareF _,   Inv_ss pre, Inv_ss post -> t_hoareF_conseq pre post tc
-  | FhoareS _,   Inv_ss pre, Inv_ss post -> t_hoareS_conseq pre post tc
+  | FhoareF hf, Inv_ss pre, Inv_ss post ->
+    let (_,epost,d) = (hf_po hf).hsi_inv in
+    let post = ss_inv_rebind post (hf_po hf).hsi_m in
+    let post = {hsi_m=(hf_po hf).hsi_m;hsi_inv=(post.inv,epost,d)} in
+    t_hoareF_conseq pre post tc
+  | FhoareS hs, Inv_ss pre, Inv_ss post ->
+    let (_,epost,d) = (hs_po hs).hsi_inv in
+    let post = ss_inv_rebind post (hs_po hs).hsi_m in
+    let post = {hsi_m=(hs_po hs).hsi_m;hsi_inv=(post.inv,epost,d)} in
+    t_hoareS_conseq pre post tc
+  | FhoareF _, Inv_ss pre, Inv_hs post ->
+    t_hoareF_conseq pre post tc
+  | FhoareS _, Inv_ss pre, Inv_hs post ->
+    t_hoareS_conseq pre post tc
   | FbdHoareF _, Inv_ss pre, Inv_ss post -> t_bdHoareF_conseq pre post tc
   | FbdHoareS _, Inv_ss pre, Inv_ss post -> t_bdHoareS_conseq pre post tc
   | FeHoareF _ , Inv_ss pre, Inv_ss post -> t_ehoareF_conseq pre post tc
@@ -316,11 +345,16 @@ let cond_hoareF_notmod ?(mk_other=false) tc (cond: ss_inv) =
     else [] in
   cond, bmem, bother
 
-let t_hoareF_notmod (post: ss_inv) tc =
+let t_hoareF_notmod post tc =
   let hf = tc1_as_hoareF tc in
-  let post = ss_inv_rebind post hf.hf_m in
-  let cond1, _, _ = cond_hoareF_notmod tc (map_ss_inv2 f_imp post (hf_po hf)) in
-  let cond2 = f_hoareF (hf_pr hf) hf.hf_f post in
+  let p = hs_inv_rebind post hf.hf_m in
+  let (post, epost, d) = p.hsi_inv in
+  let (fpost, fepost,fd) = (hf_po hf).hsi_inv in
+  let cond = f_imp post fpost in
+  let econd1 = EcProofTyping.merge2_poe_list f_imp (fepost,fd) (epost,d) in
+  let cond1 = List.fold f_and cond econd1 in
+  let cond1, _, _ = cond_hoareF_notmod tc {m=hf.hf_m;inv=cond1} in
+  let cond2 = f_hoareF (hf_pr hf) hf.hf_f p in
   FApi.xmutate1 tc `HlNotmod [cond1; cond2]
 
 (* -------------------------------------------------------------------- *)
@@ -341,9 +375,14 @@ let cond_hoareS_notmod ?(mk_other=false) tc cond =
 
 let t_hoareS_notmod post tc =
   let hs = tc1_as_hoareS tc in
-  let post = ss_inv_rebind post (fst hs.hs_m) in
-  let cond1, _, _ = cond_hoareS_notmod tc (map_ss_inv2 f_imp post (hs_po hs)) in
-  let cond2 = f_hoareS (snd hs.hs_m) (hs_pr hs) hs.hs_s post in
+  let p = hs_inv_rebind post (fst hs.hs_m) in
+  let (post, epost, d) = p.hsi_inv in
+  let (fpost, fepost,fd) = (hs_po hs).hsi_inv in
+  let cond = f_imp post fpost in
+  let econd1 = EcProofTyping.merge2_poe_list f_imp (fepost,fd) (epost,d) in
+  let cond1 = List.fold f_and cond econd1 in
+  let cond1, _, _ = cond_hoareS_notmod tc {m=fst hs.hs_m;inv=cond1} in
+  let cond2 = f_hoareS (snd hs.hs_m) (hs_pr hs) hs.hs_s p in
   FApi.xmutate1 tc `HlNotmod [cond1; cond2]
 
 (* -------------------------------------------------------------------- *)
@@ -417,15 +456,6 @@ let gen_conseq_nm tnm tc pre post =
     FApi.t_swap_goals 0 1 gs
   )
 
-let gen_conseq_nm_ss tnm tc (pre: ss_inv) (post: ss_inv) =
-    FApi.t_internal ~info:"generic-conseq-nm" (fun g ->
-      let gs =
-        (tnm post @+
-          [ t_id;
-            tc pre post @+ [t_id; t_trivial; t_id] ]) g in
-      FApi.t_swap_goals 0 1 gs
-    )
-
 let gen_conseq_nm_ts tnm tc (pre: ts_inv) (post: ts_inv) =
   FApi.t_internal ~info:"generic-conseq-nm" (fun g ->
     let gs =
@@ -435,8 +465,18 @@ let gen_conseq_nm_ts tnm tc (pre: ts_inv) (post: ts_inv) =
     FApi.t_swap_goals 0 1 gs
   )
 
+let gen_conseq_nm_ss tnm tc pre post =
+    FApi.t_internal ~info:"generic-conseq-nm" (fun g ->
+      let gs =
+        (tnm post @+
+          [ t_id;
+            tc pre post @+ [t_id; t_trivial; t_id] ]) g in
+      FApi.t_swap_goals 0 1 gs
+    )
+
+
 let t_hoareF_conseq_nm   = gen_conseq_nm_ss t_hoareF_notmod   t_hoareF_conseq
-let t_hoareS_conseq_nm   = gen_conseq_nm t_hoareS_notmod   t_hoareS_conseq
+let t_hoareS_conseq_nm   = gen_conseq_nm_ss t_hoareS_notmod   t_hoareS_conseq
 let t_equivF_conseq_nm   = gen_conseq_nm_ts t_equivF_notmod   t_equivF_conseq
 let t_equivS_conseq_nm   = gen_conseq_nm t_equivS_notmod   t_equivS_conseq
 let t_bdHoareF_conseq_nm = gen_conseq_nm t_bdHoareF_notmod t_bdHoareF_conseq
@@ -649,14 +689,20 @@ let process_concave ((info, fc) : pformula option tuple2 gppterm * pformula) tc
 let t_hoareS_conseq_bdhoare tc =
   let hs = tc1_as_hoareS tc in
   let f_r1 = {m=fst hs.hs_m; inv=f_r1} in
-  let concl1 = f_bdHoareS (snd hs.hs_m) (hs_pr hs) hs.hs_s (hs_po hs) FHeq f_r1 in
+  if not (is_empty_poe (hs_po hs).hsi_inv) then
+    tc_error !!tc "exception are not supported";
+  let post = lower_f (hs_po hs) in
+  let concl1 = f_bdHoareS (snd hs.hs_m) (hs_pr hs) hs.hs_s post FHeq f_r1 in
   FApi.xmutate1 tc `HlConseqBd [concl1]
 
 (* -------------------------------------------------------------------- *)
 let t_hoareF_conseq_bdhoare tc =
   let hf = tc1_as_hoareF tc in
   let f_r1 = {m=hf.hf_m; inv=f_r1} in
-  let concl1 = f_bdHoareF (hf_pr hf) hf.hf_f (hf_po hf) FHeq f_r1 in
+  if not (is_empty_poe (hf_po hf).hsi_inv) then
+    tc_error !!tc "exception are not supported";
+  let post = lower_f (hf_po hf) in
+  let concl1 = f_bdHoareF (hf_pr hf) hf.hf_f post FHeq f_r1 in
   FApi.xmutate1 tc `HlConseqBd [concl1]
 
 (* -------------------------------------------------------------------- *)
@@ -664,11 +710,11 @@ let t_hoareS_conseq_conj pre post pre' post' tc =
   let (_, hyps, _) = FApi.tc1_eflat tc in
   let hs = tc1_as_hoareS tc in
   let pre'' = map_ss_inv2 f_and pre' pre in
-  let post'' = map_ss_inv2 f_and post' post in
-  if not (ss_inv_alpha_eq hyps (hs_pr hs) pre'') 
-    then tc_error !!tc "invalid pre-condition";
-  if not (ss_inv_alpha_eq hyps (hs_po hs) post'') 
-    then tc_error !!tc "invalid post-condition";
+  let post'' = map_hs_inv2 f_and post' post in
+  if not (ss_inv_alpha_eq hyps (hs_pr hs) pre'')
+  then tc_error !!tc "invalid pre-condition";
+  if not (hs_inv_alpha_eq hyps (hs_po hs) post'')
+  then tc_error !!tc "invalid post-condition";
   let concl1 = f_hoareS (snd hs.hs_m) pre hs.hs_s post in
   let concl2 = f_hoareS (snd hs.hs_m) pre' hs.hs_s post' in
   FApi.xmutate1 tc `HlConseqBd [concl1; concl2]
@@ -678,10 +724,10 @@ let t_hoareF_conseq_conj pre post pre' post' tc =
   let (_, hyps, _) = FApi.tc1_eflat tc in
   let hf = tc1_as_hoareF tc in
   let pre'' = map_ss_inv2 f_and pre' pre in
-  let post'' = map_ss_inv2 f_and post' post in
-  if not (ss_inv_alpha_eq hyps (hf_pr hf) pre'') 
+  let post'' = map_hs_inv2 f_and post' post in
+  if not (ss_inv_alpha_eq hyps (hf_pr hf) pre'')
   then tc_error !!tc "invalid pre-condition";
-  if not (ss_inv_alpha_eq hyps (hf_po hf) post'')
+  if not (hs_inv_alpha_eq hyps (hf_po hf) post'')
   then tc_error !!tc "invalid post-condition";
   let concl1 = f_hoareF pre hf.hf_f post in
   let concl2 = f_hoareF pre' hf.hf_f post' in
@@ -695,6 +741,7 @@ let t_bdHoareS_conseq_conj ~add post post' tc =
   let posth = if add then post' else map_ss_inv2 f_and post' post in
   if not (ss_inv_alpha_eq hyps (bhs_po hs) postc) then
     tc_error !!tc "invalid post-condition";
+  let post = empty_hs post in
   let concl1 = f_hoareS (snd hs.bhs_m) (bhs_pr hs) hs.bhs_s post in
   let concl2 = f_bdHoareS (snd hs.bhs_m) (bhs_pr hs) hs.bhs_s posth 
                  hs.bhs_cmp (bhs_bd hs) in
@@ -710,6 +757,7 @@ let t_bdHoareF_conseq_conj ~add post post' tc =
   let posth = if add then post' else map_ss_inv2 f_and post' post in
   if not (ss_inv_alpha_eq hyps (bhf_po hs) postc) then
     tc_error !!tc "invalid post-condition";
+  let post = empty_hs post in
   let concl1 = f_hoareF (bhf_pr hs) hs.bhf_f post in
   let concl2 = f_bdHoareF (bhf_pr hs) hs.bhf_f posth hs.bhf_cmp (bhf_bd hs) in
   FApi.xmutate1 tc `HlConseqBd [concl1; concl2]
@@ -727,6 +775,8 @@ let t_equivS_conseq_conj pre1 post1 pre2 post2 pre' post' tc =
     tc_error !!tc "invalid pre-condition";
   if not (ts_inv_alpha_eq hyps (es_po es) (map_ts_inv f_ands [post';post1';post2'])) then
     tc_error !!tc "invalid post-condition";
+  let post1 = empty_hs post1 in
+  let post2 = empty_hs post2 in
   let concl1 = f_hoareS mtl pre1 es.es_sl post1 in
   let concl2 = f_hoareS mtr pre2 es.es_sr post2 in
   let concl3 = f_equivS mtl mtr pre' es.es_sl es.es_sr post' in
@@ -749,6 +799,9 @@ let t_equivF_conseq_conj pre1 post1 pre2 post2 pre' post' tc =
   then tc_error !!tc "invalid pre-condition";
   if not (ts_inv_alpha_eq hyps (ef_po ef) post_and)
   then tc_error !!tc "invalid post-condition";
+  let post1 = empty_hs post1 in
+  let post2 = empty_hs post2 in
+
   let concl1 = f_hoareF pre1 ef.ef_fl post1 in
   let concl2 = f_hoareF pre2 ef.ef_fr post2 in
   let concl3 = f_equivF pre' ef.ef_fl ef.ef_fr post' in
@@ -825,11 +878,16 @@ let transitivity_side_cond ?bds hyps prml poml pomr p q p2 q2 p1 q1 =
 let t_hoareF_conseq_equiv f2 p q p2 q2 tc =
   let env, hyps, _ = FApi.tc1_eflat tc in
   let hf1 = tc1_as_hoareF tc in
+  if not (is_empty_poe (hf_po hf1).hsi_inv) then
+    tc_error !!tc "exception are not supported";
   let ef  = f_equivF p hf1.hf_f f2 q in
-  let hf2 = f_hoareF p2 f2 q2 in
+  let post = empty_hs q2 in
+  let hf2 = f_hoareF p2 f2 post in
   let (prml, _prmr), (poml, pomr) = Fun.equivF_memenv p.ml p.mr hf1.hf_f f2 env in
+  let (post,_,_) = (hf_po hf1).hsi_inv in
+  let post = {m=(hf_po hf1).hsi_m;inv=post} in
   let (cond1, cond2) =
-    transitivity_side_cond hyps prml poml pomr p q p2 q2 (hf_pr hf1) (hf_po hf1) in
+    transitivity_side_cond hyps prml poml pomr p q p2 q2 (hf_pr hf1) post in
   FApi.xmutate1 tc `HoareFConseqEquiv [cond1; cond2; ef; hf2]
 
 let t_bdHoareF_conseq_equiv f2 p q p2 q2 bd2 tc =
@@ -921,10 +979,14 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
     let tac = if notmod then t_hoareS_conseq_nm else t_hoareS_conseq in
 
     t_on1seq 2
-      (tac (map_ss_inv2 f_and (hs_pr hs) (hs_pr hs2)) 
-            (map_ss_inv2 f_and (hs_po hs) (hs_po hs2)))
+      (tac
+         (map_ss_inv2 f_and (hs_pr hs) (hs_pr hs2))
+         (map_hs_inv2 f_and (hs_po hs) (hs_po hs2))
+      )
       (FApi.t_seqsub
-         (t_hoareS_conseq_conj (hs_pr hs2) (hs_po hs2) (hs_pr hs) (hs_po hs))
+         (t_hoareS_conseq_conj
+            (hs_pr hs2) (hs_po hs2)
+            (hs_pr hs) (hs_po hs))
          [t_apply_r nf2; t_apply_r nf1])
       tc
 
@@ -959,18 +1021,20 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
     let tac = if notmod then t_hoareF_conseq_nm else t_hoareF_conseq in
     let pr1, po1 = hf_pr hf, hf_po hf in
     let pr2 = ss_inv_rebind (hf_pr hs2) hf.hf_m in
-    let po2 = ss_inv_rebind (hf_po hs2) hf.hf_m in
+    let po2 = hs_inv_rebind (hf_po hs2) hf.hf_m in
     (* check that the pre- and post-conditions are well formed *)
     t_on1seq 2
-      ((tac (map_ss_inv2 f_and pr1 pr2) 
-           (map_ss_inv2 f_and po1 po2)))
+      ((tac
+          (map_ss_inv2 f_and pr1 pr2)
+          (map_hs_inv2 f_and po1 po2)
+       ))
       (FApi.t_seqsub
          (t_hoareF_conseq_conj pr2 po2 pr1 po1)
          [t_apply_r nf2; t_apply_r nf1])
       tc
 
   (* ------------------------------------------------------------------ *)
-  (* hoareF / bdhoareF / ⊥ / ⊥                                            *)
+  (* hoareF / bdhoareF / ⊥ / ⊥                                          *)
   | FhoareF _, Some ((_, {f_node = FbdHoareF hs}) as nf1), None, None ->
     let tac = if notmod then t_bdHoareF_conseq_nm else t_bdHoareF_conseq in
 
@@ -987,24 +1051,27 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
   | FhoareF _,
     Some ((_, {f_node = FequivF ef}) as nef), Some((_, f2) as nf2), _ ->
     let hf2 = pf_as_hoareF !!tc f2 in
+    if not (is_empty_poe (hf_po hf2).hsi_inv) then
+      tc_error !!tc "exception are not supported";
+    let post = lower_f (hf_po hf2) in
     FApi.t_seqsub
-      (t_hoareF_conseq_equiv hf2.hf_f (ef_pr ef) (ef_po ef) (hf_pr hf2) (hf_po hf2))
+      (t_hoareF_conseq_equiv hf2.hf_f (ef_pr ef) (ef_po ef) (hf_pr hf2) post)
       [t_id; t_id; t_apply_r nef; t_apply_r nf2] tc
 
   (* ------------------------------------------------------------------ *)
-  (* ehoareS / ehoareS / ⊥ / ⊥                                            *)
+  (* ehoareS / ehoareS / ⊥ / ⊥                                          *)
   | FeHoareS _, Some ((_, {f_node = FeHoareS hs}) as nf1), None, None ->
     let tac = if notmod then t_ehoareS_conseq_nm else t_ehoareS_conseq in
     FApi.t_last (t_apply_r nf1) (tac (ehs_pr hs) (ehs_po hs) tc)
 
   (* ------------------------------------------------------------------ *)
-  (* ehoareF / ehoareF / ⊥ / ⊥                                            *)
+  (* ehoareF / ehoareF / ⊥ / ⊥                                          *)
   | FeHoareF _, Some ((_, {f_node = FeHoareF hf}) as nf1), None, None ->
     let tac = if notmod then t_ehoareF_conseq_nm else t_ehoareF_conseq in
     FApi.t_last (t_apply_r nf1) (tac (ehf_pr hf) (ehf_po hf) tc)
 
   (* ------------------------------------------------------------------ *)
-  (* ehoareF / equivF / ehoareF                                           *)
+  (* ehoareF / equivF / ehoareF                                         *)
   | FeHoareF _,
     Some ((_, {f_node = FequivF ef}) as nef), Some((_, f2) as nf2), _ ->
     let hf2 = pf_as_ehoareF !!tc f2 in
@@ -1038,7 +1105,10 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
     let mpre   = Fsubst.f_subst_mem pre.m m pre.inv in
     let post1  = (bhs_po hs0) in
     let post   = (bhs_po hs) in
-    let posta  = map_ss_inv2 f_and post (hs_po hs2) in
+    if not (is_empty_poe (hs_po hs2).hsi_inv) then
+      tc_error !!tc "exception are not supported";
+    let posta1 = lower_f (hs_po hs2) in
+    let posta  = map_ss_inv2 f_and post posta1 in
 
     let concl1 = f_forall_mems_ss_inv hs0.bhs_m (map_ss_inv2 f_imp (bhs_pr hs0) pre) in
 
@@ -1053,7 +1123,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
             t_intro_i hh @!
             (t_bdHoareS_conseq_bd hs.bhs_cmp (bhs_bd hs) @+ [
               t_id; (* subgoal 3 : bound *)
-              t_bdHoareS_conseq_conj ~add:false (hs_po hs2) post1 @+ [
+              t_bdHoareS_conseq_conj ~add:false posta1 post1 @+ [
                 t_hoareS_conseq pre (hs_po hs2) @+ [
                   t_intros_i [m;h0] @! t_cutdef
                     (ptlocal ~args:[pamemory m; palocal h0] hi)
@@ -1063,7 +1133,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
                 tac pre posta @+ [
                   t_apply_hyp hi;
                   t_id; (* subgoal 4 : post *)
-                  t_bdHoareS_conseq_conj ~add:true (hs_po hs2) post @+ [
+                  t_bdHoareS_conseq_conj ~add:true posta1 post @+ [
                     t_apply_hyp hh;
                     t_bdHoareS_conseq (bhs_pr hs) post @+ [
                       EcLowGoal.t_trivial;
@@ -1100,7 +1170,6 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
       Some ((_, f2) as nf2),
       None
     ->
-
     let hs2 = pf_as_hoareF !!tc f2 in
     let tac = if notmod then t_bdHoareF_conseq_nm else t_bdHoareF_conseq in
     let m,hi,hh, h0 =
@@ -1111,8 +1180,12 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
     let mpre   = Fsubst.f_subst_mem pre.m m pre.inv in
     let post1  = (bhf_po hs0) in
     let post   = ss_inv_rebind (bhf_po hs) hs2.hf_m in
-    let posta  = map_ss_inv2 f_and post (hf_po hs2) in
+    if not (is_empty_poe (hf_po hs2).hsi_inv) then
+      tc_error !!tc "exception are not supported";
+    let posta1 = lower_f (hf_po hs2) in
+    let posta  = map_ss_inv2 f_and post posta1 in
     let mpr,_ = EcEnv.Fun.hoareF_memenv hs0.bhf_m hs0.bhf_f (FApi.tc1_env tc) in
+
     let concl1 = f_forall_mems_ss_inv mpr (map_ss_inv2 f_imp hs0_pr pre) in
 
     let tc = ( t_cut concl1 @+
@@ -1126,7 +1199,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
             t_intro_i hh @!
             (t_bdHoareF_conseq_bd hs.bhf_cmp (bhf_bd hs) @+ [
               t_id; (* subgoal 3 : bound *)
-              t_bdHoareF_conseq_conj ~add:false (hf_po hs2) post1 @+ [
+              t_bdHoareF_conseq_conj ~add:false posta1 post1 @+ [
                 t_hoareF_conseq pre (hf_po hs2) @+ [
                   t_intros_i [m;h0] @! t_cutdef
                     (ptlocal ~args:[pamemory m; palocal h0] hi)
@@ -1136,7 +1209,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
                 tac pre posta @+ [
                   t_apply_hyp hi;
                   t_id; (* subgoal 4 : post *)
-                  t_bdHoareF_conseq_conj ~add:true (hf_po hs2) post @+ [
+                  t_bdHoareF_conseq_conj ~add:true posta1 post @+ [
                     t_apply_hyp hh;
                     t_bdHoareF_conseq (bhf_pr hs) post @+ [
                       EcLowGoal.t_trivial;
@@ -1162,7 +1235,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
     Some ((_, {f_node = FequivF ef}) as nef), Some((_, f2) as nf2), _ ->
     let hf2 = pf_as_bdhoareF !!tc f2 in
     FApi.t_seqsub
-      (t_bdHoareF_conseq_equiv hf2.bhf_f (ef_pr ef) (ef_po ef) 
+      (t_bdHoareF_conseq_equiv hf2.bhf_f (ef_pr ef) (ef_po ef)
                                          (bhf_pr hf2) (bhf_po hf2) (bhf_bd hf2))
       [t_id; t_id; t_apply_r nef; t_apply_r nf2] tc
 
@@ -1182,10 +1255,19 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
     let hs2    = pf_as_hoareS !!tc f2 in
     let hs3    = pf_as_hoareS !!tc f3 in
     let (ml, mr) = (fst es.es_ml, fst es.es_mr) in
+
+    if not (is_empty_poe (hs_po hs2).hsi_inv) then
+      tc_error !!tc "exception are not supported";
+    let post2 = lower_f (hs_po hs2) in
+    if not (is_empty_poe (hs_po hs3).hsi_inv) then
+      tc_error !!tc "exception are not supported";
+    let post3 = lower_f (hs_po hs3) in
+
     let hs2_pr = ss_inv_generalize_as_left (hs_pr hs2) ml mr in
-    let hs2_po = ss_inv_generalize_as_left (hs_po hs2) ml mr in
+    let hs2_po = ss_inv_generalize_as_left post2 ml mr in
     let hs3_pr = ss_inv_generalize_as_right (hs_pr hs3) ml mr in
-    let hs3_po = ss_inv_generalize_as_right (hs_po hs3) ml mr in
+    let hs3_po = ss_inv_generalize_as_right post3 ml mr in
+
     let pre    = map_ts_inv f_ands [es_pr es; hs2_pr; hs3_pr] in
     let post   = map_ts_inv f_ands [es_po es; hs2_po; hs3_po] in
     let tac    = if notmod then t_equivS_conseq_nm else t_equivS_conseq in
@@ -1193,7 +1275,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
     t_on1seq 2 (tac pre post)
       (FApi.t_seqsub
          (t_equivS_conseq_conj
-            (hs_pr hs2) (hs_po hs2) (hs_pr hs3) (hs_po hs3) (es_pr es) (es_po es))
+            (hs_pr hs2) post2 (hs_pr hs3) post3 (es_pr es) (es_po es))
          [t_apply_r nf2; t_apply_r nf3; t_apply_r nf1])
       tc
 
@@ -1225,14 +1307,18 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
   (* equivS / ? / ? / ⊥                                                 *)
   | FequivS es, Some _, Some _, None ->
     let m = EcIdent.create "&hr" in
-    let f3 = f_hoareS (snd es.es_mr) {m;inv=f_true} es.es_sr {m;inv=f_true} in
+    let post = {hsi_m=m;hsi_inv=empty_poe f_true} in
+    let f3 = f_hoareS (snd es.es_mr) {m;inv=f_true} es.es_sr post
+    in
     t_hi_conseq notmod f1 f2 (Some (None, f3)) tc
 
   (* ------------------------------------------------------------------ *)
   (* equivS / ? / ⊥ / ?                                                 *)
   | FequivS es, Some _, None, Some _ ->
     let m = EcIdent.create "&hr" in
-    let f2 = f_hoareS (snd es.es_ml) {m;inv=f_true} es.es_sl {m;inv=f_true} in
+    let f2 =
+      f_hoareS (snd es.es_ml) {m;inv=f_true} es.es_sl {hsi_m=m;hsi_inv=empty_poe f_true}
+    in
     t_hi_conseq notmod f1 (Some (None, f2)) f3 tc
 
   (* ------------------------------------------------------------------ *)
@@ -1287,18 +1373,27 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
     let hs2    = pf_as_hoareF !!tc f2 in
     let hs3    = pf_as_hoareF !!tc f3 in
     let (ml, mr) = (ef.ef_ml, ef.ef_mr) in
+
+   if not (is_empty_poe (hf_po hs2).hsi_inv) then
+      tc_error !!tc "exception are not supported";
+    let post2 = lower_f (hf_po hs2) in
+    if not (is_empty_poe (hf_po hs3).hsi_inv) then
+      tc_error !!tc "exception are not supported";
+    let post3 = lower_f (hf_po hs3) in
+
     let hs2_pr = ss_inv_generalize_as_left (hf_pr hs2) ml mr in
     let hs3_pr = ss_inv_generalize_as_right (hf_pr hs3) ml mr in
     let pre    = map_ts_inv f_ands [ef_pr ef; hs2_pr; hs3_pr] in
-    let hs2_po = ss_inv_generalize_as_left (hf_po hs2) ml mr in
-    let hs3_po = ss_inv_generalize_as_right (hf_po hs3) ml mr in
+    let hs2_po = ss_inv_generalize_as_left post2 ml mr in
+    let hs3_po = ss_inv_generalize_as_right post3 ml mr in
+
     let post  = map_ts_inv f_ands [ef_po ef; hs2_po; hs3_po] in
     let tac    = if notmod then t_equivF_conseq_nm else t_equivF_conseq in
     t_on1seq 2
       (tac pre post)
       (FApi.t_seqsub
          (t_equivF_conseq_conj
-            (hf_pr hs2) (hf_po hs2) (hf_pr hs3) (hf_po hs3) (ef_pr ef) (ef_po ef))
+            (hf_pr hs2) post2 (hf_pr hs3) post3 (ef_pr ef) (ef_po ef))
          [t_apply_r nf2; t_apply_r nf3; t_apply_r nf1])
       tc
 
@@ -1306,14 +1401,16 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
   (* equivF / ? / ? / ⊥                                                 *)
   | FequivF ef, Some _, Some _, None ->
     let m = EcIdent.create "&hr" in
-    let f3 = f_hoareF {m;inv=f_true} ef.ef_fr {m;inv=f_true} in
+    let post = {hsi_m=m;hsi_inv=empty_poe f_true} in
+    let f3 = f_hoareF {m;inv=f_true} ef.ef_fr post in
     t_hi_conseq notmod f1 f2 (Some (None, f3)) tc
 
   (* ------------------------------------------------------------------ *)
   (* equivF / ? / ⊥ / ?                                                 *)
   | FequivF ef, Some _, None, Some _ ->
     let m = EcIdent.create "&hr" in
-    let f2 = f_hoareF {m;inv=f_true} ef.ef_fl {m;inv=f_true} in
+    let post = {hsi_m=m;hsi_inv=empty_poe f_true} in
+    let f2 = f_hoareF {m;inv=f_true} ef.ef_fl post in
     t_hi_conseq notmod f1 (Some (None, f2)) f3 tc
 
   | _ ->
@@ -1345,38 +1442,18 @@ type processed_conseq_info =
 let process_info pe hyps m = function
   | CQI_bd (cmp, bd) -> PCI_bd (cmp, {m; inv=TTC.pf_process_form pe hyps treal bd})
 
-let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) tc =
+let process_conseq_2 notmod ((info1, info2, info3) : conseq_ppterm option tuple3) tc =
   let hyps, concl = FApi.tc1_flat tc in
 
   let ensure_none o =
     if not (is_none o) then tc_error !!tc "cannot give a bound here" in
 
-  let process_cut1 ((pre, post), bd) =
+  let ensure_none_poe poe =
+    if not (is_none poe) then tc_error !!tc "exception are not supported" in
+
+  let process_cut1 ((pre, post, poe), bd) =
      let penv, qenv, gpre, gpost, ty, fmake =
       match concl.f_node with
-      | FhoareS hs ->
-        let env = LDecl.push_active_ss hs.hs_m hyps in
-
-        let fmake pre post c_or_bd =
-          match c_or_bd with
-          | None ->
-            f_hoareS(snd hs.hs_m) pre hs.hs_s post
-          | Some (PCI_bd (cmp, bd)) ->
-            f_bdHoareS (snd hs.hs_m) pre hs.hs_s post (oget cmp) bd
-        in (env, env, Inv_ss (hs_pr hs), Inv_ss (hs_po hs), tbool, lift_ss_inv2 fmake)
-
-      | FhoareF hf ->
-        let penv, qenv = LDecl.hoareF hf.hf_m hf.hf_f hyps in
-
-        let fmake pre post c_or_bd =
-          match c_or_bd with
-          | None ->
-            f_hoareF pre hf.hf_f post
-          | Some (PCI_bd (cmp, bd)) ->
-            f_bdHoareF pre hf.hf_f post (oget cmp) bd
-
-        in (penv, qenv, Inv_ss (hf_pr hf), Inv_ss (hf_po hf), tbool, lift_ss_inv2 fmake)
-
       | FeHoareS hs ->
         let env = LDecl.push_active_ss hs.ehs_m hyps in
         let fmake pre post bd =
@@ -1435,6 +1512,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3)
       | _ -> tc_error !!tc "conseq: not a phl/prhl judgement"
     in
 
+    ensure_none_poe poe;
     let pre  = pre  |> omap (TTC.pf_process_form !!tc penv ty) |> odfl (inv_of_inv gpre)  in
     let post = post |> omap (TTC.pf_process_form !!tc qenv ty) |> odfl (inv_of_inv gpost) in
 
@@ -1450,32 +1528,12 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3)
     | _ -> tc_error !!tc "conseq: pre and post must be of the same kind" in
 
     fmake pre post bd
+
   in
 
-  let process_cut2 side f1 ((pre, post), c_or_bd) =
+  let process_cut2 side f1 ((pre, post, poe), c_or_bd) =
     let penv, qenv, gpre, gpost, ty, fmake =
       match concl.f_node with
-      | FhoareS hs ->
-        let env = LDecl.push_active_ss hs.hs_m hyps in
-        let fmake pre post c_or_bd =
-          ensure_none c_or_bd;
-          f_hoareS (snd hs.hs_m) pre hs.hs_s post
-        in (env, env, Inv_ss (hs_pr hs), Inv_ss (hs_po hs), tbool, lift_ss_inv2 fmake)
-
-      | FhoareF hf ->
-        let m = hf.hf_m in
-        let f, pr, po = match f1 with
-        | None -> hf.hf_f, hf_pr hf, hf_po hf
-        | Some f1 -> match (snd f1).f_node with
-                     | FequivF ef when side = `Left -> 
-                      ef.ef_fr, {m; inv=f_true}, {m; inv=f_true}
-                     | _ -> hf.hf_f, hf_pr hf, hf_po hf
-        in
-        let penv, qenv = LDecl.hoareF m f hyps in
-        let fmake pre post c_or_bd =
-          ensure_none c_or_bd; f_hoareF pre f post in
-        (penv, qenv, Inv_ss pr, Inv_ss po, tbool, lift_ss_inv2 fmake)
-
       | FeHoareF hf ->
         let f, pr, po, m = match f1 with
         | None -> hf.ehf_f, ehf_pr hf, ehf_po hf, hf.ehf_m
@@ -1494,21 +1552,23 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3)
       | FbdHoareS bhs ->
         let env = LDecl.push_active_ss bhs.bhs_m hyps in
         let fmake pre post c_or_bd =
-          ensure_none c_or_bd;
-          f_hoareS (snd bhs.bhs_m) pre bhs.bhs_s post
+          let post = empty_hs post in
+          ensure_none c_or_bd; f_hoareS (snd bhs.bhs_m) pre bhs.bhs_s post
         in (env, env, Inv_ss (bhs_pr bhs), Inv_ss (bhs_po bhs), tbool, lift_ss_inv2 fmake)
 
       | FbdHoareF bhf ->
         let f, pr, po, m = match f1 with
         | None -> bhf.bhf_f, bhf_pr bhf, bhf_po bhf, bhf.bhf_m
         | Some f1 -> match (snd f1).f_node with
-                     | FequivF ef when side = `Left -> ef.ef_fr, 
+                     | FequivF ef when side = `Left -> ef.ef_fr,
                         {m=ef.ef_mr;inv=f_true}, {m=ef.ef_mr;inv=f_true}, ef.ef_mr
                      | _ -> bhf.bhf_f, bhf_pr bhf, bhf_po bhf, bhf.bhf_m
         in
         let penv, qenv = LDecl.hoareF m f hyps in
         let fmake pre post c_or_bd =
-          ensure_none c_or_bd; f_hoareF pre f post in
+          let post = empty_hs post in
+          ensure_none c_or_bd; f_hoareF pre f post
+        in
         (penv, qenv, Inv_ss pr, Inv_ss po, tbool, lift_ss_inv2 fmake)
 
       | FequivF ef ->
@@ -1516,8 +1576,9 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3)
         let m = sideif side ef.ef_ml ef.ef_mr in
         let penv, qenv = LDecl.hoareF m f hyps in
         let fmake pre post c_or_bd =
-          ensure_none c_or_bd;
-          f_hoareF pre f post in
+          let post = empty_hs post in
+          ensure_none c_or_bd; f_hoareF pre f post
+        in
         let f_true = {m; inv=f_true} in
         (penv, qenv, Inv_ss f_true, Inv_ss f_true, tbool, lift_ss_inv2 fmake)
 
@@ -1537,6 +1598,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3)
             f_bdHoareS (snd m) pre f post cmp bd
 
           | _, None ->
+            let post = empty_hs post in
             f_hoareS (snd m) pre f post
 
           | _, Some (PCI_bd (cmp,bd)) ->
@@ -1548,6 +1610,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3)
       | _ -> tc_error !!tc "conseq: not a phl/prhl judgement"
     in
 
+    ensure_none_poe poe;
     let pre  = pre  |> omap (TTC.pf_process_form !!tc penv ty) |> odfl (inv_of_inv gpre)  in
     let post = post |> omap (TTC.pf_process_form !!tc qenv ty) |> odfl (inv_of_inv gpost) in
 
@@ -1563,7 +1626,6 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3)
     | _ -> tc_error !!tc "conseq: pre and post must be of the same kind" in
 
     fmake pre post c_or_bd
-
   in
 
   if   List.for_all is_none [info1; info2; info3]
@@ -1580,9 +1642,149 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3)
 
     t_hi_conseq notmod (f1 |> ofalse) (f2 |> ofalse) (f3 |> ofalse) tc
 
+let process_conseq_1 notmod ((info1, info2, info3) : conseq_ppterm option tuple3) tc =
+  let hyps, concl = FApi.tc1_flat tc in
+
+  let ensure_none o =
+    if not (is_none o) then tc_error !!tc "cannot give a bound here" in
+
+  let process_cut1 ((pre, post, poe), bd) =
+     let penv, qenv, env_e, gpre, gpost, ty, fmake =
+      match concl.f_node with
+      | FhoareS hs ->
+        let env = LDecl.push_active_ss hs.hs_m hyps in
+        let m,_ = hs.hs_m in
+        let env_e = LDecl.inv_memenv1 m hyps in
+
+        let fmake pre post c_or_bd =
+          match c_or_bd with
+          | None ->
+            f_hoareS(snd hs.hs_m) pre hs.hs_s post
+          | Some (PCI_bd (cmp, bd)) ->
+            if not (is_empty_poe post.hsi_inv) then
+              tc_error !!tc "exception are not supported";
+            let post = lower_f post in
+            f_bdHoareS (snd hs.hs_m) pre hs.hs_s post (oget cmp) bd
+        in
+        (env, env, env_e,
+         Inv_ss (hs_pr hs), Inv_hs (hs_po hs),
+         tbool, lift_hs_ss_inv fmake)
+
+      | FhoareF hf ->
+        let penv, qenv = LDecl.hoareF hf.hf_m hf.hf_f hyps in
+        let env_e = LDecl.inv_memenv1 hf.hf_m hyps in
+
+        let fmake pre post c_or_bd =
+          match c_or_bd with
+          | None ->
+            f_hoareF pre hf.hf_f post
+          | Some (PCI_bd (cmp, bd)) ->
+            if not (is_empty_poe post.hsi_inv) then
+              tc_error !!tc "exception are not supported";
+            let post = lower_f post in
+            f_bdHoareF pre hf.hf_f post (oget cmp) bd
+        in
+        (penv, qenv, env_e,
+         Inv_ss (hf_pr hf), Inv_hs (hf_po hf),
+         tbool, lift_hs_ss_inv fmake)
+
+      | _ -> tc_error !!tc "conseq: not a phl/prhl judgement"
+    in
+
+    let pre  = pre  |> omap (TTC.pf_process_form !!tc penv ty) |> odfl (inv_of_inv gpre) in
+    let post  = post  |> omap (TTC.pf_process_form !!tc qenv ty) in
+    let poe  = poe |> omap (TTC.pf_process_poe tc env_e ty) in
+
+    let (pre, post, bd) = match gpre, gpost with
+      | Inv_ss gpre, Inv_hs gpost ->
+        let bd = bd |> omap (process_info !!tc penv gpre.m) in
+        let (gp,gpoe,gd) = gpost.hsi_inv in
+        let post = post |> odfl gp in
+        let (poe,d) = poe |> odfl (gpoe, gd) in
+        (Inv_ss {inv=pre;m=gpre.m}, Inv_hs {hsi_inv=(post,poe,d);hsi_m=gpost.hsi_m}, bd)
+      | _ -> tc_error !!tc "conseq: pre and post must be of the same kind"
+    in
+    fmake pre post bd
+
+  in
+
+  let process_cut2 side f1 ((pre, post, poe), bd) =
+    let penv, qenv, env_e, gpre, gpost, ty, fmake =
+      match concl.f_node with
+      | FhoareS hs ->
+        let env = LDecl.push_active_ss hs.hs_m hyps in
+        let m,_ = hs.hs_m in
+        let env_e = LDecl.inv_memenv1 m hyps in
+        let fmake pre post c_or_bd =
+          ensure_none c_or_bd;
+          f_hoareS (snd hs.hs_m) pre hs.hs_s post
+        in
+        (env, env, env_e,
+         Inv_ss (hs_pr hs), Inv_hs (hs_po hs),
+         tbool, lift_hs_ss_inv fmake)
+
+      | FhoareF hf ->
+        let m = hf.hf_m in
+        let f, pr, po = match f1 with
+        | None -> hf.hf_f, hf_pr hf, hf_po hf
+        | Some f1 ->
+          match (snd f1).f_node with
+          | FequivF ef when side = `Left ->
+            ef.ef_fr, {m; inv=f_true}, {hsi_m=m; hsi_inv=empty_poe f_true}
+          | _ -> hf.hf_f, hf_pr hf, hf_po hf
+        in
+        let penv, qenv = LDecl.hoareF m f hyps in
+        let env_e = LDecl.inv_memenv1 m hyps in
+        let fmake pre post c_or_bd =
+          ensure_none c_or_bd; f_hoareF pre f post
+        in
+        (penv, qenv, env_e, Inv_ss pr, Inv_hs po, tbool, lift_hs_ss_inv fmake)
+
+      | _ -> tc_error !!tc "conseq: not a phl/prhl judgement"
+    in
+
+    let pre  = pre  |> omap (TTC.pf_process_form !!tc penv ty) |> odfl (inv_of_inv gpre)  in
+    let post  = post  |> omap (TTC.pf_process_form !!tc qenv ty) in
+    let poe  = poe |> omap (TTC.pf_process_poe tc env_e ty) in
+
+    let (pre, post, bd) = match gpre, gpost with
+      | Inv_ss gpre, Inv_hs gpost ->
+        let bd = bd |> omap (process_info !!tc penv gpre.m) in
+        let (gp,gpoe,gd) = gpost.hsi_inv in
+        let post = post |> odfl gp in
+        let (poe,d) = poe |> odfl (gpoe, gd) in
+        (Inv_ss {inv=pre;m=gpre.m}, Inv_hs {hsi_inv=(post,poe,d);hsi_m=gpost.hsi_m}, bd)
+      | _ -> tc_error !!tc "conseq: pre and post must be of the same kind"
+    in
+    fmake pre post bd
+
+  in
+
+  if List.for_all is_none [info1; info2; info3]
+  then t_id tc
+  else
+    let f1 = info1 |> omap (PT.tc1_process_full_closed_pterm_cut
+                              ~prcut:(process_cut1) tc) in
+    let f2 = info2 |> omap (PT.tc1_process_full_closed_pterm_cut
+                              ~prcut:(process_cut2 `Left f1) tc) in
+    let f3 = info3 |> omap (PT.tc1_process_full_closed_pterm_cut
+                              ~prcut:(process_cut2 `Right f1) tc) in
+
+    let ofalse = omap (fun (x, y) -> (Some x, y)) in
+
+    t_hi_conseq notmod (f1 |> ofalse) (f2 |> ofalse) (f3 |> ofalse) tc
+
+let process_conseq notmod
+    ((info1, info2, info3) : conseq_ppterm option tuple3) tc =
+  let _, concl = FApi.tc1_flat tc in
+
+  match concl.f_node with
+  | FhoareS _ | FhoareF _ -> process_conseq_1 notmod (info1, info2, info3) tc
+  | _ -> process_conseq_2 notmod (info1, info2, info3) tc
+
 (* -------------------------------------------------------------------- *)
 let process_bd_equiv side (pr, po) tc =
-  let info = FPCut ((Some pr, Some po), None) in
+  let info = FPCut ((Some pr, Some po, None), None) in
   let info = Some { fp_mode = `Implicit; fp_head = info; fp_args = []; } in
   let info2, info3 = sideif side (info, None) (None, info) in
   process_conseq true (None, info2, info3) tc
@@ -1612,10 +1814,15 @@ let process_conseq_opt cqopt infos tc =
 let t_conseqauto ?(delta = true) ?tsolve tc =
   let (hyps, concl), mk_other = FApi.tc1_flat tc, true in
 
+  let t_hoareF_notmod f = t_hoareF_notmod (lift_f f) in
+  let t_hoareS_notmod f = t_hoareS_notmod (lift_f f) in
+
   let todo =
     match concl.f_node with
-    | FhoareF hf  -> Some (lift_ss_inv t_hoareF_notmod, cond_hoareF_notmod ~mk_other tc (hf_po hf))
-    | FhoareS hs  -> Some (lift_ss_inv t_hoareS_notmod, cond_hoareS_notmod ~mk_other tc (hs_po hs) )
+    | FhoareF hf when (is_empty_poe (hf_po hf).hsi_inv) ->
+      Some (lift_ss_inv t_hoareF_notmod, cond_hoareF_notmod ~mk_other tc (lower_f (hf_po hf)))
+    | FhoareS hs when (is_empty_poe (hs_po hs).hsi_inv) ->
+      Some (lift_ss_inv t_hoareS_notmod, cond_hoareS_notmod ~mk_other tc (lower_f(hs_po hs)))
     | FbdHoareF hf -> Some (lift_ss_inv t_bdHoareF_notmod, cond_bdHoareF_notmod ~mk_other tc (bhf_po hf))
     | FbdHoareS hs -> Some (lift_ss_inv t_bdHoareS_notmod, cond_bdHoareS_notmod ~mk_other tc (bhs_po hs))
     | FequivF ef   -> Some (lift_ts_inv t_equivF_notmod, cond_equivF_notmod ~mk_other tc (ef_po ef))
diff --git a/src/phl/ecPhlConseq.mli b/src/phl/ecPhlConseq.mli
index 18c2c22e4..66e1965e3 100644
--- a/src/phl/ecPhlConseq.mli
+++ b/src/phl/ecPhlConseq.mli
@@ -11,8 +11,8 @@ open EcAst
 val t_equivF_conseq       : ts_inv -> ts_inv -> FApi.backward
 val t_equivS_conseq       : ts_inv -> ts_inv -> FApi.backward
 val t_eagerF_conseq       : ts_inv -> ts_inv -> FApi.backward
-val t_hoareF_conseq       : ss_inv -> ss_inv -> FApi.backward
-val t_hoareS_conseq       : ss_inv -> ss_inv -> FApi.backward
+val t_hoareF_conseq       : ss_inv -> hs_inv  -> FApi.backward
+val t_hoareS_conseq       : ss_inv -> hs_inv  -> FApi.backward
 val t_bdHoareF_conseq     : ss_inv -> ss_inv -> FApi.backward
 val t_bdHoareS_conseq     : ss_inv -> ss_inv -> FApi.backward
 
@@ -24,8 +24,8 @@ val t_bdHoareF_conseq_bd  : hoarecmp -> ss_inv -> FApi.backward
 (* -------------------------------------------------------------------- *)
 val t_equivF_conseq_nm    : ts_inv -> ts_inv -> FApi.backward
 val t_equivS_conseq_nm    : ts_inv -> ts_inv -> FApi.backward
-val t_hoareF_conseq_nm    : ss_inv -> ss_inv -> FApi.backward
-val t_hoareS_conseq_nm    : ss_inv -> ss_inv -> FApi.backward
+val t_hoareF_conseq_nm    : ss_inv -> hs_inv -> FApi.backward
+val t_hoareS_conseq_nm    : ss_inv -> hs_inv -> FApi.backward
 val t_bdHoareF_conseq_nm  : ss_inv -> ss_inv -> FApi.backward
 val t_bdHoareS_conseq_nm  : ss_inv -> ss_inv -> FApi.backward
 (* -------------------------------------------------------------------- *)
diff --git a/src/phl/ecPhlCoreView.ml b/src/phl/ecPhlCoreView.ml
index 5ae573517..3cd8014ac 100644
--- a/src/phl/ecPhlCoreView.ml
+++ b/src/phl/ecPhlCoreView.ml
@@ -10,7 +10,14 @@ let t_hoare_of_bdhoareS_r tc =
   let bhs = tc1_as_bdhoareS tc in
   if not (bhs.bhs_cmp = FHeq && f_equal (bhs_bd bhs).inv f_r0) then
     tc_error !!tc "%s" "bound must be equal to 0%r";
-  let concl = f_hoareS (snd bhs.bhs_m) (bhs_pr bhs) bhs.bhs_s (map_ss_inv1 f_not (bhs_po bhs)) in
+  let post = (map_ss_inv1 f_not (bhs_po bhs)) in
+  let concl =
+    f_hoareS (
+      snd bhs.bhs_m)
+      (bhs_pr bhs)
+      bhs.bhs_s
+      {hsi_m=post.m;hsi_inv=empty_poe post.inv}
+  in
   FApi.xmutate1 tc `ViewBdHoare [concl]
 
 (* -------------------------------------------------------------------- *)
@@ -19,19 +26,32 @@ let t_hoare_of_bdhoareF_r tc =
   if not (bhf.bhf_cmp = FHeq && f_equal (bhf_bd bhf).inv f_r0) then
     tc_error !!tc "%s" "bound must be equal to 0%r";
   let post = map_ss_inv1 f_not (bhf_po bhf) in
-  let concl = f_hoareF (bhf_pr bhf) bhf.bhf_f post in
+  let concl =
+    f_hoareF (bhf_pr bhf) bhf.bhf_f {hsi_m=post.m;hsi_inv=empty_poe post.inv}
+  in
   FApi.xmutate1 tc `ViewBdHoare [concl]
 
 (* -------------------------------------------------------------------- *)
 let t_bdhoare_of_hoareS_r tc =
   let hs = tc1_as_hoareS tc in
-  let concl = f_bdHoareS (snd hs.hs_m) (hs_pr hs) hs.hs_s (map_ss_inv1 f_not (hs_po hs)) FHeq {m=fst hs.hs_m;inv=f_r0} in
+  let (inv,_,_) as post = (hs_po hs).hsi_inv in
+  if not (is_empty_poe post) then
+    tc_error !!tc "Exceptions are not permitted";
+  let m = (hs_po hs).hsi_m in
+  let concl =
+    f_bdHoareS (snd hs.hs_m) (hs_pr hs) hs.hs_s (map_ss_inv1 f_not {m;inv}) FHeq {m=fst hs.hs_m;inv=f_r0}
+  in
   FApi.xmutate1 tc `ViewBdHoare [concl]
 
 (* -------------------------------------------------------------------- *)
 let t_bdhoare_of_hoareF_r tc =
   let hf = tc1_as_hoareF tc in
-  let concl = f_bdHoareF (hf_pr hf) hf.hf_f (map_ss_inv1 f_not (hf_po hf)) FHeq {m=hf.hf_m;inv=f_r0} in
+  let (inv,_,_) as post = (hf_po hf).hsi_inv in
+  if not (is_empty_poe post) then
+    tc_error !!tc "Exceptions are not permitted";
+  let m = (hf_po hf).hsi_m in
+  let concl =
+    f_bdHoareF (hf_pr hf) hf.hf_f (map_ss_inv1 f_not {m;inv}) FHeq {m=hf.hf_m;inv=f_r0} in
   FApi.xmutate1 tc `ViewBdHoare [concl]
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/phl/ecPhlEager.ml b/src/phl/ecPhlEager.ml
index 72859bb28..8beb3b0e5 100644
--- a/src/phl/ecPhlEager.ml
+++ b/src/phl/ecPhlEager.ml
@@ -143,7 +143,10 @@ let t_eager_if_r tc =
     EcSubst.f_forall_mems_ss_inv es.es_mr
       (map_ss_inv1
       (f_forall [(b, GTty tbool)])
-      (ts_inv_lower_left2 (fun pr po -> f_hoareS (snd es.es_ml) pr s po) (map_ts_inv2 f_and (es_pr es) eqb) eqb)) in
+      (ts_inv_lower_left2
+         (fun pr po -> f_hoareS (snd es.es_ml) pr s (empty_hs po))
+         (map_ts_inv2 f_and (es_pr es) eqb) eqb))
+  in
 
   let cT =
     let pre = map_ts_inv2 f_and (es_pr es) (map_ts_inv2 f_eq fel {ml;mr;inv=f_true}) in
@@ -467,13 +470,7 @@ let eager pf env s s' inv eqIs eqXs c c' eqO =
         (* (h) is assumed *)
         (fhyps, eqi)
 
-    | Sassert el, Sassert er ->
-        check_args [el];
-        let eqnm = Mpv2.split_nmod env modi modi' eqo in
-        let eqm  = Mpv2.split_mod  env modi modi' eqo in
-        if not (Mpv2.subset eqm eqXs) then raise EqObsInError;
-        let eqi = Mpv2.union eqIs eqnm in
-        (fhyps, Mpv2.add_eqs env el er eqi)
+    | Sraise _e1, Sraise _e2 -> assert false (* FIXME *)
 
     | Sabstract _, Sabstract _ -> assert false (* FIXME *)
 
@@ -605,7 +602,7 @@ let process_fun_abs info eqI tc =
 let process_call info tc =
   let process_cut info =
     match info with
-    | EcParsetree.CI_spec (fpre, fpost) ->
+    | EcParsetree.CI_spec (fpre, fpost, ([],None)) ->
         let env, hyps, _ = FApi.tc1_eflat tc in
         let es  = tc1_as_equivS tc in
 
diff --git a/src/phl/ecPhlEqobs.ml b/src/phl/ecPhlEqobs.ml
index 8466ac935..0beaf5c3a 100644
--- a/src/phl/ecPhlEqobs.ml
+++ b/src/phl/ecPhlEqobs.ml
@@ -277,7 +277,6 @@ and i_eqobs_in il ir sim local (eqo:Mpv2.t) =
     let eqs = List.fold_left2 doit Mpv2.empty bsl bsr in
     !rsim, add_eqs !rsim local eqs el er
 
-  | Sassert el, Sassert er -> sim, add_eqs sim local eqo el er
   | _, _ -> raise EqObsInError
 
 and s_eqobs_in_full sl sr sim local eqo =
diff --git a/src/phl/ecPhlExists.ml b/src/phl/ecPhlExists.ml
index 70776aceb..474107e2a 100644
--- a/src/phl/ecPhlExists.ml
+++ b/src/phl/ecPhlExists.ml
@@ -27,8 +27,10 @@ let get_to_gens fs =
       | Inv_ts f -> begin match f.inv.f_node with
           | Fpvar (pv, m) -> 
             id_of_pv ~mc:(f.ml, f.mr) pv m
-          | _             -> EcIdent.create "f" 
-        end in
+          | _             -> EcIdent.create "f"
+        end
+      | Inv_hs _ -> assert false
+    in
     id, f in
   List.map do_id fs
 
@@ -70,12 +72,16 @@ let t_hr_exists_intro_r fs tc =
   let ms =
     match pre1 with
     | Inv_ts _ -> [ml; mr]
-    | Inv_ss _ -> [m] in
+    | Inv_ss _ -> [m]
+    | Inv_hs _ -> assert false
+  in
 
   let inv_rebind f =
     match f with
     | Inv_ts f -> Inv_ts (ts_inv_rebind f ml mr)
-    | Inv_ss f -> Inv_ss (ss_inv_rebind f m) in
+    | Inv_ss f -> Inv_ss (ss_inv_rebind f m)
+    | Inv_hs f -> Inv_hs (hs_inv_rebind f m)
+  in
 
   let args =
     let do1 (_, f) = PAFormula (inv_of_inv (inv_rebind f)) in
@@ -155,6 +161,9 @@ let process_ecall oside (l, tvi, fs) tc =
     | `Hoare n, _, Inv_ss p1 ->
         EcPhlApp.t_hoare_app
           (Zpr.cpos (n-1)) p1 tc
+    | `Hoare n, _, Inv_hs p1 ->
+        EcPhlApp.t_hoare_app
+          (Zpr.cpos (n-1)) (lower_f p1) tc
     | `Equiv (n1, n2), None, Inv_ts p1 ->
         EcPhlApp.t_equiv_app
           (Zpr.cpos (n1-1), Zpr.cpos (n2-1)) p1 tc
@@ -206,7 +215,6 @@ let process_ecall oside (l, tvi, fs) tc =
       List.fold_left2
         (fun s id f -> add_flocal s id (inv_of_inv f))
         empty (List.fst ids) fs in
-
     (nms, subst_inv subst sub) in
 
   let tc = t_local_seq p1 tc in
diff --git a/src/phl/ecPhlFel.ml b/src/phl/ecPhlFel.ml
index 8d4e44c34..1ae0112c8 100644
--- a/src/phl/ecPhlFel.ml
+++ b/src/phl/ecPhlFel.ml
@@ -103,7 +103,7 @@ and callable_oracles_i env modv os i =
     | Smatch (_, b)      -> callable_oracles_sx env modv os (List.map snd b)
     | Sif    (_, s1, s2) -> callable_oracles_sx env modv os [s1; s2]
 
-    | Sasgn _ | Srnd _ | Sassert _ -> os
+    | Sasgn _ | Srnd _ | Sraise _ -> os
 
     | Sabstract _ -> assert false (* FIXME *)
 
@@ -188,7 +188,8 @@ let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc =
     let pre = map_ss_inv f_ands (eqparams :: (eqxs@eqgs)) in
     let p = map_ss_inv2 f_and (map_ss_inv1 f_not f_event) (map_ss_inv2 f_eq cntr {m=cntr.m;inv=f_i0}) in
     let p = map_ss_inv2 f_and_simpl p inv in
-    let p = EcSubst.ss_inv_rebind p pre.m in
+    let p = {hsi_m=p.m;hsi_inv=(empty_poe p.inv)} in
+    let p = EcSubst.hs_inv_rebind p pre.m in
     f_hoareS (snd memenv) pre (stmt s_hd) p
   in
 
@@ -220,7 +221,8 @@ let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc =
       let pre = map_ss_inv2 f_and_simpl pre inv in
       let post = map_ss_inv2 f_int_lt old_cntr cntr in
       let post = map_ss_inv2 f_and_simpl post inv in
-        f_forall_simpl [old_cntr_id,GTty tint] (f_hoareF pre o post)
+      let post = {hsi_m=post.m;hsi_inv=(empty_poe post.inv)} in
+      f_forall_simpl [old_cntr_id,GTty tint] (f_hoareF pre o post)
     in
     let cntr_stable_goal =
       let old_cntr = {m=cntr.m;inv=old_cntr} in
@@ -232,6 +234,7 @@ let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc =
       let pre  = map_ss_inv2 f_and_simpl pre inv in
       let post = map_ss_inv f_ands [map_ss_inv2 f_eq f_event old_b; map_ss_inv2 f_int_le old_cntr cntr] in
       let post = map_ss_inv2 f_and_simpl post inv in
+      let post = {hsi_m=post.m;hsi_inv=(empty_poe post.inv)} in
         f_forall_simpl
           [old_b_id,GTty tbool; old_cntr_id,GTty tint]
           (f_hoareF pre o post)
diff --git a/src/phl/ecPhlFun.ml b/src/phl/ecPhlFun.ml
index 004e191ce..f65f7b0e0 100644
--- a/src/phl/ecPhlFun.ml
+++ b/src/phl/ecPhlFun.ml
@@ -79,8 +79,11 @@ let t_hoareF_fun_def_r tc =
   let (memenv, (fsig, fdef), env) = Fun.hoareS hf.hf_m f env in
   let m = EcMemory.memory memenv in
   let fres = odfl {m;inv=f_tt} (omap (ss_inv_of_expr m) fdef.f_ret) in
-  let post = map_ss_inv2 (PVM.subst1 env pv_res m) fres (hf_po hf) in
+  let (post,epost,d) = (hf_po hf).hsi_inv in
+  let post = {m=(hf_po hf).hsi_m;inv=post} in
+  let post = map_ss_inv2 (PVM.subst1 env pv_res m) fres  post in
   let pre  = map_ss_inv1 (PVM.subst env (subst_pre env fsig m PVM.empty)) (hf_pr hf) in
+  let post = {hsi_m=post.m;hsi_inv=(post.inv,epost,d)} in
   let concl' = f_hoareS (snd memenv) pre fdef.f_body post in
   FApi.xmutate1 tc `FunDef [concl']
 
@@ -160,7 +163,7 @@ module FunAbsLow = struct
     let (top, _, oi, _) = EcLowPhlGoal.abstract_info env f in
     let fv = PV.fv env inv.m inv.inv in
     PV.check_depend env fv top;
-    let ospec o = f_hoareF inv o inv in
+    let ospec o = f_hoareF inv o (lift_f inv) in
     let sg = List.map ospec (OI.allowed oi) in
     (inv, inv, sg)
 
@@ -248,7 +251,7 @@ let t_hoareF_abs_r inv tc =
   let pre, post, sg = FunAbsLow.hoareF_abs_spec !!tc env hf.hf_f inv in
 
   let tactic tc = FApi.xmutate1 tc `FunAbs sg in
-  FApi.t_last tactic (EcPhlConseq.t_hoareF_conseq pre post tc)
+  FApi.t_last tactic (EcPhlConseq.t_hoareF_conseq pre (lift_f post) tc)
 
 let t_ehoareF_abs_r inv tc =
   let env = FApi.tc1_env tc in
@@ -425,8 +428,8 @@ let t_fun_to_code_hoare_r tc =
   let spr = ToCodeLow.add_var_tuple env pv_arg m a m PVM.empty in
   let spo = ToCodeLow.add_var env pv_res m r m PVM.empty in
   let pre  = PVM.subst env spr (hf_pr hf).inv in
-  let post = PVM.subst env spo (hf_po hf).inv in
-  let concl = f_hoareS mt {m;inv=pre} st {m;inv=post} in
+  let post = map_poe (PVM.subst env spo) (hf_po hf).hsi_inv in
+  let concl = f_hoareS mt {m;inv=pre} st {hsi_m=m;hsi_inv=post} in
   FApi.xmutate1 tc `FunToCode [concl]
 
 (* -------------------------------------------------------------------- *)
@@ -536,7 +539,7 @@ let t_fun_r (inv: inv) tc =
   let th tc =
     let inv = match inv with
       | Inv_ss inv -> inv
-      | Inv_ts _ -> tc_error !!tc "expected a single sided invariant" in
+      | _ -> tc_error !!tc "expected a single sided invariant" in
     let env = FApi.tc1_env tc in
     let h   = destr_hoareF (FApi.tc1_goal tc) in
       if   NormMp.is_abstract_fun h.hf_f env
@@ -546,7 +549,7 @@ let t_fun_r (inv: inv) tc =
   and teh tc =
     let inv = match inv with
       | Inv_ss inv -> inv
-      | Inv_ts _ -> tc_error !!tc "expected a single sided invariant" in
+      |  _ -> tc_error !!tc "expected a single sided invariant" in
     let env = FApi.tc1_env tc in
     let h   = destr_eHoareF (FApi.tc1_goal tc) in
       if   NormMp.is_abstract_fun h.ehf_f env
@@ -556,7 +559,7 @@ let t_fun_r (inv: inv) tc =
   and tbh tc =
     let inv = match inv with
       | Inv_ss inv -> inv
-      | Inv_ts _ -> tc_error !!tc "expected a single sided invariant" in
+      |  _ -> tc_error !!tc "expected a single sided invariant" in
     let env = FApi.tc1_env tc in
     let h   = destr_bdHoareF (FApi.tc1_goal tc) in
       if   NormMp.is_abstract_fun h.bhf_f env
@@ -566,7 +569,7 @@ let t_fun_r (inv: inv) tc =
   and te tc =
     let inv = match inv with
       | Inv_ts inv -> inv
-      | Inv_ss _ -> tc_error !!tc "expected a two sided invariant" in
+      | _ -> tc_error !!tc "expected a two sided invariant" in
     let env = FApi.tc1_env tc in
     let e   = destr_equivF (FApi.tc1_goal tc) in
       if   NormMp.is_abstract_fun e.ef_fl env
diff --git a/src/phl/ecPhlInline.ml b/src/phl/ecPhlInline.ml
index d40f5ab8b..a8aab8b2d 100644
--- a/src/phl/ecPhlInline.ml
+++ b/src/phl/ecPhlInline.ml
@@ -50,7 +50,7 @@ module LowSubst = struct
     | Sif    (c, s1, s2) -> i_if     (esubst c, ssubst s1, ssubst s2)
     | Swhile (e, stmt)   -> i_while  (esubst e, ssubst stmt)
     | Smatch (e, bs)     -> i_match  (esubst e, List.Smart.map (snd_map ssubst) bs)
-    | Sassert e          -> i_assert (esubst e)
+    | Sraise e           -> i_raise  e
     | Sabstract _        -> i
 
   and issubst m (is : instr list) =
diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml
index 434dece2c..3d249ba63 100644
--- a/src/phl/ecPhlLoopTx.ml
+++ b/src/phl/ecPhlLoopTx.ml
@@ -67,7 +67,7 @@ let check_dslc pf =
     | Smatch (_, bs) ->
        List.iter (doit_s |- snd) bs
 
-    | Srnd _ | Scall _ | Swhile _ | Sassert _  | Sabstract _ ->
+    | Srnd _ | Scall _ | Swhile _ | Sraise _  | Sabstract _ ->
        error ()
 
   and doit_s c =
@@ -306,8 +306,11 @@ let process_unroll_for side cpos tc =
   let t_conseq_nm tc =
     match (tc1_get_pre tc) with
     | Inv_ss inv ->
-      (EcPhlConseq.t_hoareS_conseq_nm inv {m=inv.m;inv=f_true} @+
-      [ t_trivial; t_trivial; EcPhlTAuto.t_hoare_true]) tc
+      (EcPhlConseq.t_hoareS_conseq_nm
+         inv
+         {hsi_m=inv.m;hsi_inv=empty_poe f_true}
+       @+
+       [ t_trivial; t_trivial; EcPhlTAuto.t_hoare_true]) tc
     | _ -> tc_error !!tc "expecting single sided precondition" in
 
   let doi i tc =
diff --git a/src/phl/ecPhlRCond.ml b/src/phl/ecPhlRCond.ml
index d45a50ede..1a5379353 100644
--- a/src/phl/ecPhlRCond.ml
+++ b/src/phl/ecPhlRCond.ml
@@ -37,6 +37,8 @@ module Low = struct
     let hs = tc1_as_hoareS tc in
     let m  = EcMemory.memory hs.hs_m in
     let hd,_,e,s = gen_rcond (!!tc, env) b m at_pos hs.hs_s in
+    let (_,epost,d) = (hs_po hs).hsi_inv in
+    let e = {hsi_m=e.m;hsi_inv=(e.inv,epost,d)} in
     let concl1  = f_hoareS (snd hs.hs_m) (hs_pr hs) hd e in
     let concl2  = f_hoareS (snd hs.hs_m) (hs_pr hs) s (hs_po hs) in
     FApi.xmutate1 tc `RCond [concl1; concl2]
@@ -52,6 +54,7 @@ module Low = struct
       | o, pre :: _ when f_equal o fop_interp_ehoare_form -> pre
       | _ -> tc_error !!tc "the pre should have the form \"_ `|` _\"" in
     let pre = map_ss_inv1 pre (ehs_pr hs) in
+    let e = {hsi_m=e.m;hsi_inv=empty_poe e.inv} in
 
     let concl1  = f_hoareS (snd hs.ehs_m) pre hd e in
     let concl2  = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) s (ehs_po hs) in
@@ -63,6 +66,8 @@ module Low = struct
     let bhs = tc1_as_bdhoareS tc in
     let m  = EcMemory.memory bhs.bhs_m in
     let hd,_,e,s = gen_rcond (!!tc, env) b m at_pos bhs.bhs_s in
+    let e = {hsi_m=e.m;hsi_inv=empty_poe e.inv} in
+
     let concl1  = f_hoareS (snd bhs.bhs_m) (bhs_pr bhs) hd e in
     let concl2  = f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) s (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in
     FApi.xmutate1 tc `RCond [concl1; concl2]
@@ -85,6 +90,7 @@ module Low = struct
           let mhs = EcIdent.create "&hr" in
           let pr = ss_inv_rebind pr mhs in
           let po = ss_inv_rebind po mhs in
+          let po = {hsi_m=po.m;hsi_inv=empty_poe po.inv} in
           f_hoareS (snd m) pr hd po) (es_pr es) e) in
     let sl,sr = match side with `Left -> s, es.es_sr | `Right -> es.es_sl, s in
     let concl2 = f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) sl sr (es_po es) in
@@ -221,6 +227,8 @@ module LowMatch = struct
       gen_rcond_full (!!tc, FApi.tc1_env tc) c hs.hs_m at_pos hs.hs_s in
 
     let pr = ofold (map_ss_inv2 f_and) (hs_pr hs) epr in
+    let (_,eposts,d) = (hs_po hs).hsi_inv in
+    let po1 = {hsi_m=po1.m;hsi_inv=(po1.inv,eposts,d)} in
 
     let concl1  = f_hoareS (snd hs.hs_m) (hs_pr hs) hd po1 in
     let concl2  = f_hoareS (snd me) pr full (hs_po hs) in
@@ -247,6 +255,7 @@ module LowMatch = struct
       gen_rcond_full (!!tc, FApi.tc1_env tc) c bhs.bhs_m at_pos bhs.bhs_s in
 
     let pr = ofold (map_ss_inv2 f_and) (bhs_pr bhs) epr in
+    let po1 ={hsi_m=po1.m;hsi_inv=empty_poe po1.inv} in
 
     let concl1 = f_hoareS (snd bhs.bhs_m) (bhs_pr bhs) hd po1 in
     let concl2 = f_bdHoareS (snd me) pr full (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in
@@ -275,6 +284,7 @@ module LowMatch = struct
     let ts_inv_lower_side1 =
       sideif side ts_inv_lower_left1 ts_inv_lower_right1 in
 
+    let po1 ={hsi_m=po1.m;hsi_inv=empty_poe po1.inv} in
     let concl1 =
       f_forall_mems_ss_inv mo
         (ts_inv_lower_side1 (fun pr -> f_hoareS (snd m) pr hd po1) (es_pr es)) in
diff --git a/src/phl/ecPhlRnd.ml b/src/phl/ecPhlRnd.ml
index 35bb3de4d..e517fe03b 100644
--- a/src/phl/ecPhlRnd.ml
+++ b/src/phl/ecPhlRnd.ml
@@ -34,9 +34,14 @@ module Core = struct
     let x_id = EcIdent.create (symbol_of_lv lv) in
     let x = {m; inv=f_local x_id ty_distr} in
     let distr = EcFol.ss_inv_of_expr m distr in
-    let post = subst_form_lv env lv x (hs_po hs) in
+    if (not (is_empty_poe (hs_po hs).hsi_inv)) then
+      tc_error !!tc "exceptions are not supported";
+    let (post, _, _) = (hs_po hs).hsi_inv in
+    let post ={m=(hs_po hs).hsi_m; inv=post}in
+    let post = subst_form_lv env lv x post in
     let post = map_ss_inv2 f_imp (map_ss_inv2 f_in_supp x distr) post in
     let post = map_ss_inv1 (f_forall_simpl [(x_id,GTty ty_distr)]) post in
+    let post = lift_f post in
     let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s post in
     FApi.xmutate1 tc `Rnd [concl]
 
@@ -219,6 +224,7 @@ module Core = struct
           let bounded_distr = map_ss_inv2 f_real_le (map_ss_inv2 (f_mu env) distr event) bound in
           let pre = map_ss_inv2 f_and (bhs_pr bhs) pre_bound in
           let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in
+          let post = lift_f post in
           let concl = f_hoareS (snd bhs.bhs_m) pre s post in
           let concl = f_forall_simpl binders concl in
           [concl]
@@ -244,6 +250,7 @@ module Core = struct
           let bounded_distr = map_ss_inv2 f_real_le (map_ss_inv2 (f_mu env) distr event) bound in
           let pre = map_ss_inv2 f_and (bhs_pr bhs) pre_bound in
           let post = map_ss_inv2 f_anda bounded_distr (mk_event_cond event) in
+          let post = lift_f post in
           let concl = f_hoareS (snd bhs.bhs_m) pre s post in
           let concl = f_forall_simpl binders concl in
           [concl]
@@ -400,12 +407,17 @@ module Core = struct
     let env = FApi.tc1_env tc in
     let hs = tc1_as_hoareS tc in
     let s1, s2 = o_split env (Some pos) hs.hs_s in
+    if (not (is_empty_poe (hs_po hs).hsi_inv)) then
+      tc_error !!tc "exceptions are not supported";
+    let post = lower_f (hs_po hs) in
     let fv =
       if reduce then
-        Some (PV.fv (FApi.tc1_env tc) (fst hs.hs_m) (hs_po hs).inv)
+        Some (PV.fv (FApi.tc1_env tc) (fst hs.hs_m) post.inv)
       else None in
     let (_, mt), s2 = semrnd tc hs.hs_m fv s2 in
-    let concl = f_hoareS mt (hs_pr hs) (stmt (s1 @ s2)) (hs_po hs) in
+    let concl =
+      f_hoareS mt (hs_pr hs) (stmt (s1 @ s2)) (hs_po hs)
+    in
     FApi.xmutate1 tc (`RndSem pos) [concl]
 
  (* -------------------------------------------------------------------- *)
diff --git a/src/phl/ecPhlRwPrgm.ml b/src/phl/ecPhlRwPrgm.ml
index c24953924..59d165a88 100644
--- a/src/phl/ecPhlRwPrgm.ml
+++ b/src/phl/ecPhlRwPrgm.ml
@@ -23,10 +23,11 @@ let process_idassign ((cpos, pv) : idassign_t) (tc : tcenv1) =
     let s = Zpr.zipper_of_cpos env cpos hs.hs_s in
     let s = { s with z_tail = sasgn :: s.z_tail } in
     { hs with hs_s = Zpr.zip s } in
-  FApi.xmutate1 tc `IdAssign [EcFol.f_hoareS (snd hs.hs_m) (hs_pr hs) (hs.hs_s) (hs_po hs)]
+  FApi.xmutate1 tc `IdAssign
+    [EcFol.f_hoareS (snd hs.hs_m) (hs_pr hs) (hs.hs_s) (hs_po hs)]
 
 (* -------------------------------------------------------------------- *)
 let process_rw_prgm (mode : rwprgm) (tc : tcenv1) =
-  match mode with 
+  match mode with
   | `IdAssign (cpos, pv) ->
     process_idassign (cpos, pv) tc
diff --git a/src/phl/ecPhlSkip.ml b/src/phl/ecPhlSkip.ml
index 0f57a38b7..ec6aa200b 100644
--- a/src/phl/ecPhlSkip.ml
+++ b/src/phl/ecPhlSkip.ml
@@ -16,7 +16,8 @@ module LowInternal = struct
     if not (List.is_empty hs.hs_s.s_node) then
       tc_error !!tc "instruction list is not empty";
 
-    let concl = map_ss_inv2 f_imp (hs_pr hs) (hs_po hs) in
+    let post = lower_f (hs_po hs) in
+    let concl = map_ss_inv2 f_imp (hs_pr hs) post in
     let concl = EcSubst.f_forall_mems_ss_inv hs.hs_m concl in
 
     FApi.xmutate1 tc `Skip [concl]
diff --git a/src/phl/ecPhlSp.ml b/src/phl/ecPhlSp.ml
index ec3b2eb36..c0155d70a 100644
--- a/src/phl/ecPhlSp.ml
+++ b/src/phl/ecPhlSp.ml
@@ -246,7 +246,13 @@ let t_sp_side pos tc =
       let stmt1, hs_pr = LI.sp_stmt hs.hs_m env stmt1 (hs_pr hs).inv in
       check_sp_progress pos stmt1;
       let m = fst hs.hs_m in
-      let subgoal = f_hoareS (snd hs.hs_m) {m;inv=hs_pr} (stmt (stmt1@stmt2)) (hs_po hs) in
+      let subgoal =
+        f_hoareS
+          (snd hs.hs_m)
+          {m;inv=hs_pr}
+          (stmt (stmt1@stmt2))
+          (hs_po hs)
+      in
       FApi.xmutate1 tc `Sp [subgoal]
 
 
diff --git a/src/phl/ecPhlTAuto.ml b/src/phl/ecPhlTAuto.ml
index ed07c0359..62e8a8c60 100644
--- a/src/phl/ecPhlTAuto.ml
+++ b/src/phl/ecPhlTAuto.ml
@@ -6,12 +6,13 @@ open EcCoreGoal
 open EcLowPhlGoal
 
 (* -------------------------------------------------------------------- *)
+
 let t_hoare_true_r tc =
   match (FApi.tc1_goal tc).f_node with
-  | FhoareF hf when f_equal (hf_po hf).inv f_true ->
+  | FhoareF hf when forall_poe (f_equal f_true) (hf_po hf).hsi_inv ->
       FApi.xmutate1 tc `HoareTrue []
 
-  | FhoareS hs when f_equal (hs_po hs).inv f_true ->
+  | FhoareS hs when forall_poe (f_equal f_true) (hs_po hs).hsi_inv ->
       FApi.xmutate1 tc `HoareTrue []
 
   | _ ->
diff --git a/src/phl/ecPhlUpto.ml b/src/phl/ecPhlUpto.ml
index 7dc597b9e..e019ddd0a 100644
--- a/src/phl/ecPhlUpto.ml
+++ b/src/phl/ecPhlUpto.ml
@@ -62,7 +62,7 @@ let rec check_bad_true env bad s =
     | Smatch(_,bs) ->
       let check_branch (_, s) = check_bad_true env bad s.s_node in
       List.iter (check_branch) bs
-    | Sassert _ -> ()
+    | Sraise _ -> assert false
     | Sabstract _ -> ()
     end;
     check_bad_true env bad c
@@ -142,8 +142,7 @@ and i_upto env alpha bad i1 i2 =
     with E.NotConv -> false
   end
 
-  | Sassert a1, Sassert a2 ->
-    EqTest.for_expr env ~alpha a1 a2
+  | Sraise e1, Sraise e2 -> EcPath.p_equal e1 e2
 
   | Sabstract id1, Sabstract id2 ->
     EcIdent.id_equal id1 id2
diff --git a/src/phl/ecPhlWhile.ml b/src/phl/ecPhlWhile.ml
index c54b43ea4..89290aa1f 100644
--- a/src/phl/ecPhlWhile.ml
+++ b/src/phl/ecPhlWhile.ml
@@ -42,8 +42,7 @@ let while_info env e s =
         let f = EcEnv.NormMp.norm_xfun env f in
         (w, r, Sx.add f c)
 
-    | Sassert e ->
-        (w, e_read_r env r e, c)
+    | Sraise _ -> assert false
 
     | Sabstract id ->
         let add_pv x (pv,ty) = PV.add env pv ty x in
@@ -70,15 +69,19 @@ let t_hoare_while_r inv tc =
   let e = ss_inv_of_expr m e in
   (* the body preserves the invariant *)
   let b_pre  = map_ss_inv2 f_and_simpl inv e in
-  let b_post = inv in
+  let inv = EcSubst.ss_inv_rebind inv (hs_po hs).hsi_m in
+  let b_post = update_hs_ss inv (hs_po hs) in
   let b_concl = f_hoareS mt b_pre c b_post in
   (* the wp of the while *)
   let f_imps_simpl' f = f_imps_simpl (List.tl f) (List.hd f) in
-  let post = map_ss_inv f_imps_simpl' [hs_po hs;map_ss_inv1 f_not_simpl e; inv]  in
+  let post =
+    map_ss_inv f_imps_simpl' [lower_f (hs_po hs);map_ss_inv1 f_not_simpl e; inv]
+  in
   let modi = s_write env c in
   let post = generalize_mod_ss_inv env modi post in
   let post = map_ss_inv2 f_and_simpl inv post in
-  let concl = f_hoareS mt (hs_pr hs) s post in
+  let post = update_hs_ss post (hs_po hs) in
+  let concl = f_hoareS mt (hs_pr hs) s post  in
 
   FApi.xmutate1 tc `While [b_concl; concl]
 
@@ -187,7 +190,8 @@ let t_bdhoare_while_rev_r inv tc =
       (map_ss_inv2 f_eq bound {m;inv=f_r1}) in
     let term_post = generalize_mod_ss_inv env modi term_post in
     let term_post = map_ss_inv2 f_and inv term_post in
-    f_hoareS mt b_pre rem_s term_post
+    let post = {hsi_m=term_post.m;hsi_inv=empty_poe term_post.inv} in
+    f_hoareS mt b_pre rem_s post
   in
 
   FApi.xmutate1_hyps tc `While [(hyps', body_concl); (hyps, rem_concl)]
@@ -662,13 +666,13 @@ let process_async_while (winfos : EP.async_while_info) tc =
       let el = ss_inv_generalize_right (ss_inv_of_expr ml el) mr in
       let pre = map_ts_inv f_ands [inv; el ; map_ts_inv1 f_not p0; p1] in
       EcSubst.f_forall_mems_ss_inv evs.es_mr
-        (ts_inv_lower_left2 (fun pr po -> f_hoareS (snd evs.es_ml) pr cl po) pre inv)
+        (ts_inv_lower_left2 (fun pr po -> f_hoareS (snd evs.es_ml) pr cl (lift_f po)) pre inv)
 
     and hr2 =
       let er = ss_inv_generalize_left (ss_inv_of_expr mr er) ml in
       let pre = map_ts_inv f_ands [inv; er; map_ts_inv1 f_not p0; map_ts_inv1 f_not p1] in
       EcSubst.f_forall_mems_ss_inv evs.es_ml
-        (ts_inv_lower_right2 (fun pr po -> f_hoareS (snd evs.es_mr) pr cr po) pre inv)
+        (ts_inv_lower_right2 (fun pr po -> f_hoareS (snd evs.es_mr) pr cr (lift_f po)) pre inv)
 
     in (hr1, hr2)
   in
diff --git a/src/phl/ecPhlWp.ml b/src/phl/ecPhlWp.ml
index 49a8d6d13..b6c12f8ad 100644
--- a/src/phl/ecPhlWp.ml
+++ b/src/phl/ecPhlWp.ml
@@ -3,6 +3,7 @@ open EcUtils
 open EcAst
 open EcModules
 open EcFol
+open EcMaps
 
 open EcCoreGoal
 open EcLowPhlGoal
@@ -11,32 +12,39 @@ open EcLowPhlGoal
 module LowInternal = struct
   exception No_wp
 
+  let find_poe (epost,d) (e:EcPath.path) =
+    try DMap.find e epost with
+    | Not_found ->
+      match d with
+      | Some d -> d
+      | None -> tacuerror "unknow exception %a" EcPrinting.pp_path e
+
   let wp_asgn_aux c_pre memenv lv e (lets, f) =
     let m = EcMemory.memory memenv in
     let let1 = lv_subst ?c_pre m lv (ss_inv_of_expr m e).inv in
       (let1::lets, f)
 
   let rec wp_stmt ?mc
-      onesided c_pre env memenv (stmt: EcModules.instr list) letsf
+      onesided c_pre env memenv (stmt: EcModules.instr list) letsf epost
   =
     match stmt with
     | [] -> (stmt, letsf)
     | i :: stmt' ->
         try
-          let letsf = wp_instr ?mc onesided c_pre env memenv i letsf in
-          wp_stmt ?mc onesided c_pre env memenv stmt' letsf
+          let letsf = wp_instr ?mc onesided c_pre env memenv i letsf epost in
+          wp_stmt ?mc onesided c_pre env memenv stmt' letsf epost
         with No_wp -> (stmt, letsf)
 
-  and wp_instr ?mc onesided c_pre env memenv i letsf =
+  and wp_instr ?mc onesided c_pre env memenv i letsf epost =
     match i.i_node with
     | Sasgn (lv,e) ->
       wp_asgn_aux c_pre memenv lv e letsf
 
     | Sif (e,s1,s2) ->
         let (r1,letsf1) =
-          wp_stmt ?mc onesided c_pre env memenv (List.rev s1.s_node) letsf in
+          wp_stmt ?mc onesided c_pre env memenv (List.rev s1.s_node) letsf epost in
         let (r2,letsf2) =
-          wp_stmt ?mc onesided c_pre env memenv (List.rev s2.s_node) letsf in
+          wp_stmt ?mc onesided c_pre env memenv (List.rev s2.s_node) letsf epost in
         if List.is_empty r1 && List.is_empty r2 then begin
           let post1 = mk_let_of_lv_substs ?mc:mc env letsf1 in
           let post2 = mk_let_of_lv_substs ?mc:mc env letsf2 in
@@ -49,7 +57,7 @@ module LowInternal = struct
     | Smatch (e, bs) -> begin
         let wps =
           let do1 (_, s) =
-            wp_stmt ?mc onesided c_pre env memenv (List.rev s.s_node) letsf in
+            wp_stmt ?mc onesided c_pre env memenv (List.rev s.s_node) letsf epost in
           List.map do1 bs
         in
 
@@ -70,10 +78,7 @@ module LowInternal = struct
         ([],post)
       end
 
-    | Sassert e when onesided ->
-        let phi = ss_inv_of_expr (EcMemory.memory memenv) e in
-        let lets, f = letsf in
-        (lets, EcFol.f_and_simpl phi.inv f)
+    | Sraise e when onesided -> ([], find_poe epost e)
 
     | _ -> raise No_wp
 
@@ -120,10 +125,10 @@ module LowInternal = struct
 
 end
 
-let wp ?mc ?(uselet=true) ?(onesided=false) ?c_pre env m s post =
+let wp ?mc ?(uselet=true) ?(onesided=false) ?c_pre env m s (post,epost,d) =
   let (r, letsf) =
     LowInternal.wp_stmt ?mc
-      onesided c_pre env m (List.rev s.s_node) ([], post)
+      onesided c_pre env m (List.rev s.s_node) ([], post) (epost,d)
   in
   let pre = mk_let_of_lv_substs ?mc ~uselet env letsf in
   List.rev r, pre
@@ -144,12 +149,14 @@ module TacInternal = struct
     let hs = tc1_as_hoareS tc in
     let (s_hd, s_wp) = o_split env i hs.hs_s in
     let s_wp = EcModules.stmt s_wp in
+    let (_, eposts,d) as post = (hs_po hs).hsi_inv in
     let s_wp, post =
-      wp ~uselet ~onesided:true env hs.hs_m s_wp (hs_po hs).inv in
+      wp ~uselet ~onesided:true env hs.hs_m s_wp post in
     check_wp_progress tc i hs.hs_s s_wp;
     let s = EcModules.stmt (s_hd @ s_wp) in
     let m = fst hs.hs_m in
-    let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s {m;inv=post} in
+    let post ={hsi_m=m;hsi_inv=(post,eposts,d)} in
+    let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s post in
     FApi.xmutate1 tc `Wp [concl]
 
   let t_ehoare_wp ?(uselet=true) i tc =
@@ -169,7 +176,9 @@ module TacInternal = struct
     let bhs = tc1_as_bdhoareS tc in
     let (s_hd, s_wp) = o_split env i bhs.bhs_s in
     let s_wp = EcModules.stmt s_wp in
-    let s_wp,post = wp ~uselet env bhs.bhs_m s_wp (bhs_po bhs).inv in
+    let s_wp,post =
+      wp ~uselet env bhs.bhs_m s_wp (empty_poe (bhs_po bhs).inv)
+    in
     check_wp_progress tc i bhs.bhs_s s_wp;
     let s = EcModules.stmt (s_hd @ s_wp) in
     let m = fst bhs.bhs_m in
@@ -186,8 +195,12 @@ module TacInternal = struct
     let meml, s_wpl = es.es_ml, EcModules.stmt s_wpl in
     let memr, s_wpr = es.es_mr, EcModules.stmt s_wpr in
     let post = es_po es in
-    let s_wpl, post = wp ~mc:(ml,mr) ~uselet env meml s_wpl post.inv in
-    let s_wpr, post = wp ~mc:(ml,mr) ~uselet env memr s_wpr post in
+    let s_wpl, post =
+      wp ~mc:(ml,mr) ~uselet env meml s_wpl (empty_poe post.inv)
+    in
+    let s_wpr, post =
+      wp ~mc:(ml,mr) ~uselet env memr s_wpr (empty_poe post)
+    in
     check_wp_progress tc i es.es_sl s_wpl;
     check_wp_progress tc j es.es_sr s_wpr;
     let sl = EcModules.stmt (s_hdl @ s_wpl) in