diff options
Diffstat (limited to 'src/theory/quantifiers/candidate_generator.cpp')
| -rw-r--r-- | src/theory/quantifiers/candidate_generator.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 7c9a6196f..17c8e0300 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -284,7 +284,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() { TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n ); if( !nh.isNull() ){ if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){ - nh = d_qe->getEqualityQuery()->getInternalRepresentative( nh, d_f, d_index ); + nh = d_qe->getInternalRepresentative( nh, d_f, d_index ); //don't consider this if already the instantiation is ineligible if( !d_qe->getTermDatabase()->isTermEligibleForInstantiation( nh, d_f, false ) ){ nh = Node::null(); |