<!-- Please report security concerns to us on the [AWS vulnerability reporting](http://aws.amazon.com/security/vulnerability-reporting/) page. --> <!-- Thank you for filing a bug report! 🐛 Please provide a short summary of the issue, along with the information necessary to replicate. --> I tried this code: <!-- If the reproducing code is small, please post it here. Otherwise, please attach the relevant files to this issue. Alternatively, post a link to the repository and branch that exposes the issue. --> ```rust fn main() { let a: bool = __nondet(); let b: bool = __nondet(); let c = a ^ b; assert!((a == b && !c) || (a != b && c)); } ``` <!-- If RMC crashed, please include a backtrace in the code block by setting `RUST_BACKTRACE=1` in your environment. E.g. `RUST_BACKTRACE=1 rmc ...` --> and it crashed with the following message: ``` thread 'rustc' panicked at 'BinaryOperation Expression does not typecheck Xor Expr { value: Symbol { identifier: "main::1::var_5" }, typ: CInteger(Bool), location: None } Expr { value: Symbol { identifier: "main::1::var_6" }, typ: CInteger(Bool), location: None }', compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs:863:9 ```
Activity