Malte Schwerhoff

Could have the same root cause as issue #228.

Since the [message is a logger warning](https://github.com/viperproject/silicon/blob/master/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala#L154), you could set Silicon's log level to error (`--logLevel ERROR`), which should suppress any message of lower severity.

Thanks for reporting the issue. In order to pinpoint the root course, it is important to have an example that is as minimal as possible. I know that cutting down...

For documentation purposes, this is the current CFG: 

Do we have a separate issue tracker for IDE/ViperServer issues? People who stumble across this issue and don't know the architecture of Viper well might assume that the unsoundness affects...

I'd also love to see this feature re-enabled. It is a real pitty that IntelliJ still doesn't provide good native support for sbt tasks such as test-only.

That's due to how Silicon handles triggers. In your example, the trigger `{ apply_on(k) }` is silently (good design choice) ignored because 1. it is a program function (heap-dependent function)...

Yes, that should work. We should get rid of heap-dependent triggers anyway ... :-)

We don't have a good term for non-domain functions, and simply called them heap-dependent so far. If they don't access the heap, their footprint is empty, but they nonetheless have...

Interesting catch :-) I have the vague feeling this was observed before, and we concluded it's an incompleteness.