From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 21 Nov 2018 14:59:51 +0000 (-0600)
Subject:  Fix type enumerator for FP (#2717)
X-Git-Tag: cvc5-1.0.0~4361
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b3b1fffb390d19312227d7095fb404e9e0447d95;p=cvc5.git

 Fix type enumerator for FP (#2717)
---

diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h
index 96a61f207..eeb1ac4f8 100644
--- 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);
   }