Regression same_package/import-fail01/main fails non-deterministically

[jcp19]

No description provided.

[jcp19]

I believe this is caused by the changes introduced in PR #634 that made the Desugarer parallel. In turn, this seems to be causing a race condition in the collection of all import preconditions when we generate proof obligations for initialization.

For now, I suggest we do not introduce a PR to fix this, as I am currently re-designing how we do static initialization in Gobra. After that, I will make the Desugarer sequential again, and I will undo #541, as the new encoding should work just fine, even with imports to packages for which we did not verify initialization.

[ArquintL]

To sequentialize the desugarer, you only have to make sure that the following promises execute sequentially.
// we place mainPackageFut at index 0 val allPackagesFut = Future.sequence(mainPackageFut +: importedProgramsFuts) val futResults = Await.result(allPackagesFut, Duration.Inf)

I‘m not sure how the preconditions are collected but my changeset did imho not introduce any concurrent datastructures for the desugarer. This might alternatively be a somewhat easy solution too