diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-10-19 17:44:12 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-19 19:44:12 -0500 |
| commit | 96c6ec71ccdde72c6cbc850df94c8965cda8d7db (patch) | |
| tree | 511d4d38af86ed097b88d62d0454c31bd2465d9f /src/theory/strings/term_registry.cpp | |
| parent | 5a2f629f138f31e27965ede4884284437e30e801 (diff) | |
Expand `seq.nth` lazily (#5287)
Our first support for seq.nth eliminated it eagerly during expandDefinitions.
This PR changes that, by eliminating it lazily, as done with other extended string operators.
Diffstat (limited to 'src/theory/strings/term_registry.cpp')
| -rw-r--r-- | src/theory/strings/term_registry.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 71671d8f1..b5b2a5a13 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -141,7 +141,7 @@ void TermRegistry::preRegisterTerm(TNode n) { if (k == STRING_STRIDOF || k == STRING_ITOS || k == STRING_STOI || k == STRING_STRREPL || k == STRING_SUBSTR || k == STRING_STRREPLALL - || k == STRING_REPLACE_RE || k == STRING_REPLACE_RE_ALL + || k == SEQ_NTH || k == STRING_REPLACE_RE || k == STRING_REPLACE_RE_ALL || k == STRING_STRCTN || k == STRING_LEQ || k == STRING_TOLOWER || k == STRING_TOUPPER || k == STRING_REV || k == STRING_UPDATE) { |