Skip to content

Fix a regression in ecall from #789 #833

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
strub merged 1 commit into from
Nov 18, 2025
Merged

Fix a regression in ecall from #789 #833

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 8 additions & 5 deletions src/phl/ecPhlExists.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,18 +56,21 @@ let t_hr_exists_intro_r fs tc =
| FeHoareF _ | FeHoareS _ -> true
| _ -> false in
let pre =
let eqs = match eqs with
| [] -> map_inv1 (fun _ -> f_true) pre1
| _ -> map_inv f_ands eqs in
if is_ehoare then
map_inv2 f_interp_ehoare_form (map_inv1 (f_exists bd) (map_inv f_ands eqs)) pre1
map_inv2 f_interp_ehoare_form (map_inv1 (f_exists bd) eqs) pre1
else
map_inv1 (f_exists bd) (map_inv2 f_and (map_inv f_ands eqs) pre1) in
map_inv1 (f_exists bd) (map_inv2 f_and eqs pre1) in

let h = LDecl.fresh_id hyps "h" in
let ml, mr = as_seq2 (LDecl.fresh_ids hyps ["&ml"; "&mr"]) in
let m = LDecl.fresh_id hyps "&m" in
let ms =
match List.hd gen with
| (_, Inv_ts _) -> [ml; mr]
| (_, Inv_ss _) -> [m] in
match pre1 with
| Inv_ts _ -> [ml; mr]
| Inv_ss _ -> [m] in

let inv_rebind f =
match f with
Expand Down