float_utils: normalization shift for very short fractions

regression/smt2_solver/fp/bit-to-fp1.desc

@@ -0,0 +1,7 @@
+CORE
+bit-to-fp1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--

regression/smt2_solver/fp/bit-to-fp1.smt2

@@ -0,0 +1,14 @@
+;
+; convert (_ bv1 1) to double precision FP,
+; and check whether that is equal to 1.0.
+;
+(define-fun B0 () Bool (=
+  ((_ to_fp_unsigned 11 53) roundNearestTiesToAway (_ bv1 1))
+  (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)))
+
+(assert (not B0))
+
+; expected to be UNSAT, i.e., they are equal
+(check-sat)
+
+(exit)

src/solvers/floatbv/float_utils.cpp

@@ -917,7 +917,7 @@ void float_utilst::normalization_shift(bvt &fraction, bvt &exponent)
     literalt shift=prop.land(equal);
 
     // build shifted value
-    bvt shifted_fraction=bv_utils.shift(fraction, bv_utilst::LEFT, i);
+    bvt shifted_fraction=bv_utils.shift(fraction, bv_utilst::shiftt::SHIFT_LEFT, i);
     bv_utils.cond_implies_equal(shift, shifted_fraction, new_fraction);
 
     // build new exponent
@@ -950,11 +950,18 @@ void float_utilst::normalization_shift(bvt &fraction, bvt &exponent)
 
   bvt exponent_delta=bv_utils.zeros(exponent.size());
 
+  // Fraction smaller than the max distance? Pad up with zeros.
+  std::size_t max_distance = 1 << (depth - 1);
+
+  if(fraction.size() < max_distance)
+    fraction = bv_utils.zero_extension(fraction, max_distance);
+
   for(int d=depth-1; d>=0; d--)
   {
     std::size_t distance=(1<<d);
+
     INVARIANT(
-      fraction.size() > distance, "fraction must be larger than distance");
+      fraction.size() >= distance, "fraction must be larger or equal distance");
 
     // check if first 'distance'-many bits are zeros
     const bvt prefix=bv_utils.extract_msb(fraction, distance);