Property verified on larger input box, but may be violated on strict subset [SpacecraftDocking]

[HyberionBrew]

When running SpacecraftDocking on the default input set
X₀ = Hyperrectangle(low=[70, 70, -0.14, -0.14], high=[106, 106, 0.14, 0.14]),
verified is returned.
Surprisingly (to me), when reducing the input set to
X₀ = Hyperrectangle(low=[70.0, 70.0, -0.14, -0.14],high=[80, 80, -0.1, -0.1],) may be violated gets returned.

I'm curious why this could be the case, and if this is a bug, as I would expect a subset of the original set to be easier to verify.

To reproduce: clone the repo and run 'SpacecraftDocking.jl' with the two different input sets; nothing else was changed.

Additionally, one of the simulations appears to be outside the yellow (overapproximated?) region when examining the returned .png.

.toml:
Project.txt

[schillic]

You are right that this is wrong. Specifically, the issue is that the variables for dimensions 3 and 4 are not updated correctly for the original set (left plot). They are updated correctly for your reduced set (right plot).

We are aware of a bug in the TaylorModels algorithm, but we cannot fix it. I presume it happens here if 0 is included in the initial set for dimensions 3 and 4 (which is not the case for your updated initial set).

(FWIW, the investigation also uncovered another bug in the specification.)

[HyberionBrew]

Thank you very much for the fast answer! Is there a correct/reasonable way to work around the bug in the TaylorModels, or must I use a different framework? If I always exclude 0, should no bug occur?

[schillic]

If I always exclude 0, should no bug occur?

This was only speculation. Nobody knows the root cause of the bug (main reason why it is not fixed). So I unfortunately cannot give you a workaround. My best advice is to avoid models where this problem occurs; if you have to use the model, look at the plot and compare to the simulations.