I'm working with the Boogie verification language, where I have the following example that gives a result that is counterintuitive to me.
// Defining a function and giving it a meaning through axiomatization.
function EqualsInt(x: int, y: int) : bool;
axiom (forall x: int, y: int :: EqualsInt(x, y) == (x == y));
procedure main()
{
assert (exists i: int :: i == i); // Assertion is verified.
assert (forall i: int :: EqualsInt(i,i)); // Assertion is verified.
assert (exists i: int :: EqualsInt(i,i)); // Assertion does not hold.
}
Why do the first two assertions hold, but the last one not?
Now i wonder if that is a bug in boogie or if it is a fundamental result of logic that I don't grasp correctly?
