prusti-dev
prusti-dev copied to clipboard
Switch to the domain definition of `read$`
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.