From e9db423b6824713cede751f96720a54cecd76ea5 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Mon, 10 Aug 2026 11:29:08 +0200 Subject: [PATCH] use memory bound by Pr in fel post --- src/phl/ecPhlFel.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/phl/ecPhlFel.ml b/src/phl/ecPhlFel.ml index dfb9d2203..8ea5e6e5b 100644 --- a/src/phl/ecPhlFel.ml +++ b/src/phl/ecPhlFel.ml @@ -126,7 +126,6 @@ let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc = | _ -> tc_error !!tc "a goal of the form Pr[ _ ] <= _ is required" in - let pr_m = oget (Memory.byid pr.pr_mem env) in let f = NormMp.norm_xfun env pr.pr_fun in let ev = pr.pr_event in @@ -161,7 +160,7 @@ let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc = (* we must quantify over memories *) let post_goal = let lev = map_ss_inv2 f_and f_event (map_ss_inv1 (fun cnt -> f_int_le cnt q) cntr) in - let m = (EcIdent.create "&hr", snd pr_m) in + let m = EcEnv.Fun.prF_memenv ev.m f env in let lev = EcSubst.ss_inv_rebind lev (fst m) in let ev = EcSubst.ss_inv_rebind ev (fst m) in let inv = EcSubst.ss_inv_rebind inv (fst m) in