Baptiste Lepers

File attached. [Scheduler.txt](https://github.com/epfl-lara/leon/files/380946/Scheduler.txt) Now I have the following error: :) ``` ../leon/leon Scheduler.scala --functions=testEvolutionSimpleProofRec scala.MatchError: rec$0 (of class leon.purescala.Expressions$FunctionInvocation) at leon.transformations.SerialInstrumenter.mapInstCallWithArgs(SerialInstrumentationPhase.scala:261) at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:575) at leon.transformations.ExprInstrumenter.tupleifyRecur(SerialInstrumentationPhase.scala:480) at leon.transformations.ExprInstrumenter.tupleify(SerialInstrumentationPhase.scala:446) at leon.transformations.ExprInstrumenter.transform(SerialInstrumentationPhase.scala:687) at...

What I would like to prove is: ``` scala def testEvolutionSimpleProofRec(c: Core, e:Task): Core = { require(isUnique(c.tasks) && c.tasks.contains(e) && !c.current.isDefined && find(c.tasks,e).isDefined && !c.tasks.isEmpty); val c2 = doubleTimer(c,e) //...

Here is a higher level view of what I try to prove, if it might help: I have two values: **a** and **b**. doubleTimer either increments **a** if **a** <...

Here is a minimal example that corresponds to the logic of what I want to prove (but for some reason I have a compile error due to rec? Am I...

Indeed :) With this function it works :) ``` scala def recF(c:Core):Core = { val c2 = doubleTimer(c); if(c2.b == c.b - 1) { c } else { recF(c); }...

Yes, the functions I check in the real example terminate :) (Actually in the small example the function should have too... I wanted to do the recursion with c2 as...

The file I use is: https://github.com/epfl-lara/leon/files/383971/Scheduler.txt I did ``` $ git pull $ sbt clean compile (3 warnings, no error) $ sbt script $ wget https://github.com/epfl-lara/leon/files/383971/Scheduler.txt $ ./leon ./Scheduler.txt #Same...

Without rec it compiles now :) The only issue I currently have is that Leon is not able to prove functions that it used to be able to prove (e.g.,...

Ok... Would it be possible to give an error in that case? It is a bit strange to see that this code passes verification :)

The termination checker says that a does not finish: ``` [ Info ] ║ apply ✓ Terminates (Non-recursive) [ Info ] ║ apply ✓ Terminates (Non-recursive) [ Info ] ║...