Quick benchmark for pysmt

[karmacoma-eth]

Do a quick comparison for a given trace of z3 ops including simplify with the equivalent pysmt api. We want to see if this can lower our overhead.

Some extra context: every bytecode operates on symbolic operand, i.e. Z3 objects. Everything that is put on the EVM stack is a Z3 object. That's a lot of Z3 objects. We suspect this contributes significantly to our overhead. For instance:

PUSH1 1
PUSH1 2
ADD

will result in the following objects on the stack:

• [BitVec(1, 256)]
• [BitVec(1, 256), BitVec(2, 256)]
• [BitVec(3, 256)]

It would be great to investigate if manipulating pysmt objects is any more efficient than Z3 objects.

[karmacoma-eth]

side questions: are z3 objects costly in general, or are some objects more costly than others?

• concat
• extract
• zeroext
• uninterpreted functions
• arrays
• ...