2019-04-09 15:15:15 (GMT)
You guys have seen this work that was published at TACAS?
https://link.springer.com/chapter/10.1007/978-3-030-17462-0_6
It seems like a next step in the work by Leino and Pit-Claudel on trying to deal with matching loops. It reminded me of an old discussion in the matryoshka list on "evil axioms"
2019-04-09 15:20:8 (GMT)
I remember that alt-ergo's GUI (control-alt-ergo, I think) displays data and stats on triggers, it's definitely a concern
2019-04-09 15:21:6 (GMT)
I did not really read this paper, but skimming seems like they have some interesting ways of inferring why stuff gets bad