Dafny verifies an assert when used with an assume which does not hold

I used assume and assert as in the following method:

method testAssumes(x:int)  returns (s:int)
 {
  var z:int:=-1;
  assume {:axiom} z>0;
  var y:int;
  y:=x+z+1;
  assert y>0;  
  return y;
}

Strangely enough it verifies while it should not since y:=x+z+1 and x could be negative.
When I changed the value of z to 1, the verifies complaints that the assert might not hold.

Is there an explanation for this behavior?

You are assuming something that is not true. As a result, you can derive any conclusion (by the Principle of explosion).

A quote from Dafny documentation regarding assume:

> The assume statement lets the user specify a logical proposition that
> Dafny may assume to be true without proof. If in fact the proposition
> is not true this may lead to invalid conclusions.

Edit:
Here is an example of how Dafny could (possibly, not saying that it happens this way) derive the assert condition (y > 0) to be true:

1. var z:int:=-1; tells Dafny that z == -1, so Dafny can later use this fact.
2. assume {:axiom} z>0; tells Dafny that z > 0, therefore Dafny can later use this fact too.
3. Dafny starts by proving that y > 0 || z > 0 is true. This is easy, since Dafny knows z > 0 to be true.
4. To show that y > 0, Dafny needs to prove that z > 0 is false (and since y > 0 || z > 0 is true, y > 0 must be true). But this can be shown using the fact from 1., i.e., that z == -1.