SMTChecker: Fix equality of array literals

[blishko]

There are two kinds of array literals in Solidity: string literals (arrays of characters/bytes) and proper array literals (e.g., [1,2,3]). While array literals cannot be directly tested for equality in Solidity, it is possible to compute hash of these values and compare hashes. The expectation is that hashes of the same array literals would be the same, but previously SMTChecker returned false positive in this case, saying that they don't have to be equal.

The reason for the false positive was the following. We represent Solidity array literal as a tuple (elements, length) where length is an integer representing the actualy length of the array literal, and elements are an SMT-LIB array, where the first length elements represent the actual content of the array literal. However, SMT-LIB arrays are infinite objects (more like functions from indices to elements). Previously, we left the part after length-th element unspecified. For the solver this meant that two array literals equal at the Solidity level were represented with two different SMT-LIB arrays.

The proposed solution is to always start from a constant-zero array, and use store operations to build an SMT-LIB array that matches the Solidity array literal.

Fixes #14983.