Created attachment 299 [details] stratego model demonstrating the problem (see the 1st query) The attached model demonstrates the problem. The problem does not appear in 4.1.20-2 version and it is not manifest for simple simulations. This is specific to optimization query in 4.1.20-3, something is odd with evaluating possible successors when processing optimization query.
Created attachment 319 [details] Initial state sometimes fails for optimising query with time-locked error This model sometimes fails optimisation queries, and it fails for all version of stratego (4.1.20-*). I have tried queries on the form E[] time < 10, so see if I can find live locks, but have not found any.
There seems to be an issue with CSDecorator; CSDecorator.maxDelay() returns inf even when CSDecorator.zeroDelay() returns true. The problem can be fixed by replacing the maxDelay() implementation with double maxDelay() const { return cannotDelay ? 0 : max; } The method is only called in very few places, so I belive this fix is sound.
*** Bug 678 has been marked as a duplicate of this bug. ***
@pgj the fix seems to have been applied, but the issue is still there.
stratego-5 does not show this issue. stratego-6 and stratego-7 complains