Celina G. Val

I think the problem here might be related to different versions of the same crate. The libc you are pulling from crates.io might not have the same version as the...

Regarding the last topic: > [ ] Assess currently takes "prepended flags" (like cargo kani --flag assess) and should not actually permit this we could use https://docs.rs/clap/latest/clap/struct.Command.html#method.args_conflicts_with_subcommands.

I don't think Kani should always fail on those cases. That's a well defined operation in the rust language and some users may rely on that. Maybe we can add...

Thanks for reporting this issue @roypat. I believe this is a duplicate of #1997. Let me know if the original issue covers your use case, and we can close this...

That said, I wonder if we should just split #1997 into two issues. We can use #1997 to track disambiguation using the [qualified path type](https://doc.rust-lang.org/reference/paths.html#qualified-paths) and use this issue to...

BTW, @feliperodri I wonder if we can at least improve the error message now. We could add a note saying that trait methods are not supported.

Just to clarify, the problem is that slice methods are represented using [qualified paths](https://doc.rust-lang.org/reference/paths.html#qualified-paths), and today we only support simple paths. For example, here is a dummy test that calls...

Yeah, I need to fix that. Thanks

This ensures seems to fail, which makes me think that this could be something weird is going on with promoted constants: ```rust #[kani::ensures(Foo::A != Foo::B)] ```

Something is very weird... I created the following code: ```rust extern crate kani; use kani::Arbitrary; #[derive(PartialEq, Eq, kani::Arbitrary)] pub struct Foo(u8); #[kani::requires(foo == Foo(1))] pub fn foo_a(foo: Foo) -> Foo...