search

viperproject / prusti-dev

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

Fix encoding of mutually recursive pure functions #1440

Closed fpoli closed 1 year ago

fpoli commented 1 year ago

Use the f_ prefix for encoding pure function names instead of m_.

Partially addresses #1214. Fixes #1267.

fpoli commented 1 year ago

@vakaras The fix made the purification test fail/core_proof/model2.rs fail with 3 more errors of the kind "the termination measure of this call is not necessarily lower". I have no clue what caused them, so I excluded your encoder from this PR.