(* Next Obligation should fail normally, not with an anomaly. *)
Fail Next Obligation.