Minor change to trigger selection, fixes related to subtypes (in macros, cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.

19 files changed, 108 insertions, 84 deletions

diff --git a/contrib/run-script-casc26-fnt b/contrib/run-script-casc26-fnt
index c3c12f937..c89d3eb0a 100644
--- a/contrib/run-script-casc26-fnt
+++ b/contrib/run-script-casc26-fnt
@@ -33,5 +33,5 @@ function finishwith {
 trywith 60 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair
 trywith 30 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair
 trywith 60 --finite-model-find --decision=internal --sort-inference --uf-ss-fair
-finishwith --finite-model-find --mbqi=abs --sort-inference --uf-ss-fair
+finishwith --finite-model-find --macros-quant --macros-quant-mode=all --sort-inference --uf-ss-fair
 # echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/run-script-casc26-fof b/contrib/run-script-casc26-fof
index 376d18b15..5ec312cb7 100644
--- a/contrib/run-script-casc26-fof
+++ b/contrib/run-script-casc26-fof
@@ -34,7 +34,7 @@ function finishwith {
 # designed for 300 seconds
 trywith 20 --relational-triggers --full-saturate-quant 
 trywith 20 --no-e-matching --full-saturate-quant 
-trywith 15 --finite-model-find --mbqi=abs
+trywith 15 --finite-model-find --uf-ss=no-minimal
 trywith 5 --multi-trigger-when-single --full-saturate-quant 
 trywith 5 --trigger-sel=max --full-saturate-quant
 trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant  
@@ -43,8 +43,8 @@ trywith 15 --prenex-quant=none --full-saturate-quant
 trywith 15 --fs-inst --decision=internal --full-saturate-quant
 trywith 15 --relevant-triggers --full-saturate-quant 
 trywith 15 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair
-trywith 30 --full-saturate-quant --macros-quant
-trywith 30 --fs-inst --full-saturate-quant
+trywith 30 --decision=internal --full-saturate-quant
+trywith 30 --qcf-vo-exp --full-saturate-quant
 trywith 30 --no-quant-cf --full-saturate-quant 
-finishwith --qcf-vo-exp --full-saturate-quant 
+finishwith --macros-quant --macros-quant-mode=all --full-saturate-quant
 # echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/run-script-casc26-tfa b/contrib/run-script-casc26-tfa
index aa65a938f..05062bf5c 100644
--- a/contrib/run-script-casc26-tfa
+++ b/contrib/run-script-casc26-tfa
@@ -31,9 +31,9 @@ function finishwith {
 
 trywith 10 --decision=internal --full-saturate-quant
 trywith 10 --finite-model-find --decision=internal
-trywith 10 --nl-ext --nl-ext-tplanes --full-saturate-quant
+trywith 10 --multi-trigger-when-single --multi-trigger-priority --nl-ext --nl-ext-tplanes --full-saturate-quant
 trywith 10 --partial-triggers --full-saturate-quant
 trywith 15 --cbqi-all --purify-triggers --full-saturate-quant 
 trywith 15 --nl-ext --fs-inst --full-saturate-quant
-finishwith --full-saturate-quant --macros-quant
+finishwith --macros-quant --macros-quant-mode=all --full-saturate-quant
 # echo "% SZS status" "GaveUp for $filename"
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 4e73fa6cf..dcee52337 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -353,7 +353,7 @@ definedFun[CVC4::Expr& expr]
                                       MK_EXPR(CVC4::kind::TO_INTEGER, expr),
                                       MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, expr))));
       if(remainder) {
-        expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d));
+        expr = MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d)));
       }
       expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
     }
@@ -368,7 +368,7 @@ definedFun[CVC4::Expr& expr]
                                       MK_EXPR(CVC4::kind::TO_INTEGER, expr),
                                       MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, expr))));
       if(remainder) {
-        expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d));
+        expr = MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d)));
       }
       expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
     }
@@ -381,7 +381,7 @@ definedFun[CVC4::Expr& expr]
       expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d);
       expr = MK_EXPR(CVC4::kind::TO_INTEGER, expr);
       if(remainder) {
-        expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d));
+        expr = MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d)));
       }
       expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
     }
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index d817fb179..082fa2580 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -37,6 +37,7 @@ struct ArraySelectTypeRule {
       }
       TypeNode indexType = n[1].getType(check);
       if(!indexType.isComparableTo(arrayType.getArrayIndexType())){
+      //if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){  //FIXME:typing
         throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array");
       }
     }
