diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-20 17:01:01 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-20 22:01:01 +0000 |
| commit | 57f8d6c04430277abdb98916b8ac407930abd215 (patch) | |
| tree | 085a7f4493cec54c12c685de46eeb6fb503284bc /src/theory/uf/ho_extension.cpp | |
| parent | 79fb4d7cb03b5fe254fb0c43f5dc6e885cfbf013 (diff) | |
Check for higher-order variables in TheoryUF::ppRewrite (#7408)
Fixes #7000. That sequence of API calls now throws a logic exception.
Diffstat (limited to 'src/theory/uf/ho_extension.cpp')
| -rw-r--r-- | src/theory/uf/ho_extension.cpp | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 096a47c86..fd7cd467e 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -43,13 +43,16 @@ HoExtension::HoExtension(Env& env, Node HoExtension::ppRewrite(Node node) { // convert HO_APPLY to APPLY_UF if fully applied - if (node[0].getType().getNumChildren() == 2) + if (node.getKind() == HO_APPLY) { - Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl; - Node ret = getApplyUfForHoApply(node); - Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret - << std::endl; - return ret; + if (node[0].getType().getNumChildren() == 2) + { + Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl; + Node ret = getApplyUfForHoApply(node); + Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret + << std::endl; + return ret; + } } return node; } |