implement symbolic execution, but only half tested.

it runs without causing issues, but we are not using its results
yet, so I'm not sure how much I trust it.