[Bug] MVP proves arbitrary postconditions when unsupported operations exist

[xudon9]

🐛 Bug

When MVP sees an unsupported operation in a function, it proves arbitrary postconditions.

To reproduce

MVP can find that this postcondition doesn't hold:

address 0x123 {
  module M {
    public fun foo(i: u64): u64 { i + 0 }
    spec foo { ensures false; } // :)
  }
}

But it falsely "proves" this one because of the bit-and operator:

address 0x123 {
  module M {
    public fun foo(i: u64): u64 { i & 0 }
    spec foo { ensures false; } // :(
  }
}

Expected Behavior

For unsupported operations, MVP currently generates an assert false in bpl. Correct me if I am wrong, Boogie should immediately report an assertion failure upon seeing assert false. But now seems like it sliently skipped everything.