Basile Clément
Basile Clément
Actually this case might be covered by the use of `explain_repr_of_distinct`? Marking as draft until I investigate further.
Would it make sense to use [dune-site's plugin mechanism](https://dune.readthedocs.io/en/stable/sites.html#plugins-and-dynamic-loading-of-packages) for this? Dolmen could expose a registry of builtins that plugins can register themselves into to provide the implementation of such...
I took a quick look. It is more complicated than I expected because we also need to be able to *type* the builtins, which I think the right way to...
Is there a reason for refusing to check models with an `unknown` status? My understanding of the SMT-LIB specification is that the solver should move to `sat` mode after replying...
Maybe display warnings rather than errors for failed assertions?
This function: ```alt-ergo logic match_bool : bool, 'a, 'a -> 'a ``` which is at the top of every Alt-Ergo file generated by Why3 does not seem to translate with...
> the existing `bvconv` extension is moved to use the plugin mechanism In retrospect, I am not 100% sure this is a good idea. I did this initially to have...
> > the existing `bvconv` extension is moved to use the plugin mechanism This was causing build failures on the CI so no longer part of the PR. Instead there...
I did some late cleanup but this should be ready to review @Gbury
Made the requested changes + some others following (old) offline discussions: - Move code dealing with extensions out of the Options module and into a new Extensions module - Clean...