prusti-dev icon indicating copy to clipboard operation
prusti-dev copied to clipboard

Fold-unfold internal error for snapshot (in)equality of integer literals

Open vfukala opened this issue 2 years ago • 0 comments

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 !==)

vfukala avatar Apr 10 '23 16:04 vfukala