@@ -56,9 +57,11 @@ struct ArrayStoreTypeRule {
         TypeNode indexType = n[1].getType(check);
         TypeNode valueType = n[2].getType(check);
         if(!indexType.isComparableTo(arrayType.getArrayIndexType())){
+        //if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){  //FIXME:typing
           throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array");
         }
-        if(!valueType.isComparableTo(arrayType.getArrayConstituentType())){
+        if(!valueType.isComparableTo(arrayType.getArrayConstituentType())){  
+        //if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){  //FIXME:typing
           Debug("array-types") << "array type: "<< arrayType.getArrayConstituentType() << std::endl;
           Debug("array-types") << "value types: " << valueType << std::endl;
           throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array");
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 412b3d7ec..0540044b5 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -80,9 +80,12 @@ struct DatatypeConstructorTypeRule {
                                  << (*tchild_it) << std::endl;
           TypeNode argumentType = *tchild_it;
           if (!childType.isComparableTo(argumentType)) {
+          //if (!childType.isSubtypeOf(argumentType)) {   //FIXME:typing
             std::stringstream ss;
-            ss << "bad type for constructor argument:\nexpected: "
-               << argumentType << "\ngot     : " << childType;
+            ss << "bad type for constructor argument:\n"
+               << "child type:  " << childType << "\n"
+               << "not subtype: " << argumentType << "\n"
+               << "in term : " << n;
             throw TypeCheckingExceptionPrivate(n, ss.str());
           }
         }
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 1543b2ebd..521f1c978 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -502,6 +502,14 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
       }
     }
   }
+  if( Trace.isOn("cegqi-si-apply-subs-debug") ){
+    Trace("cegqi-si-apply-subs-debug") << "req_coeff = " << req_coeff << "  " << tn << std::endl;
+    for( unsigned i=0; i<subs.size(); i++ ){
+      Trace("cegqi-si-apply-subs-debug") << "  " << vars[i] << " -> " << subs[i] << "   types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl;
+      Assert( subs[i].getType().isSubtypeOf( vars[i].getType() ) );
+    }
+  }
+  
   if( !req_coeff ){
     Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
     if( n!=nret ){
@@ -515,8 +523,12 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
       std::vector< Node > nsubs;
       for( unsigned i=0; i<vars.size(); i++ ){
         if( !coeff[i].isNull() ){
+          Assert( vars[i].getType().isInteger() );
           Assert( coeff[i].isConst() );
-          nsubs.push_back( Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/coeff[i].getConst<Rational>() ) ) ));
+          Node nn =NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/coeff[i].getConst<Rational>() ) );
+          nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn );
+          nn =  Rewriter::rewrite( nn );
+          nsubs.push_back( nn );
         }else{
           nsubs.push_back( subs[i] );
         }
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 2cef4f6a1..2a7b589d0 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -659,6 +659,10 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) {
 }
 
 bool FullSaturation::process( Node f, bool fullEffort ){
+  // ignore if constant true (rare case of non-standard quantifier whose body is rewritten to true)
+  if( f[1].isConst() && f[1].getConst<bool>() ){
+    return false;
+  }
   //first, try from relevant domain
   RelevantDomain * rd = d_quantEngine->getRelevantDomain();
   unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
@@ -770,7 +774,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){
       }
     }
   }
-  //term enumerator?
+  //TODO : term enumerator?
   return false;
 }
 
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 636bfdb59..99dbb7ab9 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -44,7 +44,7 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
     Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl;
     //first, collect macro definitions
     std::vector< Node > macro_assertions;
