Malte Schwerhoff

Corrections: * State entry `constrainingARPs` is currently still used to record currently constrainable wildcards, e.g. for `fold P(x)`, where `P`'s body contains a wildcard. The state entry should be renamed...

If I remember correctly, heap-dependent triggers are currently not inferred by Silver's trigger inference code, and thus need to be provided manually.

Added [corresponding regression test](https://github.com/viperproject/silver/blob/master/src/test/resources/all/issues/silicon/0496.vpr) with an additional variant that should definitely verify.

Currently not. Silicon merely calls Viper's trigger inference, though, which Prusti could as well. Not convenient, but might suffice for the time being. @ArquintL Hovering over Viper quantifiers to reveal...

Good point, I had not thought about Silicon's own trigger generator: it shares the general approach with Viper, but is for Silicon's internal representation ("terms", basically SMT expressions). Some quantifiers...

@dohrau Any progress on this?

Still doesn't verify, using the latest Silicon version, neither with Z3 4.8.7, nor 4.8.14.

Each assertion is symbolically evaluated independently, which can give rise to semantically equivalent but syntactically different snapshots. This can result in incompletenesses, and you unfortunately hit on such incompleteness (triggering)....

Before getting into details: the QP assertions in `matrixValues` and `maxFlow` don't have triggers. That's hardly ever good. Generally, Silicon symbolically evaluates each Viper expression (assertion), i.e. translates it from...

You could dump Z3 statistics between check-sat calls to see which numbers increase, and from that get an idea of which subsolvers uses up the time bound. However, in my...