Jad Hamza

Positions count 1 tab as 8 spaces

3

cc: @deiruch This makes IDEs who count 1 tab = 1 column misreport positions of warnings and errors. We could adjust positions down by fetching the source code line and...

This is an example that seems to be solved by Z3 in non-incremental mode, but times out with incremental mode. We can add it to the test suite if we...

Not really a Stainless issue, but we can leave this open until this works better in Z3. This example generates a VC for the assertion, which is hard to solve...

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() =...

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...

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])])...

Problem with preprocessing?

3

``` scala import leon.lang._ import leon.proof._ object Preprocessing { def theorem(b: Boolean): Unit = { require (b) check(b) true } ensuring ( _ => true ) } ``` The check(b)...

``` scala import leon.lang._ object TODO { def contains(m: Map[BigInt,Actor], id: BigInt) = { m.contains(id) } holds case class Actor(myId: BigInt) { require(myId == 0) } } ``` The problem...

I tried setting `m_gravityFactor` to `0` to prevent my softbody to react to gravity but gravity would always apply. Is this a proper fix?

Fix damping constraint index in ConstraintDemo

1

Fix minor index error in `setDamping`, maybe a copy/paste error?