Skip to content

Commit

Permalink
fix(UF): Use proper explanation for neqs when initializing leaf
Browse files Browse the repository at this point in the history
When initializing a leaf, the equality `p = rp` between `p` and its
normal form `rp` w.r.t the current environment is justified by `ex_rp`,
which is usually but not necessarily `Ex.empty` and needs to be added to
a conflict found while adding the equality `p = rp`.
  • Loading branch information
bclement-ocp committed May 7, 2024
1 parent e91bd66 commit 4ea0644
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/lib/reasoners/uf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -529,7 +529,7 @@ module Env = struct
else add_to_gamma p rp env.gamma ;
neqs =
if MapX.mem p env.neqs then env.neqs
else update_neqs p rp Ex.empty env }
else update_neqs p rp ex_rp env }
in
Debug.check_invariants "init_leaf" env;
env
Expand Down

0 comments on commit 4ea0644

Please sign in to comment.