Marco Eilers

The issue is that Silicon verifies ``funThatUnfolds`` before ``nonNull``, and thus the postcondition of ``nonNull`` is not available yet. Silicon computes which functions rely on which other functions to determine...

Thanks for filing this issue! However, I don't think I agree that this qualifies as a type safety violation or a soundness issue; IMO it's simply the case that 2vyper's...

I had looked at this and thought it didn't do what we need in a concurrent setting, but I'll have another look.

The problem is basically this: We'd need to clone the solver before executing the then or else branch. However, at that point we don't know if we're going to execute...

> > We'd need to clone the solver before executing the then or else branch. > > If the decision to parallelize happens after the branching point, it might be...

Right. It might still be worth it of course, I'll definitely try it.

I tried it. Apparently, cloning solvers is not supported when using push/pop (I get the error ``translation of contexts is only supported at base level``). See https://github.com/Z3Prover/z3/issues/556.

Another update: I made a branch with a Silicon version that doesn't use push/pop at all (meilers_solver_clone_pure_sc) when assertionMode sc is chosen. There the solver cloning works, but overall it's...

An updated list: 8 tests fail in total. Most fail because test annotations expect errors caused by incompleteness (i.e., these are not actual test failures): - all/issues/silicon/0072.vpr - all/issues/silicon/0232.vpr -...

Update: quantifiedpermissions/sequences/mergesort.vpr works now. That means that currently, there are no test cases that fail with moreCompleteExhale except for the ones mentioned above that aren't actual test failures.