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.
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.