diff --git a/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_Gmpz.h b/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_Gmpz.h
index e68ab5ae756..adb1192e6e0 100644
--- a/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_Gmpz.h
+++ b/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_Gmpz.h
@@ -38,8 +38,16 @@ inline CGAL_Interval_nt_advanced CGAL_convert_to (const CGAL_Gmpz &z)
     CGAL_FPU_set_rounding_to_nearest();
     double approx = CGAL_to_double(z);
     CGAL_FPU_set_rounding_to_infinity();
-    return CGAL_Interval_nt_advanced (approx) +
-	   CGAL_Interval_nt_advanced::smallest;
+    const CGAL_Interval_nt_advanced result =
+	CGAL_Interval_nt_advanced (approx) +
+	CGAL_Interval_nt_advanced::smallest;
+#ifndef CGAL_NO_POSTCONDITIONS
+    CGAL_FPU_set_rounding_to_nearest();
+    CGAL_assertion(	CGAL_Gmpz(result.lower_bound()) <= z &&
+			CGAL_Gmpz(result.upper_bound()) >= z);
+    CGAL_FPU_set_rounding_to_infinity();
+#endif
+    return result;
 }
 
 #endif	 // CGAL_IA_GMPZ_H
diff --git a/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_leda_bigfloat.h b/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_leda_bigfloat.h
index 10209ef4b30..9f37b973b4b 100644
--- a/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_leda_bigfloat.h
+++ b/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_leda_bigfloat.h
@@ -36,8 +36,16 @@ inline CGAL_Interval_nt_advanced CGAL_convert_to (const leda_bigfloat &z)
     CGAL_FPU_set_rounding_to_nearest();
     double approx = CGAL_to_double(z);
     CGAL_FPU_set_rounding_to_infinity();
-    return CGAL_Interval_nt_advanced (approx) +
-	   CGAL_Interval_nt_advanced::smallest;
+    const CGAL_Interval_nt_advanced result = 
+	CGAL_Interval_nt_advanced (approx) +
+	CGAL_Interval_nt_advanced::smallest;
+#ifndef CGAL_NO_POSTCONDITIONS
+    CGAL_FPU_set_rounding_to_nearest();
+    CGAL_assertion(     leda_bigfloat(result.lower_bound()) <= z &&
+			leda_bigfloat(result.upper_bound()) >= z);
+    CGAL_FPU_set_rounding_to_infinity();
+#endif
+    return result;
 }
 
 #endif	 // CGAL_IA_LEDA_BIGFLOAT_H
diff --git a/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_leda_integer.h b/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_leda_integer.h
index a57367e0964..aeb892f34b0 100644
--- a/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_leda_integer.h
+++ b/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_leda_integer.h
@@ -38,8 +38,16 @@ inline CGAL_Interval_nt_advanced CGAL_convert_to (const leda_integer &z)
     CGAL_FPU_set_rounding_to_nearest();
     double approx = CGAL_to_double(z);
     CGAL_FPU_set_rounding_to_infinity();
-    return CGAL_Interval_nt_advanced (approx) +
-	   CGAL_Interval_nt_advanced::smallest;
+    const CGAL_Interval_nt_advanced result = 
+	CGAL_Interval_nt_advanced (approx) +
+	CGAL_Interval_nt_advanced::smallest;
+#ifndef CGAL_NO_POSTCONDITIONS
+    CGAL_FPU_set_rounding_to_nearest();
+    CGAL_assertion(     leda_integer(result.lower_bound()) <= z &&
+			leda_integer(result.upper_bound()) >= z);
+    CGAL_FPU_set_rounding_to_infinity();
+#endif
+    return result;
 }
 
 #endif	 // CGAL_IA_LEDA_INTEGER_H
diff --git a/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_leda_rational.h b/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_leda_rational.h
index 49bca368bb3..4a358e17c5d 100644
--- a/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_leda_rational.h
+++ b/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_leda_rational.h
@@ -24,7 +24,7 @@
 #ifndef CGAL_IA_LEDA_RATIONAL_H
 #define CGAL_IA_LEDA_RATIONAL_H
 
-// For this one, I hope that adding 2 ulps will be enough for an exact
+// For this one, I hope that adding 3 ulps will be enough for an exact
 // conversion.  Since LEDA types (except real) don't give information on the
 // precision of to_double(), we can't do much...
 
@@ -37,12 +37,21 @@ inline CGAL_Interval_nt_advanced CGAL_convert_to (const leda_rational &z)
     double approx = CGAL_to_double(z);
     CGAL_FPU_set_rounding_to_infinity();
 
-    return (CGAL_Interval_nt_advanced (approx)
+    const CGAL_Interval_nt_advanced result =
+	((CGAL_Interval_nt_advanced (approx)
+	  + CGAL_Interval_nt_advanced::smallest)
 	  + CGAL_Interval_nt_advanced::smallest)
 	  + CGAL_Interval_nt_advanced::smallest;
 // The following is bad because overflow is highly probable with rationals.
     // return CGAL_convert_to<CGAL_Interval_nt_advanced>(z.numerator())
 	// /  CGAL_convert_to<CGAL_Interval_nt_advanced>(z.denominator());
+#ifndef CGAL_NO_POSTCONDITIONS
+    CGAL_FPU_set_rounding_to_nearest();
+    CGAL_assertion( leda_rational(result.lower_bound()) <= z &&
+		    leda_rational(result.upper_bound()) >= z );
+    CGAL_FPU_set_rounding_to_infinity();
+#endif
+    return result;
 }
 
 #endif	 // CGAL_IA_LEDA_RATIONAL_H
diff --git a/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_leda_real.h b/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_leda_real.h
index d8fd165f580..51ceca81187 100644
--- a/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_leda_real.h
+++ b/Packages/Interval_arithmetic/include/CGAL/Interval_arithmetic/IA_leda_real.h
@@ -33,8 +33,16 @@ inline CGAL_Interval_nt_advanced CGAL_convert_to (const leda_real &z)
     const double approx = CGAL_to_double(z);
     const double rel_error = z.get_double_error();
     CGAL_FPU_set_rounding_to_infinity();
-    return ( CGAL_Interval_nt_advanced(-rel_error,rel_error) + 1 )
-	 * CGAL_Interval_nt_advanced(approx);
+    const CGAL_Interval_nt_advanced result =
+	( CGAL_Interval_nt_advanced(-rel_error,rel_error) + 1 )
+	* CGAL_Interval_nt_advanced(approx);
+#ifndef CGAL_NO_POSTCONDITIONS
+    CGAL_FPU_set_rounding_to_nearest();
+    CGAL_assertion( leda_real(result.lower_bound()) <= z &&
+		    leda_real(result.upper_bound()) >= z );
+    CGAL_FPU_set_rounding_to_infinity();
+#endif
+    return result;
 }
 
 #endif	 // CGAL_IA_LEDA_REAL_H