diff options
Diffstat (limited to 'src/theory/fp')
-rw-r--r-- | src/theory/fp/theory_fp_type_rules.h | 11 |
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"); } |