From: Martin Brain <martin.brain@cs.ox.ac.uk>
Date: Wed, 27 Sep 2017 03:00:17 +0000 (-0700)
Subject: Fix type checking of to_real (#1127)
X-Git-Tag: cvc5-1.0.0~5608
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f82e4308d1f1b8cc033ca6bfd70e707e4695a47d;p=cvc5.git

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 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");
       }