Alexander Stekelenburg

I ended up finding another source of unsoundness which I fixed in #1252 by not allowing AutoValue to be used with other permission annotations for the same permission. It'd be...

Hey @sakehl I ran into an issue here where SimplifyNestedQuantifiers was changing the trigger I had generated for a quantifier. Specifically I had the quantifier: ``` \forall int i =...

> > Additionally, I'll add support for taking differently typed pointers to a struct. (i.e. an integer pointer pointing to a struct is the same as pointing to the first...

> And that's strange, it should not rewrite anything if a trigger is present. This part should do that: > > ```scala > // PB: do not attempt to reshape...

> Hmm sorry, this behaviour was already possible without any of the things you are doing. > > E.g. > > ```c > #include > > void f(){ > int...

Superseded by #1159

Here you go: https://gist.github.com/superaxander/b7a80e5de28cbb8a4597acf72387b782 With Z3 4.8.7 on the master branch with an assertTimeout of 10 seconds this takes around 50 seconds (with a timeout of 5s it sometimes fails)...

Thanks for submitting the issue. We are planning on deprecating the VC.contract stuff in the future in favor of our new contract format which is automatically generated from source code...

Indeed we currently do not keep track of the origin of pointers. We should look at how other verifiers do this. For example in VeriFast you can have: ```c #include...

> Thanks for taking a look! > > It looks like the fact that enums can be null is encoded as an `Option`, so e.g. the argument `emp` gets type...