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.