Fix type checking of to_real (#1127)

to_real takes a single argument as given in kinds.

diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h
index 54205315fb25d0981a55c49ffdaa01ae26450412..fe39993d403feae4c4393f7f9a91f22d8b9b805b 100644 (file)
--- 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");
       }