From 1ec2e4637e092f1e62005bb3cffc3696d6099679 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 18 Mar 2020 23:54:57 -0500 Subject: [PATCH] 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. --- src/expr/type_node.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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; } -- 2.30.2