"runtime code cannot have an abstract length"

[charles-cooper]

hevm raises the following warning when running hevm equivalence:

WARNING: hevm was only able to partially explore the given contract due to the following issues:

  - Unexpected Symbolic Arguments to Opcode
    msg: "runtime code cannot have an abstract length"
    program counter: 1328
    arguments: 

command:

time hevm equivalence --code-a "$(<legacy.txt)" --code-b "$(<venom.txt)"

legacy.txt
venom.txt

[msooseth]

With newer hevm, we get a bit more info:

WARNING: hevm was only able to partially explore the given contract due to the following issue(s):
  - Unexpected Symbolic Arguments to Opcode
    msg: "runtime code cannot have an abstract length"
    opcode: RETURN
    program counter: 1328
    arguments:
      (CopySlice
        srcOffset: 64
        dstOffset: 0
        size:      (Add
          32
          (And
            115792089237316195423570985008687907853269984665640564039457584007913129639904
            (Add
              31
              (Add
                32
                (ReadWord
                  idx:
                    0
                  buf:
                    (WriteWord
                      idx:
                        0
                      val:
                        (ReadWord
                          idx:

So it's triggering on Return. Looking into it...

[msooseth]

I have a feeling this may need a similar solution as in #581 In other words, it'd need to use an SMT solver and get out all possible solutions. Maybe that'd work. I can try to make the solution to #581 a bit more generic and then it may be reusable here.