"Initial" proof obligation missing

[scmu]

Load this file

var r : Int 

{r = 0}

We correctly get a proof obligation True => r = 0 (which is not provable in general, and implies that we should initialize r).

If we load this file:

var r : Int 

{r = 0}
{r >= 0}

We get only r = 0 => r >= 0, but not the initial True => r = 0 . The "initial" proof obligation is missing.

We might need to check whether this is a bug or a feature (e.g. with multiple assertions presenting, the first assertion is considered an assumption). In the latter case we might argue whether this is a good design.