Ensure model construction for parametric sorts involving uninterpreted sorts respect cardinality bounds on when finite model finding is enabled.

1 files changed, 3 insertions, 0 deletions

diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index fb2c3cd01..8ee4e843d 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -260,6 +260,9 @@ protected:
   /** is v an excluded codatatype value */
   bool isExcludedCdtValue( Node v, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc );
   bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m );
+  /** involves usort */
+  bool involvesUSort( TypeNode tn );
+  bool isExcludedUSortValue( std::map< TypeNode, unsigned >& eqc_usort_count, Node v, std::map< Node, bool >& visited );
 public:
   TheoryEngineModelBuilder(TheoryEngine* te);
   virtual ~TheoryEngineModelBuilder(){}