Fix related to parametric sorts whose interpretation is finite due to uninterpreted sorts + FMF. Generalizes previous fix in term registration visitor.

1 files changed, 5 insertions, 35 deletions

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 830e7f809..6b268805a 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -64,14 +64,8 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
       TypeNode type = current.getType();
       typeTheoryId = Theory::theoryOf(type);
       if (typeTheoryId != currentTheoryId) {
-        if (options::finiteModelFind() && type.isSort()) {
-          // We're looking for finite models
+        if (type.isInterpretedFinite()) {
           useType = true;
-        } else {
-          Cardinality card = type.getCardinality();
-          if (card.isFinite()) {
-            useType = true;
-          }
         }
       }
     }
@@ -130,14 +124,8 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
       TypeNode type = current.getType();
       typeTheoryId = Theory::theoryOf(type);
       if (typeTheoryId != currentTheoryId) {
-        if (options::finiteModelFind() && type.isSort()) {
-          // We're looking for finite models
+        if (type.isInterpretedFinite()) {
           useType = true;
-        } else {
-          Cardinality card = type.getCardinality();
-          if (card.isFinite()) {
-            useType = true;
-          }
         }
       }
     }
@@ -222,14 +210,8 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
       TypeNode type = current.getType();
       typeTheoryId = Theory::theoryOf(type);
       if (typeTheoryId != currentTheoryId) {
-        if (options::finiteModelFind() && type.isSort()) {
-          // We're looking for finite models
+        if (type.isInterpretedFinite()) {
           useType = true;
-        } else {
-          Cardinality card = type.getCardinality();
-          if (card.isFinite()) {
-            useType = true;
-          }
         }
       }
     }
@@ -244,14 +226,8 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
       TypeNode type = current.getType();
       typeTheoryId = Theory::theoryOf(type);
       if (typeTheoryId != currentTheoryId) {
-        if (options::finiteModelFind() && type.isSort()) {
-          // We're looking for finite models
+        if (type.isInterpretedFinite()) {
           useType = true;
-        } else {
-          Cardinality card = type.getCardinality();
-          if (card.isFinite()) {
-            useType = true;
-          }
         }
       }
     }
@@ -297,14 +273,8 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) {
       TypeNode type = current.getType();
       typeTheoryId = Theory::theoryOf(type);
       if (typeTheoryId != currentTheoryId) {
-        if (options::finiteModelFind() && type.isSort()) {
-          // We're looking for finite models
+        if (type.isInterpretedFinite()) {
           useType = true;
-        } else {
-          Cardinality card = type.getCardinality();
-          if (card.isFinite()) {
-            useType = true;
-          }
         }
       }
     }