From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 18 Feb 2016 21:21:34 +0000 (-0600)
Subject: Correct subtyping for arrays, disable subtyping for predicate subtypes.  Bug fixes... 
X-Git-Tag: cvc5-1.0.0~6049^2~120
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=793361d81f0766c6a28ff699ed5447d9b8f8c123;p=cvc5.git

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.
---

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index eecb2c206..0c9445051 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -107,16 +107,14 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
     }
     return true;
   }else if( t.isRecord() && t.isRecord() ){
-    //TBD
+    //records are not subtypes of each other in current implementation
   }
   if(isFunction()) {
     // A function is a subtype of another if the args are the same type, and
     // the return type is a subtype of the other's.  This is enough for now
     // (and it's necessary for model generation, since a Real-valued function
     // might return a constant Int and thus the model value is typed differently).
-    return t.isFunction() &&
-           getArgTypes() == t.getArgTypes() &&
-           getRangeType().isSubtypeOf(t.getRangeType());
+    return t.isFunction() && getArgTypes() == t.getArgTypes() && getRangeType().isSubtypeOf(t.getRangeType());
   }
   if(isParametricDatatype() && t.isParametricDatatype()) {
     Assert(getKind() == kind::PARAMETRIC_DATATYPE);
@@ -137,6 +135,11 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
   if(isSet() && t.isSet()) {
     return getSetElementType().isSubtypeOf(t.getSetElementType());
   }
+  if(isArray() && t.isArray()) {
+    //reverse for index type
+    return t.getArrayIndexType().isSubtypeOf(getArrayIndexType()) && 
+           getArrayConstituentType().isSubtypeOf(t.getArrayConstituentType());
+  }
   return false;
 }
 
@@ -160,8 +163,8 @@ bool TypeNode::isComparableTo(TypeNode t) const {
       }
     }
     return true;
-  }else if( isRecord() && t.isRecord() ){
-    //TBD
+  //}else if( isRecord() && t.isRecord() ){
+    //record types are incomparable in current implementation
   } else if(isParametricDatatype() && t.isParametricDatatype()) {
     Assert(getKind() == kind::PARAMETRIC_DATATYPE);
     Assert(t.getKind() == kind::PARAMETRIC_DATATYPE);
@@ -177,10 +180,12 @@ bool TypeNode::isComparableTo(TypeNode t) const {
   } else if(isSet() && t.isSet()) {
     return getSetElementType().isComparableTo(t.getSetElementType());
   }
-
-  if(isPredicateSubtype()) {
-    return t.isComparableTo(getSubtypeParentType());
+  if(isArray() && t.isArray()) {
+    return getArrayIndexType().isComparableTo(t.getArrayIndexType()) && getArrayConstituentType().isComparableTo(t.getArrayConstituentType());
   }
+  //if(isPredicateSubtype()) {
+  //  return t.isComparableTo(getSubtypeParentType());
+  //}
   return false;
 }
 
@@ -309,6 +314,14 @@ bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const {
 }
 
 TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
+  return commonTypeNode( t0, t1, true );
+}
+
+TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){
+  return commonTypeNode( t0, t1, false );
+}
+
+TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
   Assert( NodeManager::currentNM() != NULL,
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
@@ -329,65 +342,75 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
         return t0; //IntegerType
       } else if(t1.isReal()) {
         // t0 == IntegerType && t1.isReal() && !t1.isInteger()
-        return NodeManager::currentNM()->realType(); // RealType
+        return isLeast ? t1 : t0; // RealType
       } else {
         return TypeNode(); // null type
       }
     case REAL_TYPE:
       if(t1.isReal()) {
-        return t0; // RealType
+        return isLeast ? t0 : t1; // RealType
       } else {
         return TypeNode(); // null type
       }
     default:
