Christian Schilling

I think there are some confusions here. Some observations: 1. With the current implementation, `a ⊂ b` is *not* equivalent to `a ⊆ interior(b)`, even in 1D. Hence I think...

The [installation instructions](https://github.com/ultimate-pa/ultimate/wiki/Installation) are now updated for Eclipse Oxygen.

Is it not even worse if the removal of redundant constraints from an empty set results in a non-empty set?

> Isn't the bug in CDD ? The problem also occurs with the "default library". (EDIT: simplified the numbers) ```julia for backend in [CDDLib.Library(), default_library(2, Float64)] p = polyhedron(hrep([HalfSpace([1.0, 0.0],...

Confirmed in Julia v1.6.0 (and Polyhedra v0.6.13): ```julia julia> using Polyhedra julia> poly = polyhedron(HalfSpace([-1.0, 0.0], 0.0) ∩ HalfSpace([0.0, -1.0], 0.0) ∩ HalfSpace([1.0, 0.0], 1.0) ∩ HalfSpace([0.0, 1.0], 1.0) ∩...

That or always use `solver = default_solver(p)` (but maybe there is a reason for not doing that).

Yes, I used `GLPK` but the default is `nothing`. https://github.com/JuliaPolyhedra/Polyhedra.jl/blob/485f7dfb2abb93b9032d711bc017c355796ad02e/src/default.jl#L45-L51 https://github.com/JuliaPolyhedra/Polyhedra.jl/blob/485f7dfb2abb93b9032d711bc017c355796ad02e/src/defaultlibrary.jl#L11-L13

It goes to line 72 which is the `solver === nothing` branch. The error message say that `presolve` was not activated but I think the solver I passed had it...

But that one does not have `presolve` activated.

~I tried to reproduce what I did but the behavior is not the same as in the OP. I guess I did not pass the solver to the correct polyhedron...