diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-18 23:54:57 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-18 23:54:57 -0500 |
| commit | 1ec2e4637e092f1e62005bb3cffc3696d6099679 (patch) | |
| tree | ec30c5ba9b6c6b36df46994f898e37735e360a1e /src/expr | |
| parent | 236337b3df1fa6c7627537f0d783d3d3f568b068 (diff) | |
Explicitly handle isFinite for rounding modes (#4115)
The function TypeNode::isFinite is designed to compute finiteness without computing cardinality for the sake of efficiency; there was a missing case for rounding modes, leading to an assertion failure.
Fixes #4101.
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/type_node.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 0aa622bfb..e6c695dd6 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -117,7 +117,8 @@ bool TypeNode::isFiniteInternal(bool usortFinite) { ret = usortFinite; } - else if (isBoolean() || isBitVector() || isFloatingPoint()) + else if (isBoolean() || isBitVector() || isFloatingPoint() + || isRoundingMode()) { ret = true; } |