diff --git a/proofs/secded.txt b/proofs/secded.txt
index be13de1..3791974 100644
--- a/proofs/secded.txt
+++ b/proofs/secded.txt
@@ -83,7 +83,7 @@ inline int correct(unsigned pr, unsigned *ur) {
 
     // One error, and syn bits 5:0 tell where it is in ur.
     b = syn - 31 - (syn >> 5);   // Map syn to range 0 to 31.  
-    *ur = *ur ^ (1 << b);       // Correct the bit.
+    *ur = *ur ^ (1u << b);       // Correct the bit.
     return 1;
 }
 
diff --git a/proofs/turn_off_rightmost_one.txt b/proofs/turn_off_rightmost_one.txt
index 0c3c0bd..6225d2b 100644
--- a/proofs/turn_off_rightmost_one.txt
+++ b/proofs/turn_off_rightmost_one.txt
@@ -13,6 +13,6 @@ int main() {
     unsigned x = nondet_unsigned() | 1;
     unsigned y = nondet_unsigned() & 31;
     unsigned z = x << y;
-    assert(turn_off_rightmost_one(z) == (z ^ (1<<y)));
+    assert(turn_off_rightmost_one(z) == (z ^ (1u<<y)));
 }
 ----