What am I doing wrong with contracts? Why are they succeeding when they should be failing?

[Andrew Shvets <andrew.shvets@gmail.com>]

This is the piece of code that I whipped up (Int_Array is an array of integers):

procedure Multiply_By_Two(Arr : in out Int_Array)
  with Pre  => (for all Item in Arr'Range =>
                  Arr(Item) /= 6),
       Post => (for all Item in Arr'Range =>
                  Arr(Item) = Arr'Old(Item) * 2);


And the implementation in the package:

procedure Multiply_By_Two(
  Arr : in out Int_Array) is

begin
  for iter in Arr'Range loop
    Arr(iter) := Arr(iter) * 2;
  end loop;
end Multiply_By_Two;


I simply pass in the array into Multiply_By_Two and then print out the array as needed.  This is what gets me.  The array has elements going from 6 to 45.  The "Pre" aspect that I created should raise an exception that the passed in element does not meet the conditions for the function to execute successfully.  However, that is not the case.  Why?  I was under the impression that this contract will begin raising exceptions when the Pre aspect evaluates to the condition of False.

Am I missing something?  A compiler flag?

Thank you in advance.