blob: 286fbc557ca962a0d4181f092e86e21c1c0ed06e [file] [log] [blame]
-- { dg-do compile }
-- { dg-options "-gnatd.F -gnatwa" }
with Ada.Dispatching;
procedure Contract1 with SPARK_Mode is
function Foo return Boolean is
begin
Ada.Dispatching.Yield;
return True;
end Foo;
Dummy : constant Integer := 0;
begin
if Foo and then True then
raise Program_Error;
end if;
end Contract1;