Puzzled by this behavior

[Ola Fosheim Grøstad]

On Thursday, 2 June 2022 at 22:50:30 UTC, deadalnix wrote:
> As for an SMT solver, that sound like a good way to destroy 
> your compile time.

Yes, but you can cache results and compile in the background 
while editing and also add an option for distributed analysis 
(cloud solution). Most function bodies dont change frequently. 
All you want to cache is a list of asserts that have been proven 
and what that proof depends on. Besides, this is just a release 
optimization...

> BTW, Swift is using an SSA, but without phi nodes, then instead 
> have basic block take arguments and branch instruction take 
> parameters.

Maybe tell the Swift people that you are considering something 
similar and ask them if they feel that the Swift IR is flexible 
enough, basically ask about the limitations they have seen.

> SDC already has a full mid level IR that supports most of the 
> language.

So, if that is simple enough after template expansion, then that 
would be sufficient for Boogie. Then maybe Swift is not a bad 
starting point if you can get some info from the Swift people.