How sure are you that you don't have the words "minimal" and "maximal" switched here?

In particular, later in variance.rs you say that `solve_constraints` finds the maximal solution.

Also, since `invariant` is at the Bottom of the lattice, I take it to be "below" the other elements of the lattice, and a minimal solution would be one that tends to favor choices towards the bottom of the lattice rather than towards the top, right?

(I might be confused myself.  Or it might be that the paper is confusing us since it is the one that chose to write the lattice with `bivariant` at the top, when I myself would probably have put it at the bottom.  But again, maybe I am myself confused.)