diff options
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
| -rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 0829ccd9c..f89f9f0ea 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -628,8 +628,8 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, //check constraints for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){ //apply substitution to the tconstraint - Node cons = - p->getTermUtil()->substituteBoundVariables(it->first, d_q, terms); + Node cons = p->getQuantifiersRegistry().substituteBoundVariables( + it->first, d_q, terms); cons = it->second ? cons : cons.negate(); if (!entailmentTest(p, cons, p->atConflictEffort())) { return true; |