diff --git a/proof-libs/fstar/core/Core.Num.fsti b/proof-libs/fstar/core/Core.Num.fsti
index c1a2d6acb..8e8af77d7 100644
--- a/proof-libs/fstar/core/Core.Num.fsti
+++ b/proof-libs/fstar/core/Core.Num.fsti
@@ -38,7 +38,7 @@ val impl__u16__pow (base: u16) (exponent: u32): result : u16 {v base == 2 /\ v e
 val impl__u32__pow (base: u32) (exponent: u32): result : u32 {v base == 2 /\ v exponent <= 16 ==> result == mk_int #Lib.IntTypes.U32 (pow2 (v exponent))}
 val impl__u64__pow: u64 -> u32 -> u64
 val impl__u128__pow: u128 -> u32 -> u128
-val impl__i16__pow (base: i16) (exponent: u32): result: i16 {v base == 2 /\ v exponent < 16 ==> result == mk_int #Lib.IntTypes.S16 (pow2 (v exponent))}
+val impl__i16__pow (base: i16) (exponent: u32): result: i16 {v base == 2 /\ v exponent < 15 ==> result == mk_int #Lib.IntTypes.S16 (pow2 (v exponent))}
 val impl__i32__pow (base: i32) (exponent: u32): result: i32 {v base == 2 /\ v exponent <= 16 ==> result == mk_int #Lib.IntTypes.S32 (pow2 (v exponent))}
 
 val impl__u8__count_ones: u8 -> u32