Jad Hamza

Crash in compileLambda in CodeGeneration

8

This files (a minimized version of `GodelNumbering`) crashes on the assertion here: https://github.com/epfl-lara/stainless/blob/729aa8b1666f101f82d918f6caeccd18115ec7f8/core/src/main/scala/stainless/codegen/CodeGeneration.scala#L355 ``` stainless Test.scala --solvers=smt-z3 --batched --vc-cache=false --codegen --debug=stack --feeling-lucky ``` ```scala import stainless.lang._ import stainless.equations._ import stainless.annotation._...

Discussion on May 7th 2021 **Jad**: Is there a workaround to avoid type-encoding for something like that? https://gist.github.com/jad-hamza/d5b4ce6b3d8e0fec7ca18e786c7ac4bf I tried to use the SortedArray in another file, but this requires...

Problem proving lemma with imperative features

1

Thanks to Romain (J) for reporting Stainless times out on the assertion `arePositive(l)`. ```scala import stainless.collection._ object Imperative { case class Test(var l: List[BigInt]) { def lemma(x: BigInt, amount: BigInt)...

@inlineOnce on recursive functions

3

Since I've enabled inlining (once) of recursive functions in themselves, this example fails: ```scala import stainless.annotation._ import stainless.collection._ import stainless.lang._ object InlineOnce { def test(l: List[BigInt]): Unit = { require(arePositive(l)...

Type in variable after type encoding is missing refinement

7

In the function binding, `elemRef$0` goes from type `Array[(K$24, T$78)]` (before `TypeEncoding`) to ` Array[({ x$629: Object$0 | ⟨@unchecked ⟨⟨K$40 : (Object$0) => Boolean ⟩(⟨x$629 : Object$0 ⟩) : Boolean...

Add support for RefinementType in unapply pattern

9

This file fails: https://github.com/epfl-lara/bolts/blob/4cf535349deca6f2d27fefe8ba5490e1ae0f7a83/data-structures/seqs/ArrayList.scala Edit: maybe here: https://github.com/epfl-lara/inox/blob/22de8d6b6af51fbe09bca2fc26dbdd596de8e3e8/src/main/scala/inox/ast/TypeOps.scala#L48-L83

Assert false after lambda equality (2)

7

Maybe related to #710? The `assert(false)` goes through. I added type annotations to make sure both lambdas have the same type. Moving the `leq` or `order` to function paramers of...

Slowness in verification condition checking + Array encoding for CVC4

7

In this example, the VC for the precondition check in the call to `gg` in the `insert` function takes ~2 minutes to solve. It's probably `z3` (tried with 4.8.6 and...

Strange timing for valid VCs in portfolio mode with timeout

2

Running the example from https://github.com/epfl-lara/stainless/issues/979 in portfolio mode with `--vc-cache=false --solvers=smt-z3,smt-cvc4 --timeout=N` takes around `N` seconds (+loading) and succeeds with the (body assertion) VC being verified in exactly `N` seconds....

https://github.com/epfl-lara/stainless/blob/391088ee6ea1154db23e1320d8f637b350c593c0/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala#L162-L180 See discussion: https://github.com/epfl-lara/stainless/pull/985#discussion_r614204561