procedure Schrodinger with SPARK_Mode, No_Return is
   Cat_Is_Alive : Boolean := False with Ghost;
begin
   loop
      null;
   end loop;
   pragma Assert (Cat_Is_Alive and not Cat_Is_Alive);
end Schrodinger;