-      if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
-        return t0; // t0 is a constant type
-      } else {
+      //if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
+      //  return t0; // t0 is a constant type
+      //} else {
         return TypeNode(); // null type
-      }
+      //}
     }
   } else if(t1.getKind() == kind::TYPE_CONSTANT) {
-    return leastCommonTypeNode(t1, t0); // decrease the number of special cases
+    return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases
   }
 
   // t0 != t1 &&
   // t0.getKind() == kind::TYPE_CONSTANT &&
   // t1.getKind() == kind::TYPE_CONSTANT
   switch(t0.getKind()) {
-  case kind::ARRAY_TYPE:
   case kind::BITVECTOR_TYPE:
   case kind::SORT_TYPE:
   case kind::CONSTRUCTOR_TYPE:
   case kind::SELECTOR_TYPE:
   case kind::TESTER_TYPE:
-    if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
-      return t0;
-    } else {
+    //if( t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
+    //  return t0;
+    //} else {
       return TypeNode();
-    }
+    //}
   case kind::FUNCTION_TYPE:
     return TypeNode(); // Not sure if this is right
   case kind::SET_TYPE: {
     // take the least common subtype of element types
     TypeNode elementType;
-    if(t1.isSet() &&
-       ! (elementType = leastCommonTypeNode(t0[0], t1[0])).isNull() ) {
+    if(t1.isSet() && !(elementType = commonTypeNode(t0[0], t1[0], isLeast)).isNull() ) {
       return NodeManager::currentNM()->mkSetType(elementType);
     } else {
       return TypeNode();
     }
   }
+  case kind::ARRAY_TYPE: {
+    TypeNode indexType, elementType;
+    if(t1.isArray() &&
+       ! (indexType = commonTypeNode(t0[0], t1[0], !isLeast)).isNull() && 
+       ! (elementType = commonTypeNode(t0[1], t1[1], isLeast)).isNull() ) {
+      return NodeManager::currentNM()->mkArrayType(indexType, elementType);
+    } else {
+      return TypeNode();
+    }
+  }
   case kind::SEXPR_TYPE:
     Unimplemented("haven't implemented leastCommonType for symbolic expressions yet");
     return TypeNode();
   case kind::SUBTYPE_TYPE:
-    if(t1.isPredicateSubtype()){
-      // This is the case where both t0 and t1 are predicate subtypes.
-      return leastCommonPredicateSubtype(t0, t1);
-    }else{ // t0 is a predicate subtype and t1 is not
-      return leastCommonTypeNode(t1, t0); //decrease the number of special cases
-    }
+    //if(t1.isPredicateSubtype()){
+    //  // This is the case where both t0 and t1 are predicate subtypes.
+    //  return leastCommonPredicateSubtype(t0, t1);
+    //}else{ // t0 is a predicate subtype and t1 is not
+    //  return commonTypeNode(t1, t0, isLeast); //decrease the number of special cases
+    //}
+    return TypeNode();
   case kind::SUBRANGE_TYPE:
+    /*
     if(t1.isSubrange()) {
       const SubrangeBounds& t0SR = t0.getSubrangeBounds();
       const SubrangeBounds& t1SR = t1.getSubrangeBounds();
@@ -417,6 +440,8 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
       Assert(t1.isInteger());
       return TypeNode();
     }
+*/
+    return TypeNode();
   case kind::DATATYPE_TYPE:
     if( t0.isTuple() && t1.isTuple() ){
       const Datatype& dt1 = t0.getDatatype();
@@ -424,7 +449,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
       if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){
         std::vector< TypeNode > lc_types;
         for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){
-          TypeNode tc = leastCommonTypeNode( TypeNode::fromType( dt1[0][i].getRangeType() ), TypeNode::fromType( dt2[0][i].getRangeType() ) );
+          TypeNode tc = commonTypeNode( TypeNode::fromType( dt1[0][i].getRangeType() ), TypeNode::fromType( dt2[0][i].getRangeType() ), isLeast );
           if( tc.isNull() ){
             return tc;
           }else{
@@ -433,9 +458,10 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
         }
         return NodeManager::currentNM()->mkTupleType( lc_types );
       }
-    }else if( t0.isRecord() && t1.isRecord() ){
-      //TBD
     }
