Fix issue with niches on signed values (rust-lang#1542)

Author: danielsn

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

@@ -1308,13 +1308,19 @@ impl<'tcx> GotocCtx<'tcx> {
 /// where "-" is wrapping subtraction, i.e., the result should be interpreted as
 /// an unsigned value (2's complement).
 fn wrapping_sub(expr: &Expr, constant: u64) -> Expr {
-    if constant == 0 {
-        // No need to subtract.
+    let unsigned_expr = if expr.typ().is_pointer() {
         expr.clone()
     } else {
         let unsigned = expr.typ().to_unsigned().unwrap();
-        let constant = Expr::int_constant(constant, unsigned.clone());
-        expr.clone().cast_to(unsigned).sub(constant)
+        expr.clone().cast_to(unsigned)
+    };
+    if constant == 0 {
+        // No need to subtract.
+        // But we still need to make sure we return an unsigned value.
+        unsigned_expr
+    } else {
+        let constant = Expr::int_constant(constant, unsigned_expr.typ().clone());
+        unsigned_expr.sub(constant)
     }
 }
 

tests/kani/Arbitrary/nonzero_fixme.rs renamed to tests/kani/Arbitrary/nonzero.rs

@@ -2,8 +2,6 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 //! Ensure that kani::any behaves correcty with NonZero types.
-//! This is currently failing due to some issue in the niche optimization.
-//! See <https://github.com/model-checking/kani/issues/1533> for more details.
 
 use std::num::*;