- purity check does no descend beyond eq and neq
 - op without known identities are send verbatim to smt solver
 - penalty computation depends on prover depth