// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
// @expect error
// kani-verify-fail

struct Point<T> {
    pub x: T,
    pub y: T,
}

struct Point3<T> {
    pub x: T,
    pub y: T,
    pub z: T,
}

trait S<T> {
    fn swap_items(self) -> Self;
}

impl<T> S<T> for Point<T> {
    fn swap_items(self) -> Point<T> {
        Point::<T> { x: self.y, y: self.x }
    }
}

impl<T> S<T> for Point3<T> {
    fn swap_items(self) -> Point3<T> {
        Point3::<T> { x: self.y, y: self.z, z: self.x }
    }
}

fn swapem<T, U: S<T>>(s: U) -> U {
    s.swap_items()
}

#[kani::proof]
pub fn main() {
    let x2 = kani::any();
    let y2 = kani::any();
    let x3 = kani::any();
    let y3 = kani::any();
    let z3 = kani::any();
    let p2 = Point::<i64> { x: x2, y: y2 };
    let p3 = Point3::<i64> { x: x3, y: y3, z: z3 };

    let q2 = swapem(p2);
    let q3 = swapem(p3);
    assert!(q2.x == y2);
    assert!(q2.y != x2);
    assert!(q3.x == y3);
    assert!(q3.y == z3);
    assert!(q3.z == x3);
}