Selective Symbolic Execution

TODO

Maybe example: if x == hash(y): return .... If hash is cryptographic, cannot be reasoned about symbolically (we won’t find (test) inputs x and y satisfying this equation). See [God07]