Xavier Denis

Ah yes, i understand why this happens but we should just silently swallow the variant instead.

> Could we emit a warning instead? I understand that you may want to do this, but having a variant clause on a trusted function is not something that one...

Really, we only need this for `Resolve` and I actually think that even for that we might be able to instead use a default instance on `Resolve`!

This is quite a tricky issue, it arises when the loop is no longer a loop in the underlying MIR, so we are correct to say there is no loop...

We're correct to error as the underlying stackify algorithm in why3 will have exactly the same issue when it attempts to attach the `invariant` to a loop since it won't...

This is a bool field on basic blocks so it shouldn't be hard to check

> Hmm I don't see what problem would be solved by using smallvec. It will store the data inline under a certain size rather than performing a seperate allocation. >...

> I think the good design is to have the clause db be a 1d vec with manual handling of clauses as a header and lits. This is the part...

Right now things look something like this ``` ┌─────┐ │ l_0 │ ├─────┤ ┌──────►│ │ ┌────────┐ │ ├─────┤ │ c_0 │ ─────┘ │ l_i │ ├────────┤ └─────┘ │ │ ├────────┤...

> It seems like we might be talking past each other. ClauseDB = formula, and does thus not add another level of indirection. I was using ClauseDB to refer specifically...