Merge pull request #10149 from blishko/issue-10034

[SMTChecker] Creating Verification targets in two stages.

docs/security-considerations.rst

@@ -620,26 +620,32 @@ types.
 
     // SPDX-License-Identifier: GPL-3.0
     pragma solidity >=0.5.0;
+    pragma experimental ABIEncoderV2;
     pragma experimental SMTChecker;
     // This will report a warning
 
     contract Aliasing
     {
-        uint[] array;
+        uint[] array1;
+        uint[][] array2;
         function f(
             uint[] memory a,
             uint[] memory b,
             uint[][] memory c,
             uint[] storage d
-        ) internal view {
-            require(array[0] == 42);
-            require(a[0] == 2);
-            require(c[0][0] == 2);
-            require(d[0] == 2);
+        ) internal {
+            array1[0] = 42;
+            a[0] = 2;
+            c[0][0] = 2;
             b[0] = 1;
             // Erasing knowledge about memory references should not
             // erase knowledge about state variables.
-            assert(array[0] == 42);
+            assert(array1[0] == 42);
+            // However, an assignment to a storage reference will erase
+            // storage knowledge accordingly.
+            d[0] = 2;
+            // Fails as false positive because of the assignment above.
+            assert(array1[0] == 42);
             // Fails because `a == b` is possible.
             assert(a[0] == 2);
             // Fails because `c[i] == b` is possible.
@@ -647,6 +653,14 @@ types.
             assert(d[0] == 2);
             assert(b[0] == 1);
         }
+        function g(
+            uint[] memory a,
+            uint[] memory b,
+            uint[][] memory c,
+            uint x
+        ) public {
+            f(a, b, c, array2[x]);
+        }
     }
 
 After the assignment to ``b[0]``, we need to clear knowledge about ``a`` since