If the return value of a function is used to bound a clock in an invariant or a
guard, the engine segfaults (or fails in an assertion if assertions are enabled)
if the return type of the function is not explicitly bounded.
Created attachment 62 [details]
Minimal test case
A fix has been checkd into CVS.