stainless

stainless copied to clipboard

0.7.1 regression: exception when building projects on windows 10 x64

3

I'm currently using the 0.7.1 stainless jar release resulting from a publishLocal on Windows (have also tried a set of build artifacts built on MacOS). The 'tester' project referenced below...

mwookawa

Infinite loop in InnerClasses

4

I'm getting an infinite loop on this example during phase `InnerClasses`. @romac Maybe you know why? ``` stainless -XX:MaxJavaStackTraceDepth=1000000 File.scala --debug=trees,stack --batched ``` ```scala object Main { def twoOrders() =...

jad-hamza

Assert false after lambda equality

2

While writing https://github.com/epfl-lara/stainless/issues/709, I noticed that the call to `notEqual` is not required to `assert(false)`. I guess it's not the same issue because there are no precondition VCs here. Writing...

jad-hamza

induction lemma with forall ensuring clause is sometimes wrongly marked as invalid

1

In the example bellow, it is easy to see that the updateValid and updateValid2 lemma are equivalent but the updateValid lemma is easily proven while the updateValid2 is considered INVALID...

Zyfarok

Checking measure on type-parametric class method leads to invalid context in type checker

1

Ran into this while trying some to prove some laws example on polymorphic lists: ```scala import stainless.lang._ import stainless.collection._ abstract class Equals[A] { def law_refl(x: A): Boolean = true }...

gsps

This results in type error ```scala import stainless.lang._ import stainless.collection._ object TypeError { def some_lemma(x: Int, xs: List[Int]): Boolean = { !the_law(xs) || the_law(xs) } def the_law(xs: List[Int]): Boolean =...

gsps

only literal arguments are allowed for Bigint (.apply)

1

Scala wants to do promotion using an implicit function called long2bigInt. Unfortunately, I can't define this function, even using the brute force implicit def long2bigInt l: Long = BigInt(l.toString) because...

mwookawa

This crashes with mismatch between List[(Int,Char)] and List[(Int,T)]: ```scala import stainless.collection._ object Test { type T = Char case class C(u: List[(Int,T)]) } ``` Having a list of pairs as...

vkuncak

Cannot instantiate a non-mutable type parameter T in Option[T]

5

Given ``` @mutable trait B {} case class A (var foo: Int) extends B { val baz: Int = foo } object D { def bar(a: Option[B] = None()) {...

mwookawa

Type encoding issue with equality between different types

1

This example uses an equality between different types, and type encoding introduces a type error: ```scala import stainless.collection._ import stainless.lang._ object TypeEncodingEquality { case class P[A](p: List[BigInt] => Option[(A, List[BigInt])])...

jad-hamza