1 files changed, 10 insertions, 7 deletions

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index cc5a31aa8..79c300401 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -231,6 +231,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
   Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl;
   RewriteStatus status = REWRITE_DONE;
   Node ret = in;
+  int rew_op = -1;
   //get the body
   if( in.getKind()==EXISTS ){
     std::vector< Node > children;
@@ -251,6 +252,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
         if( doOperation( in, op, qa ) ){
           ret = computeOperation( in, op, qa );
           if( ret!=in ){
+            rew_op = op;
             status = REWRITE_AGAIN_FULL;
             break;
           }
@@ -260,7 +262,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
   }
   //print if changed
   if( in!=ret ){
-    Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
+    Trace("quantifiers-rewrite") << "*** rewrite (op=" << rew_op << ") " << in << std::endl;
     Trace("quantifiers-rewrite") << " to " << std::endl;
     Trace("quantifiers-rewrite") << ret << std::endl;
   }
@@ -1537,8 +1539,9 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg
   return mkForAll( args, body, qa );
 }
 
-bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& qa ){
-  bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef();
+bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& qa ){
+  bool is_strict_trigger = qa.d_hasPattern && options::userPatternsQuant()==USER_PAT_MODE_TRUST;
+  bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef() && !is_strict_trigger;
   if( computeOption==COMPUTE_ELIM_SYMBOLS ){
     return true;
   }else if( computeOption==COMPUTE_MINISCOPING ){
@@ -1551,15 +1554,15 @@ bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& q
     return true;
     //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
   }else if( computeOption==COMPUTE_COND_SPLIT ){
-    return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && is_std;
+    return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && !is_strict_trigger;
   }else if( computeOption==COMPUTE_PRENEX ){
-    return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
+    return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std;
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     return ( options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant() ) && is_std;
   //}else if( computeOption==COMPUTE_CNF ){
   //  return options::cnfQuant();
   }else if( computeOption==COMPUTE_PURIFY_EXPAND ){
-    return options::purifyQuant();
+    return options::purifyQuant() && is_std;
   }else{
     return false;
   }
@@ -1617,7 +1620,7 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
       std::vector< Node > children;
       children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
       children.push_back( n );
-      if( !qa.d_ipl.isNull() ){
+      if( !qa.d_ipl.isNull() && args.size()==f[0].getNumChildren() ){
         children.push_back( qa.d_ipl );
       }
       return NodeManager::currentNM()->mkNode(kind::FORALL, children );