prusti-dev
prusti-dev copied to clipboard
Fold-unfold internal error for snapshot (in)equality of integer literals
The verification of this program
use prusti_contracts::*;
fn main() {
prusti_assert!(0 !== 1);
}
fails with
error: [Prusti internal error] Prusti encountered an unexpected internal error
--> enum.rs:3:1
|
3 | / fn main() {
4 | | prusti_assert!(0 !== 1);
5 | | }
| |_^
|
= note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
= note: Details: cannot generate fold-unfold Viper statements. The required permission Acc(_1.val_int, read) cannot be obtained.
(and one gets the same error for === instead of !==)