diff options
Diffstat (limited to 'src/theory/quantifiers/instantiate.cpp')
| -rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index ea90ddd66..c6427a4c4 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/instantiate.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" @@ -170,8 +171,7 @@ bool Instantiate::addInstantiation( << terms[i] << std::endl; bad_inst = true; } - else if (quantifiers::TermUtil::containsTerms( - terms[i], d_term_util->d_inst_constants[q])) + else if (expr::hasSubterm(terms[i], d_term_util->d_inst_constants[q])) { Trace("inst") << "***& inst contains inst constants : " << terms[i] << std::endl; |