+    //else if( t0.isRecord() && t1.isRecord() ){
+      //record types are not related in current implementation
+    //}
     // otherwise no common ancestor
     return TypeNode();
   case kind::PARAMETRIC_DATATYPE: {
@@ -450,12 +476,12 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
     }
     vector<Type> v;
     for(size_t i = 1; i < t0.getNumChildren(); ++i) {
-      v.push_back(leastCommonTypeNode(t0[i], t1[i]).toType());
+      v.push_back(commonTypeNode(t0[i], t1[i], isLeast).toType());
     }
     return TypeNode::fromType(t0[0].getDatatype().getDatatypeType(v));
   }
   default:
-    Unimplemented("don't have a leastCommonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str());
+    Unimplemented("don't have a commonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str());
     return TypeNode();
   }
 }
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 4c48cc3ca..099be5d80 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -642,8 +642,10 @@ public:
    * For more information see: http://cvc4.cs.nyu.edu/wiki/Cvc4_Type_Lattice
    */
   static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1);
+  static TypeNode mostCommonTypeNode(TypeNode t0, TypeNode t1);
 
 private:
+  static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast);
 
   /**
    * Returns the leastUpperBound in the extended type lattice of two
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index a5e3dada8..b7321a8e0 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -39,9 +39,15 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
     d_ground_macros = (r==0);
     Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl;
     //first, collect macro definitions
-    for( int i=0; i<(int)assertions.size(); i++ ){
+    std::vector< Node > macro_assertions;
+    for( unsigned i=0; i<assertions.size(); i++ ){
       Trace("macros-debug") << "  process assertion " << assertions[i] << std::endl;
       if( processAssertion( assertions[i] ) ){
+        PROOF( 
+          if( std::find( macro_assertions.begin(), macro_assertions.end(), assertions[i] )==macro_assertions.end() ){
+            macro_assertions.push_back( assertions[i] );
+          }
+        );
         //process this assertion again
         i--;
       }
@@ -56,7 +62,17 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
         if( curr!=assertions[i] ){
           curr = Rewriter::rewrite( curr );
           Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl;
-          PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
+          //for now, it is dependent upon all assertions involving macros, this is an over-approximation.
+          //a more fine-grained unsat core computation would require caching dependencies for each subterm of the formula, 
+          // which is expensive.
+          PROOF( 
+            ProofManager::currentPM()->addDependence(curr, assertions[i]); 
+            for( unsigned j=0; j<macro_assertions.size(); j++ ){
+              if( macro_assertions[j]!=assertions[i] ){
+                ProofManager::currentPM()->addDependence(curr,macro_assertions[j]);
+              }
+            }
+          );
           assertions[i] = curr;
           retVal = true;
         }
@@ -68,7 +84,7 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
     }
   }
   if( Trace.isOn("macros-warn") ){
-    for( int i=0; i<(int)assertions.size(); i++ ){
+    for( unsigned i=0; i<assertions.size(); i++ ){
       debugMacroDefinition( assertions[i], assertions[i] );
     }
   }
@@ -145,18 +161,24 @@ bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
 
 bool QuantifierMacros::isBoundVarApplyUf( Node n ) {
   Assert( n.getKind()==APPLY_UF );
-  TypeNode tn = n.getOperator().getType();
+  TypeNode tno = n.getOperator().getType();
+  std::map< Node, bool > vars;
   for( unsigned i=0; i<n.getNumChildren(); i++ ){
     if( n[i].getKind()!=BOUND_VARIABLE ){
       return false;
     }
-    if( n[i].getType()!=tn[i] ){
+    if( n[i].getType()!=tno[i] ){
       return false;
     }
-    for( unsigned j=0; j<i; j++ ){
-      if( n[j]==n[i] ){
-        return false;
-      }
+    if( !tno[i].isSort() && !tno[i].isReal() && ( !tno[i].isDatatype() || tno[i].isParametricDatatype() ) && 
+        !tno[i].isBitVector() && !tno[i].isString() && !tno[i].isFloatingPoint() ){
+      //only non-parametric types are supported
+      return false;
+    }
+    if( vars.find( n[i] )==vars.end() ){
+      vars[n[i]] = true;
+    }else{
+      return false;
     }
   }
   return true;
@@ -388,13 +410,33 @@ Node QuantifierMacros::simplify( Node n ){
         Node op = n.getOperator();
         std::map< Node, Node >::iterator it = d_macro_defs.find( op );
         if( it!=d_macro_defs.end() && !it->second.isNull() ){
-          //do substitution if necessary
-          ret = it->second;
-          std::map< Node, std::vector< Node > >::iterator itb = d_macro_basis.find( op );
-          if( itb!=d_macro_basis.end() ){
-            ret = ret.substitute( itb->second.begin(), itb->second.end(), children.begin(), children.end() );
+          //only apply if children are subtypes of arguments
+          bool success = true;
+          std::vector< Node > cond;
+          TypeNode tno = op.getType();
+          for( unsigned i=0; i<children.size(); i++ ){
+            if( !TermDb::getEnsureTypeCondition( children[i], tno[i], cond ) ){
+              //if this does fail, we are incomplete, since we are eliminating quantified formula corresponding to op, 
+              //  and not ensuring it applies to n when its types are correct.
+              //however, this should never fail: we never process types for which we cannot constuct conditions that ensure correct types, e.g. (is-int t).
+              Assert( false );
+              success = false;
+              break;
+            }
+          }
+          if( success ){
+            //do substitution if necessary
+            ret = it->second;
+            std::map< Node, std::vector< Node > >::iterator itb = d_macro_basis.find( op );
+            if( itb!=d_macro_basis.end() ){
+              ret = ret.substitute( itb->second.begin(), itb->second.end(), children.begin(), children.end() );
+            }
+            if( !cond.empty() ){
+              Node cc = cond.size()==1 ? cond[0] : NodeManager::currentNM()->mkNode( kind::AND, cond );
+              ret = NodeManager::currentNM()->mkNode( kind::ITE, cc, ret, n );
+            }
+            retSet = true;
           }
-          retSet = true;
         }
       }
       if( !retSet && childChanged ){
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;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 3fa0fbd29..c770f0e6f 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -418,9 +418,10 @@ public:
   bool containsVtsTerm( std::vector< Node >& n, bool isFree = false );
   /** simple check for contains term */
   bool containsVtsInfinity( Node n, bool isFree = false );
