Marco Eilers

Apparently this was also fixed by PR #846 (although there are some fundamental issues here that we're essentially just working around with a bunch of caching).

Regarding point 2, the issue is that that would require us to check domain axioms for well-definedness, which currently isn't necessary and thus doesn't happen at all. Alternatively, we could...

Functions that don't have preconditions but do have decreases-clauses can now be used in domain axioms (https://github.com/viperproject/silver/pull/802).

Fixed in https://github.com/viperproject/silver/pull/890.

Right, this happens because the quantifier declares a variable whose name is in use in its parent scope. Our scopes basically mostly ignore *where* in them a variable is declared...

I think this is the RC that basically doesn't work on Windows because of a name clash between ``defaultHeapSupporter`` and ``DefaultHeapSupporter``. So you should move to the actual release version.

@Dev-XYS: I remembered why I added the ``uniqueName`` stuff: Since this is a Viper-to-Viper rewrite, I need a name that's unique inside the *Viper* program, not just in the final...

With current master Silicon, the warning still shows up, but Silicon is no longer slow. It takes 6.4 seconds on my laptop when started from scratch, so I'd assume like...

Okay, I no longer believe my explanation from above, that actually seems fine as long as the definitional axiom contains only definitions. So maybe the problem is that it doesn't,...

> Is there any reason why this might be expected behaviour in Silicon, perhaps based on Silicon's heap model? No, this is not expected, it's an incompleteness. I'll look into...