From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 19 Mar 2020 04:54:57 +0000 (-0500)
Subject: Explicitly handle isFinite for rounding modes (#4115)
X-Git-Tag: cvc5-1.0.0~3477
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1ec2e4637e092f1e62005bb3cffc3696d6099679;p=cvc5.git

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 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;
   }