diff --git a/Number_types/include/CGAL/MP_Float.h b/Number_types/include/CGAL/MP_Float.h
index f6811a0f116..f5790515241 100644
--- a/Number_types/include/CGAL/MP_Float.h
+++ b/Number_types/include/CGAL/MP_Float.h
@@ -167,7 +167,7 @@ public:
     low = static_cast<limb>(l & mask); //extract low bits from l
     high= static_cast<limb>((l - low) >> sizeof_limb); //extract high bits from l
 
-    CGAL_postcondition ( l == low + ( static_cast<limb2>(high) << sizeof_limb ) );
+    CGAL_postcondition ( l == low + ( high * (limb2(1) << sizeof_limb) ) );
   }
 
   // Given a limb2, returns the higher limb.