alexanderjsummers

Interestingly, if one removes the `val` field from the program, the analogous program verifies. I guess this must either be a back-end issue or an issue with the snapshots encoding:...

Thanks for the speedy response! As far as I can tell this doesn't seem to be an example in which triggering unfoldings of function definitions should be particularly problematic; the...

Thanks! I suspect that we can generate a similar issue for Silicon just by setting up similar predicates at the Viper level. I assume this behaviour is not expected with...

@vakaras ah thanks - is there an issue to link to?

Same issue posted for Carbon here: https://github.com/viperproject/carbon/issues/437

It could be that the code in [viper.silver.ast.MagicWand.structure](https://github.com/viperproject/silver/blob/bab3e3ef57b3cbdead702ca5641a5a3dd0c69750/src/main/scala/viper/silver/ast/Expression.scala#L165) should be adapted; the "identity" of the old state used is not considered a "hole" in the structure generated. I'm not exactly...

Interesting. I think the second method's behaviour might be expected: after checking a property, verification continues under the assumption that it was true, and in test03b that assumption leads to...

The example also illustrates that we should pick an order in which these checks should be made, since one can potentially observe the difference between different orders (in both tools).

I can't reproduce the error in Carbon (I get a well-definedness error, but I think that's correct with the latest design)

Here is a hypothesis from our earlier discussions, assuming a version with none of the spurious set == set conjuncts: - `assert a(0)` assumes literal `¬a(0)` (when checking the assert)...