Samuel Chassot

Okay I found that it is in fact `quackyducky` which does that (it is in the paper but almost absent from the documentation). I am however not able to produce...

Great! Thanks for the reply! Okay, I see, it makes sense. And, if I understood correctly, the same apply to write data to a buffer: one has to use different...

Thanks a lot for your reply :) That makes more sense now 👍 I am trying to write an example and I still have something I don't know: I made...

This can be reproduced with https://github.com/epfl-lara/bolts/tree/master/WIP/SLOW/longmap for example, with or without `smt-cvc4` in the config: `stainless-dotty --config-file=stainless.conf StrictlyOrderedLongListMap.scala `

> @samuelchassot maybe we should write slightly more general remark on using vscode as a default IDE for Stainless? Because we are not using Scala 3 and that only really...

> Can you remove scala 2 references in the example repo https://github.com/samuelchassot/Stainless-codespaces Then we can link the documentation change. Done! I also applied the suggested change above

This function is rejected by AntiAliasing: ``` def antiAliasingRejected(): Unit = { val newV = X(1) val b = Cell(newV) assert(b.v.x == 1) newV.x = 3 assert(b.v.x == 3) }...

This version of the function with `Cell` `swap` is rejected. This one and the example above are essentially identical and should both be rejected: ``` def simplerUnsoundExampleCellRejected(): Unit = {...

After reflexion, it is due to the fact that `swap` modifies the targets in AntiAliasing: it should indeed swap the targets because the values are swapped, so should the targets....

> Let's generalize it to return an environment! It's a non-trivial change, but opens up many different possibilities, including WSkS transductions as in https://www.brics.dk/PALE/ Okay! I'll work on that, maybe...