Sort-erased tools built on the solver: transition systems and bounded model checking