Compare peercheck and symbolic pathfinder (and others?) in terms of
Add symbolic evaluation of functions?
Get graph of behavior of Y combinator (plus other usual combinators, S, K, I) via symbolic execution
merge the various symbolic entities into a single class (eg we give the target a symbolic input, and only later determine its an int, etc).