Error "Reached assignment statement with unequal types Pointer" with Result<(), Error> #729
Description
I tried this code:
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
enum Error {
Error1,
Error2,
}
fn to_option<T: Copy, E>(result: &Result<T, E>) -> Option<T> {
if let Ok(v) = result {
Some(*v)
} else {
None
}
}
fn main() {
let result: Result<(), Error> = Ok(());
assert!(to_option(&result).is_some());
}using the following command line invocation:
rmc <test_file>
with RMC version:
I expected to see this happen: Verification should succeed
Instead, this happened:
$ rmc fixme_niche_opt.rs | grep FAIL
(standard input):34:[assertion.1] Reached assignment statement with unequal types Pointer { typ: StructTag("tag-Unit") } Pointer { typ: StructTag("tag-_3943305294634710273") }: FAILURE
(standard input):66:VERIFICATION FAILED