Malte Schwerhoff

> Ah, interesting, will do. Do you then close this issue? I'll keep it open, as the Silicon-specific instance of the problem.

Nice catch! We've only experimented with MBQI a few times and ran into nontermination of Z3 right away, but otherwise, using MBQI should be OK. That's at least my guts...

For what it's worth: I believe we consistently report well-formedness issues mid-program (and in contrast to pre-/postconditions and invariants) as statement failures. E.g. `assert x.f != 0` will fail with...

AFAIK, Silicon's terms implement `hashCode` and `equals` as expected, so using a set here should work. Adding a second, set-typed collection of terms incurs additional bookkeeping costs, though (add/remove terms...

Potentially related: #367, #480, #481

In Silicon, well-definedness checks are often intertwined with producing/consuming assertions. Upon unfolding, there might thus be errors from a potentially not well-defined predicate body. I guess that here, the permission-wise...

Yes, but that would actually make Silicon's implementation quite a bit more complex. Unlike Carbon, which implements total heap semantics, Silicon can't (easily) handle a heap access if permissions are...

Verification fails with Z3 4.8.7, but succeeds with Z3 4.8.9 and 4.8.14. I'll therefore close this issue.

OmerSakar: Silicon now provides a command-line option to override, and thus extend, the set/multiset/sequence axioms Silicon uses. To locally fix the issue you reported, follow these steps: 1. Create a...

That looks like a consequence of this Z3 issue: https://github.com/Z3Prover/z3/issues/4713. It was closed, but the comment could also be interpreted as "closed and won't fix (for now)". AFAICS, our only...