Associativity in floating point arithmetic failing by two values

Question

Assume all numbers and operations below are in floating-point arithmetic with finite precision, bounded exponent, and rounding to the nearest integer.

Are there $x,y$ positive such that $$\begin{align}(x+y)-x&>y\\(x+y)-s(x)&>y\end{align}$$ where $s(x)$ denotes the successor of $x$?

---

This question appeared while designing a test for a software.

It is easy to write a program that searches for such an example, but it is unfeasible to test all possibilities and show that the example doesn't exist. So far my code hasn't got any example.

Example: In case seeing an example of $(x+y)-x>y$ helps somehow, take $$ \begin{align} x&=1.1234567891234568\\ y&=1e-5\text{ ( denoting }10^{-5}) \end{align} $$ Then $(x+y)-x=1.0000000000065512e-05 > y$. There are many examples of the first inequality.

---

Link to scicomp.stackexchange's copy of this post in case a solution appears there first. There is already a solution there.

Answer 1

This is precisely the kind of question that an SMT solver like Z3 was made to solve. We can use the following python code:

from z3 import *

x = FP('x', FPSort(8,24))
y = FP('y', FPSort(8,24))

s = Solver()
s.add((x + y) - x > y)
s.add((x + y) - (x+1) > y)
print(s.check())
print(s.model())

This will create two local representations of floating point numbers (the FPSort specifies how many bits of exponent, followed by how many bits of data, so these are 32 bit floats), and then attempt to find a model where both of the required statements are true. We run this code and get the following model:

[x = -1.869740962982177734375*(2**127),
y = -1.47381579875946044921875*(2**127)]