Does BilevelJuMP linearize terms (if possible) after reformulation?

How does BilevelJuMP.jl deal with non-linear terms in the complementarity conditions arising from the product of dual variables and the upper-level variables, especially when the upper-level variables are binary?
For example, suppose we have a model as follows:

using JuMP, BilevelJuMP, Gurobi

model = BilevelModel(Gurobi.Optimizer, mode = BilevelJuMP.SOS1Mode())

@variable(Lower(model), x)
@variable(Upper(model), y, Bin)

@objective(Upper(model), Min, 3x + y)
@constraints(Upper(model), begin
    x <= 5
    y <= 8
    y >= 0
end)

@objective(Lower(model), Min, -x)
@constraints(Lower(model), begin
     x +  y <= 8
    4x +  y >= 8
    2x +  y <= 13
    2x - 7y <= 0
end)

optimize!(model)

Now, in theory, if we write the KKT of the lower level problem, we will have terms where the Lagrange multipliers are multiplied to the binary variable y , leading to non-linearity. However, since this is a product of a binary variable and a continuous variable, in practice, we can linearize such terms, eventually leading to a single-level LP problem. Does BilevelJuMP.jl do it automatically, or does it treat it as a non-linear problem? Additionally, if BilevelJuMP.jl does not eliminate these bilinear terms, does a solver like Gurobi detect it and linearize it?

Thanks.

This is what happens. Gurobi automatically linearizes x * y if x is binary.

(It can even solve if x is not binary, but that’s a different problem.)

Thanks @odow. I had another question: during the KKT reformulation of the lower-level problem, BilevelJuMP treats y as a parameter (since y is an upper-level variable)? Is that right?