discrete `and(X, next(Y))` drop `next(Y)` when X large-magnitude

[tsindel-pecz]

Env

• rtamt==0.3.5, py3.10

Symptom

StlDiscreteTimeSpecification, formula eventually((X) and next(Y)). Y ignored.
Result = just robustness(X) at binding sample. next(Y) never gate result.

Trigger condition

Bug show only when X large-magnitude (real signal scale, e.g. ~1e5). Small ±1
boolean-style signals (x,y in {-1,1}) — NOT trigger bug, and+next work fine there.

Minimal repro (standalone, no custom helper fn)

import rtamt

dataset = {
    'time': [0, 1, 2, 3, 4, 5],
    'x': [136900.0, 136900.0, 136900.0, 0.0, 0.0, 136900.0],  # drop to 0 at t=3
}

spec = rtamt.StlDiscreteTimeSpecification()
spec.declare_var('x', 'float')
spec.set_var_io_type('x', 'input')
spec.spec = 'eventually((x > 0) and next(abs(x) <= 1e-3))'
spec.set_sampling_period(1, 's', 0.1)
spec.parse()
rob_wave = spec.evaluate(dataset)
print(rob_wave)
print(rob_wave[0][1])

Result

[[0, 136900.0], [1, 136900.0], [2, 136900.0], [3, 136900.0], [4, 136900.0], [5, 136900.0]]
rho_global = 136900.0

Expect vs actual

• Expect: small POSITIVE (~1e-3), only real gate = t=2→3 transition (x[2]>0
  AND x[3]≈0 within tol). Everywhere else next(Y) false → AND false.
• Actual: 136900.0 constant everywhere = raw x>0 robustness at t=0. Looks
  like next(Y) clause silently drop from and, whole formula collapse to X alone.