diff options
author | Martin Brain <martin.brain@cs.ox.ac.uk> | 2017-09-26 20:00:17 -0700 |
---|---|---|
committer | Andres Noetzli <noetzli@stanford.edu> | 2017-09-26 20:03:31 -0700 |
commit | f82e4308d1f1b8cc033ca6bfd70e707e4695a47d (patch) | |
tree | 421c33ec98e4ac2104671a6ee28a9006687bf586 /src/theory/fp | |
parent | e23377411d993e126403eb186c80f664419d512c (diff) |
Fix type checking of to_real (#1127)
to_real takes a single argument as given in kinds.
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"); } |