-  /** make type */
-  static Node mkNodeType( Node n, TypeNode tn );
-
+  /** ensure type */
+  static Node ensureType( Node n, TypeNode tn );
+  /** get ensure type condition */
+  static bool getEnsureTypeCondition( Node n, TypeNode tn, std::vector< Node >& cond );
 private:
   //helper for contains term
   static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ca8a09082..ce6c929b2 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -687,13 +687,6 @@ bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& v
   Assert( f.getKind()==FORALL );
   Assert( vars.size()==terms.size() );
   Node body = getInstantiation( f, vars, terms, doVts );  //do virtual term substitution
-  if( doVts ){
-    body = Rewriter::rewrite( body );
-    Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl;
-    Node body_r = d_term_db->rewriteVtsSymbols( body );
-    Trace("quant-vts-debug") << "            ...result: " << body_r << std::endl;
-    body = body_r;
-  }
   body = quantifiers::QuantifiersRewriter::preprocess( body, true );
   Trace("inst-debug") << "...preprocess to " << body << std::endl;
   Trace("inst-assert") << "(assert " << body << ")" << std::endl;
@@ -934,10 +927,13 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
       terms[i] = d_eq_query->getInternalRepresentative( terms[i], q, i );
     }else{
       //ensure the type is correct
-      terms[i] = quantifiers::TermDb::mkNodeType( terms[i], q[0][i].getType() );
+      terms[i] = quantifiers::TermDb::ensureType( terms[i], q[0][i].getType() );
     }
     Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
