diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-10 09:25:57 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-10 09:25:57 -0500 |
| commit | e2758b664c43de299d0ba80537f09ccdda026119 (patch) | |
| tree | 01aa01e1c8eb0fb8e9b352a6d9bfd3c17212c249 /src/preprocessing | |
| parent | 426469ee6b6e5f9e0f4f720d62ec3798b7badff7 (diff) | |
Do not traverse quantifiers in nl ext purify (#3982)
Diffstat (limited to 'src/preprocessing')
| -rw-r--r-- | src/preprocessing/passes/nl_ext_purify.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp index a6da281ba..eb5728228 100644 --- a/src/preprocessing/passes/nl_ext_purify.cpp +++ b/src/preprocessing/passes/nl_ext_purify.cpp @@ -45,6 +45,11 @@ Node NlExtPurify::purifyNlTerms(TNode n, return (*find).second; } } + if (n.isClosure()) + { + // don't traverse quantified formulas + return n; + } Node ret = n; if (n.getNumChildren() > 0) { |