1--  { dg-do compile }
2--  { dg-options "-gnatd.F -gnatwa" }
3
4with Ada.Dispatching;
5
6procedure Contract1 with SPARK_Mode is
7
8   function Foo return Boolean is
9   begin
10      Ada.Dispatching.Yield;
11      return True;
12   end Foo;
13
14   Dummy : constant Integer := 0;
15
16begin
17   if Foo and then True then
18      raise Program_Error;
19   end if;
20end Contract1;
21