Ravichandhran Madhavan

Sorry for the delayed reponse. Can you send me the source file Scheduler.scala ? Btw, you may have try out the latest updates to the Orb (resource bounds) inference engine,...

At line 396, the code uses 'rec' in the body of the function. Instrumentation variables `rec` and `steps`, `alloc` should be used only in the postcondition (only then they have...

Btw, if for some reason you need to count the number of recursions in the implementation, you have to maintain a counter say `c` and use it instead. However, in...

The minimal example is much better for me to debug. In your example, there is a function called `rec` so Scala compiler thinks you are referring to the function `rec`...

As the counter-example indicates: c.a could be greater than c.max and hence the function may not terminate

There is one subtle issue here. The above function is non-terminating since you are making the recursive call with the same argument. Did you mean rec(c2) ? In any case,...

Actually, it is somewhat unsound in your example because your example does not terminate on all inputs. As I had mentioned, you must make sure that all functions terminate. Run...

I will look into the crash

I have fixed the crash in your example. Can you try it again. But, remember that you need to check termination of all functions as well.

I don't get this error. Did you compile the build ? Also, can you run without --functions option. Also send me the Scheduler.scala file you are using.