Basile Clément

Some updates here: - Doing constraint propagation on `bv2nat` and `int2bv` is not easy to do properly, because we don't have access to the arithmetic domains from `Bitv_rel` - This...

The PR shouldn't block additional improvements to command line parsing (which, indeed, is a mess); the behavior change itself is trivial and can easily be replicated if command line parsing...

Note: this is +107-515 or a net regression of about 400 problems on our QF_BV subset. This is expected: this PR uses bit-vector domains for `bvule` / `bvult` / etc....

After reading and thinking a lot (and starting a small Coq developement) about the explanations for intervals: - I am quite confident that the `map_monotone` function introduced in this PR,...

> I am quite confident that the map_monotone function introduced in this PR, and the map2_monotone function introduced inhttps://github.com/OCamlPro/alt-ergo/pull/1085, are correct Turns out they are not (: I thought I...

Everything except for changes to the `Intervals.ml` module is still valid and can be reviewed. There are subtleties in the interval module (I am starting to believe that there are...

> Honestly, when I read this module months ago, my conclusion was we should rewrite it completely. It's not a priority but I plan to work on it later. I...

I have adapted the code on top of #1108 (unfortunately I messed up the rebase so the history is a bit weird, apologies for that!).

> I am about 99% sure there currently are soundness bugs that can be triggered by properly crafted formulas so I am actually looking into it now. Hopefully I will...

The total time above is for all problems, not only `unsat` problems I believe?