The boolean operator "imply" is broken when used with clocks in UPPAAL SMC

[scarburato]

Describe the bug

SMC expressions like t >= 3 imply expr, where t is a clock, return always false, unless the clock value is cast to a float.

For instance

• Pr[<= 200] ([] t >= 180 imply car.v >= 26) is estimated to be ~0%
• Pr[<= 200] ([] fabs(t) >= 180 imply car.v >= 26) is estimated to be ~34%
• Pr[<= 200] ([] 1.0*t >= 180 imply car.v >= 26) is estimated, again, to be ~34%

To Reproduce

1. Open the bug report.xml in UPPAAL
2. Go the "Verifier" tab
3. Run the Pr queries (There's also a simulate query that causes a crash, like described in boolean expression with a clock in a simulate query results in segfault #307)
4. You'll see mismatching results. For instance the result of Pr[<= 200] ([] fabs(t) >= 180 imply car.v >= 26) is different from the result of Pr[<= 200] ([] t >= 180 imply car.v >= 26)

Expected behavior

Expressions with imply should work as expected.

Version(s) of UPPAAL tested
UPPAAL 5.0.0 (rev. 714BA9DB36F49691), 2023-06-21
UPPAAL 5.1.0-beta5 (rev. C7C01B0740E14075), 2023-12-11

Desktop (please complete the following information):

• Version 5.0.0.
• OS Ubuntu 24.04.3
• Java:

openjdk version "21.0.8" 2025-07-15
OpenJDK Runtime Environment (build 21.0.8+9-Ubuntu-0ubuntu124.04.1)
OpenJDK 64-Bit Server VM (build 21.0.8+9-Ubuntu-0ubuntu124.04.1, mixed mode, sharing)

Additional context

I'm having the same issue on my laptop running Arch Linux

[mikucionisaau]

Thank you for the nice report.
I see that Uppaal also crashes on simulate[<=200;10]{t>=180}, which tells me that t>=180 is being interpreted as a symbolic constraint, which is wrong in SMC context.
So that explains the error and it is not an issue with imply itself, it just helped uncover the bug.
The conversion to float by multiplying or adding 0.0 is a good workaround.