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.

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 0aa622bfbec269c5c950493e3f4cefb6ae725a10..e6c695dd65bc697d37839bd740b4d319344f569a 100644 (file)
--- 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;
   }