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.