Add options for symmetry breaking in uf+ss totality axiom approach, option for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine

1 files changed, 7 insertions, 0 deletions

diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index b71a1486c..39063942d 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -73,6 +73,7 @@ d_quantEngine( qe ), d_f( f ){
       qe->getTermDatabase()->registerTrigger( this, d_nodes[i].getOperator() );
     }
   }
+  Trace("trigger-debug") << "Finished making trigger." << std::endl;
 }
 
 void Trigger::resetInstantiationRound(){
@@ -144,6 +145,12 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
       }
     }
     if( varCount<f[0].getNumChildren() ){
+      Trace("trigger-debug") << "Don't consider trigger since it does not contain all variables in " << f << std::endl;
+      for( unsigned i=0; i<nodes.size(); i++) {
+        Trace("trigger-debug") << nodes[i] << " ";
+      }
+      Trace("trigger-debug") << std::endl;
+
       //do not generate multi-trigger if it does not contain all variables
       return NULL;
     }else{