From f94d1b5a21d63e2146dda06eb791ccce3660b7ea Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 14 Feb 2025 17:58:08 +0100 Subject: [PATCH] Add a link to issue 1296 --- src/lib/reasoners/adt_rel.ml | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index 2dbdda111..dbda63748 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -472,15 +472,9 @@ let build_constr_eq r c = in let xs = List.map (fun (_, ty) -> E.fresh_name ty) ds in let cons = E.mk_constr c xs ty in - (* In `X.make`, we produce a non-empty context for record constructors. - In the below case, the context [ctx] has the form: - cons.x1 = .k1, ..., cons.xn = .kn - where x1, ..., xn are the record fields and .k1, ..., .kn are fresh - terms generated earlier. - - Usually, the equations of the context are propagated as facts to - CC(X) via [Ccx.add_term]. Since .ki are fresh terms, adding these - facts could not contribute to any meaningful reasoning. *) + (* XXX: we do not propagate the context of X.make to the matching + environment. It could be better to do it. See issue + https://github.com/OCamlPro/alt-ergo/issues/1296 *) let r', _ctx = X.make cons in let eq = Shostak.L.(view @@ mk_eq r r') in Some (eq, cons)