Fix type enumerator for FP (#2717)

diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h
index 96a61f2075e3560af99bd15fab30c6e7abf1f9f9..eeb1ac4f8ed61c5c7619aa61b0ff7a44f271cda3 100644 (file)
--- a/src/theory/fp/type_enumerator.h
+++ b/src/theory/fp/type_enumerator.h
@@ -64,8 +64,12 @@ class FloatingPointEnumerator
  protected:
   FloatingPoint createFP(void) const {
     // Rotate the LSB into the sign so that NaN is the last value
-    const BitVector value =
-        d_state.logicalRightShift(1) | d_state.leftShift(d_state.getSize() - 1);
+    uint64_t vone = 1;
+    uint64_t vmax = d_state.getSize() - 1;
+    BitVector bva =
+        d_state.logicalRightShift(BitVector(d_state.getSize(), vone));
+    BitVector bvb = d_state.leftShift(BitVector(d_state.getSize(), vmax));
+    const BitVector value = (bva | bvb);
 
     return FloatingPoint(d_e, d_s, value);
   }