Match expressions with | and variables causing spurious failure.

I tried this code:

```rust
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum AbstractInt {
    Bottom = 0,
    Zero = 1,
    Top = 2,
}

impl AbstractInt {
    pub fn merge(self, other: Self) -> Self {
        use AbstractInt::*;
        match (self, other) {
            (Bottom, x) => x,
            (x, Bottom) => x,
            (Zero, Zero) => Zero,
            (Top, _) | (_, Top) => Top,
        }
    }
}

#[cfg(kani)]
mod test {
    use super::*;
    impl kani::Arbitrary for AbstractInt {
        fn any() -> Self {
            use AbstractInt::*;
            match kani::any::<u8>() {
                0 => Bottom,
                1 => Zero,
                _ => Top,
            }
        }
    }
    #[kani::proof]
    fn merge_with_bottom() {
        let x: AbstractInt = kani::any();
        assert!(x.merge(AbstractInt::Bottom) == x);
        assert!(AbstractInt::Bottom.merge(x) == x)
    }
}
```

and the equivalent implementaion of merge, using a | in the pattern:
```rust

impl AbstractInt {
    pub fn merge(self, other: Self) -> Self {
        use AbstractInt::*;
        match (self, other) {
            (Bottom, x) |(x, Bottom) => x,
            (Zero, Zero) => Zero,
            (Top, _) | (_, Top) => Top,
        }
    }
}
```

using the following command line invocation:

```
kani src/repro.rs
```

with Kani version: Kani Rust Verifier 0.53.0 (standalone)

I expected to see this happen: I expected the proof to verify with both implementations of merge. 


Instead, this happened: The proof verifies with the implementation where (Bottom, x) and (x, Bottom) are on separate lines, but fails when they are on the same line separated by a |:

```
Kani Rust Verifier 0.53.0 (standalone)
Checking harness test::merge_with_bottom...
CBMC 5.95.1 (cbmc-5.95.1)
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Reading GOTO program from file /home/lorinc/github.com/B-Lorentz/kan/src/repro__RNvNtCsiCi0JD7ZDuS_5repro4test17merge_with_bottom.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Runtime Symex: 0.0190811s
size of program expression: 825 steps
slicing removed 508 assignments
Generated 28 VCC(s), 6 remaining after simplification
Runtime Postprocess Equation: 0.000188282s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000896564s
Running propositional reduction
Post-processing
Runtime Post-process: 6.136e-06s
Solving with CaDiCaL 1.7.2
390 variables, 437 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 6.5924e-05s
Runtime decision procedure: 0.00102995s
Running propositional reduction
Solving with CaDiCaL 1.7.2
390 variables, 438 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 2.3305e-05s
Runtime decision procedure: 4.6675e-05s
Running propositional reduction
Solving with CaDiCaL 1.7.2
390 variables, 439 clauses
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 2.043e-05s
Runtime decision procedure: 3.7687e-05s

RESULTS:
Check 1: test::merge_with_bottom.assertion.1
         - Status: FAILURE
         - Description: "assertion failed: x.merge(AbstractInt::Bottom) == x"
         - Location: src/repro.rs:35:9 in function test::merge_with_bottom

Check 2: test::merge_with_bottom.assertion.2
         - Status: SUCCESS
         - Description: "assertion failed: AbstractInt::Bottom.merge(x) == x"
         - Location: src/repro.rs:36:9 in function test::merge_with_bottom

Check 3: AbstractInt::merge.unreachable.1
         - Status: SUCCESS
         - Description: "unreachable code"
         - Location: src/repro.rs:11:15 in function AbstractInt::merge

Check 4: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.1
         - Status: SUCCESS
         - Description: "dereference failure: pointer NULL"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 5: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.2
         - Status: SUCCESS
         - Description: "dereference failure: pointer invalid"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 6: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.3
         - Status: SUCCESS
         - Description: "dereference failure: deallocated dynamic object"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 7: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.4
         - Status: SUCCESS
         - Description: "dereference failure: dead object"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 8: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.5
         - Status: SUCCESS
         - Description: "dereference failure: pointer outside object bounds"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 9: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.6
         - Status: SUCCESS
         - Description: "dereference failure: invalid integer address"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 10: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.7
         - Status: SUCCESS
         - Description: "dereference failure: pointer NULL"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 11: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.8
         - Status: SUCCESS
         - Description: "dereference failure: pointer invalid"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 12: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.9
         - Status: SUCCESS
         - Description: "dereference failure: deallocated dynamic object"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 13: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.10
         - Status: SUCCESS
         - Description: "dereference failure: dead object"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 14: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.11
         - Status: SUCCESS
         - Description: "dereference failure: pointer outside object bounds"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 15: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.12
         - Status: SUCCESS
         - Description: "dereference failure: invalid integer address"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq


SUMMARY:
 ** 1 of 15 failed
Failed Checks: assertion failed: x.merge(AbstractInt::Bottom) == x
 File: "src/repro.rs", line 35, in test::merge_with_bottom

VERIFICATION:- FAILED
Verification Time: 0.047771145s

Summary:
Verification failed for - test::merge_with_bottom
Complete - 0 successfully verified harnesses, 1 failures, 1 total.
```

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Match expressions with | and variables causing spurious failure. #3432

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Match expressions with | and variables causing spurious failure. #3432

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions