Translating the trace predicates produced by TLC to B predicates.