Basile Clément

EDIT: I made a dumb typo. The average don't look right, but the slowdown is always around 4%. Ah, I seemed to recall different numbers. But there is still a...

Assuming that by "the SAT API" you mean the `Frontend` / `Sat_solver_sig` API, they don't currently have a concept of symbols being declared; switching to using the Dolmen AST instead...

I am not sure we should be inspecting the formulas for this; it'd be better to have some sort of context object (see e.g. Z3's API) to keep track of...

> The following test have a different behavior given if the push instruction is here or not: Can you clarify what behavior is different and if either behavior is incorrect/unsound?

Interesting. I actually don't understand how we prove this in the first place… Here is a simpler example that we are able to prove: ```smt-lib (set-logic ALL) (declare-datatype t ((A)...

Ah, interesting. Did it only happen once, or does it keep happening? In the latter case, we should open a bug report on the dune repo.

Before reviewing the code in detail, I want to better understand what we are trying to achieve with that feature, so I will only make high-level remarks here. It was...

We don't have support for the smtlib FloatingPoint theory as far as I'm aware (we only have support for floating-point rounding with underflow, but nothing related to NaNs, infinites, or...

Benchmarks are +9-3 on benchtop-tests and +24-6 on ae-format (from a cursory look at the actual problems, this seems to come from the more precise tracking of explanations performed by...

@Gbury given that you have made a bunch of fixes to the intervals module in the past & some conversations we had wrt API for this module, I'd appreciate your...