viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.
http://prusti.org
Other
1.52k stars 102 forks source link

Fix issue #1505 #1511

Closed fpoli closed 3 months ago

fpoli commented 3 months ago

Fixes #1505

Note that this PR also changes the default of simplify_encoding to false, because Viper's optimization of signed integer divisions is wrong (https://github.com/viperproject/silver/issues/782).