diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-14 14:07:18 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-14 14:07:18 -0500 |
| commit | 29639a7df6ddf105803431cc85888c9416af6af6 (patch) | |
| tree | de6304838c8b642b40fb243b763fd9662195cbbf /src/theory/quantifiers/quantifiers_rewriter.cpp | |
| parent | c130a81b3578898dcb5cacaf746e4dd923e2c5d6 (diff) | |
Update to standard implementation of getting free variables (#3175)
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 63f193557..fb21d6895 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1245,9 +1245,9 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, { // compute variables in itm->first, these are not eligible for // elimination - std::vector<Node> bvs; - TermUtil::getBoundVars(m.first, bvs); - for (TNode v : bvs) + std::unordered_set<Node, NodeHashFunction> fvs; + expr::getFreeVariables(m.first, fvs); + for (const Node& v : fvs) { Trace("var-elim-ineq-debug") << "...ineligible " << v |