epfl-lara/leon — pull request #36 by xcodevn (2013-09-19 14:01:00+00:00)
Title: Fixed a bug, using old blockers which causes Leon unrolling forever in some cases (e.g Red-Black Tree)

This bug, I found when try to understand why sometimes Leon returns right answer and sometimes it runs forever.

The problem is that when we get list of id of blockers, Scala returns a randomize order of ids (because we get the list from a map). In some "right order", we will not get into the situation, re-use old blocker ids. In some other, we re-use old blocker ids and .....

I fixed this bug by checking if we re-use a old blocker id or not. Now, Leon does well with my example and with Red-black tree also. But I'm not sure whether it really fixed the problem ;)