FuzzingLabs / thoth

Cairo/Starknet security toolkit (bytecode analyzer, disassembler, decompiler, symbolic execution, SBMC)
https://fuzzinglabs.com/
GNU Affero General Public License v3.0
245 stars 21 forks source link

Add inequalities and variables comparisons for the symbolic execution #118

Closed Rog3rSm1th closed 1 year ago

Rog3rSm1th commented 1 year ago

For the moment the symbolic execution only allows to define constraints using equalities. It would be good to add the possibility to use inequalities for constraints in this way: -constraint v4!=0 v6!=0

Or variable comparison constraints like this: -constraint v4==v6