Infinite loop with nested arrays

[msooseth]

Following runs a (seemingly) infinite number of queries to the solver. Related #434

Definitely some bug. Change the testEnv to have more debug and we get a lot of queries being dumped. Weird.

    , test "decompose-bug" $ do
      Just c <- solcRuntime "MyContract"
        [i|
        contract MyContract {
          uint[][] arr2;
          function prove_nested_append(uint v, uint w) public {
            arr2.push([1,2]);
          }
        }
        |]
      let fun = (Just (Sig "prove_nested_append(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256]))
      (_, [Qed _]) <- withSolvers Bitwuzla 1 Nothing $ \s -> checkAssert s defaultPanicCodes c fun [] defaultVeriOpts
      putStrLnM "All good."

[msooseth]

Note to self. This is tracked as fix-506. The issue seems to be a loop in the YUL due to the nested array. solc --ir a.sol > stuff gets us a loop in the yul:

            function copy_array_to_storage_from_t_array$_t_uint8_$2_memory_ptr_to_t_array$_t_uint256_$dyn_storage
(dst, src) {

                let length := array_length_t_array$_t_uint8_$2_memory_ptr(src)
                // Make sure array length is sane
                if gt(length, 0xffffffffffffffff) { panic_error_0x41() }
                resize_array_t_array$_t_uint256_$dyn_storage(dst, length)

                let srcPtr := array_dataslot_t_array$_t_uint8_$2_memory_ptr(src)
                let dstSlot := array_dataslot_t_array$_t_uint256_$dyn_storage(dst)

                let fullSlots := div(length, 1)

                for { let i := 0 } lt(i, fullSlots) { i := add(i, 1) } {
                    let dstSlotValue := 0

                    {

                        let stackItem_0 := read_from_memoryt_uint8(srcPtr)

                        let itemValue := prepare_store_t_uint256(stackItem_0)
                        dstSlotValue :=

                        itemValue

                        srcPtr := add(srcPtr, 32)

                    }

                    sstore(add(dstSlot, i), dstSlotValue)
                }

            }

Here, array length is symbolic, since we start with symbolic state.