1 files changed, 2 insertions, 2 deletions
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index 42f411ab2..cebdbbb29 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -361,8 +361,8 @@ FloatingPoint FloatingPoint::makeMaxNormal(const FloatingPointSize& size,
                                            bool sign)
 {
   BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
-  BitVector bvexp =
-      BitVector::mkOnes(size.packedExponentWidth()).setBit(0, false);
+  BitVector bvexp = BitVector::mkOnes(size.packedExponentWidth());
+  bvexp.setBit(0, false);
   BitVector bvsig = BitVector::mkOnes(size.packedSignificandWidth());
   return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig));
 }