diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-23 17:27:05 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-23 17:27:05 -0500 |
| commit | 0faead1572109c1d7cb3d67647da02d0b4600a20 (patch) | |
| tree | e0bd28feb049be6a36a63fd73df37f9d3cc7aa54 /src/theory/strings/infer_info.cpp | |
| parent | eaf29fee0871f1b7a8c9cc7c208c6b6d5570bae5 (diff) | |
Infer emptiness instead of splitting when a string equality rewrites to a constant (#3218)
Diffstat (limited to 'src/theory/strings/infer_info.cpp')
| -rw-r--r-- | src/theory/strings/infer_info.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index a20f608a6..b2c88d068 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -24,6 +24,7 @@ std::ostream& operator<<(std::ostream& out, Inference i) { switch (i) { + case INFER_INFER_EMP: out << "Infer-Emp"; break; case INFER_SSPLIT_CST_PROP: out << "S-Split(CST-P)-prop"; break; case INFER_SSPLIT_VAR_PROP: out << "S-Split(VAR)-prop"; break; case INFER_LEN_SPLIT: out << "Len-Split(Len)"; break; |