Malte Schwerhoff

This won't be easy to fix. An additional case-split might be a potential work-around, e.g. adding `if (x == y) { assert false }` to the body of the `package`...

Updates on Silicon's side, see https://github.com/viperproject/silicon/issues/104#issuecomment-596196782

@ArquintL Could this be an IDE issue? It seems that the temporary switch to Carbon produces a cache entry that is then picked up by Silicon, resulting in the changed...

Hi Pieter, interesting observation! The tutorial even hints at the opposite: > Viper supports assertions of the form `unfolding P(...) in A`, which temporarily unfolds the predicate instance `P(...)` for...

Thank you for investigating the issue. I assume the PR is WIP until a complete solution is found. If so, please mark the PR as such, so that it doesn't...

Z3 also supports floating-point numbers directly, which we could lift to Viper. @marcoeilers developed a prototypical extension of Viper for lifting more Z3 types to Viper, but I don't think...

@martijnrenssen PR #428 is the one Marco mentioned. It maybe take a while until it is merged into the Silver code base, but you could locally merge it to see...

A cursory inspection suggests a triggering problem, as explained in [Silicon issue #537](https://github.com/viperproject/silicon/issues/537).

With IMAP (maybe with POP3 as well?) you can simply unsubscribe from certain folders in Thunderbird. Right-click your account, then choose "Subscribe...".

Did you try deleting the "cache" files that Thunderbird creates for IMAP folders? Check your Thunderbird profile folder, then probably `ImapMail/`. There, you'll see files and directories named after your...