--  { 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;