Properly implement function extensionality based on cardinality (#1765)

1 files changed, 16 insertions, 0 deletions

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 9e61e713b..e7775cf7f 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -82,6 +82,22 @@ bool TypeNode::isInterpretedFinite() const {
       }else if( isSet() ) {
         return getSetElementType().isInterpretedFinite();
       }
+      else if (isFunction())
+      {
+        if (!getRangeType().isInterpretedFinite())
+        {
+          return false;
+        }
+        std::vector<TypeNode> argTypes = getArgTypes();
+        for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
+        {
+          if (!argTypes[i].isInterpretedFinite())
+          {
+            return false;
+          }
+        }
+        return true;
+      }
     }
     return false;
   }