Can't prove simple snapshot inequality of different enum variants

[vfukala]

This program should verify:

use prusti_contracts::*;

enum MyEnum {
    A,
    B,
}

fn main() {
    prusti_assert!(MyEnum::A !== MyEnum::B);
}

However, verification fails with

error: [Prusti: verification error] the asserted expression might not hold

on the prusti_assert!.

[fpoli]

As discussed, in that program Prusti does not generate the axiom that encodes that the discriminants are different. This seems the result of a too aggressive optimization because the following code verifies as expected. The bug is probably in the definition collector.

use prusti_contracts::*;

enum MyEnum {
    A,
    B,
}

fn main() {
    prusti_assert!(MyEnum::A !== MyEnum::B); // now verifies
    let _ = MyEnum::A; // triggers the generation of the needed axioms
}