diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs
index d3dae46e4f82..2a513e3033f9 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs
@@ -52,21 +52,21 @@ impl<'tcx> GotocCtx<'tcx> {
             BinOp::Rem => ce1.rem(ce2),
             BinOp::BitXor => {
                 if self.operand_ty(e1).is_bool() {
-                    ce1.xor(ce2)
+                    ce1.cast_to(Type::bool()).xor(ce2.cast_to(Type::bool()))
                 } else {
                     ce1.bitxor(ce2)
                 }
             }
             BinOp::BitAnd => {
                 if self.operand_ty(e1).is_bool() {
-                    ce1.and(ce2)
+                    ce1.cast_to(Type::bool()).and(ce2.cast_to(Type::bool()))
                 } else {
                     ce1.bitand(ce2)
                 }
             }
             BinOp::BitOr => {
                 if self.operand_ty(e1).is_bool() {
-                    ce1.or(ce2)
+                    ce1.cast_to(Type::bool()).or(ce2.cast_to(Type::bool()))
                 } else {
                     ce1.bitor(ce2)
                 }
diff --git a/src/test/cbmc/Bool-BoolOperators/xor.rs b/src/test/cbmc/Bool-BoolOperators/xor.rs
new file mode 100644
index 000000000000..01b3a979e5ad
--- /dev/null
+++ b/src/test/cbmc/Bool-BoolOperators/xor.rs
@@ -0,0 +1,10 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+include!("../../rmc-prelude.rs");
+
+fn main() {
+    let a: bool = __nondet();
+    let b: bool = __nondet();
+    let c = a ^ b;
+    assert!((a == b && !c) || (a != b && c));
+}