diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-12 17:31:22 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-12 17:31:22 -0500 |
commit | a117e2b45539a822aa480b90558c2c0da6031dd9 (patch) | |
tree | 5006484b1794943a1f049247ebbb2a63cb82dbfb /src/theory/quantifiers/instantiate.cpp | |
parent | bee3c7f6840e531bc91d990b98f2b331d1f2f82c (diff) |
Update to standard implementation of contains term (#3270)
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; |