diff --git a/src/floatbv/float_utils.h b/src/floatbv/float_utils.h
index 78add233e7..dcd0cc42b8 100644
--- a/src/floatbv/float_utils.h
+++ b/src/floatbv/float_utils.h
@@ -157,7 +157,7 @@ protected:
   void round_fraction(unbiased_floatt &result);
   void round_exponent(unbiased_floatt &result);
   
-  // rounding decision for fraction using sticky bit
+  // rounding decision for fraction
   literalt fraction_rounding_decision(
     const unsigned dest_bits,
     const literalt sign,