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.

1 files changed, 3 insertions, 2 deletions

diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index 179bb1a23..066ba6103 100644
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -23,6 +23,7 @@
 #include "theory/uf/options.h"
 #include "smt/options.h"
 #include "theory/rewriter.h"
+#include "theory/quantifiers/options.h"
 
 using namespace CVC4;
 using namespace std;
@@ -333,7 +334,7 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
   for( size_t i=0; i<n.getNumChildren(); i++ ){
     bool processChild = true;
     if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
-      processChild = i==1;
+      processChild = options::userPatternsQuant()==theory::quantifiers::USER_PAT_MODE_IGNORE ? i==1 : i>=1;
     }
     if( processChild ){
       children.push_back( n[i] );
@@ -531,7 +532,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
   for( size_t i=0; i<n.getNumChildren(); i++ ){
     bool processChild = true;
     if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
-      processChild = i>=1;
+      processChild = options::userPatternsQuant()==theory::quantifiers::USER_PAT_MODE_IGNORE ? i==1 : i>=1;
     }
     if( processChild ){
       children.push_back( simplify( n[i], var_bound ) );