-    Assert( !terms[i].isNull() );
+    if( terms[i].isNull() ){
+      Trace("inst-add-debug") << " -> Failed to make term vector, due to term/type restrictions." << std::endl;
+      return false;
+    }
 #ifdef CVC4_ASSERTIONS
     Assert( !quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) );
 #endif
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index df146752e..02eaeeb47 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -70,7 +70,11 @@ TESTS =	\
   agg-rew-test.smt2 \
   agg-rew-test-cf.smt2 \
   rew-to-0211-dd.smt2 \
-  rew-to-scala.smt2
+  rew-to-scala.smt2 \
+  macro-subtype-param.smt2 \
+  macros-real-arg.smt2 \
+  subtype-param-unk.smt2 \
+  subtype-param.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 b/test/regress/regress0/quantifiers/macro-subtype-param.smt2
new file mode 100644
index 000000000..20de79047
--- /dev/null
+++ b/test/regress/regress0/quantifiers/macro-subtype-param.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --macros-quant
+; EXPECT: unknown
+; this will fail if type rule for APPLY_UF requires to be subtypes
+(set-logic ALL_SUPPORTED)
+
+(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil))))
+
+(declare-fun R ((List Int)) Bool)
+(assert (forall ((x (List Int))) (R x)))
+(declare-fun j1 () (List Real))
+(assert (not (R j1)))
+
+(declare-fun Q ((Array Real Int)) Bool)
+(assert (forall ((x (Array Real Int))) (Q x)))
+(declare-fun j2 () (Array Int Real))
+(assert (not (Q j2)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/macros-real-arg.smt2 b/test/regress/regress0/quantifiers/macros-real-arg.smt2
new file mode 100644
index 000000000..675c96d68
--- /dev/null
+++ b/test/regress/regress0/quantifiers/macros-real-arg.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --macros-quant
+; EXPECT: unsat
+; this will fail if type rule for APPLY_UF is made strict
+(set-logic UFLIRA)
+(declare-fun P (Int) Bool)
+(assert (forall ((x Int)) (P x)))
+(declare-fun k () Real)
+(declare-fun k2 () Int)
+(assert (or (not (P k)) (not (P k2))))
+(assert (= k 0))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/subtype-param-unk.smt2 b/test/regress/regress0/quantifiers/subtype-param-unk.smt2
new file mode 100644
index 000000000..836449cb9
--- /dev/null
+++ b/test/regress/regress0/quantifiers/subtype-param-unk.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: 
+; EXPECT: unknown
+; this will fail if type rule for APPLY_UF requires arguments to be subtypes
+(set-logic ALL_SUPPORTED)
+
+(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil))))
+
+(declare-fun R ((List Int)) Bool)
+
+(assert (forall ((x (List Int))) (R x)))
+(declare-fun j1 () (List Real))
+(assert (not (R j1)))
+
+(declare-fun Q ((Array Int Real)) Bool)
+(assert (forall ((x (Array Int Int))) (Q x)))
+(declare-fun j2 () (Array Int Real))
+(assert (not (Q j2)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/subtype-param.smt2 b/test/regress/regress0/quantifiers/subtype-param.smt2
new file mode 100644
index 000000000..08615abf6
--- /dev/null
+++ b/test/regress/regress0/quantifiers/subtype-param.smt2
@@ -0,0 +1,16 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil))))
+
+(declare-fun R ((List Int)) Bool)
+(assert (forall ((x (List Real))) (R x)))
+
+(declare-fun Q ((Array Int Real)) Bool)
+(assert (forall ((x (Array Int Int))) (Q x)))
+
+(declare-fun k1 () (List Int))
+(declare-fun k2 () (Array Real Int))
+(assert (or (not (R k1)) (not (Q k2))))
+
+(check-sat)