1 files changed, 2 insertions, 9 deletions
diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h
index 54205315f..fe39993d4 100644
--- a/src/theory/fp/theory_fp_type_rules.h
+++ b/src/theory/fp/theory_fp_type_rules.h
@@ -445,16 +445,9 @@ class FloatingPointToRealTypeRule {
     TRACE("FloatingPointToRealTypeRule");
 
     if (check) {
-      TypeNode roundingModeType = n[0].getType(check);
-
-      if (!roundingModeType.isRoundingMode()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "first argument must be a rounding mode");
-      }
-
-      TypeNode operand = n[1].getType(check);
+      TypeNode operandType = n[0].getType(check);
 
-      if (!operand.isFloatingPoint()) {
+      if (!operandType.isFloatingPoint()) {
         throw TypeCheckingExceptionPrivate(
             n, "floating-point to real applied to a non floating-point sort");
       }