-    for( unsigned i=0; i<assertions.size(); i++ ){
+    for( int i=0; i<(int)assertions.size(); i++ ){
       Trace("macros-debug") << "  process assertion " << assertions[i] << std::endl;
       if( processAssertion( assertions[i] ) ){
         PROOF( 
@@ -167,6 +167,7 @@ bool QuantifierMacros::isBoundVarApplyUf( Node n ) {
   Assert( n.getKind()==APPLY_UF );
   TypeNode tno = n.getOperator().getType();
   std::map< Node, bool > vars;
+  // allow if a vector of unique variables of the same type as UF arguments
   for( unsigned i=0; i<n.getNumChildren(); i++ ){
     if( n[i].getKind()!=BOUND_VARIABLE ){
       return false;
@@ -174,11 +175,6 @@ bool QuantifierMacros::isBoundVarApplyUf( Node n ) {
     if( n[i].getType()!=tno[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{
@@ -331,6 +327,7 @@ bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
   }else{
     //literal case
     if( isMacroLiteral( n, pol ) ){
+      Trace("macros-debug") << "Check macro literal : " << n << std::endl;
       std::map< Node, bool > visited;
       std::vector< Node > candidates;
       for( size_t i=0; i<n.getNumChildren(); i++ ){
@@ -339,6 +336,7 @@ bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
       for( size_t i=0; i<candidates.size(); i++ ){
         Node m = candidates[i];
         Node op = m.getOperator();
+        Trace("macros-debug") << "Check macro candidate : " << m << std::endl;
         if( d_macro_defs.find( op )==d_macro_defs.end() ){
           std::vector< Node > fvs;
           visited.clear();
@@ -416,6 +414,7 @@ Node QuantifierMacros::simplify( Node n ){
         if( it!=d_macro_defs.end() && !it->second.isNull() ){
           //only apply if children are subtypes of arguments
           bool success = true;
+          // FIXME : this can be eliminated when we have proper typing rules
           std::vector< Node > cond;
           TypeNode tno = op.getType();
           for( unsigned i=0; i<children.size(); i++ ){
@@ -423,13 +422,13 @@ Node QuantifierMacros::simplify( Node n ){
             if( etc.isNull() ){
               //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 );
+              //Assert( false );
               success = false;
               break;
             }else if( !etc.isConst() ){
               cond.push_back( etc );
             }
+            Assert( children[i].getType().isSubtypeOf( tno[i] ) );
           }
           if( success ){
             //do substitution if necessary
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index f2a4e6d17..5b02a877a 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -398,49 +398,46 @@ bool Trigger::isSimpleTrigger( Node n ){
 }
 
 //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula
-void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
+void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
                                 quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
-                                bool pol, bool hasPol, bool epol, bool hasEPol ){
-  std::map< Node, Node >::iterator itv = visited.find( n );
+                                bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable ){
+  std::map< Node, std::vector< Node > >::iterator itv = visited.find( n );
   if( itv==visited.end() ){
-    visited[ n ] = Node::null();
+    visited[ n ].clear();
     Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl;
     if( n.getKind()!=FORALL && n.getKind()!=INST_CONSTANT ){
       Node nu;
       bool nu_single = false;
-      if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
+      if( knowIsUsable ){
+        nu = n;
+      }else if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
         nu = getIsUsableTrigger( n, q );
-        if( !nu.isNull() ){
-          Assert( nu.getKind()!=NOT );
-          Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl;
-          Node reqEq;
-          if( nu.getKind()==EQUAL ){
-            if( isAtomicTrigger( nu[0] ) && !quantifiers::TermDb::hasInstConstAttr(nu[1]) ){
-              if( hasPol ){
-                reqEq = nu[1];
-              }
-              nu = nu[0];
-            }
-          }
-          Assert( reqEq.isNull() || !quantifiers::TermDb::hasInstConstAttr( reqEq ) );
-          Assert( isUsableTrigger( nu, q ) );
-          //do not add if already visited
-          bool add = true;
-          if( n!=nu ){
-            std::map< Node, Node >::iterator itvu = visited.find( nu );
-            if( itvu!=visited.end() ){
-              add = false;
+        if( !nu.isNull() && nu!=n ){
+          collectPatTerms2( q, nu, visited, tinfo, tstrt, exclude, added, pol, hasPol, epol, hasEPol, true );
+          // copy to n
+          visited[n].insert( visited[n].end(), added.begin(), added.end() );
+          return;
+        }
+      }
+      if( !nu.isNull() ){
+        Assert( nu==n );
+        Assert( nu.getKind()!=NOT );
+        Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl;
+        Node reqEq;
+        if( nu.getKind()==EQUAL ){
+          if( isAtomicTrigger( nu[0] ) && !quantifiers::TermDb::hasInstConstAttr(nu[1]) ){
+            if( hasPol ){
+              reqEq = nu[1];
             }
-          }
-          if( add ){
-            Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl;
-            visited[ nu ] = nu;
-            tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq );
-            nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren();
-          }else{
-            nu = Node::null();
+            nu = nu[0];
           }
         }
+        Assert( reqEq.isNull() || !quantifiers::TermDb::hasInstConstAttr( reqEq ) );
+        Assert( isUsableTrigger( nu, q ) );
+        //tinfo.find( nu )==tinfo.end()
+        Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl;
+        tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq );
+        nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren();
       }
       Node nrec = nu.isNull() ? n : nu;
       std::vector< Node > added2;
@@ -451,6 +448,7 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited,
         QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol );
         collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol );
       }
+      // if this is not a usable trigger, don't worry about caching the results, since triggers do not contain non-usable subterms
       if( !nu.isNull() ){
         bool rm_nu = false;
         for( unsigned i=0; i<added2.size(); i++ ){
@@ -461,7 +459,7 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited,
             if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
               //discard all subterms
               Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl;
-              visited[added2[i]] = Node::null();
+              visited[ added2[i] ].clear();
               tinfo.erase( added2[i] );
             }else{
               if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){
@@ -476,18 +474,20 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited,
           }
         }
         if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){
-          visited[nu] = Node::null();
           tinfo.erase( nu );
         }else{
-          Assert( std::find( added.begin(), added.end(), nu )==added.end() );
-          added.push_back( nu );
+          if( std::find( added.begin(), added.end(), nu )==added.end() ){
+            added.push_back( nu );
+          }
         }
+        visited[n].insert( visited[n].end(), added.begin(), added.end() );
       }
     }
   }else{
-    if( !itv->second.isNull() ){
-      if( std::find( added.begin(), added.end(), itv->second )==added.end() ){
-        added.push_back( itv->second );
+    for( unsigned i=0; i<itv->second.size(); ++i ){
+      Node t = itv->second[i];
+      if( std::find( added.begin(), added.end(), t )==added.end() ){
+        added.push_back( t );
       }
     }
   }
@@ -573,7 +573,7 @@ bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector<
 
 void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, 
                                std::map< Node, TriggerTermInfo >& tinfo, bool filterInst ){
-  std::map< Node, Node > visited;
+  std::map< Node, std::vector< Node > > visited;
   if( filterInst ){
     //immediately do not consider any term t for which another term is an instance of t
     std::vector< Node > patTerms2;
@@ -607,7 +607,7 @@ void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, qu
       //do not consider terms that have instances
       for( unsigned i=0; i<patTerms2.size(); i++ ){
         if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){
-          visited[ patTerms2[i] ] = Node::null();
+          visited[ patTerms2[i] ].clear();
         }
       }
     }
@@ -615,9 +615,7 @@ void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, qu
   std::vector< Node > added;
   collectPatTerms2( q, n, visited, tinfo, tstrt, exclude, added, true, true, false, true );
   for( std::map< Node, TriggerTermInfo >::iterator it = tinfo.begin(); it != tinfo.end(); ++it ){
-    if( !visited[it->first].isNull() ){
-      patTerms.push_back( it->first );
-    }
+    patTerms.push_back( it->first );
   }
 }
 
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 234025e7b..8d8f01926 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -137,9 +137,9 @@ private:
   static Node getIsUsableEq( Node q, Node eq );
   static bool isUsableEqTerms( Node q, Node n1, Node n2 );
   /** collect all APPLY_UF pattern terms for f in n */
-  static void collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
+  static void collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
                                 quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
-                                bool pol, bool hasPol, bool epol, bool hasEPol );
+                                bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable = false );
 
   std::vector< Node > d_nodes;
 
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index a5a78e691..e2830b57e 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -116,7 +116,13 @@ struct MemberTypeRule {
       }
       TypeNode elementType = n[0].getType(check);
       if(!elementType.isComparableTo(setType.getSetElementType())) {
-        throw TypeCheckingExceptionPrivate(n, "member operating on sets of different types");
+      //if(!elementType.isSubtypeOf(setType.getSetElementType())) {     //FIXME:typing
+        std::stringstream ss;
+        ss << "member operating on sets of different types:\n"
+           << "child type:  " << elementType << "\n"
+           << "not subtype: " << setType.getSetElementType() << "\n"
+           << "in term : " << n;
+        throw TypeCheckingExceptionPrivate(n, ss.str());
       }
     }
     return nodeManager->booleanType();
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 5d97dda38..6f97a9662 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -46,12 +46,14 @@ class UfTypeRule {
         TypeNode currentArgument = (*argument_it).getType();
         TypeNode currentArgumentType = *argument_type_it;
         if (!currentArgument.isComparableTo(currentArgumentType)) {
+        //if (!currentArgument.isSubtypeOf(currentArgumentType)) {   //FIXME:typing
           std::stringstream ss;
           ss << "argument type is not a subtype of the function's argument "
              << "type:\n"
              << "argument:  " << *argument_it << "\n"
              << "has type:  " << (*argument_it).getType() << "\n"
-             << "not subtype: " << *argument_type_it;
+             << "not subtype: " << *argument_type_it << "\n"
+             << "in term : " << n;
           throw TypeCheckingExceptionPrivate(n, ss.str());
         }
       }
diff --git a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 b/test/regress/regress0/quantifiers/macro-subtype-param.smt2
index 20de79047..586aa64c7 100644
--- a/test/regress/regress0/quantifiers/macro-subtype-param.smt2
+++ b/test/regress/regress0/quantifiers/macro-subtype-param.smt2
@@ -1,18 +1,17 @@
 ; 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)
+(declare-fun R ((List Real)) Bool)
 (assert (forall ((x (List Int))) (R x)))
 (declare-fun j1 () (List Real))
 (assert (not (R j1)))
 
-(declare-fun Q ((Array Real Int)) Bool)
+(declare-fun Q ((Array Int Real)) Bool)
 (assert (forall ((x (Array Real Int))) (Q x)))
-(declare-fun j2 () (Array Int Real))
+(declare-fun j2 () (Array Real 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
index 675c96d68..edacdbe37 100644
--- a/test/regress/regress0/quantifiers/macros-real-arg.smt2
+++ b/test/regress/regress0/quantifiers/macros-real-arg.smt2
@@ -6,6 +6,6 @@
 (assert (forall ((x Int)) (P x)))
 (declare-fun k () Real)
 (declare-fun k2 () Int)
-(assert (or (not (P k)) (not (P k2))))
+(assert (or (not (P (to_int 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
index 836449cb9..42cfb3a11 100644
--- a/test/regress/regress0/quantifiers/subtype-param-unk.smt2
+++ b/test/regress/regress0/quantifiers/subtype-param-unk.smt2
@@ -5,8 +5,7 @@
 
 (declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil))))
 
-(declare-fun R ((List Int)) Bool)
-
+(declare-fun R ((List Real)) Bool)
 (assert (forall ((x (List Int))) (R x)))
 (declare-fun j1 () (List Real))
 (assert (not (R j1)))
diff --git a/test/regress/regress0/quantifiers/subtype-param.smt2 b/test/regress/regress0/quantifiers/subtype-param.smt2
index 08615abf6..a7fe58ac9 100644
--- a/test/regress/regress0/quantifiers/subtype-param.smt2
+++ b/test/regress/regress0/quantifiers/subtype-param.smt2
@@ -3,7 +3,7 @@
 
 (declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil))))
 
-(declare-fun R ((List Int)) Bool)
+(declare-fun R ((List Real)) Bool)
 (assert (forall ((x (List Real))) (R x)))
 
 (declare-fun Q ((Array Int Real)) Bool)
diff --git a/test/regress/regress0/sets/sets-poly-nonint.smt2 b/test/regress/regress0/sets/sets-poly-nonint.smt2
index 441716dcf..a0e883ace 100644
--- a/test/regress/regress0/sets/sets-poly-nonint.smt2
+++ b/test/regress/regress0/sets/sets-poly-nonint.smt2
@@ -7,5 +7,5 @@
 (assert (member 1.5 t))
 (assert (member 2.5 r))
 (assert (member 3.5 u))
-(assert (or (member 4.5 s) (= s t) (= s r) (= s u) (= s (singleton 6.5))))
+(assert (or (= s t) (= s r) (= s u)))
 (check-sat)
diff --git a/test/regress/regress0/sets/sets-tuple-poly.cvc b/test/regress/regress0/sets/sets-tuple-poly.cvc
index 8d87345f6..64fb310be 100644
--- a/test/regress/regress0/sets/sets-tuple-poly.cvc
+++ b/test/regress/regress0/sets/sets-tuple-poly.cvc
@@ -7,11 +7,10 @@ b : SET OF [INT, REAL];
 
 x : [ REAL, REAL ];
 
-
 ASSERT NOT x = (0,0);
 
-ASSERT x IS_IN a;
-ASSERT x IS_IN b;
+ASSERT (x.0, FLOOR(x.1)) IS_IN a;
+ASSERT (FLOOR(x.0), x.1) IS_IN b;
 
 ASSERT NOT x.0 = x.1;