Jacob, folks, I think the current Dejagnu codebase (4e4eb1534b4) contains a bug that was initially reported here:
https://bugzilla.redhat.com/show_bug.cgi?id=460153 The bug contains both reproducer and a short patch. Please, consider upstreaming it. Thank you, Martin
