Properly distinguish which EQC to assign values in datatypes, use assertRepresentative. Disable regression related to records. Enable fmf-fun related regression (modified). Apply modified version of Morgan's patch to fix tuples/records in model. Fix bug with sort inference + patterns. Minor infrastructure.

2 files changed, 4 insertions, 0 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 5c7b31d33..ffe64beba 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -88,6 +88,9 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) {
 bool CegInstantiation::needsModel( Theory::Effort e ) {
   return true;
 }
+bool CegInstantiation::needsFullModel( Theory::Effort e ) {
+  return false;
+}
 
 void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
   if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 67125a8ad..235f2b01c 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -99,6 +99,7 @@ public:
 public:
   bool needsCheck( Theory::Effort e );
   bool needsModel( Theory::Effort e );
+  bool needsFullModel( Theory::Effort e );
   /* Call during quantifier engine's check */
   void check( Theory::Effort e, unsigned quant_e );
   /* Called for new quantifiers */