diff --git a/core/convert.h b/core/convert.h
index 348ab59..fedbfcc 100644
--- a/core/convert.h
+++ b/core/convert.h
@@ -483,17 +483,23 @@ template <class t>
 
    // Put the result together
    bwt roundSigWidth(rounded.significand.getWidth());
+   prop msbSet(rounded.significand.extract(roundSigWidth - 1,
+                                           roundSigWidth - 1).isAllOnes());
+   // -2^{n-1} is the only safe "overflow" case
+   prop safeOverflow(input.getSign() &&
+                     msbSet &&
+                     rounded.significand.extract(roundSigWidth - 2,
+                                                 0).isAllZeros());
    prop undefinedResult(earlyUndefinedResult ||
-			rounded.incrementExponent ||    // Definite Overflow
-			(rounded.significand.extract(roundSigWidth - 1,
-						     roundSigWidth - 1).isAllOnes() &&
-			 !(input.getSign() && rounded.significand.extract(roundSigWidth - 2, 0).isAllZeros()))); // -2^{n-1} is the only safe "overflow" case
-
-   
-   sbv result(ITE(undefinedResult,
-		  undefValue,
-		  conditionalNegate<t,sbv,prop>(input.getSign(), rounded.significand.toSigned())));
-
+                        rounded.incrementExponent ||    // Definite Overflow
+                        (msbSet && !safeOverflow));
+
+   sbv definedResult(
+      ITE(safeOverflow,
+          rounded.significand.toSigned(),
+          conditionalNegate<t,sbv,prop>(input.getSign(),
+                                        rounded.significand.toSigned())));
+   sbv result(ITE(undefinedResult, undefValue, definedResult));
    return result;
  }
 
diff --git a/core/operations.h b/core/operations.h
index 41d8367..f61021e 100644
--- a/core/operations.h
+++ b/core/operations.h
@@ -134,8 +134,12 @@ namespace symfpu {
   bv conditionalNegate (const prop &p, const bv &b) {
     typename t::bwt w(b.getWidth());
     PRECONDITION(w >= 2);
-    PRECONDITION(IMPLIES(p, !(b.extract(w - 1, w - 1).isAllOnes() &&
-			      b.extract(w - 2,     0).isAllZeros())));
+    // We may be tempted to check that we are not trying to negate the smallest
+    // value that can be represented using two's complement (i.e., `100...0`).
+    // This is problematic, however, in cases where we apply
+    // `conditionalNegate()` conditionally (e.g., in `convertFloatToSBV()`),
+    // because the arguments to the branches are evaluated eagerly, so the
+    // assertion fails, even though the result is not used.
     
     return bv(ITE(p, -b, b));
   }