prusti-dev icon indicating copy to clipboard operation
prusti-dev copied to clipboard

Switch to the domain definition of `read$`

Open fpoli opened this issue 2 years ago • 0 comments

The domain definition of read$ seems to be strictly better than the current function definition that is used by Prusti. On a Rust function of 150 lines full of shared references and no functional properties I observed that the verification time (after warmups) goes from 5.5 to 5.0 seconds. It's a small but nice improvement.

fpoli avatar Oct 27 '23 10:10 fpoli