aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/bug_13320.v
blob: 6f3c51bbe71b784d93006a2994bc9ea192619db7 (plain)
1
2
(* Next Obligation should fail normally, not with an anomaly. *)
Fail Next Obligation.