Adding ensuring(rec < ...) in a function prevents other functions from being verified

[BLepers]

Strange issue :)

   def insertBack(c: Core, t: Task): Core = {
      require(!contains(c.tasks, t))
      if(containsEquivLemma(c.tasks, t, tick(t))) {
         Core(c.id, sortedIns(c.tasks, tick(t)), None[Task]())
      } else {
         error[Core]("Tick changes task id\n");
      }
   }

   def test(c: Core): Core = {
      c
   } ensuring(rec < 5);

Without the "test" function insertBack is successfully verified by Leon. Adding test prevents insertBack from being verified. The issue is due to the "rec < 5".

Here is a more complete example: Scheduler-simple.txt (If you comment the "test" function, the code verifies.)

I've tried comparing the --instrument output with and without the test function. The layout is different, but I haven't spotted any significant change (might be worth double-checking though).

git bisect blames 0ba77a29cb46ebb60237395747a348df23b515a4 for the problem.