Christian Schilling

> we need to pass `overapproximation` to discrete solver Yeah, obviously :wink: > we need to pass `block_options` to continuous solver I do not see why. The clustering happens in...

I noticed that we might not even properly support this type in the input. It currently only makes sense if `δ` is fixed by the user. Otherwise the discretization that...

Okay for later, but then I suggest that we should currently crash if the time steps do not coincide.

An idea could be that we add a variant where we compute the inputs lazily. This is interesting for the check mode with early termination.

We should separate algorithm-specific options and outsource them to the respective `PostOperator`s. It is not totally clear how to do that, maybe with a filter (but careful: some of the...

It would be helpful to have an example (model, branches, etc.) for debugging.

This is the default implementation: https://github.com/JuliaReach/Reachability.jl/blob/156e5f5a3fb38176de897625044dc3574fedfee5/src/ReachSets/DiscretePost/DiscretePost.jl#L100-L104 We override this policy for `LazyDiscretePost`: https://github.com/JuliaReach/Reachability.jl/blob/156e5f5a3fb38176de897625044dc3574fedfee5/src/ReachSets/DiscretePost/LazyDiscretePost.jl#L203-L214 So the question is whether you use `LazyDiscretePost` or a different operator. What is your expected result?

#415 made the subindices optional.

#712 used option 2 (i.e., it changed the default to not use subindices). The remaining action point here is to add the option 1 to the documentation.

True, the "real" solution is to have #255. Both approaches are not perfect. The current implementation uses functions that are not supposed to be used that way. So it is...