Basile Clément

Quick proof of concept (the code for array models needs to be adapted): ```patch diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml index cb8e1170..b14b3d56 100644 --- a/src/lib/reasoners/records.ml +++ b/src/lib/reasoners/records.ml @@ -390,12 +390,12 @@ module...

> I think we have to accept `Name { ns = User; _ }` in `is_model_term` too? I don't think so (and I think that is the source of the...

After investigations, it does not look like it is a problem with the new intervals module, but rather a pre-existing incompleteness issue in either the arithmetic or FPA modules (in...

As discussed privately, this seems to be because Dolmen ignores ``Exit` statements, while solvers are expected to quit when encountering them.

After thinking about it I am a bit on the fence on the topic. I would like the Dolmen experience to be consistent w.r.t builtins: either a builtin is fully...

@Gbury I think this can be merged, I'll do another PR with additional Alt-Ergo primitives.

I think we can disable typer extensions, it should just be a matter of resetting the appropriate key on the state (it might not be exposed but we can expose...

@Gbury ping — if you agree with the analysis above, removing the Tableaux-CDCL variant would make it easier to implement features needed for FPA support in the CDCL (and CDCL-Tableaux)...

I have a half-finished PR for this lying around somewhere — I will try to dig it up.

> It also fixes an issue in the (unused) unsafe_nocopy_to_array for floats where we call unsafe_get before checking for the dummy. I said it's not used, but that's because I...