From 4ea0644dc1a2c4d83b8d672c7eec0d57f2095df4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Tue, 7 May 2024 17:24:22 +0200 Subject: [PATCH] fix(UF): Use proper explanation for neqs when initializing leaf 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`. --- src/lib/reasoners/uf.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 53ccef25e..c693b64a6 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -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