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.
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.