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