summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/candidate_generator.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/candidate_generator.cpp')
-rw-r--r--src/theory/quantifiers/candidate_generator.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 1b34bc118..9b5e506ea 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -63,7 +63,7 @@ CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) :
Assert( !d_op.isNull() );
}
void CandidateGeneratorQE::resetInstantiationRound(){
- d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size();
+ d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms( d_op );
}
void CandidateGeneratorQE::reset( Node eqc ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback