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 ...
mouth_policy_pkg.ads:36:13: info: implicit aspect Always_Terminates on "Decide" has been proved, subprogram will terminate
mouth_policy_pkg.ads:41:08: info: postcondition proved
Summary logged in /Users/tony/dev/ada-factory/wu-mouth-policy/ab-20260826-1345/obj/gnatprove/gnatprove.out
