Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...
Phase 3 of 3: flow analysis and proof ...
guard_nudge_policy_pkg.ads:50:13: info: implicit aspect Always_Terminates on "Decide" has been proved, subprogram will terminate
guard_nudge_policy_pkg.ads:55:08: info: postcondition proved
Summary logged in /Users/tony/dev/ada-factory/wu-guard-nudge-policy/ab-20260826-1350/obj/gnatprove/gnatprove.out
