Initializes RoundingMode::roundNearestTiesToAway to a distinct value.

diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h
index 7b18d542a69a28e03c7e82ee7125729855257779..af909dfa424565c146400fbfeb9e6265efa1dd08 100644 (file)
--- a/src/util/floatingpoint.h
+++ b/src/util/floatingpoint.h
@@ -80,10 +80,12 @@ namespace CVC4 {
    */
   enum CVC4_PUBLIC RoundingMode {
     roundNearestTiesToEven = FE_TONEAREST,
-    roundNearestTiesToAway,
     roundTowardPositive = FE_UPWARD,
     roundTowardNegative = FE_DOWNWARD,
-    roundTowardZero = FE_TOWARDZERO
+    roundTowardZero = FE_TOWARDZERO,
+    // Initializes this to the diagonalization of the 4 other values.
+    roundNearestTiesToAway = (((~FE_TONEAREST) & 0x1) | ((~FE_UPWARD) & 0x2) |
+                              ((~FE_DOWNWARD) & 0x4) | ((~FE_TOWARDZERO) & 0x8))
   }; /* enum RoundingMode */
 
   struct CVC4_PUBLIC RoundingModeHashFunction {