Pointerbender

> I looked into the Viper encoding for a bit, but I, unfortunately, do not see what is going wrong here. Coming back to: > > > Would it be...

> Would be nice to get a repro on a 20 or so lines example. I'll see if I can whip up something during the weekend :) > An alternative...

> I'll see if I can whip up something during the weekend :) This is the smallest version I could come up with: [lib.rs_prusti_example::foo 20220228 small.vpr.txt](https://github.com/viperproject/prusti-dev/files/8151574/lib.rs_prusti_example.foo.20220228.small.vpr.txt) Surprisingly, the confusing behavior...

@vakaras In case the refactoring is not a blocker for adding support for triggers on domain functions, and if it's not a super non-trivial fix, maybe I could take a...

It works okay through the Viper JNI bridge, it only gives problem in the file names :)

Note to self: since its not (yet?) possible to pin-point any specific clause of the predicate that is causing the memory problems, the root cause may be related to the...

> Could you attach the `.dot` dump of the MIR of `cursor_invariant`? The definition is quite big and I wonder what its CFG looks like. Sure thing! There are multiple...

Wow, that's a swift find! That saves a lot of debugging, thanks! :smile: > A further alternative, as noted in that old comment, is to convert the encoding to a...

The predicate-splitting work-around seems to do the trick, thanks @fpoli!

One important detail I just noticed, is that the encoding problem in this issue only happens when running Prusti in debug mode. In release mode the encoding performance problem is...