Correct subtyping for arrays, disable subtyping for predicate subtypes. Bug fixes in quantifiers related to subtypes/parametric sorts. Make macros trace dependencies for get-unsat-core. Add regressions.

1 files changed, 15 insertions, 1 deletions

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 284cae2e0..3e5e30bd7 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1585,7 +1585,7 @@ bool TermDb::containsVtsInfinity( Node n, bool isFree ) {
   return containsTerms( n, t );
 }
 
-Node TermDb::mkNodeType( Node n, TypeNode tn ) {
+Node TermDb::ensureType( Node n, TypeNode tn ) {
   TypeNode ntn = n.getType();
   Assert( ntn.isComparableTo( tn ) );
   if( ntn.isSubtypeOf( tn ) ){
@@ -1598,6 +1598,20 @@ Node TermDb::mkNodeType( Node n, TypeNode tn ) {
   }
 }
 
+bool TermDb::getEnsureTypeCondition( Node n, TypeNode tn, std::vector< Node >& cond ) {
+  TypeNode ntn = n.getType();
+  Assert( ntn.isComparableTo( tn ) );
+  if( !ntn.isSubtypeOf( tn ) ){
+    if( tn.isInteger() ){
+      cond.push_back( NodeManager::currentNM()->mkNode( IS_INTEGER, n ) );
+      return true;
+    }
+    return false;
+  }else{
+    return true;
+  }
+}
+
 bool TermDb::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) {
   if( n==t ){
     return true;