From f82e4308d1f1b8cc033ca6bfd70e707e4695a47d Mon Sep 17 00:00:00 2001 From: Martin Brain Date: Tue, 26 Sep 2017 20:00:17 -0700 Subject: [PATCH] Fix type checking of to_real (#1127) to_real takes a single argument as given in kinds. --- src/theory/fp/theory_fp_type_rules.h | 11 ++--------- 1 file 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"); } -- 2.30.2