From 9c1b041dcb1aeec4026df6e8b3047fad419823e6 Mon Sep 17 00:00:00 2001
From: Alex Beregszaszi <alex@rtfs.hu>
Date: Fri, 25 Sep 2020 10:34:18 +0100
Subject: [PATCH] [SMTChecker] Keep constraints of string literals after
 assignment

---
 Changelog.md                                                  | 2 +-
 libsolidity/formal/SMTEncoder.cpp                             | 4 +---
 .../smtCheckerTests/operators/index_access_for_bytes.sol      | 2 +-
 .../smtCheckerTests/operators/index_access_for_string.sol     | 3 +--
 test/libsolidity/smtCheckerTests/types/bytes_length.sol       | 1 -
 test/libsolidity/smtCheckerTests/types/string_length.sol      | 3 ---
 6 files changed, 4 insertions(+), 11 deletions(-)

diff --git a/Changelog.md b/Changelog.md
index be808276a..bb1b2c7b4 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -5,7 +5,7 @@ Language Features:
 
 Compiler Features:
  * Export compiler-generated utility sources via standard-json or combined-json.
- * SMTChecker: Keep knowledge about string literals and thus support the ``.length`` property properly.
+ * SMTChecker: Keep knowledge about string literals, even through assignment, and thus support the ``.length`` property properly.
  * SMTChecker: Support events and low-level logs.
  * SMTChecker: Support ``revert()``.
  * SMTChecker: Support shifts.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index fa6b74399..540c2a7dc 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1690,9 +1690,7 @@ void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression con
 	// This is a special case where the SMT sorts are different.
 	// For now we are unaware of other cases where this happens, but if they do appear
 	// we should extract this into an `implicitConversion` function.
-	if (_variable.type()->category() != Type::Category::Array || _value.annotation().type->category() != Type::Category::StringLiteral)
-		assignment(_variable, expr(_value, _variable.type()));
-	// TODO else { store each string literal byte into the array }
+	assignment(_variable, expr(_value, _variable.type()));
 }
 
 void SMTEncoder::assignment(VariableDeclaration const& _variable, smtutil::Expression const& _value)
diff --git a/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol b/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol
index ebd97db67..bc6de0c57 100644
--- a/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol
+++ b/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol
@@ -10,4 +10,4 @@ contract C {
     }
 }
 // ----
-// Warning 6328: (161-181): Assertion violation happens here.
+// Warning 6328: (215-235): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/index_access_for_string.sol b/test/libsolidity/smtCheckerTests/operators/index_access_for_string.sol
index 93a620f9d..e4cef695f 100644
--- a/test/libsolidity/smtCheckerTests/operators/index_access_for_string.sol
+++ b/test/libsolidity/smtCheckerTests/operators/index_access_for_string.sol
@@ -11,5 +11,4 @@ contract C {
     }
 }
 // ----
-// Warning 6328: (164-184): Assertion violation happens here.
-// Warning 6328: (194-214): Assertion violation happens here.
+// Warning 6328: (248-268): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/bytes_length.sol b/test/libsolidity/smtCheckerTests/types/bytes_length.sol
index 4959b170b..e248165af 100644
--- a/test/libsolidity/smtCheckerTests/types/bytes_length.sol
+++ b/test/libsolidity/smtCheckerTests/types/bytes_length.sol
@@ -11,4 +11,3 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (106-127): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/string_length.sol b/test/libsolidity/smtCheckerTests/types/string_length.sol
index 5cc8910f0..632eada19 100644
--- a/test/libsolidity/smtCheckerTests/types/string_length.sol
+++ b/test/libsolidity/smtCheckerTests/types/string_length.sol
@@ -16,6 +16,3 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (111-140): Assertion violation happens here.
-// Warning 6328: (217-246): Assertion violation happens here.
-// Warning 6328: (353-382): Assertion violation happens here.