Measure verification time per "assertion" #1597
Labels
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
Milestone
Follow-up on the
/verificationLogger:trx
feature. It looks possible to use the splitting feature of Boogie to support a mode where each assertion in a procedure is verified separately, to gain more insight into which assertions in particular are the most expensive and should be refactored to bring the overall verification time down.While I'm at it, I should be able to improve how Dafny program elements are identified in the TRX format: what is currently something like
Impl$$MyModule.__default.MyMethod
should be something more likeMyModule.MyMethod (implementation)
.The text was updated successfully, but these errors were encountered: