Baptiste Lepers

Z3 exception

3

```scala import leon.lang._ import leon.lang.xlang._ import leon.util.Random import leon.collection._ object DataRacing { case class Core(val r:BigInt, val choice:Core, val nbtasks:BigInt) case class SharedState(val progress:BigInt, val cores:BigInt => Core) case class...

Bug in proofs

10

Pretty serious bug, or did I miss something? ```scala import leon.collection._ import leon.lang._ import scala.Any object Scheduler { def a(i: BigInt):BigInt = { i - 1; } ensuring(res => b(i)...

Strange issue :) ``` scala 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");...

ensuring(rec <= ...) -- big verification time variation

21

Using 624e5a728ddde77b6ca707300be4cdbfc7173627 I am trying to prove that a function terminates by ensuring that "rec

Simple use of lemmas for preconditions (feature request?)

4

Imagine I have the following lemma: ``` scala def lemma(l:List[A], e1:A, e2:A) = { e1.prop == e2.prop ==> cond(l, e1) == cond(l, e2) }.holds; ``` and the following code: ```...