Change BiAbd search to take into account modality compatibility
For a goal Δ, P ⊢ SolveSep M Q T
and a BiAbd P ∗ [R] ⊲ [M2] Q ∗ [S]
, compatibility of M
and M2
is only tested after the BiAbd is found. Also, search then just fails, and does not look for other instances with possibly compatible modalities.
The fixed algorithm should not make that last mistake. Additionally, by adding a fupd-open modality for invariants/accessors, this should also prevent invariant reentrancy.