ucsb-seclab / greed

A symbolic execution engine for EVM smart contract binaries.
https://ucsb-seclab.github.io/greed/
MIT License
73 stars 10 forks source link

keep solver state in the "right" branch #3

Open ruaronicola opened 1 year ago

ruaronicola commented 1 year ago

Currently there is no such thing as "cloning" in yices. This means that---whenever we fork the execution---one of the two branches will use a fresh solver, that does not benefit from incremental solving. If such branch is the only one that's NOT pruned/reverted, then the choice of giving it the fresh solver was sub-optimal, as we throw away incremental solving for no reason.

NOTE: keep in mind that this is only meaningful as long as yices devs don't implement a cloning mechanism.