diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-13 15:14:59 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-13 15:14:59 -0500 |
| commit | e69f6c3aa94e382d082d23f847709a97d9470f31 (patch) | |
| tree | 814080b7c1b473e03928b339b99d653819246185 /src/theory/uf/ho_extension.cpp | |
| parent | bfd8e5426cfa5d8955e62c822d61536e42b3eff9 (diff) | |
Move higher-order matching predicate (#3280)
Diffstat (limited to 'src/theory/uf/ho_extension.cpp')
| -rw-r--r-- | src/theory/uf/ho_extension.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 4d5a879ad..88b2ba8d2 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -316,7 +316,8 @@ unsigned HoExtension::checkAppCompletion() // add to pending list apply_uf[rop].push_back(n); } - // arguments are also relevant operators FIXME (github issue #1115) + // Arguments are also relevant operators. + // It might be possible include fewer terms here, see #1115. for (unsigned k = 0; k < n.getNumChildren(); k++) { if (n[k].getType().isFunction()) |