Prove false with bitvectors

[MikaelMayer]

I have no idea why, but I can prove false with the following code:

lemma false_lemma(a:bv64, b: bv64)
  requires a != b
  ensures false
{
  var tmp := a ^ b;
  while tmp != 0
    decreases tmp
  {
    tmp := tmp >> 1;
  }
  assert false;
}
lemma ensures_false()
  ensures false
{
  false_lemma(0, 1);
}

[cpitclaudel]

Ouch, nice find!

Here is an even smaller example:

lemma false_lemma()
  ensures false
{
  var tmp: bv64 := 1;
  while tmp != 0
    decreases tmp
  {
    tmp := tmp >> 1;
  }
  assert false;
}

I have a fix coming up, I think.

[cpitclaudel]

Another variant:

method Infloop(b: bv8)
  requires b == 3
  ensures false
  decreases b
{
  Infloop'(b + 1);
}

method Infloop'(b: bv8)
  requires b == 4
  decreases b, 0
  ensures false
{
  Infloop(b - 1);
}

method Boom()
  ensures false
{
  Infloop(3);
}

[cpitclaudel]

And another one:

  trait T {
    method Infloop(b: bv8)
      requires b == 3
      ensures false
      decreases b
  }

  class C extends T {
    method Infloop(b: bv8)
      requires b == 3
      ensures false
      decreases b + 1, 0
    {
      (this as T).Infloop(b);
    }
  }