CODEWITHSUNDEEP
logicverificationsmtformal-verificationboogie
tyr.bentsen
tyr.bentsen

Reputation: 153

Logic error or Boogie bug? Quantifiers: exists of a forall

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?

Upvotes: 1

Views: 113

Answers (0)

Related Questions