Here is an example of a loop translated by TinyBCT in which corral reaches the recursion bound. However the same loop translated by BCT, corral is able to prove no bugs without reaching the recursion bound.
The procedure (name in dll) is STATE$System_Collections2_Queue_ContainsSystem_Object$System_Collections2_Queue_EnqueueSystem_Object~System_Collections2_Queue_ContainsSystem_Object~System_Collections2_Queue_ContainsSystem_Object
It is declared in System.Collections2.Queue
The BCT version that I used is the present in contractor-net dependencies folder.
Here is an example of a loop translated by TinyBCT in which corral reaches the recursion bound. However the same loop translated by BCT, corral is able to prove no bugs without reaching the recursion bound.
The procedure (name in dll) is STATE$System_Collections2_Queue_ContainsSystem_Object$System_Collections2_Queue_EnqueueSystem_Object~System_Collections2_Queue_ContainsSystem_Object~System_Collections2_Queue_ContainsSystem_Object
It is declared in System.Collections2.Queue
The BCT version that I used is the present in contractor-net dependencies folder.
Queue.zip Password: tinybct