Basile Clément

> The second issue is more serious. It will hide a bug in CDCL. The symbol f should not be in the union-find after (pop 1), but it still appears...

Yes I understand you were not looking for this specifically — all I am saying is that I don't think it is worth expending too much effort fixing it in...

I don't think this is related to Dolmen -- this file is also proved by the legacy frontend. This seems to be due to the [`Backward` instantiation pass](https://github.com/OCamlPro/alt-ergo/blob/e32e5755f5b9d81967066ea08f74971486a024eb/src/lib/reasoners/fun_sat.ml#L1527) which seems...

Ah duh. Yeah I don't think we can preserve the current API then :cry:

Oh, I forgot this was an issue for theories that create fresh terms… I think for the purpose of #1095 as long as there are no regressions it is OK...

As discussed previously, I believe a (the?) good criterion is to extend the well-founded criterion to also include non-mutually-recursive **parametric** datatypes, because the well-foundedness of a parametric datatype can in...

Sorry, I got confused — I was thinking of this part of the SMT-LIB criterion: > The datatype δ must be well founded in the following inductive > sense: it...

> Oh, I missed that part. Then I'm confused. The above example (with mutually recursive `list` and `tree`) is rejected by Dolmen, and if it's not by that criterion, I...

Ah, yes. `list` is not the issue, `tree` is — got it. Thanks for the explanation.

Actually there is a difference between `additional_builtins` and extensions: `additional_builtins` give access to the state, while extensions do not. I'm not sure if this functionality is needed (in fact I...