1 files changed, 24 insertions, 8 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 680be77da..1f68884b6 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -130,21 +130,37 @@ Node CandidateGeneratorQE::getNextCandidate(){
 
 CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) :
   d_match_pattern( mpat ), d_qe( qe ){
-
+  Assert( mpat.getKind()==EQUAL );
+  for( unsigned i=0; i<2; i++ ){
+    if( !quantifiers::TermDb::hasInstConstAttr(mpat[i]) ){
+      d_match_gterm = mpat[i];
+    }
+  }
 }
 void CandidateGeneratorQELitEq::resetInstantiationRound(){
 
 }
 void CandidateGeneratorQELitEq::reset( Node eqc ){
-  d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );
+  if( d_match_gterm.isNull() ){
+    d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );
+  }else{
+    d_do_mgt = true;
+  }
 }
 Node CandidateGeneratorQELitEq::getNextCandidate(){
-  while( !d_eq.isFinished() ){
-    Node n = (*d_eq);
-    ++d_eq;
-    if( n.getType().isComparableTo( d_match_pattern[0].getType() ) ){
-      //an equivalence class with the same type as the pattern, return reflexive equality
-      return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
+  if( d_match_gterm.isNull() ){
+    while( !d_eq.isFinished() ){
+      Node n = (*d_eq);
+      ++d_eq;
+      if( n.getType().isComparableTo( d_match_pattern[0].getType() ) ){
+        //an equivalence class with the same type as the pattern, return reflexive equality
+        return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
+      }
+    }
+  }else{
+    if( d_do_mgt ){
+      d_do_mgt = false;
+      return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_gterm, d_match_gterm );
     }
   }
   return Node::null();